English
For appropriate f, the n-th derivative of the Fourier integral of f, when multiplied by (L v w)^k, equals the Fourier integral of the n-th derivative of (L v w)^k times f. This expresses a compatibility between differentiation and a polynomial weight in the Fourier domain.
Русский
Для подходящей f производная порядка n от Фурье-преобразования f, умноженная на (L v w)^k, равна Фурье-преобразованию от производной порядка n от (L v w)^k · f. Это выражает совместимость дифференцирования и полиномиального веса в частотной области.
LaTeX
$$$$ \text{fourierPowSMulRight}(-L.flip)\bigl( D^{k} (\mathcal{F}f) \bigr)(w)^{(n)} = \mathcal{F}\bigl( D^{n}( (L\,v\,w)^{k} f) \bigr)(w) $$$$
Lean4
/-- The `k`-th derivative of the Fourier integral of `f`, multiplied by `(L v w) ^ n`, is the
Fourier integral of the `n`-th derivative of `(L v w) ^ k * f`. -/
theorem fourierPowSMulRight_iteratedFDeriv_fourierIntegral [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 =
fourierIntegral 𝐞 μ L.toLinearMap₁₂ (iteratedFDeriv ℝ n (fun v ↦ fourierPowSMulRight L f v k)) w :=
by
rw [fourierIntegral_iteratedFDeriv (N := N) _ (hf.fourierPowSMulRight _ _) _ hn]
· congr
rw [iteratedFDeriv_fourierIntegral (N := K) _ _ hf.continuous.aestronglyMeasurable hk]
intro k hk
simpa only [norm_iteratedFDeriv_zero] using h'f k 0 hk bot_le
· intro m hm
have I :
Integrable (fun v ↦ ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖)
μ :=
by
apply integrable_finset_sum _ (fun p hp ↦ ?_)
simp only [Finset.mem_product, Finset.mem_range_succ_iff] at hp
exact h'f _ _ ((Nat.cast_le.2 hp.1).trans hk) ((Nat.cast_le.2 hp.2).trans hm)
apply
(I.const_mul ((2 * π) ^ k * (2 * k + 2) ^ m * ‖L‖ ^ k)).mono'
((hf.fourierPowSMulRight L k).continuous_iteratedFDeriv (mod_cast hm)).aestronglyMeasurable
filter_upwards with v
refine norm_iteratedFDeriv_fourierPowSMulRight _ hf (mod_cast hm) (fun 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
· simpa only [Finset.mem_product, Finset.mem_range_succ_iff] using ⟨hj, hi⟩
