feat(Analysis/Distribution/SchwartzSpace): generalize the integral (#…

…11373)

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

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

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 => ?_)