English
There is a uniform bound for the k-th derivative of the Fourier integral of f, multiplied by |L v w|^n, in terms of integrals of iterated derivatives of f up to order n, weighted by powers of ||v||.
Русский
Существует универсальное неравенство для k-й производной Фурье-интеграла f, умноженной на |L v w|^n: она ограничена суммой по p≤(k,n) от интегралов по v с весами ||v||^p1 и ||D^p2 f(v)||.
LaTeX
$$$$ \big|L v w\bigr|^{n} \; \big\| D^{k}(\mathcal{F}f)(w) \big\| \le (2\pi)^{k} (2k+2)^{n} \|L\|^{k} \sum_{p \in \{0..k\} \times \{0..n\}} \int_V \|v\|^{p_{1}} \| D^{p_{2}} f(v) \| \, d\mu(v) $$$$
Lean4
/-- One can bound the `k`-th derivative of the Fourier integral of `f`, multiplied by `(L v w) ^ n`,
in terms of integrals of iterated derivatives of `f` (of order up to `n`) multiplied by `‖v‖ ^ i`
(for `i ≤ k`).
Auxiliary version in terms of the operator norm of `fourierPowSMulRight (-L.flip) ⬝`. For a version
in terms of `|L v w| ^ n * ⬝`, see `pow_mul_norm_iteratedFDeriv_fourierIntegral_le`.
-/
theorem norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le [FiniteDimensional ℝ V] {μ : Measure V}
[Measure.IsAddHaarMeasure μ] {K N : ℕ∞} (hf : ContDiff ℝ N f)
(h'f : ∀ (k n : ℕ), k ≤ K → n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ) {k n : ℕ}
(hk : k ≤ K) (hn : n ≤ N) {w : W} :
‖fourierPowSMulRight (-L.flip) (iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)) w n‖ ≤
(2 * π) ^ k * (2 * k + 2) ^ n * ‖L‖ ^ k *
∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ v, ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂μ :=
by
rw [fourierPowSMulRight_iteratedFDeriv_fourierIntegral L hf h'f hk hn]
apply (norm_fourierIntegral_le_integral_norm _ _ _ _ _).trans
have I p (hp : p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1)) :
Integrable (fun v ↦ ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ :=
by
simp only [Finset.mem_product, Finset.mem_range_succ_iff] at hp
exact h'f _ _ (le_trans (by simpa using hp.1) hk) (le_trans (by simpa using hp.2) hn)
rw [← integral_finset_sum _ I, ← integral_const_mul]
apply integral_mono_of_nonneg
· filter_upwards with v using norm_nonneg _
· exact (integrable_finset_sum _ I).const_mul _
· filter_upwards with v
apply norm_iteratedFDeriv_fourierPowSMulRight _ hf (mod_cast hn) _
intro i hi j hj
apply Finset.single_le_sum (f := fun p ↦ ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) (a := (j, i))
· intro i _hi
positivity
· simp only [Finset.mem_product, Finset.mem_range_succ_iff]
exact ⟨hj, hi⟩
