From 2a2022b5c91a6b7e57b5eebfa491df3c889d46a9 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sat, 2 Mar 2024 13:38:09 +0000 Subject: [PATCH] Refactor(Analysis): from BilinForm to LinearMap.BilinForm (#11097) Replaces `BilinForm` with `LinearMap.BilinForm` in support of #10553 Co-authored-by: Christopher Hoskin Co-authored-by: Eric Wieser --- Archive/Hairer.lean | 1 + .../Analysis/Fourier/RiemannLebesgueLemma.lean | 6 +++--- Mathlib/Analysis/InnerProductSpace/Basic.lean | 16 +++++++--------- .../Analysis/InnerProductSpace/Orthogonal.lean | 4 ++-- 4 files changed, 13 insertions(+), 14 deletions(-) diff --git a/Archive/Hairer.lean b/Archive/Hairer.lean index dd54d1ff82c23..bd37ac9b66f67 100644 --- 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 index 88e8ba0e31bdc..d65467bee70a7 100644 --- 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 index 44c9c7060f8cc..eb1b6d80286a7 100644 --- 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 index fb5ec636e58f4..bdfb6192a4e23 100644 --- 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