Refactor(Analysis): from BilinForm to LinearMap.BilinForm (#11097)

Replaces `BilinForm` with `LinearMap.BilinForm` in support of #10553 Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
leanprover-community · Mar 2, 2024 · 4e3cf2f · 4e3cf2f
1 parent 1aabff1
commit 4e3cf2f
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 14 deletions.
diff --git a/Archive/Hairer.lean b/Archive/Hairer.lean
@@ -8,6 +8,7 @@ import Mathlib.Analysis.Analytic.Polynomial
 import Mathlib.Analysis.Analytic.Uniqueness
 import Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
 import Mathlib.Data.MvPolynomial.Funext
+import Mathlib.LinearAlgebra.Dual
 import Mathlib.RingTheory.MvPolynomial.Basic
 import Mathlib.Topology.Algebra.MvPolynomial
 

diff --git a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean
@@ -61,10 +61,10 @@ variable [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] [InnerProduct
 /-- 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 => BilinForm.toLin bilinFormOfRealInner p.1 p.2 :=
+  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 [BilinForm.toLin_apply, bilinFormOfRealInner_apply]
+  simp only [bilinFormOfRealInner_apply_apply, ofAdd_neg, map_inv, coe_inv_unitSphere]
 #align fourier_integrand_integrable fourier_integrand_integrable
 
 variable [CompleteSpace E]
@@ -234,7 +234,7 @@ theorem tendsto_integral_exp_inner_smul_cocompact :
       ← smul_sub, ← Pi.sub_apply]
     exact
       VectorFourier.norm_fourierIntegral_le_integral_norm 𝐞 volume
-        (BilinForm.toLin bilinFormOfRealInner) (f - g) w
+        (bilinFormOfRealInner) (f - g) w
   replace := add_lt_add_of_le_of_lt this hI
   rw [add_halves] at this
   refine' ((le_of_eq _).trans (norm_add_le _ _)).trans_lt this

diff --git a/Mathlib/Analysis/InnerProductSpace/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Basic.lean
@@ -8,7 +8,6 @@ import Mathlib.Analysis.Complex.Basic
 import Mathlib.Analysis.Convex.Uniform
 import Mathlib.Analysis.NormedSpace.Completion
 import Mathlib.Analysis.NormedSpace.BoundedLinearMaps
-import Mathlib.LinearAlgebra.BilinearForm.Basic
 
 #align_import analysis.inner_product_space.basic from "leanprover-community/mathlib"@"3f655f5297b030a87d641ad4e825af8d9679eb0b"
 
@@ -71,6 +70,8 @@ open IsROrC Real Filter
 
 open BigOperators Topology ComplexConjugate
 
+open LinearMap (BilinForm)
+
 variable {𝕜 E F : Type*} [IsROrC 𝕜]
 
 /-- Syntactic typeclass for types endowed with an inner product -/
@@ -498,14 +499,11 @@ def sesqFormOfInner : E →ₗ[𝕜] E →ₗ⋆[𝕜] 𝕜 :=
     (fun _x _y _z => inner_add_left _ _ _) fun _r _x _y => inner_smul_left _ _ _
 #align sesq_form_of_inner sesqFormOfInner
 
-/-- The real inner product as a bilinear form. -/
-@[simps]
-def bilinFormOfRealInner : BilinForm ℝ F where
-  bilin := inner
-  bilin_add_left := inner_add_left
-  bilin_smul_left _a _x _y := inner_smul_left _ _ _
-  bilin_add_right := inner_add_right
-  bilin_smul_right _a _x _y := inner_smul_right _ _ _
+/-- The real inner product as a bilinear form.
+
+Note that unlike `sesqFormOfInner`, this does not reverse the order of the arguments. -/
+@[simps!]
+def bilinFormOfRealInner : BilinForm ℝ F := sesqFormOfInner.flip
 #align bilin_form_of_real_inner bilinFormOfRealInner
 
 /-- An inner product with a sum on the left. -/

diff --git a/Mathlib/Analysis/InnerProductSpace/Orthogonal.lean b/Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhouhang Zhou, Sébastien Gouëzel, Frédéric Dupuis
 -/
 import Mathlib.Analysis.InnerProductSpace.Basic
-import Mathlib.LinearAlgebra.BilinearForm.Orthogonal
+import Mathlib.LinearAlgebra.SesquilinearForm
 
 #align_import analysis.inner_product_space.orthogonal from "leanprover-community/mathlib"@"f0c8bf9245297a541f468be517f1bde6195105e9"
 
@@ -223,7 +223,7 @@ end Submodule
 
 @[simp]
 theorem bilinFormOfRealInner_orthogonal {E} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
-    (K : Submodule ℝ E) : bilinFormOfRealInner.orthogonal K = Kᗮ :=
+    (K : Submodule ℝ E) : K.orthogonalBilin bilinFormOfRealInner = Kᗮ :=
   rfl
 #align bilin_form_of_real_inner_orthogonal bilinFormOfRealInner_orthogonal