English
There is a HasFTaylorSeriesUpTo statement for the Fourier integral up to any finite order, with terms given by the corresponding FourierPowSMulRight expressions.
Русский
Сформулирована лемма HasFTaylorSeriesUpTo для Фурье-интеграла до любого конечного порядка, где члены задаются через соответствующие выражения FourierPowSMulRight.
LaTeX
$$$\\text{HasFTaylorSeriesUpTo}\\; N\\; (\\text{fourierIntegral} \\; \\ldots)\\; (\\ldots) $$$
Lean4
theorem hasFTaylorSeriesUpTo_fourierIntegral {N : WithTop ℕ∞}
(hf : ∀ (n : ℕ), n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ) (h'f : AEStronglyMeasurable f μ) :
HasFTaylorSeriesUpTo N (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)
(fun w n ↦ fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun v ↦ fourierPowSMulRight L f v n) w) :=
by
constructor
· intro w
rw [curry0_apply, Matrix.zero_empty,
fourierIntegral_continuousMultilinearMap_apply' (integrable_fourierPowSMulRight L (hf 0 bot_le) h'f)]
simp only [fourierPowSMulRight_apply, pow_zero, Finset.univ_eq_empty, Finset.prod_empty, one_smul]
· intro n hn w
have I₁ : Integrable (fun v ↦ fourierPowSMulRight L f v n) μ := integrable_fourierPowSMulRight L (hf n hn.le) h'f
have I₂ : Integrable (fun v ↦ ‖v‖ * ‖fourierPowSMulRight L f v n‖) μ :=
by
apply
((hf (n + 1) (ENat.add_one_natCast_le_withTop_of_lt hn)).const_mul ((2 * π * ‖L‖) ^ n)).mono'
(continuous_norm.aestronglyMeasurable.mul (h'f.fourierPowSMulRight L n).norm)
filter_upwards with v
simp only [Pi.mul_apply, norm_mul, norm_norm]
calc
‖v‖ * ‖fourierPowSMulRight L f v n‖ ≤ ‖v‖ * ((2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖) := by gcongr;
apply norm_fourierPowSMulRight_le
_ = (2 * π * ‖L‖) ^ n * (‖v‖ ^ (n + 1) * ‖f v‖) := by rw [pow_succ]; ring
have I₃ : Integrable (fun v ↦ fourierPowSMulRight L f v (n + 1)) μ :=
integrable_fourierPowSMulRight L (hf (n + 1) (ENat.add_one_natCast_le_withTop_of_lt hn)) h'f
have I₄ : Integrable (fun v ↦ fourierSMulRight L (fun v ↦ fourierPowSMulRight L f v n) v) μ :=
by
apply (I₂.const_mul ((2 * π * ‖L‖))).mono' (h'f.fourierPowSMulRight L n).fourierSMulRight
filter_upwards with v
exact (norm_fourierSMulRight_le _ _ _).trans (le_of_eq (by ring))
have E :
curryLeft (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun v ↦ fourierPowSMulRight L f v (n + 1)) w) =
fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L fun v ↦ fourierPowSMulRight L f v n) w :=
by
ext w' m
rw [curryLeft_apply, fourierIntegral_continuousMultilinearMap_apply' I₃,
fourierIntegral_continuousLinearMap_apply' I₄,
fourierIntegral_continuousMultilinearMap_apply' (I₄.apply_continuousLinearMap _)]
congr with v
simp only [fourierPowSMulRight_apply, mul_comm, pow_succ, neg_mul, Fin.prod_univ_succ, Fin.cons_zero,
Fin.cons_succ, neg_smul, fourierSMulRight_apply, neg_apply, smul_apply, smul_comm (M := ℝ) (N := ℂ) (α := E),
smul_smul]
exact E ▸ hasFDerivAt_fourierIntegral L I₁ I₂ w
· intro n hn
apply fourierIntegral_continuous Real.continuous_fourierChar (by apply L.continuous₂)
exact integrable_fourierPowSMulRight L (hf n hn) h'f
