chore: deprecate duplicate declaration for the scalar product as a sesquilinear form (leanprover-community#33316)

Zulip discussion at [#mathlib4 > Duplication @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Duplication/near/565217359)

Author: sgouezel

Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

@@ -199,7 +199,7 @@ theorem tendsto_integral_exp_inner_smul_cocompact :
     simp_rw [← integral_sub ((Real.fourierIntegral_convergent_iff w).2 hfi)
       ((Real.fourierIntegral_convergent_iff w).2 (hg_cont.integrable_of_hasCompactSupport hg_supp)),
       ← smul_sub, ← Pi.sub_apply]
-    exact VectorFourier.norm_fourierIntegral_le_integral_norm 𝐞 _ bilinFormOfRealInner (f - g) w
+    exact VectorFourier.norm_fourierIntegral_le_integral_norm 𝐞 _ (innerₗ V) (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

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

@@ -246,10 +246,10 @@ instance : CStarRing (E →L[𝕜] E) where
   norm_mul_self_le x := le_of_eq <| Eq.symm <| norm_adjoint_comp_self x
 
 theorem isAdjointPair_inner (A : E →L[𝕜] F) :
-    LinearMap.IsAdjointPair (sesqFormOfInner : E →ₗ[𝕜] E →ₗ⋆[𝕜] 𝕜)
-      (sesqFormOfInner : F →ₗ[𝕜] F →ₗ⋆[𝕜] 𝕜) A (A†) := by
+    LinearMap.IsAdjointPair (LinearMap.flip (innerₛₗ 𝕜 (E := E)))
+      (innerₛₗ 𝕜 (E := F)).flip A (A†) := by
   intro x y
-  simp only [sesqFormOfInner_apply_apply, adjoint_inner_left]
+  simp [adjoint_inner_left]
 
 theorem adjoint_innerSL_apply (x : E) :
     adjoint (innerSL 𝕜 x) = toSpanSingleton 𝕜 x :=
@@ -574,10 +574,10 @@ theorem isSymmetric_iff_isSelfAdjoint (A : E →ₗ[𝕜] E) : IsSymmetric A ↔
   exact eq_comm
 
 theorem isAdjointPair_inner (A : E →ₗ[𝕜] F) :
-    IsAdjointPair (sesqFormOfInner : E →ₗ[𝕜] E →ₗ⋆[𝕜] 𝕜) (sesqFormOfInner : F →ₗ[𝕜] F →ₗ⋆[𝕜] 𝕜) A
-      A.adjoint := by
+    IsAdjointPair (innerₛₗ 𝕜 (E := E)).flip
+      (innerₛₗ 𝕜 (E := F)).flip A A.adjoint := by
   intro x y
-  simp only [sesqFormOfInner_apply_apply, adjoint_inner_left]
+  simp [adjoint_inner_left]
 
 /-- The Gram operator T†T is symmetric. -/
 theorem isSymmetric_adjoint_mul_self (T : E →ₗ[𝕜] E) : IsSymmetric (T.adjoint * T) := by

Mathlib/Analysis/InnerProductSpace/Basic.lean

@@ -120,30 +120,50 @@ theorem real_inner_smul_right (x y : F) (r : ℝ) : ⟪x, r • y⟫_ℝ = r * 
 theorem inner_smul_real_right (x y : E) (r : ℝ) : ⟪x, (r : 𝕜) • y⟫ = r • ⟪x, y⟫ := by
   rw [inner_smul_right, Algebra.smul_def]
 
-/-- The inner product as a sesquilinear form.
+
+variable (𝕜)
+
+/-- The inner product as a sesquilinear map.
 
 Note that in the case `𝕜 = ℝ` this is a bilinear form. -/
-@[simps!]
-def sesqFormOfInner : E →ₗ[𝕜] E →ₗ⋆[𝕜] 𝕜 :=
-  LinearMap.mk₂'ₛₗ (RingHom.id 𝕜) (starRingEnd _) (fun x y => ⟪y, x⟫)
-    (fun _x _y _z => inner_add_right _ _ _) (fun _r _x _y => inner_smul_right _ _ _)
-    (fun _x _y _z => inner_add_left _ _ _) fun _r _x _y => inner_smul_left _ _ _
+def innerₛₗ : E →ₗ⋆[𝕜] E →ₗ[𝕜] 𝕜 :=
+  LinearMap.mk₂'ₛₗ _ _ (fun v w => ⟪v, w⟫) inner_add_left (fun _ _ _ => inner_smul_left _ _ _)
+    inner_add_right fun _ _ _ => inner_smul_right _ _ _
+
+@[simp]
+theorem coe_innerₛₗ_apply (v : E) : ⇑(innerₛₗ 𝕜 v) = fun w => ⟪v, w⟫ :=
+  rfl
+
+@[simp]
+theorem innerₛₗ_apply_apply (v w : E) : innerₛₗ 𝕜 v w = ⟪v, w⟫ :=
+  rfl
+
+variable (F)
+/-- The inner product as a bilinear map in the real case. -/
+def innerₗ : F →ₗ[ℝ] F →ₗ[ℝ] ℝ := innerₛₗ ℝ
+
+@[simp] lemma flip_innerₗ : (innerₗ F).flip = innerₗ F := by
+  ext v w
+  exact real_inner_comm v w
 
-/-- The real inner product as a bilinear form.
+variable {F}
+
+@[simp] lemma innerₗ_apply_apply (v w : F) : innerₗ F v w = ⟪v, w⟫_ℝ := rfl
+
+variable {𝕜}
 
-Note that unlike `sesqFormOfInner`, this does not reverse the order of the arguments. -/
-@[simps!]
-def bilinFormOfRealInner : BilinForm ℝ F := sesqFormOfInner.flip
+@[deprecated (since := "2025-12-26")] alias sesqFormOfInner := innerₛₗ
+@[deprecated (since := "2025-12-26")] alias bilinFormOfRealInner := innerₗ
 
 /-- An inner product with a sum on the left. -/
 theorem sum_inner {ι : Type*} (s : Finset ι) (f : ι → E) (x : E) :
     ⟪∑ i ∈ s, f i, x⟫ = ∑ i ∈ s, ⟪f i, x⟫ :=
-  map_sum (sesqFormOfInner (𝕜 := 𝕜) (E := E) x) _ _
+  map_sum ((innerₛₗ 𝕜).flip x) _ _
 
 /-- An inner product with a sum on the right. -/
 theorem inner_sum {ι : Type*} (s : Finset ι) (f : ι → E) (x : E) :
     ⟪x, ∑ i ∈ s, f i⟫ = ∑ i ∈ s, ⟪x, f i⟫ :=
-  map_sum (LinearMap.flip sesqFormOfInner x) _ _
+  map_sum (innerₛₗ 𝕜 x) _ _
 
 /-- An inner product with a sum on the left, `Finsupp` version. -/
 protected theorem Finsupp.sum_inner {ι : Type*} (l : ι →₀ 𝕜) (v : ι → E) (x : E) :

Mathlib/Analysis/InnerProductSpace/CanonicalTensor.lean

@@ -32,7 +32,7 @@ variable (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E]
 
 /-- The canonical contravariant tensor corresponding to the inner product -/
 noncomputable def InnerProductSpace.canonicalContravariantTensor :
-    E ⊗[ℝ] E →ₗ[ℝ] ℝ := lift bilinFormOfRealInner
+    E ⊗[ℝ] E →ₗ[ℝ] ℝ := lift (innerₗ E)
 
 /--
 The canonical covariant tensor corresponding to `InnerProductSpace.canonicalContravariantTensor`

Mathlib/Analysis/InnerProductSpace/LinearMap.lean

@@ -14,8 +14,7 @@ This file studies linear maps on inner product spaces.
 
 ## Main results
 
-- We define `innerSL` as the inner product bundled as a continuous sesquilinear map, and
-  `innerₛₗ` for the non-continuous version.
+- We define `innerSL` as the inner product bundled as a continuous sesquilinear map
 - We prove a general polarization identity for linear maps (`inner_map_polarization`)
 - We show that a linear map preserving the inner product is an isometry
   (`LinearMap.isometryOfInner`) and conversely an isometry preserves the inner product
@@ -159,31 +158,6 @@ end
 
 variable (𝕜)
 
-/-- The inner product as a sesquilinear map. -/
-def innerₛₗ : E →ₗ⋆[𝕜] E →ₗ[𝕜] 𝕜 :=
-  LinearMap.mk₂'ₛₗ _ _ (fun v w => ⟪v, w⟫) inner_add_left (fun _ _ _ => inner_smul_left _ _ _)
-    inner_add_right fun _ _ _ => inner_smul_right _ _ _
-
-@[simp]
-theorem coe_innerₛₗ_apply (v : E) : ⇑(innerₛₗ 𝕜 v) = fun w => ⟪v, w⟫ :=
-  rfl
-
-@[simp]
-theorem innerₛₗ_apply_apply (v w : E) : innerₛₗ 𝕜 v w = ⟪v, w⟫ :=
-  rfl
-
-variable (F)
-/-- The inner product as a bilinear map in the real case. -/
-def innerₗ : F →ₗ[ℝ] F →ₗ[ℝ] ℝ := innerₛₗ ℝ
-
-@[simp] lemma flip_innerₗ : (innerₗ F).flip = innerₗ F := by
-  ext v w
-  exact real_inner_comm v w
-
-variable {F}
-
-@[simp] lemma innerₗ_apply_apply (v w : F) : innerₗ F v w = ⟪v, w⟫_ℝ := rfl
-
 /-- The inner product as a continuous sesquilinear map. Note that `toDualMap` (resp. `toDual`)
 in `InnerProductSpace.Dual` is a version of this given as a linear isometry (resp. linear
 isometric equivalence). -/

Mathlib/Analysis/InnerProductSpace/Orthogonal.lean

@@ -203,10 +203,13 @@ theorem orthogonalFamily_self :
 end Submodule
 
 @[simp]
-theorem bilinFormOfRealInner_orthogonal {E} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
-    (K : Submodule ℝ E) : K.orthogonalBilin bilinFormOfRealInner = Kᗮ :=
+theorem orthogonalBilin_innerₗ {E} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
+    (K : Submodule ℝ E) : K.orthogonalBilin (innerₗ E) = Kᗮ :=
   rfl
 
+@[deprecated (since := "2025-12-26")]
+alias bilinFormOfRealInner_orthogonal := orthogonalBilin_innerₗ
+
 /-!
 ### Orthogonality of submodules
 

Mathlib/Analysis/InnerProductSpace/Symmetric.lean

@@ -63,7 +63,7 @@ section Real
 /-- An operator `T` on an inner product space is symmetric if and only if it is
 `LinearMap.IsSelfAdjoint` with respect to the sesquilinear form given by the inner product. -/
 theorem isSymmetric_iff_sesqForm (T : E →ₗ[𝕜] E) :
-    T.IsSymmetric ↔ LinearMap.IsSelfAdjoint (R := 𝕜) (M := E) sesqFormOfInner T :=
+    T.IsSymmetric ↔ LinearMap.IsSelfAdjoint (R := 𝕜) (M := E) (LinearMap.flip (innerₛₗ 𝕜)) T :=
   ⟨fun h x y => (h y x).symm, fun h x y => (h y x).symm⟩
 
 end Real

Mathlib/MeasureTheory/Measure/CharacteristicFunction.lean

@@ -66,7 +66,7 @@ variable {E F : Type*} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E]
 /-- The bounded continuous map `x ↦ exp(⟪x, t⟫ * I)`. -/
 noncomputable
 def innerProbChar (t : E) : E →ᵇ ℂ :=
-  char continuous_probChar (L := bilinFormOfRealInner) continuous_inner t
+  char continuous_probChar (L := innerₗ E) continuous_inner t
 
 lemma innerProbChar_apply (t x : E) : innerProbChar t x = exp (⟪x, t⟫ * I) := rfl
 
@@ -155,15 +155,15 @@ lemma charFun_eq_integral_probChar (t : E) : charFun μ t = ∫ x, (probChar ⟪
 
 /-- `charFun` is a Fourier integral for the inner product and the character `probChar`. -/
 lemma charFun_eq_fourierIntegral (t : E) :
-    charFun μ t = VectorFourier.fourierIntegral probChar μ bilinFormOfRealInner 1 (-t) := by
+    charFun μ t = VectorFourier.fourierIntegral probChar μ (innerₗ E) 1 (-t) := by
   simp [charFun_apply, VectorFourier.fourierIntegral_probChar]
 
 /-- `charFun` is a Fourier integral for the inner product and the character `fourierChar`. -/
 lemma charFun_eq_fourierIntegral' (t : E) :
     charFun μ t
-      = VectorFourier.fourierIntegral fourierChar μ bilinFormOfRealInner 1 (-(2 * π)⁻¹ • t) := by
+      = VectorFourier.fourierIntegral fourierChar μ (innerₗ E) 1 (-(2 * π)⁻¹ • t) := by
   simp only [charFun_apply, VectorFourier.fourierIntegral, neg_smul,
-    bilinFormOfRealInner_apply_apply, inner_neg_right, inner_smul_right, neg_neg,
+    innerₗ_apply_apply, inner_neg_right, inner_smul_right, neg_neg,
     fourierChar_apply', Pi.ofNat_apply, Circle.smul_def, Circle.coe_exp, ofReal_mul, ofReal_ofNat,
     ofReal_inv, smul_eq_mul, mul_one]
   congr with x
@@ -238,7 +238,7 @@ theorem Measure.ext_of_charFun [CompleteSpace E]
     [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h : charFun μ = charFun ν) :
     μ = ν := by
   simp_rw [funext_iff, charFun_eq_integral_innerProbChar] at h
-  refine ext_of_integral_char_eq continuous_probChar probChar_ne_one (L := bilinFormOfRealInner)
+  refine ext_of_integral_char_eq continuous_probChar probChar_ne_one (L := innerₗ E)
     ?_ ?_ h
   · exact fun v hv ↦ DFunLike.ne_iff.mpr ⟨v, inner_self_ne_zero.mpr hv⟩
   · exact continuous_inner

Mathlib/Probability/Moments/ComplexMGF.lean

@@ -320,14 +320,14 @@ theorem _root_.MeasureTheory.Measure.ext_of_complexMGF_eq [IsFiniteMeasure μ]
     [IsFiniteMeasure μ'] (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ')
     (h : complexMGF X μ = complexMGF Y μ') :
     μ.map X = μ'.map Y := by
-  have inner_ne_zero (x : ℝ) (h : x ≠ 0) : bilinFormOfRealInner x ≠ 0 :=
+  have inner_ne_zero (x : ℝ) (h : x ≠ 0) : innerₗ ℝ  x ≠ 0 :=
     DFunLike.ne_iff.mpr ⟨x, inner_self_ne_zero.mpr h⟩
   apply MeasureTheory.ext_of_integral_char_eq continuous_probChar probChar_ne_one inner_ne_zero
     continuous_inner (fun w ↦ ?_)
   rw [funext_iff] at h
   specialize h (Multiplicative.toAdd w * I)
   simp_rw [complexMGF, mul_assoc, mul_comm I, ← mul_assoc] at h
-  simp only [BoundedContinuousFunction.char_apply, bilinFormOfRealInner_apply_apply,
+  simp only [BoundedContinuousFunction.char_apply, innerₗ_apply_apply,
     RCLike.inner_apply, conj_trivial, probChar_apply, ofReal_mul]
   rwa [integral_map hX (by fun_prop), integral_map hY (by fun_prop)]