English
A refined bound for the k-th derivative of 𝓕 f, weighted by |L v w|^n, in terms of integrals of derivatives of f up to order n with polynomial weights in v.
Русский
Уточненная граница для k-й производной 𝓕 f, взвешенная весом |L v w|^n, через интегралы производных f до порядка n с полиномиальными весами по v.
LaTeX
$$$$ \| (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 `‖w‖^n * ‖D^k (𝓕 f) w‖` in terms of integrals of the derivatives of `f` (or order
at most `n`) multiplied by powers of `v` (of order at most `k`). -/
theorem pow_mul_norm_iteratedFDeriv_fourierIntegral_le {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 : V) :
‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤
(2 * π) ^ k * (2 * k + 2) ^ n *
∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ v, ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ :=
by
have Z :
‖w‖ ^ n * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
‖w‖ ^ n *
((2 * (π * ‖innerSL (E := V) ℝ‖)) ^ k *
((2 * k + 2) ^ n *
∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂volume)) :=
by
have := VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le (innerSL ℝ) hf h'f hk hn w w
simp only [innerSL_apply _ w w, real_inner_self_eq_norm_sq w, abs_pow, abs_norm, mul_assoc] at this
rwa [pow_two, mul_pow, mul_assoc] at this
rcases eq_or_ne n 0 with rfl | hn
· simp only [pow_zero, one_mul, mul_one, zero_add, Finset.range_one, Finset.product_singleton, Finset.sum_map,
Function.Embedding.coeFn_mk, norm_iteratedFDeriv_zero] at Z ⊢
apply Z.trans
conv_rhs => rw [← mul_one π]
gcongr
exact norm_innerSL_le _
rcases eq_or_ne w 0 with rfl | hw
· simp [hn]
positivity
rw [mul_le_mul_iff_right₀ (pow_pos (by simp [hw]) n)] at Z
apply Z.trans
conv_rhs => rw [← mul_one π]
simp only [mul_assoc]
gcongr
exact norm_innerSL_le _
