diff --git a/Mathlib/Analysis/Distribution/FourierSchwartz.lean b/Mathlib/Analysis/Distribution/FourierSchwartz.lean index db60ee250ce3c5..538ed67294ef6a 100644 --- a/Mathlib/Analysis/Distribution/FourierSchwartz.lean +++ b/Mathlib/Analysis/Distribution/FourierSchwartz.lean @@ -29,23 +29,21 @@ variable {D : Type*} [NormedAddCommGroup D] [NormedSpace ℝ D] /-- Multiplication by a linear map on Schwartz space: for `f : D → V` a Schwartz function and `L` a bilinear map from `D × E` to `ℝ`, we define a new Schwartz function on `D` taking values in the space of linear maps from `E` to `V`, given by -`(VectorFourier.mul_L_schwartz L f) (v) = -(2 * π * I) • L (v, ⬝) • f v`. +`(VectorFourier.fourierSMulRightSchwartz L f) (v) = -(2 * π * I) • L (v, ⬝) • f v`. The point of this definition is that the derivative of the Fourier transform of `f` is the -Fourier transform of `VectorFourier.mul_L_schwartz L f`. -/ -def VectorFourier.mul_L_schwartz : 𝓢(D, V) →L[ℝ] 𝓢(D, E →L[ℝ] V) := +Fourier transform of `VectorFourier.fourierSMulRightSchwartz L f`. -/ +def VectorFourier.fourierSMulRightSchwartz : 𝓢(D, V) →L[ℝ] 𝓢(D, E →L[ℝ] V) := -(2 * π * I) • (bilinLeftCLM (ContinuousLinearMap.smulRightL ℝ E V).flip L.hasTemperateGrowth) @[simp] -lemma VectorFourier.mul_L_schwartz_apply (f : 𝓢(D, V)) (d : D) : - VectorFourier.mul_L_schwartz L f d = -(2 * π * I) • (L d).smulRight (f d) := rfl - -attribute [local instance 200] secondCountableTopologyEither_of_left +lemma VectorFourier.fourierSMulRightSchwartz_apply (f : 𝓢(D, V)) (d : D) : + VectorFourier.fourierSMulRightSchwartz L f d = -(2 * π * I) • (L d).smulRight (f d) := rfl /-- The Fourier transform of a Schwartz map `f` has a Fréchet derivative (everywhere in its domain) and its derivative is the Fourier transform of the Schwartz map `mul_L_schwartz L f`. -/ -theorem SchwartzMap.hasFDerivAt_fourier [CompleteSpace V] [MeasurableSpace D] [BorelSpace D] - {μ : Measure D} [FiniteDimensional ℝ D] [IsAddHaarMeasure μ] (f : 𝓢(D, V)) (w : E) : +theorem SchwartzMap.hasFDerivAt_fourierIntegral [CompleteSpace V] [MeasurableSpace D] [BorelSpace D] + {μ : Measure D} [SecondCountableTopology D] [HasTemperateGrowth μ] (f : 𝓢(D, V)) (w : E) : HasFDerivAt (fourierIntegral fourierChar μ L.toLinearMap₂ f) - (fourierIntegral fourierChar μ L.toLinearMap₂ (mul_L_schwartz L f) w) w := - VectorFourier.hasFDerivAt_fourier L f.integrable + (fourierIntegral fourierChar μ L.toLinearMap₂ (fourierSMulRightSchwartz L f) w) w := + VectorFourier.hasFDerivAt_fourierIntegral L f.integrable (by simpa using f.integrable_pow_mul μ 1) w diff --git a/Mathlib/Analysis/Fourier/FourierTransform.lean b/Mathlib/Analysis/Fourier/FourierTransform.lean index 08a62dd08c9458..61daf7b217f64c 100644 --- a/Mathlib/Analysis/Fourier/FourierTransform.lean +++ b/Mathlib/Analysis/Fourier/FourierTransform.lean @@ -128,9 +128,9 @@ variable [TopologicalSpace 𝕜] [TopologicalRing 𝕜] [TopologicalSpace V] [Bo [TopologicalSpace W] {e : AddChar 𝕜 𝕊} {μ : Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} /-- For any `w`, the Fourier integral is convergent iff `f` is integrable. -/ -theorem fourier_integral_convergent_iff (he : Continuous e) +theorem fourierIntegral_convergent_iff (he : Continuous e) (hL : Continuous fun p : V × W ↦ L p.1 p.2) {f : V → E} (w : W) : - Integrable f μ ↔ Integrable (fun v : V ↦ e (-L v w) • f v) μ := by + Integrable (fun v : V ↦ e (-L v w) • f v) μ ↔ Integrable f μ := by -- first prove one-way implication have aux {g : V → E} (hg : Integrable g μ) (x : W) : Integrable (fun v : V ↦ e (-L v x) • g v) μ := by @@ -139,12 +139,15 @@ theorem fourier_integral_convergent_iff (he : Continuous e) simp_rw [← integrable_norm_iff (c.aestronglyMeasurable.smul hg.1), norm_circle_smul] exact hg.norm -- then use it for both directions - refine ⟨fun hf ↦ aux hf w, fun hf ↦ ?_⟩ + refine ⟨fun hf ↦ ?_, fun hf ↦ aux hf w⟩ have := aux hf (-w) simp_rw [← mul_smul (e _) (e _) (f _), ← e.map_add_mul, LinearMap.map_neg, neg_add_self, e.map_zero_one, one_smul] at this -- the `(e _)` speeds up elaboration considerably exact this -#align vector_fourier.fourier_integral_convergent_iff VectorFourier.fourier_integral_convergent_iff +#align vector_fourier.fourier_integral_convergent_iff VectorFourier.fourierIntegral_convergent_iff + +@[deprecated] alias fourier_integral_convergent_iff := + VectorFourier.fourierIntegral_convergent_iff -- 2024-03-29 variable [CompleteSpace E] @@ -155,8 +158,8 @@ theorem fourierIntegral_add (he : Continuous e) (hL : Continuous fun p : V × W dsimp only [Pi.add_apply, fourierIntegral] simp_rw [smul_add] rw [integral_add] - · exact (fourier_integral_convergent_iff he hL w).mp hf - · exact (fourier_integral_convergent_iff he hL w).mp hg + · exact (fourierIntegral_convergent_iff he hL w).2 hf + · exact (fourierIntegral_convergent_iff he hL w).2 hg #align vector_fourier.fourier_integral_add VectorFourier.fourierIntegral_add /-- The Fourier integral of an `L^1` function is a continuous function. -/ @@ -164,7 +167,7 @@ theorem fourierIntegral_continuous [FirstCountableTopology W] (he : Continuous e (hL : Continuous fun p : V × W ↦ L p.1 p.2) {f : V → E} (hf : Integrable f μ) : Continuous (fourierIntegral e μ L f) := by apply continuous_of_dominated - · exact fun w ↦ ((fourier_integral_convergent_iff he hL w).mp hf).1 + · exact fun w ↦ ((fourierIntegral_convergent_iff he hL w).2 hf).1 · exact fun w ↦ ae_of_all _ fun v ↦ le_of_eq (norm_circle_smul _ _) · exact hf.norm · refine ae_of_all _ fun v ↦ (he.comp ?_).smul continuous_const @@ -195,7 +198,7 @@ theorem integral_bilin_fourierIntegral_eq_flip _ = ∫ ξ, (∫ x, M.flip (g ξ) (e (-L x ξ) • f x) ∂μ) ∂ν := by congr with ξ apply (ContinuousLinearMap.integral_comp_comm _ _).symm - exact (fourier_integral_convergent_iff he hL _).1 hf + exact (fourierIntegral_convergent_iff he hL _).2 hf _ = ∫ x, (∫ ξ, M.flip (g ξ) (e (-L x ξ) • f x) ∂ν) ∂μ := by rw [integral_integral_swap] have : Integrable (fun (p : W × V) ↦ ‖M‖ * (‖g p.1‖ * ‖f p.2‖)) (ν.prod μ) := @@ -222,7 +225,7 @@ theorem integral_bilin_fourierIntegral_eq_flip _ = ∫ x, M (f x) (∫ ξ, e (-L.flip ξ x) • g ξ ∂ν) ∂μ := by congr with x apply ContinuousLinearMap.integral_comp_comm - apply (fourier_integral_convergent_iff he _ _).1 hg + apply (fourierIntegral_convergent_iff he _ _).2 hg exact hL.comp continuous_swap /-- The Fourier transform satisfies `∫ 𝓕 f * g = ∫ f * 𝓕 g`, i.e., it is self-adjoint. -/ @@ -317,6 +320,16 @@ theorem vector_fourierIntegral_eq_integral_exp_smul {V : Type*} [AddCommGroup V] neg_mul] #align real.vector_fourier_integral_eq_integral_exp_smul Real.vector_fourierIntegral_eq_integral_exp_smul +/-- The Fourier integral is well defined iff the function is integrable. Version with a general +continuous bilinear function `L`. For the specialization to the inner product in an inner product +space, see `Real.fourierIntegral_convergent_iff`. -/ +@[simp] +theorem fourierIntegral_convergent_iff' {V W : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] + [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace V] [BorelSpace V] {μ : Measure V} + {f : V → E} (L : V →L[ℝ] W →L[ℝ] ℝ) (w : W) : + Integrable (fun v : V ↦ 𝐞 (- L v w) • f v) μ ↔ Integrable f μ := + VectorFourier.fourierIntegral_convergent_iff (E := E) (L := L.toLinearMap₂) + continuous_fourierChar L.continuous₂ _ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type*} [NormedAddCommGroup V] @@ -384,4 +397,8 @@ theorem fourierIntegral_real_eq_integral_exp_smul (f : ℝ → E) (w : ℝ) : @[deprecated] alias fourierIntegral_eq_integral_exp_smul := fourierIntegral_real_eq_integral_exp_smul -- deprecated on 2024-02-21 +@[simp] theorem fourierIntegral_convergent_iff {μ : Measure V} {f : V → E} (w : V) : + Integrable (fun v : V ↦ 𝐞 (- ⟪v, w⟫) • f v) μ ↔ Integrable f μ := + fourierIntegral_convergent_iff' (innerSL ℝ) w + end Real diff --git a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean index d2175fcbc958ef..704c7fed158e22 100644 --- a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean +++ b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean @@ -6,23 +6,58 @@ Authors: Alex Kontorovich, David Loeffler, Heather Macbeth import Mathlib.Analysis.Calculus.ParametricIntegral import Mathlib.Analysis.Fourier.AddCircle import Mathlib.Analysis.Fourier.FourierTransform + /-! # Derivative of the Fourier transform -In this file we compute the Fréchet derivative of `𝓕 f`, where `f` is a function such that both -`f` and `v ↦ ‖v‖ * ‖f v‖` are integrable. Here `𝓕` is understood as an operator `(V → E) → (W → E)`, -where `V` and `W` are normed `ℝ`-vector spaces and the Fourier transform is taken with respect to a -continuous `ℝ`-bilinear pairing `L : V × W → ℝ`. +In this file we compute the Fréchet derivative of the Fourier transform of `f`, where `f` is a +function such that both `f` and `v ↦ ‖v‖ * ‖f v‖` are integrable. Here the Fourier transform is +understood as an operator `(V → E) → (W → E)`, where `V` and `W` are normed `ℝ`-vector spaces +and the Fourier transform is taken with respect to a continuous `ℝ`-bilinear +pairing `L : V × W → ℝ` and a given reference measure `μ`. + +We give specialized versions of these results on inner product spaces (where `L` is the scalar +product) and on the real line, where we express the one-dimensional derivative in more concrete +terms, as the Fourier transform of `x * f x`. + +## Main definitions and results + +We introduce one convenience definition: + +* `VectorFourier.fourierSMulRight L f`: given `f : V → E` and `L` a bilinear pairing + between `V` and `W`, then this is the function `fun v ↦ -(2 * π * I) (L v ⬝) • f v`, + from `V` to `Hom (W, E)`. + This is essentially `ContinousLinearMap.smulRight`, up to the factor `- 2πI` designed to make sure + that the Fourier integral of `fourierSMulRight L f` is the derivative of the Fourier + integral of `f`. -We also give a separate lemma for the most common case when `V = W = ℝ` and `L` is the obvious -multiplication map. +With this definition, the statements read as follows, first in a general context +(arbitrary `L` and `μ`): + +* `VectorFourier.hasFDerivAt_fourierIntegral`: the Fourier integral of `f` is differentiable, with + derivative the Fourier integral of `fourierSMulRight L f`. +* `VectorFourier.differentiable_fourierIntegral`: the Fourier integral of `f` is differentiable. +* `VectorFourier.fderiv_fourierIntegral`: formula for the derivative of the Fourier integral of `f`. + +These statements are then specialized to the case of the usual Fourier transform on +finite-dimensional inner product spaces with their canonical Lebesgue measure (covering in +particular the case of the real line), replacing the namespace `VectorFourier` by +the namespace `Real` in the above statements. + +We also give specialized versions of the one-dimensional real derivative +in `Real.deriv_fourierIntegral`. -/ noncomputable section open Real Complex MeasureTheory Filter TopologicalSpace -open scoped FourierTransform Topology +open scoped FourierTransform Topology BigOperators + +-- without this local instance, Lean tries first the instance +-- `secondCountableTopologyEither_of_right` (whose priority is 100) and takes a very long time to +-- fail. Since we only use the left instance in this file, we make sure it is tried first. +attribute [local instance 101] secondCountableTopologyEither_of_left lemma Real.hasDerivAt_fourierChar (x : ℝ) : HasDerivAt (𝐞 · : ℝ → ℂ) (2 * π * I * 𝐞 x) x := by have h1 (y : ℝ) : 𝐞 y = fourier 1 (y : UnitAddCircle) := by @@ -39,117 +74,146 @@ variable {V W : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) /-- Send a function `f : V → E` to the function `f : V → Hom (W, E)` given by -`v ↦ (w ↦ -2 * π * I * L(v, w) • f v)`. -/ -def mul_L (v : V) : (W →L[ℝ] E) := -(2 * π * I) • (L v).smulRight (f v) +`v ↦ (w ↦ -2 * π * I * L (v, w) • f v)`. This is designed so that the Fourier transform of +`fourierSMulRight L f` is the derivative of the Fourier transform of `f`. -/ +def fourierSMulRight (v : V) : (W →L[ℝ] E) := -(2 * π * I) • (L v).smulRight (f v) + +@[simp] lemma fourierSMulRight_apply (v : V) (w : W) : + fourierSMulRight L f v w = -(2 * π * I) • L v w • f v := rfl /-- The `w`-derivative of the Fourier transform integrand. -/ -lemma hasFDerivAt_fourier_transform_integrand_right (v : V) (w : W) : - HasFDerivAt (fun w' ↦ 𝐞 (-L v w') • f v) (𝐞 (-L v w) • mul_L L f v) w := by +lemma hasFDerivAt_fourierChar_smul (v : V) (w : W) : + HasFDerivAt (fun w' ↦ 𝐞 (-L v w') • f v) (𝐞 (-L v w) • fourierSMulRight L f v) w := by have ha : HasFDerivAt (fun w' : W ↦ L v w') (L v) w := ContinuousLinearMap.hasFDerivAt (L v) convert ((hasDerivAt_fourierChar (-L v w)).hasFDerivAt.comp w ha.neg).smul_const (f v) ext1 w' - simp_rw [mul_L, ContinuousLinearMap.smul_apply, ContinuousLinearMap.smulRight_apply] + simp_rw [fourierSMulRight, ContinuousLinearMap.smul_apply, ContinuousLinearMap.smulRight_apply] rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.neg_apply, ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, ← smul_assoc, smul_comm, ← smul_assoc, real_smul, real_smul, Submonoid.smul_def, smul_eq_mul] push_cast ring_nf -/-- Norm of the `w`-derivative of the Fourier transform integrand. -/ -lemma norm_fderiv_fourier_transform_integrand_right - (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (v : V) (w : W) : - ‖𝐞 (-L v w) • mul_L L f v‖ = (2 * π) * ‖L v‖ * ‖f v‖ := by - rw [norm_circle_smul (𝐞 (-L v w)) (mul_L L f v), mul_L, - norm_smul _ (ContinuousLinearMap.smulRight (L v) (f v)), norm_neg, norm_mul, norm_mul, - norm_eq_abs I, abs_I, mul_one, norm_eq_abs ((_ : ℝ) : ℂ), - Complex.abs_of_nonneg pi_pos.le, norm_eq_abs (2 : ℂ), +lemma norm_fourierSMulRight (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (v : V) : + ‖fourierSMulRight L f v‖ = (2 * π) * ‖L v‖ * ‖f v‖ := by + rw [fourierSMulRight, norm_smul _ (ContinuousLinearMap.smulRight (L v) (f v)), + norm_neg, norm_mul, norm_mul, norm_eq_abs I, abs_I, + mul_one, norm_eq_abs ((_ : ℝ) : ℂ), Complex.abs_of_nonneg pi_pos.le, norm_eq_abs (2 : ℂ), Complex.abs_two, ContinuousLinearMap.norm_smulRight_apply, ← mul_assoc] -lemma norm_fderiv_fourier_transform_integrand_right_le (v : V) (w : W) : - ‖𝐞 (-L v w) • (mul_L L f v)‖ ≤ (2 * π) * ‖L‖ * ‖v‖ * ‖f v‖ := by - rw [norm_fderiv_fourier_transform_integrand_right] - refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _) - conv_rhs => rw [mul_assoc] - exact mul_le_mul_of_nonneg_left (L.le_opNorm _) two_pi_pos.le +lemma norm_fourierSMulRight_le (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (v : V) : + ‖fourierSMulRight L f v‖ ≤ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖ := calc + ‖fourierSMulRight L f v‖ = (2 * π) * ‖L v‖ * ‖f v‖ := norm_fourierSMulRight _ _ _ + _ ≤ (2 * π) * (‖L‖ * ‖v‖) * ‖f v‖ := by gcongr; exact L.le_opNorm _ + _ = 2 * π * ‖L‖ * ‖v‖ * ‖f v‖ := by ring + +lemma _root_.MeasureTheory.AEStronglyMeasurable.fourierSMulRight + [SecondCountableTopologyEither V (W →L[ℝ] ℝ)] [MeasurableSpace V] [BorelSpace V] + {L : V →L[ℝ] W →L[ℝ] ℝ} {f : V → E} {μ : Measure V} + (hf : AEStronglyMeasurable f μ) : + AEStronglyMeasurable (fun v ↦ fourierSMulRight L f v) μ := by + apply AEStronglyMeasurable.const_smul' + have aux0 : Continuous fun p : (W →L[ℝ] ℝ) × E ↦ p.1.smulRight p.2 := + (ContinuousLinearMap.smulRightL ℝ W E).continuous₂ + have aux1 : AEStronglyMeasurable (fun v ↦ (L v, f v)) μ := + L.continuous.aestronglyMeasurable.prod_mk hf + exact aux0.comp_aestronglyMeasurable aux1 variable {f} /-- Main theorem of this section: if both `f` and `x ↦ ‖x‖ * ‖f x‖` are integrable, then the Fourier transform of `f` has a Fréchet derivative (everywhere in its domain) and its derivative is -the Fourier transform of `mul_L L f`. -/ -theorem hasFDerivAt_fourier [CompleteSpace E] [MeasurableSpace V] [BorelSpace V] {μ : Measure V} - [SecondCountableTopologyEither V (W →L[ℝ] ℝ)] +the Fourier transform of `smulRight L f`. -/ +theorem hasFDerivAt_fourierIntegral [CompleteSpace E] + [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] {μ : Measure V} (hf : Integrable f μ) (hf' : Integrable (fun v : V ↦ ‖v‖ * ‖f v‖) μ) (w : W) : - HasFDerivAt (VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ f) - (VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ (mul_L L f) w) w := by + HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₂ f) + (fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f) w) w := by let F : W → V → E := fun w' v ↦ 𝐞 (-L v w') • f v - let F' : W → V → W →L[ℝ] E := fun w' v ↦ 𝐞 (-L v w') • mul_L L f v + let F' : W → V → W →L[ℝ] E := fun w' v ↦ 𝐞 (-L v w') • fourierSMulRight L f v let B : V → ℝ := fun v ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖ have h0 (w' : W) : Integrable (F w') μ := - (VectorFourier.fourier_integral_convergent_iff continuous_fourierChar - (by apply L.continuous₂ : Continuous (fun p : V × W ↦ L.toLinearMap₂ p.1 p.2)) w').mp hf + (fourierIntegral_convergent_iff continuous_fourierChar + (by apply L.continuous₂ : Continuous (fun p : V × W ↦ L.toLinearMap₂ p.1 p.2)) w').2 hf have h1 : ∀ᶠ w' in 𝓝 w, AEStronglyMeasurable (F w') μ := eventually_of_forall (fun w' ↦ (h0 w').aestronglyMeasurable) have h3 : AEStronglyMeasurable (F' w) μ := by - refine .smul ?_ ?_ - · refine (continuous_fourierChar.comp ?_).aestronglyMeasurable - exact (L.continuous₂.comp (Continuous.Prod.mk_left w)).neg - · apply AEStronglyMeasurable.const_smul' - have aux0 : Continuous fun p : (W →L[ℝ] ℝ) × E ↦ p.1.smulRight p.2 := - (ContinuousLinearMap.smulRightL ℝ W E).continuous₂ - have aux1 : AEStronglyMeasurable (fun v ↦ (L v, f v)) μ := - L.continuous.aestronglyMeasurable.prod_mk hf.1 - apply aux0.comp_aestronglyMeasurable aux1 + refine .smul ?_ hf.1.fourierSMulRight + refine (continuous_fourierChar.comp ?_).aestronglyMeasurable + exact (L.continuous₂.comp (Continuous.Prod.mk_left w)).neg have h4 : (∀ᵐ v ∂μ, ∀ (w' : W), w' ∈ Metric.ball w 1 → ‖F' w' v‖ ≤ B v) := by filter_upwards with v w' _ - exact norm_fderiv_fourier_transform_integrand_right_le L f v w' + rw [norm_circle_smul _ (fourierSMulRight L f v)] + exact norm_fourierSMulRight_le L f v have h5 : Integrable B μ := by simpa only [← mul_assoc] using hf'.const_mul (2 * π * ‖L‖) have h6 : ∀ᵐ v ∂μ, ∀ w', w' ∈ Metric.ball w 1 → HasFDerivAt (fun x ↦ F x v) (F' w' v) w' := - ae_of_all _ (fun v w' _ ↦ hasFDerivAt_fourier_transform_integrand_right L f v w') + ae_of_all _ (fun v w' _ ↦ hasFDerivAt_fourierChar_smul L f v w') exact hasFDerivAt_integral_of_dominated_of_fderiv_le one_pos h1 (h0 w) h3 h4 h5 h6 -section inner - -variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [SecondCountableTopology V] - [MeasurableSpace V] [BorelSpace V] [CompleteSpace E] - -/-- Notation for the Fourier transform on a real inner product space -/ -abbrev integralFourier (f : V → E) (μ : Measure V := by volume_tac) := - fourierIntegral 𝐞 μ (innerₛₗ ℝ) f - -/-- The Fréchet derivative of the Fourier transform of `f` is the Fourier transform of - `fun v ↦ ((-2 * π * I) • f v) ⊗ (innerSL ℝ v)`. -/ -theorem InnerProductSpace.hasFDerivAt_fourier {f : V → E} {μ : Measure V} - (hf_int : Integrable f μ) (hvf_int : Integrable (fun v ↦ ‖v‖ * ‖f v‖) μ) (x : V) : - HasFDerivAt (integralFourier f μ) (integralFourier (mul_L (innerSL ℝ) f) μ x) x := by - haveI : SecondCountableTopologyEither V (V →L[ℝ] ℝ) := - secondCountableTopologyEither_of_left V _ -- for some reason it fails to synthesize this? - exact VectorFourier.hasFDerivAt_fourier (innerSL ℝ) hf_int hvf_int x +lemma fderiv_fourierIntegral [CompleteSpace E] + [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] {μ : Measure V} + (hf : Integrable f μ) (hf' : Integrable (fun v : V ↦ ‖v‖ * ‖f v‖) μ) (w : W) : + fderiv ℝ (fourierIntegral 𝐞 μ L.toLinearMap₂ f) w = + fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f) w := + (hasFDerivAt_fourierIntegral L hf hf' w).fderiv -end inner +lemma differentiable_fourierIntegral [CompleteSpace E] + [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] {μ : Measure V} + (hf : Integrable f μ) (hf' : Integrable (fun v : V ↦ ‖v‖ * ‖f v‖) μ) : + Differentiable ℝ (fourierIntegral 𝐞 μ L.toLinearMap₂ f) := + fun w ↦ (hasFDerivAt_fourierIntegral L hf hf' w).differentiableAt end VectorFourier +namespace Real open VectorFourier -lemma hasDerivAt_fourierIntegral [CompleteSpace E] +variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] + [MeasurableSpace V] [BorelSpace V] [CompleteSpace E] {f : V → E} + +/-- The Fréchet derivative of the Fourier transform of `f` is the Fourier transform of + `fun v ↦ -2 * π * I ⟪v, ⬝⟫ f v`. -/ +theorem hasFDerivAt_fourierIntegral + (hf_int : Integrable f) (hvf_int : Integrable (fun v ↦ ‖v‖ * ‖f v‖)) (x : V) : + HasFDerivAt (𝓕 f) (𝓕 (fourierSMulRight (innerSL ℝ) f) x) x := + VectorFourier.hasFDerivAt_fourierIntegral (innerSL ℝ) hf_int hvf_int x + +/-- The Fréchet derivative of the Fourier transform of `f` is the Fourier transform of + `fun v ↦ -2 * π * I ⟪v, ⬝⟫ f v`. -/ +theorem fderiv_fourierIntegral + (hf_int : Integrable f) (hvf_int : Integrable (fun v ↦ ‖v‖ * ‖f v‖)) (x : V) : + fderiv ℝ (𝓕 f) x = 𝓕 (fourierSMulRight (innerSL ℝ) f) x := + VectorFourier.fderiv_fourierIntegral (innerSL ℝ) hf_int hvf_int x + +theorem differentiable_fourierIntegral + (hf_int : Integrable f) (hvf_int : Integrable (fun v ↦ ‖v‖ * ‖f v‖)) : + Differentiable ℝ (𝓕 f) := + VectorFourier.differentiable_fourierIntegral (innerSL ℝ) hf_int hvf_int + +lemma hasDerivAt_fourierIntegral {f : ℝ → E} (hf : Integrable f) (hf' : Integrable (fun x : ℝ ↦ x • f x)) (w : ℝ) : - HasDerivAt (𝓕 f) (𝓕 (fun x : ℝ ↦ (-2 * ↑π * I * x) • f x) w) w := by + HasDerivAt (𝓕 f) (𝓕 (fun x : ℝ ↦ (-2 * π * I * x) • f x) w) w := by have hf'' : Integrable (fun v : ℝ ↦ ‖v‖ * ‖f v‖) := by simpa only [norm_smul] using hf'.norm let L := ContinuousLinearMap.mul ℝ ℝ - have h_int : Integrable fun v ↦ mul_L L f v := by + have h_int : Integrable fun v ↦ fourierSMulRight L f v := by suffices Integrable fun v ↦ ContinuousLinearMap.smulRight (L v) (f v) by - simpa only [mul_L, neg_smul, neg_mul, Pi.smul_apply] using this.smul (-2 * π * I) + simpa only [fourierSMulRight, neg_smul, neg_mul, Pi.smul_apply] using this.smul (-2 * π * I) convert ((ContinuousLinearMap.ring_lmap_equiv_self ℝ E).symm.toContinuousLinearEquiv.toContinuousLinearMap).integrable_comp hf' using 2 with v apply ContinuousLinearMap.ext_ring rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.mul_apply', mul_one, ContinuousLinearMap.map_smul] exact congr_arg (fun x ↦ v • x) (one_smul ℝ (f v)).symm - rw [fourier_integral_convergent_iff continuous_fourierChar L.continuous₂ w] at h_int - convert (hasFDerivAt_fourier L hf hf'' w).hasDerivAt using 1 + rw [← VectorFourier.fourierIntegral_convergent_iff continuous_fourierChar L.continuous₂ w] + at h_int + convert (VectorFourier.hasFDerivAt_fourierIntegral L hf hf'' w).hasDerivAt using 1 erw [ContinuousLinearMap.integral_apply h_int] - simp_rw [ContinuousLinearMap.smul_apply, mul_L, ContinuousLinearMap.smul_apply, + simp_rw [ContinuousLinearMap.smul_apply, fourierSMulRight, ContinuousLinearMap.smul_apply, ContinuousLinearMap.smulRight_apply, L, ContinuousLinearMap.mul_apply', mul_one, ← neg_mul, mul_smul] rfl + +theorem deriv_fourierIntegral + {f : ℝ → E} (hf : Integrable f) (hf' : Integrable (fun x : ℝ ↦ x • f x)) (x : ℝ) : + deriv (𝓕 f) x = 𝓕 (fun x : ℝ ↦ (-2 * π * I * x) • f x) x := + (hasDerivAt_fourierIntegral hf hf' x).deriv diff --git a/Mathlib/Analysis/Fourier/Inversion.lean b/Mathlib/Analysis/Fourier/Inversion.lean index fb02a862603f66..82d6ff12384fd2 100644 --- a/Mathlib/Analysis/Fourier/Inversion.lean +++ b/Mathlib/Analysis/Fourier/Inversion.lean @@ -77,7 +77,7 @@ lemma tendsto_integral_gaussian_smul (hf : Integrable f) (h'f : Integrable (𝓕 have : Integrable (fun w ↦ 𝐞 ⟪w, v⟫ • (𝓕 f) w) := by have B : Continuous fun p : V × V => (- innerₗ V) p.1 p.2 := continuous_inner.neg simpa using - (VectorFourier.fourier_integral_convergent_iff Real.continuous_fourierChar B v).1 h'f + (VectorFourier.fourierIntegral_convergent_iff Real.continuous_fourierChar B v).2 h'f convert tendsto_integral_cexp_sq_smul this using 4 with c w · rw [Submonoid.smul_def, Real.fourierChar_apply, smul_smul, ← Complex.exp_add, real_inner_comm] congr 3 diff --git a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean index c225636b72fc48..1219eee829f29c 100644 --- a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean +++ b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean @@ -58,21 +58,14 @@ section InnerProductSpace variable [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] -/-- The integrand in the Riemann-Lebesgue lemma for `f` is integrable iff `f` is. -/ -theorem fourier_integrand_integrable (w : V) : - Integrable f ↔ Integrable fun v : V => 𝐞 (-⟪v, w⟫) • f v := by - have hL : Continuous fun p : V × V => bilinFormOfRealInner p.1 p.2 := - continuous_inner - rw [VectorFourier.fourier_integral_convergent_iff Real.continuous_fourierChar hL w] - simp only [bilinFormOfRealInner_apply_apply, ofAdd_neg, map_inv, coe_inv_unitSphere] -#align fourier_integrand_integrable fourier_integrand_integrable +#align fourier_integrand_integrable Real.fourierIntegral_convergent_iff variable [CompleteSpace E] local notation3 "i" => fun (w : V) => (1 / (2 * ‖w‖ ^ 2) : ℝ) • w /-- Shifting `f` by `(1 / (2 * ‖w‖ ^ 2)) • w` negates the integral in the Riemann-Lebesgue lemma. -/ -theorem fourier_integral_half_period_translate {w : V} (hw : w ≠ 0) : +theorem fourierIntegral_half_period_translate {w : V} (hw : w ≠ 0) : (∫ v : V, 𝐞 (-⟪v, w⟫) • f (v + i w)) = -∫ v : V, 𝐞 (-⟪v, w⟫) • f v := by have hiw : ⟪i w, w⟫ = 1 / 2 := by rw [inner_smul_left, inner_self_eq_norm_sq_to_K, RCLike.ofReal_real_eq_id, id.def, @@ -97,19 +90,19 @@ theorem fourier_integral_half_period_translate {w : V} (hw : w ≠ 0) : ((fun w ↦ (1 / (2 * ‖w‖ ^ (2 : ℕ))) • w) w) rw [this] simp only [neg_smul, integral_neg] -#align fourier_integral_half_period_translate fourier_integral_half_period_translate +#align fourier_integral_half_period_translate fourierIntegral_half_period_translate /-- Rewrite the Fourier integral in a form that allows us to use uniform continuity. -/ -theorem fourier_integral_eq_half_sub_half_period_translate {w : V} (hw : w ≠ 0) +theorem fourierIntegral_eq_half_sub_half_period_translate {w : V} (hw : w ≠ 0) (hf : Integrable f) : ∫ v : V, 𝐞 (-⟪v, w⟫) • f v = (1 / (2 : ℂ)) • ∫ v : V, 𝐞 (-⟪v, w⟫) • (f v - f (v + i w)) := by simp_rw [smul_sub] - rw [integral_sub, fourier_integral_half_period_translate hw, sub_eq_add_neg, neg_neg, ← + rw [integral_sub, fourierIntegral_half_period_translate hw, sub_eq_add_neg, neg_neg, ← two_smul ℂ _, ← @smul_assoc _ _ _ _ _ _ (IsScalarTower.left ℂ), smul_eq_mul] norm_num - exacts [(fourier_integrand_integrable w).mp hf, - (fourier_integrand_integrable w).mp (hf.comp_add_right _)] -#align fourier_integral_eq_half_sub_half_period_translate fourier_integral_eq_half_sub_half_period_translate + exacts [(Real.fourierIntegral_convergent_iff w).2 hf, + (Real.fourierIntegral_convergent_iff w).2 (hf.comp_add_right _)] +#align fourier_integral_eq_half_sub_half_period_translate fourierIntegral_eq_half_sub_half_period_translate /-- Riemann-Lebesgue Lemma for continuous and compactly-supported functions: the integral `∫ v, exp (-2 * π * ⟪w, v⟫ * I) • f v` tends to 0 wrt `cocompact V`. Note that this is primarily @@ -153,7 +146,7 @@ theorem tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support sq, ← div_div, ← div_div, ← div_div, div_mul_cancel₀ _ (norm_eq_zero.not.mpr hw_ne)] --* Rewrite integral in terms of `f v - f (v + w')`. have : ‖(1 / 2 : ℂ)‖ = 2⁻¹ := by norm_num - rw [fourier_integral_eq_half_sub_half_period_translate hw_ne + rw [fourierIntegral_eq_half_sub_half_period_translate hw_ne (hf1.integrable_of_hasCompactSupport hf2), norm_smul, this, inv_mul_eq_div, div_lt_iff' two_pos] refine' lt_of_le_of_lt (norm_integral_le_integral_norm _) _ @@ -210,7 +203,7 @@ theorem tendsto_integral_exp_inner_smul_cocompact : by_cases hfi : Integrable f; swap · convert tendsto_const_nhds (x := (0 : E)) with w apply integral_undef - rwa [← fourier_integrand_integrable w] + rwa [Real.fourierIntegral_convergent_iff] refine' Metric.tendsto_nhds.mpr fun ε hε => _ obtain ⟨g, hg_supp, hfg, hg_cont, -⟩ := hfi.exists_hasCompactSupport_integral_sub_le (div_pos hε two_pos) @@ -223,8 +216,8 @@ theorem tendsto_integral_exp_inner_smul_cocompact : rw [dist_eq_norm] at hI ⊢ have : ‖(∫ v, 𝐞 (-⟪v, w⟫) • f v) - ∫ v, 𝐞 (-⟪v, w⟫) • g v‖ ≤ ε / 2 := by refine' le_trans _ hfg - simp_rw [← integral_sub ((fourier_integrand_integrable w).mp hfi) - ((fourier_integrand_integrable w).mp (hg_cont.integrable_of_hasCompactSupport hg_supp)), + simp_rw [← integral_sub ((Real.fourierIntegral_convergent_iff w).2 hfi) + ((Real.fourierIntegral_convergent_iff w).2 (hg_cont.integrable_of_hasCompactSupport hg_supp)), ← smul_sub, ← Pi.sub_apply] exact VectorFourier.norm_fourierIntegral_le_integral_norm 𝐞 _ bilinFormOfRealInner (f - g) w replace := add_lt_add_of_le_of_lt this hI