From e6beef21a8aee01f05b02ea03dcd2f54a5c179f5 Mon Sep 17 00:00:00 2001 From: Moritz Doll Date: Thu, 21 Mar 2024 14:51:09 +0000 Subject: [PATCH] feat(Analysis/Distribution/SchwartzSpace): generalize the integral (#11373) --- .../Distribution/FourierSchwartz.lean | 5 +- .../Analysis/Distribution/SchwartzSpace.lean | 96 ++++++++++++------- .../SpecialFunctions/JapaneseBracket.lean | 15 ++- 3 files changed, 74 insertions(+), 42 deletions(-) diff --git a/Mathlib/Analysis/Distribution/FourierSchwartz.lean b/Mathlib/Analysis/Distribution/FourierSchwartz.lean index f230722b2be16d..db60ee250ce3c5 100644 --- a/Mathlib/Analysis/Distribution/FourierSchwartz.lean +++ b/Mathlib/Analysis/Distribution/FourierSchwartz.lean @@ -35,8 +35,9 @@ Fourier transform of `VectorFourier.mul_L_schwartz L f`. -/ def VectorFourier.mul_L_schwartz : 𝓢(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 = VectorFourier.mul_L L f d := rfl + VectorFourier.mul_L_schwartz L f d = -(2 * π * I) • (L d).smulRight (f d) := rfl attribute [local instance 200] secondCountableTopologyEither_of_left @@ -47,4 +48,4 @@ theorem SchwartzMap.hasFDerivAt_fourier [CompleteSpace V] [MeasurableSpace D] [B HasFDerivAt (fourierIntegral fourierChar μ L.toLinearMap₂ f) (fourierIntegral fourierChar μ L.toLinearMap₂ (mul_L_schwartz L f) w) w := VectorFourier.hasFDerivAt_fourier L f.integrable - (by simpa using f.integrable_pow_mul (μ := μ) 1) w + (by simpa using f.integrable_pow_mul μ 1) w diff --git a/Mathlib/Analysis/Distribution/SchwartzSpace.lean b/Mathlib/Analysis/Distribution/SchwartzSpace.lean index 114852b2c8e2e8..be6a916125e0be 100644 --- a/Mathlib/Analysis/Distribution/SchwartzSpace.lean +++ b/Mathlib/Analysis/Distribution/SchwartzSpace.lean @@ -7,10 +7,10 @@ import Mathlib.Analysis.Calculus.ContDiff.Bounds import Mathlib.Analysis.Calculus.IteratedDeriv.Defs import Mathlib.Analysis.Calculus.LineDeriv.Basic import Mathlib.Analysis.LocallyConvex.WithSeminorms -import Mathlib.Topology.Algebra.UniformFilterBasis import Mathlib.Analysis.Normed.Group.ZeroAtInfty import Mathlib.Analysis.SpecialFunctions.Pow.Real import Mathlib.Analysis.SpecialFunctions.JapaneseBracket +import Mathlib.Topology.Algebra.UniformFilterBasis #align_import analysis.schwartz_space from "leanprover-community/mathlib"@"e137999b2c6f2be388f4cd3bbf8523de1910cd2b" @@ -658,6 +658,23 @@ lemma _root_.ContinuousLinearMap.hasTemperateGrowth (f : E →L[ℝ] F) : simpa [this] using .const _ · exact (f.le_op_norm x).trans (by simp [mul_add]) +variable [NormedAddCommGroup D] [NormedSpace ℝ D] +variable [MeasurableSpace D] [BorelSpace D] [SecondCountableTopology D] [FiniteDimensional ℝ D] + +open MeasureTheory FiniteDimensional + +/-- A measure `μ` has temperate growth if there is an `n : ℕ` such that `(1 + ‖x‖) ^ (- n)` is +`μ`-integrable. -/ +class _root_.MeasureTheory.Measure.HasTemperateGrowth (μ : Measure D) : Prop := + exists_integrable : ∃ (n : ℕ), Integrable (fun x ↦ (1 + ‖x‖) ^ (- (n : ℝ))) μ + +instance _root_.MeasureTheory.Measure.IsFiniteMeasure.instHasTemperateGrowth {μ : Measure D} + [h : IsFiniteMeasure μ] : μ.HasTemperateGrowth := ⟨⟨0, by simp⟩⟩ + +instance _root_.MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth {μ : Measure D} + [h : μ.IsAddHaarMeasure] : μ.HasTemperateGrowth := + ⟨⟨finrank ℝ D + 1, by apply integrable_one_add_norm; norm_num⟩⟩ + end TemperateGrowth section CLM @@ -1009,63 +1026,66 @@ section Integration open Real Complex Filter MeasureTheory MeasureTheory.Measure FiniteDimensional -variable [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup V] [NormedSpace ℂ V] -variable [MeasurableSpace D] [BorelSpace D] [FiniteDimensional ℝ D] +variable [IsROrC 𝕜] +variable [NormedAddCommGroup D] [NormedSpace ℝ D] +variable [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedSpace 𝕜 V] +variable [MeasurableSpace D] [BorelSpace D] [SecondCountableTopology D] + +variable {μ : Measure D} [hμ : HasTemperateGrowth μ] -lemma integrable_pow_mul (f : 𝓢(D, V)) {μ : Measure D} (k : ℕ) [IsAddHaarMeasure μ] : - Integrable (fun x ↦ ‖x‖ ^ k * ‖f x‖) μ := by - let l := finrank ℝ D + 1 + k +variable (μ) in +lemma integrable_pow_mul (f : 𝓢(D, V)) + (k : ℕ) : Integrable (fun x ↦ ‖x‖ ^ k * ‖f x‖) μ := by + rcases hμ.exists_integrable with ⟨n, h⟩ + let l := n + k obtain ⟨C, C_nonneg, hC⟩ : ∃ C, 0 ≤ C ∧ ∀ x, (1 + ‖x‖) ^ l * ‖f x‖ ≤ C := by use 2 ^ l * (Finset.Iic (l, 0)).sup (fun m ↦ SchwartzMap.seminorm ℝ m.1 m.2) f, by positivity simpa using f.one_add_le_sup_seminorm_apply (m := (l, 0)) (k := l) (n := 0) le_rfl le_rfl - have : Integrable (fun x : D ↦ C * (1 + ‖x‖) ^ (-((finrank ℝ D + 1 : ℕ) : ℝ))) μ := by - apply (integrable_one_add_norm ?_).const_mul - exact Nat.cast_lt.mpr Nat.le.refl + have : Integrable (fun x : D ↦ C * (1 + ‖x‖) ^ (-(n : ℝ))) μ := h.const_mul _ apply this.mono ((aestronglyMeasurable_id.norm.pow _).mul f.continuous.aestronglyMeasurable.norm) (eventually_of_forall (fun x ↦ ?_)) conv_rhs => rw [norm_of_nonneg (by positivity), rpow_neg (by positivity), ← div_eq_mul_inv] rw [le_div_iff' (by positivity)] simp only [id_eq, Pi.mul_apply, Pi.pow_apply, norm_mul, norm_pow, norm_norm, rpow_nat_cast] calc - (1 + ‖x‖) ^ (finrank ℝ D + 1) * (‖x‖ ^ k * ‖f x‖) - ≤ (1 + ‖x‖) ^ (finrank ℝ D + 1) * ((1 + ‖x‖) ^ k * ‖f x‖) := by gcongr; simp - _ = (1 + ‖x‖) ^ (finrank ℝ D + 1 + k) * ‖f x‖ := by simp only [pow_add, mul_assoc] + (1 + ‖x‖) ^ n * (‖x‖ ^ k * ‖f x‖) + ≤ (1 + ‖x‖) ^ n * ((1 + ‖x‖) ^ k * ‖f x‖) := by gcongr; simp + _ = (1 + ‖x‖) ^ (n + k) * ‖f x‖ := by simp only [pow_add, mul_assoc] _ ≤ C := hC x -lemma integrable (f : 𝓢(D, V)) {μ : Measure D} [IsAddHaarMeasure μ] : - Integrable f μ := - (f.integrable_pow_mul (μ := μ) 0).mono f.continuous.aestronglyMeasurable +lemma integrable (f : 𝓢(D, V)) : Integrable f μ := + (f.integrable_pow_mul μ 0).mono f.continuous.aestronglyMeasurable (eventually_of_forall (fun _ ↦ by simp)) +variable (𝕜 μ) in /-- The integral as a continuous linear map from Schwartz space to the codomain. -/ -def integralCLM (μ : Measure D) [IsAddHaarMeasure μ] : 𝓢(D, V) →L[ℝ] V := +def integralCLM : 𝓢(D, V) →L[𝕜] V := mkCLMtoNormedSpace (∫ x, · x ∂μ) - (fun f g ↦ integral_add f.integrable g.integrable) + (fun f g ↦ by + exact integral_add f.integrable g.integrable) (integral_smul · ·) (by - let l := finrank ℝ D + 1 - let m := (l, 0) - use Finset.Iic (l, 0), 2 ^ l * ∫ x : D, (1 + ‖x‖) ^ (- (l : ℝ)) ∂μ - have hpos : 0 ≤ ∫ x : D, (1 + ‖x‖) ^ (- (l : ℝ)) ∂μ := by + rcases hμ.exists_integrable with ⟨n, h⟩ + let m := (n, 0) + use Finset.Iic m, 2 ^ n * ∫ x : D, (1 + ‖x‖) ^ (- (n : ℝ)) ∂μ + have hpos : 0 ≤ ∫ x : D, (1 + ‖x‖) ^ (- (n : ℝ)) ∂μ := by apply integral_nonneg intro positivity refine ⟨by positivity, fun f ↦ (norm_integral_le_integral_norm f).trans ?_⟩ - have h : ∀ x, ‖f x‖ ≤ (1 + ‖x‖) ^ (-(l : ℝ)) * - (2^l * ((Finset.Iic m).sup (fun m' => SchwartzMap.seminorm ℝ m'.1 m'.2) f)) := by + have h' : ∀ x, ‖f x‖ ≤ (1 + ‖x‖) ^ (-(n : ℝ)) * + (2 ^ n * ((Finset.Iic m).sup (fun m' => SchwartzMap.seminorm 𝕜 m'.1 m'.2) f)) := by intro x rw [rpow_neg (by positivity), ← div_eq_inv_mul, le_div_iff' (by positivity), rpow_nat_cast] - simpa using one_add_le_sup_seminorm_apply (m := m) (k := l) (n := 0) le_rfl le_rfl f x - apply (integral_mono (by simpa using f.integrable_pow_mul (μ := μ) 0) _ h).trans - · rw [integral_mul_right, ← mul_assoc] - gcongr ?_ * ?_ - · rw [mul_comm] - · rfl - apply (integrable_one_add_norm (by simp)).mul_const) + simpa using one_add_le_sup_seminorm_apply (m := m) (k := n) (n := 0) le_rfl le_rfl f x + apply (integral_mono (by simpa using f.integrable_pow_mul μ 0) _ h').trans + · rw [integral_mul_right, ← mul_assoc, mul_comm (2 ^ n)] + rfl + apply h.mul_const) +variable (𝕜) in @[simp] -lemma integralCLM_apply {μ : Measure D} [IsAddHaarMeasure μ] (f : 𝓢(D, V)) : - integralCLM μ f = ∫ x, f x ∂μ := rfl +lemma integralCLM_apply (f : 𝓢(D, V)) : integralCLM 𝕜 μ f = ∫ x, f x ∂μ := by rfl end Integration @@ -1120,6 +1140,8 @@ theorem toBoundedContinuousFunctionCLM_apply (f : 𝓢(E, F)) (x : E) : variable {E} +section DiracDelta + /-- The Dirac delta distribution -/ def delta (x : E) : 𝓢(E, F) →L[𝕜] F := (BoundedContinuousFunction.evalCLM 𝕜 x).comp (toBoundedContinuousFunctionCLM 𝕜 E F) @@ -1130,6 +1152,16 @@ theorem delta_apply (x₀ : E) (f : 𝓢(E, F)) : delta 𝕜 F x₀ f = f x₀ : rfl #align schwartz_map.delta_apply SchwartzMap.delta_apply +open MeasureTheory MeasureTheory.Measure + +variable [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace F] + +/-- Integrating against the Dirac measure is equal to the delta distribution. -/ +@[simp] +theorem integralCLM_dirac_eq_delta (x : E) : integralCLM 𝕜 (dirac x) = delta 𝕜 F x := by aesop + +end DiracDelta + end BoundedContinuousFunction section ZeroAtInfty diff --git a/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean b/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean index e097ea35f67ba9..b13d93f77cd028 100644 --- a/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean +++ b/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean @@ -94,8 +94,9 @@ theorem finite_integral_rpow_sub_one_pow_aux {r : ℝ} (n : ℕ) (hnr : (n : ℝ rwa [neg_lt_neg_iff, inv_mul_lt_iff' hr, one_mul] #align finite_integral_rpow_sub_one_pow_aux finite_integral_rpow_sub_one_pow_aux -theorem finite_integral_one_add_norm [MeasurableSpace E] [BorelSpace E] {μ : Measure E} - [μ.IsAddHaarMeasure] {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r) : +variable [MeasurableSpace E] [BorelSpace E] {μ : Measure E} [μ.IsAddHaarMeasure] + +theorem finite_integral_one_add_norm {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r) : (∫⁻ x : E, ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) ∂μ) < ∞ := by have hr : 0 < r := lt_of_le_of_lt (finrank ℝ E).cast_nonneg hnr -- We start by applying the layer cake formula @@ -137,9 +138,8 @@ theorem finite_integral_one_add_norm [MeasurableSpace E] [BorelSpace E] {μ : Me exact WithTop.zero_lt_top #align finite_integral_one_add_norm finite_integral_one_add_norm -theorem integrable_one_add_norm [MeasurableSpace E] [BorelSpace E] {μ : Measure E} - [μ.IsAddHaarMeasure] - {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r) : Integrable (fun x : E => (1 + ‖x‖) ^ (-r)) μ := by +theorem integrable_one_add_norm {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r) : + Integrable (fun x ↦ (1 + ‖x‖) ^ (-r)) μ := by constructor · measurability -- Lower Lebesgue integral @@ -149,9 +149,8 @@ theorem integrable_one_add_norm [MeasurableSpace E] [BorelSpace E] {μ : Measure exact finite_integral_one_add_norm hnr #align integrable_one_add_norm integrable_one_add_norm -theorem integrable_rpow_neg_one_add_norm_sq [MeasurableSpace E] [BorelSpace E] {μ : Measure E} - [μ.IsAddHaarMeasure] {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r) : - Integrable (fun x : E => ((1 : ℝ) + ‖x‖ ^ 2) ^ (-r / 2)) μ := by +theorem integrable_rpow_neg_one_add_norm_sq {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r) : + Integrable (fun x ↦ ((1 : ℝ) + ‖x‖ ^ 2) ^ (-r / 2)) μ := by have hr : 0 < r := lt_of_le_of_lt (finrank ℝ E).cast_nonneg hnr refine ((integrable_one_add_norm hnr).const_mul <| (2 : ℝ) ^ (r / 2)).mono' ?_ (eventually_of_forall fun x => ?_)