use innerSL from Mathlib instead of continuousBilinFormOfInner

Clt/Inversion.lean

@@ -52,12 +52,12 @@ variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
 lemma MeasureTheory.ProbabilityMeasure.tendsto_charPoly_of_tendsto_charFun
     (h : ∀ t : E, Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (charFun μ₀ t)))
     {g : E →ᵇ ℂ}
-    (hg : g ∈ charPoly continuous_probChar (L := bilinFormOfRealInner) continuous_inner) :
+    (hg : g ∈ charPoly continuous_probChar (L := innerₗ E) continuous_inner) :
     Tendsto (fun n ↦ ∫ x, g x ∂(μ n)) atTop (𝓝 (∫ x, g x ∂μ₀)) := by
   rw [mem_charPoly] at hg
   obtain ⟨w, hw⟩ := hg
   have h_eq (μ : Measure E) (hμ : IsProbabilityMeasure μ) :
-      ∫ x, g x ∂μ = ∑ a ∈ w.support, w a * ∫ x, (probChar (bilinFormOfRealInner x a) : ℂ) ∂μ := by
+      ∫ x, g x ∂μ = ∑ a ∈ w.support, w a * ∫ x, (probChar (innerₗ E x a) : ℂ) ∂μ := by
     simp_rw [hw]
     rw [integral_finset_sum]
     · congr with y
@@ -68,18 +68,18 @@ lemma MeasureTheory.ProbabilityMeasure.tendsto_charPoly_of_tendsto_charFun
       exact BoundedContinuousFunction.integrable μ _
   simp_rw [h_eq (μ _), h_eq μ₀]
   refine tendsto_finset_sum _ fun y hy ↦ Tendsto.const_mul _ ?_
-  simp only [bilinFormOfRealInner_apply_apply]
+  simp only [innerₗ_apply_apply]
   simp_rw [← charFun_eq_integral_probChar]
   exact h y
 
 lemma MeasureTheory.ProbabilityMeasure.tendsto_of_tendsto_charFun
-    [CompleteSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E]
+    [FiniteDimensional ℝ E]
     (h : ∀ t : E, Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (charFun μ₀ t))) :
     Tendsto μ atTop (𝓝 μ₀) := by
   have h_tight : IsTightMeasureSet (𝓧 := E) {μ n | n} :=
     isTightMeasureSet_of_tendsto_charFun (by fun_prop) (by fun_prop) h
   refine tendsto_of_tight_of_separatesPoints h_tight (𝕜 := ℂ)
-    (A := charPoly continuous_probChar (L := bilinFormOfRealInner) continuous_inner) ?_ ?_
+    (A := charPoly continuous_probChar (L := innerₗ E) continuous_inner) ?_ ?_
   · refine separatesPoints_charPoly continuous_probChar probChar_ne_one _ ?_
     exact fun v hv ↦ DFunLike.ne_iff.mpr ⟨v, inner_self_ne_zero.mpr hv⟩
   · exact fun g ↦ tendsto_charPoly_of_tendsto_charFun h
@@ -98,7 +98,7 @@ The => direction is much harder:
 
 -/
 theorem MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun
-    [CompleteSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E] :
+    [FiniteDimensional ℝ E] :
     Tendsto μ atTop (𝓝 μ₀) ↔
       ∀ t : E, Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (charFun μ₀ t)) := by
   refine ⟨fun h t ↦ ?_, tendsto_of_tendsto_charFun⟩

Clt/MomentGenerating.lean

@@ -65,28 +65,14 @@ end ForMathlib
 
 section InnerProductSpace
 
-variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
-
 /-!
 The `n`th derivative of `charFun μ`.
 The proof uses results on iterated derivatives of the Fourier transform.
 -/
 
-/-- The scalar product as a continuous bilinear map.
-TODO: this is already in Mathlib, as `innerSL ℝ`. Use that instead. -/
-noncomputable
-def continuousBilinFormOfInner : E →L[ℝ] E →L[ℝ] ℝ :=
-  (isBoundedBilinearMap_inner (𝕜 := ℝ)).toContinuousLinearMap
-
-@[simp]
-lemma continuousBilinFormOfInner_apply {x y : E} : continuousBilinFormOfInner x y = ⟪x, y⟫ := rfl
 
-@[simp]
-lemma toLinearMap₂_continuousBilinFormOfInner :
-    ContinuousLinearMap.toLinearMap₁₂ (continuousBilinFormOfInner : E →L[ℝ] E →L[ℝ] ℝ)
-      = bilinFormOfRealInner := rfl
-
-variable [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
+variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
+  [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
   {μ : Measure E} [IsProbabilityMeasure μ]
 
 @[fun_prop]
@@ -98,8 +84,7 @@ theorem contDiff_charFun
     rw [Nat.cast_le] at hk
     exact integrable_norm_pow_antitone μ aestronglyMeasurable_id hk hint
   simp_rw [funext charFun_eq_fourierIntegral']
-  rw [← toLinearMap₂_continuousBilinFormOfInner]
-  refine (VectorFourier.contDiff_fourierIntegral (L := continuousBilinFormOfInner) hint').comp ?_
+  refine (VectorFourier.contDiff_fourierIntegral (L := innerSL ℝ) hint').comp ?_
   exact contDiff_const_smul _
 
 @[fun_prop]
@@ -116,7 +101,7 @@ variable {μ : Measure ℝ} [IsProbabilityMeasure μ]
 open VectorFourier in
 theorem iteratedDeriv_charFun {n : ℕ} {t : ℝ} (hint : Integrable (|·| ^ n) μ) :
     iteratedDeriv n (charFun μ) t = I ^ n * ∫ x, x ^ n * exp (t * x * I) ∂μ := by
-  have h : bilinFormOfRealInner = (ContinuousLinearMap.mul ℝ ℝ).toLinearMap₁₂ := by ext; rfl
+  have h : innerₗ ℝ = (ContinuousLinearMap.mul ℝ ℝ).toLinearMap₁₂ := by ext; rfl
   have hint' (k : ℕ) (hk : k ≤ (n : ℕ∞)) : Integrable (fun x ↦ ‖x‖ ^ k * ‖(1 : ℝ → ℂ) x‖) μ := by
     simp only [Pi.one_apply, norm_one, mul_one]
     rw [Nat.cast_le] at hk

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "26440c825575eea64509c91cf9e1ab3ede95de9b",
+   "rev": "a36c84ab8236a4869899268a42a44af07daa21ed",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dff865b7ee7011518d59abfc101c368293173150",
+   "rev": "2e16f91af2a97975e5d2fac906494cd6c17ba255",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",