English
An auxiliary bound in terms of the operator norm of a certain Fourier-multiplication operator, yielding an upper bound for the same quantity as in the previous bound, but phrased through operator norms.
Русский
Вспомогательная граница через норму оператора для нормированного домножения в пределах Фурье-преобразования, дающая верхнюю границу аналогичную предыдущей, через норму оператора.
LaTeX
$$$$ \| \mathrm{fourierPowSMulRight}(-L.flip) \; (D^{k}(\mathcal{F}f))(w) \| \le (2\pi)^{k} (2k+2)^{n} \|L\|^{k} \sum_{p} \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`). -/
theorem pow_mul_norm_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) (v : V) (w : W) :
|L v w| ^ n * ‖(iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)) w‖ ≤
‖v‖ ^ n * (2 * π * ‖L‖) ^ k * (2 * k + 2) ^ n *
∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ v, ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂μ :=
calc
|L v w| ^ n * ‖(iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)) w‖
_ ≤ (2 * π) ^ n * (|L v w| ^ n * ‖iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) w‖) :=
by
apply le_mul_of_one_le_left (by positivity)
apply one_le_pow₀
linarith [one_le_pi_div_two]
_ = ‖fourierPowSMulRight (-L.flip) (iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)) w n (fun _ ↦ v)‖ :=
by simp [norm_smul, abs_of_nonneg pi_nonneg]
_ ≤
‖fourierPowSMulRight (-L.flip) (iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)) w n‖ *
∏ _ : Fin n, ‖v‖ :=
(le_opNorm _ _)
_ ≤
((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‖ ∂μ) *
‖v‖ ^ n :=
by
gcongr
· apply norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le _ hf h'f hk hn
· simp
_ =
‖v‖ ^ n * (2 * π * ‖L‖) ^ k * (2 * k + 2) ^ n *
∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ v, ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂μ :=
by
simp [mul_pow]
ring
