refactor(Analysis/Fourier/Convolution): drop continuity hypotheses from the convolution theorems (leanprover-community#40583)

drop continuity hypotheses from the convolution theorems

Author: dennj

Mathlib/Analysis/Fourier/Convolution.lean

@@ -41,35 +41,19 @@ variable [NontriviallyNormedField 𝕜] [NormedAddCommGroup E]
   [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
   [NormedSpace 𝕜 F₁] [NormedSpace 𝕜 F₂] [NormedSpace 𝕜 F₃]
 
-/-- The norm of the integrant of the convolution is integrable if the functions are integrable
-and continuous. -/
+/-- The norm of the integrand of the convolution is integrable if the functions are integrable. -/
 theorem integrable_prod_sub (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) {f₁ : E → F₁} {f₂ : E → F₂}
-    (hf₁ : Integrable f₁) (hf₂ : Integrable f₂) (hf₁' : Continuous f₁) (hf₂' : Continuous f₂) :
+    (hf₁ : Integrable f₁) (hf₂ : Integrable f₂) :
     Integrable (fun (p : E × E) ↦ ‖B‖ * (‖f₁ (p.1 - p.2)‖ * ‖f₂ p.2‖)) (volume.prod volume) := by
-  apply Integrable.const_mul
-  rw [integrable_prod_iff' (by fun_prop)]
-  constructor
-  · filter_upwards with x
-    exact (hf₁.comp_sub_right x).norm.mul_const _
-  have : Integrable (fun x ↦ ((∫ y, ‖f₁ y‖) * ‖f₂ x‖)) := by
-    apply hf₂.norm.bdd_mul (by fun_prop) (c := ‖(∫ y, ‖f₁ y‖)‖)
-    filter_upwards with; rfl
-  convert! this using 1
-  ext x
-  simp_rw [norm_mul, norm_norm]
-  rw [integral_mul_const]
-  congr 1
-  convert! integral_sub_right_eq_self _ x (μ := volume)
-  rfl
+  simpa [mul_comm] using (hf₂.norm.convolution_integrand (.mul ℝ ℝ) hf₁.norm).const_mul ‖B‖
 
 open FourierTransform
 
 variable [NormedSpace ℂ F₃]
 
 /-- Calculate the Fourier transform of the convolution as a symmetric integral. -/
 theorem fourier_bilin_convolution_eq_integral (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) {f₁ : E → F₁} {f₂ : E → F₂}
-    (hf₁ : Integrable f₁) (hf₂ : Integrable f₂) (hf₁' : Continuous f₁) (hf₂' : Continuous f₂)
-    (ξ : E) :
+    (hf₁ : Integrable f₁) (hf₂ : Integrable f₂) (ξ : E) :
     𝓕 (f₁ ⋆[B] f₂) ξ = ∫ y, ∫ x, 𝐞 (-inner ℝ (y + x) ξ) • B (f₁ x) (f₂ y) := calc
   _ = 𝓕 (f₂ ⋆[B.flip] f₁) ξ := by
     rw [convolution_flip]
@@ -80,11 +64,11 @@ theorem fourier_bilin_convolution_eq_integral (B : F₁ →L[𝕜] F₂ →L[
     simp_rw [Circle.smul_def, integral_smul]
   _ = ∫ y, ∫ x, 𝐞 (-inner ℝ x ξ) • B (f₁ (x - y)) (f₂ y) := by
     refine integral_integral_swap ?_
-    apply (integrable_prod_sub B hf₁ hf₂ hf₁' hf₂').mono (by measurability)
-    filter_upwards with ⟨y, x⟩
-    have : ‖(B (f₁ (y - x))) (f₂ x)‖ ≤ ‖B‖ * (‖f₁ (y - x)‖ * ‖f₂ x‖) := by
-      grw [B.le_opNorm₂ (f₁ (y - x)) (f₂ x), mul_assoc]
-    simpa
+    have hB := hf₂.convolution_integrand B.flip hf₁
+    refine hB.mono ?_ ?_
+    · exact continuous_fourierChar.comp (by fun_prop) |>.aestronglyMeasurable.smul
+        hB.aestronglyMeasurable
+    · filter_upwards with ⟨x, y⟩ using by simp
   _ = ∫ y, ∫ x, 𝐞 (-inner ℝ (y + x) ξ) • B (f₁ x) (f₂ y) := by
     congr
     ext y
@@ -101,31 +85,18 @@ open ContinuousLinearMap
 /-- The Fourier transform of the convolution is given by the bilinear map applied to the Fourier
 transform of the individual functions. -/
 theorem fourier_bilin_convolution_eq (B : F₁ →L[ℂ] F₂ →L[ℂ] F₃) {f₁ : E → F₁} {f₂ : E → F₂}
-    (hf₁ : Integrable f₁) (hf₂ : Integrable f₂) (hf₁' : Continuous f₁) (hf₂' : Continuous f₂)
-    (ξ : E) :
+    (hf₁ : Integrable f₁) (hf₂ : Integrable f₂) (ξ : E) :
     𝓕 (f₁ ⋆[B] f₂) ξ = B (𝓕 f₁ ξ) (𝓕 f₂ ξ) := calc
   _ = ∫ y, ∫ x, 𝐞 (-inner ℝ (y + x) ξ) • B (f₁ x) (f₂ y) :=
-    fourier_bilin_convolution_eq_integral B hf₁ hf₂ hf₁' hf₂' _
+    fourier_bilin_convolution_eq_integral B hf₁ hf₂ _
   _ = ∫ y, ∫ x, 𝐞 (-inner ℝ y ξ) • 𝐞 (-inner ℝ x ξ) • B (f₁ x) (f₂ y) := by
-    congr
-    ext y
-    congr
-    ext x
-    rw [smul_smul, ← AddChar.map_add_eq_mul, inner_add_left]
-    congr
-    grind
+    simp_rw [inner_add_left, neg_add, AddChar.map_add_eq_mul, smul_smul]
   _ = ∫ y, (∫ x, B (𝐞 (-inner ℝ x ξ) • f₁ x)) (𝐞 (-inner ℝ y ξ) • f₂ y) := by
-    congr
-    ext y
-    simp_rw [Circle.smul_def, map_smul, MeasureTheory.integral_smul]
-    congr
-    rw [integral_apply ?_ (f₂ y)]
-    · simp
-    have : MeasureTheory.Integrable (fun x ↦ ‖B‖ * ‖f₁ x‖) MeasureTheory.volume :=
-      hf₁.norm.const_mul _
-    apply this.mono (by fun_prop)
-    filter_upwards with x
-    simpa [← Circle.smul_def] using le_opNorm B (f₁ x)
+    congr with y
+    have : Integrable (fun x ↦ (𝐞 (-inner ℝ x ξ) : ℂ) • B (f₁ x)) volume := by
+      simpa [Circle.smul_def] using
+        (Real.fourierIntegral_convergent_iff ξ).2 (B.integrable_comp hf₁)
+    simp [Circle.smul_def, MeasureTheory.integral_smul, integral_apply this (f₂ y)]
   _ = B (∫ x, 𝐞 (-inner ℝ x ξ) • f₁ x) (∫ y, 𝐞 (-inner ℝ y ξ) • f₂ y) := by
     rw [← integral_comp_comm _ (by simpa using hf₂), ← integral_comp_comm _ (by simpa using hf₁)]
 
@@ -134,10 +105,9 @@ of the individual functions.
 
 Version for scalar multiplication. -/
 theorem fourier_smul_convolution_eq {f₁ : E → ℂ} {f₂ : E → F₁}
-    (hf₁ : Integrable f₁) (hf₂ : Integrable f₂) (hf₁' : Continuous f₁) (hf₂' : Continuous f₂)
-    (ξ : E) :
+    (hf₁ : Integrable f₁) (hf₂ : Integrable f₂) (ξ : E) :
     𝓕 (f₁ ⋆[lsmul ℂ ℂ] f₂) ξ = (𝓕 f₁ ξ) • (𝓕 f₂ ξ) :=
-  fourier_bilin_convolution_eq (lsmul ℂ ℂ) hf₁ hf₂ hf₁' hf₂' ξ
+  fourier_bilin_convolution_eq (lsmul ℂ ℂ) hf₁ hf₂ ξ
 
 variable [NormedRing R] [NormedSpace ℂ R] [IsScalarTower ℂ R R] [SMulCommClass ℂ R R]
   [CompleteSpace R]
@@ -147,10 +117,9 @@ of the individual functions.
 
 Version for multiplication. -/
 theorem fourier_mul_convolution_eq {f₁ : E → R} {f₂ : E → R}
-    (hf₁ : Integrable f₁) (hf₂ : Integrable f₂) (hf₁' : Continuous f₁) (hf₂' : Continuous f₂)
-    (ξ : E) :
+    (hf₁ : Integrable f₁) (hf₂ : Integrable f₂) (ξ : E) :
     𝓕 (f₁ ⋆[mul ℂ R] f₂) ξ = (𝓕 f₁ ξ) * (𝓕 f₂ ξ) :=
-  fourier_bilin_convolution_eq (mul ℂ R) hf₁ hf₂ hf₁' hf₂' ξ
+  fourier_bilin_convolution_eq (mul ℂ R) hf₁ hf₂ ξ
 
 end Real
 
@@ -198,7 +167,7 @@ open MeasureTheory
 theorem fourier_convolution_apply (B : F₁ →L[ℂ] F₂ →L[ℂ] F₃) (f : 𝓢(E, F₁)) (g : 𝓢(E, F₂)) (x : E) :
     𝓕 (convolution B f g) x = 𝓕 (f ⋆[B] g) x := by
   simp [fourier_convolution, fourier_coe,
-    Real.fourier_bilin_convolution_eq B f.integrable g.integrable f.continuous g.continuous]
+    Real.fourier_bilin_convolution_eq B f.integrable g.integrable]
 
 /-- The convolution on Schwartz functions is equal to the convolution on functions. -/
 theorem convolution_apply (B : F₁ →L[ℂ] F₂ →L[ℂ] F₃) (f : 𝓢(E, F₁)) (g : 𝓢(E, F₂)) (x : E) :

Mathlib/Analysis/Fourier/FourierTransform.lean

@@ -177,7 +177,7 @@ section Fubini
 variable [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [TopologicalSpace V] [BorelSpace V]
   [TopologicalSpace W] [MeasurableSpace W] [BorelSpace W]
   {e : AddChar 𝕜 𝕊} {μ : Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜}
-  {ν : Measure W} [SigmaFinite μ] [SigmaFinite ν] [SecondCountableTopology V]
+  {ν : Measure W} [SigmaFinite μ] [SigmaFinite ν] [SecondCountableTopologyEither W V]
 
 variable {σ : ℂ →+* ℂ} [RingHomIsometric σ]