feat: introduce Gram matrices (leanprover-community#25883)

A Gram matrix has entry `⟪v i, v j⟫` at `i j : n`, where `v : n → α` is an `InnerProductSpace 𝕜 α`. 
Give this notion and show that Gram matrices are positive semi-definite.
This will be used later in order to show that the covariance matrix for Brownian Motion is positive semi-definite.


[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: pfaffelh <p.p@stochastik.uni-freiburg.de>
Co-authored-by: Matthew Robert Ballard <matt@mrb.email>
Co-authored-by: pfaffelh <pfaffelh@gmail.com>
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

Author: 5 people

Mathlib.lean

@@ -1706,6 +1706,7 @@ import Mathlib.Analysis.InnerProductSpace.Convex
 import Mathlib.Analysis.InnerProductSpace.Defs
 import Mathlib.Analysis.InnerProductSpace.Dual
 import Mathlib.Analysis.InnerProductSpace.EuclideanDist
+import Mathlib.Analysis.InnerProductSpace.GramMatrix
 import Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
 import Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
 import Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

Mathlib/Analysis/InnerProductSpace/GramMatrix.lean

@@ -0,0 +1,114 @@
+/-
+Copyright (c) 2025 Peter Pfaffelhuber. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Peter Pfaffelhuber
+-/
+
+import Mathlib.LinearAlgebra.Matrix.PosDef
+
+/-! # Gram Matrices
+
+This file defines Gram matrices and proves their positive semidefiniteness.
+Results require `RCLike 𝕜`.
+
+## Main definition
+
+* `Matrix.gram` : the `Matrix n n 𝕜` with `⟪v i, v j⟫` at `i j : n`, where `v : n → E` for an
+  `Inner 𝕜 E`.
+
+## Main results
+
+* `Matrix.posSemidef_gram`: Gram matrices are positive semidefinite.
+* `Matrix.posDef_gram_iff_linearIndependent`: Linear independence of `v` is
+  equivalent to positive definiteness of `gram 𝕜 v`.
+-/
+
+open RCLike Real Matrix
+
+open scoped InnerProductSpace ComplexOrder ComplexConjugate
+
+variable {E n α 𝕜 : Type*}
+namespace Matrix
+
+/-- The entries of a Gram matrix are inner products of vectors in an inner product space. -/
+def gram (𝕜 : Type*) [Inner 𝕜 E] (v : n → E) : Matrix n n 𝕜 := of fun i j ↦ ⟪v i, v j⟫_𝕜
+
+@[simp]
+lemma gram_apply [Inner 𝕜 E] (v : n → E) (i j : n) :
+    (gram 𝕜 v) i j = ⟪v i, v j⟫_𝕜 := rfl
+
+variable [RCLike 𝕜]
+
+section SemiInnerProductSpace
+variable [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E]
+
+@[simp]
+lemma gram_zero : gram 𝕜 (0 : n → E) = 0 := Matrix.ext fun _ _ ↦ inner_zero_left _
+
+@[simp]
+lemma gram_single [DecidableEq n] (i : n) (x : E) :
+    gram 𝕜 (Pi.single i x) = Matrix.single i i ⟪x, x⟫_𝕜 := by
+  ext j k
+  obtain hij | rfl := ne_or_eq i j
+  · simp [hij]
+  obtain hik | rfl := ne_or_eq i k
+  · simp [hik]
+  simp
+
+lemma submatrix_gram (v : n → E) {m : Set n} (f : m → n) :
+  (gram 𝕜 v).submatrix f f = gram 𝕜 (v ∘ f) := rfl
+
+variable (𝕜) in
+/-- A Gram matrix is Hermitian. -/
+lemma isHermitian_gram (v : n → E) : (gram 𝕜 v).IsHermitian :=
+  Matrix.ext fun _ _ ↦ inner_conj_symm _ _
+
+variable [Fintype n]
+
+theorem star_dotProduct_gram_mulVec (v : n → E) (x y : n → 𝕜) :
+    star x ⬝ᵥ (gram 𝕜 v) *ᵥ y = ⟪∑ i, x i • v i, ∑ i, y i • v i⟫_𝕜 := by
+  trans ∑ i, ∑ j, conj (x i) * y j * ⟪v i, v j⟫_𝕜
+  · simp_rw [dotProduct, mul_assoc, ← Finset.mul_sum, mulVec, dotProduct, mul_comm, ← star_def,
+      gram_apply, Pi.star_apply]
+  · simp_rw [sum_inner, inner_sum, inner_smul_left, inner_smul_right, mul_assoc]
+
+variable (𝕜) in
+/-- A Gram matrix is positive semidefinite. -/
+theorem posSemidef_gram (v : n → E) :
+    PosSemidef (gram 𝕜 v) := by
+  refine ⟨isHermitian_gram _ _, fun x ↦ ?_⟩
+  rw [star_dotProduct_gram_mulVec, le_iff_re_im]
+  simp [inner_self_nonneg]
+
+/-- In a normed space, positive definiteness of `gram 𝕜 v` implies linear independence of `v`. -/
+theorem linearIndependent_of_posDef_gram {v : n → E} (h_gram : PosDef (gram 𝕜 v)) :
+    LinearIndependent 𝕜 v := by
+  rw [Fintype.linearIndependent_iff]
+  intro y hy
+  obtain ⟨h1, h2⟩ := h_gram
+  specialize h2 y
+  simp_all [star_dotProduct_gram_mulVec]
+
+end SemiInnerProductSpace
+
+section NormedInnerProductSpace
+variable [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype n]
+
+/-- In a normed space, linear independence of `v` implies positive definiteness of `gram 𝕜 v`. -/
+theorem posDef_gram_of_linearIndependent
+    {v : n → E} (h_li : LinearIndependent 𝕜 v) : PosDef (gram 𝕜 v) := by
+  rw [Fintype.linearIndependent_iff] at h_li
+  obtain ⟨h0, h1⟩ := posSemidef_gram 𝕜 v
+  refine ⟨h0, fun x hx ↦ (h1 x).lt_of_ne' ?_⟩
+  rw [star_dotProduct_gram_mulVec, inner_self_eq_zero.ne]
+  exact mt (h_li x) (mt funext hx)
+
+/-- In a normed space, linear independence of `v` is equivalent to positive definiteness of
+`gram 𝕜 v`. -/
+theorem posDef_gram_iff_linearIndependent {v : n → E} :
+    PosDef (gram 𝕜 v) ↔ LinearIndependent 𝕜 v :=
+  ⟨linearIndependent_of_posDef_gram, posDef_gram_of_linearIndependent⟩
+
+end NormedInnerProductSpace
+
+end Matrix

Mathlib/MeasureTheory/Function/L2Space.lean

@@ -27,7 +27,7 @@ noncomputable section
 
 open TopologicalSpace MeasureTheory MeasureTheory.Lp Filter
 
-open scoped NNReal ENNReal MeasureTheory
+open scoped NNReal ENNReal MeasureTheory InnerProductSpace
 
 namespace MeasureTheory
 
@@ -195,7 +195,7 @@ end InnerProductSpace
 
 section IndicatorConstLp
 
-variable (𝕜) {s : Set α}
+variable (𝕜) {s t : Set α}
 
 /-- The inner product in `L2` of the indicator of a set `indicatorConstLp 2 hs hμs c` and `f` is
 equal to the integral of the inner product over `s`: `∫ x in s, ⟪c, f x⟫ ∂μ`. -/
@@ -241,6 +241,31 @@ theorem inner_indicatorConstLp_one (hs : MeasurableSet s) (hμs : μ s ≠ ∞)
     ⟪indicatorConstLp 2 hs hμs (1 : 𝕜), f⟫ = ∫ x in s, f x ∂μ := by
   rw [L2.inner_indicatorConstLp_eq_inner_setIntegral 𝕜 hs hμs (1 : 𝕜) f]; simp
 
+/-- The inner product in `L2` of two `indicatorConstLp`s, i.e. functions which are constant `a : E`
+and `b : E` on measurable `s t : Set α` with finite measure, respectively, is `⟪a, b⟫` times the
+measure of `s ∩ t`. -/
+lemma inner_indicatorConstLp_indicatorConstLp [CompleteSpace E]
+    (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ∞ := by finiteness)
+    (hμt : μ t ≠ ∞ := by finiteness) (a b : E) :
+    ⟪indicatorConstLp 2 hs hμs a, indicatorConstLp 2 ht hμt b⟫ = μ.real (s ∩ t) • ⟪a, b⟫ := by
+  let : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E
+  rw [inner_indicatorConstLp_eq_inner_setIntegral, setIntegral_indicatorConstLp hs,
+    inner_smul_right_eq_smul, Set.inter_comm]
+
+/-- The inner product in `L2` of indicators of two sets with finite measure
+is the measure of the intersection. -/
+lemma inner_indicatorConstLp_one_indicatorConstLp_one
+    (hs : MeasurableSet s) (ht : MeasurableSet t)
+    (hμs : μ s ≠ ∞ := by finiteness) (hμt : μ t ≠ ∞ := by finiteness) :
+    ⟪indicatorConstLp 2 hs hμs (1 : 𝕜), indicatorConstLp 2 ht hμt (1 : 𝕜)⟫ = μ.real (s ∩ t) := by
+  simp [inner_indicatorConstLp_indicatorConstLp, RCLike.ofReal_alg]
+
+lemma real_inner_indicatorConstLp_one_indicatorConstLp_one
+    (hs : MeasurableSet s) (ht : MeasurableSet t)
+    (hμs : μ s ≠ ∞ := by finiteness) (hμt : μ t ≠ ∞ := by finiteness) :
+    ⟪indicatorConstLp 2 hs hμs (1 : ℝ), indicatorConstLp 2 ht hμt (1 : ℝ)⟫_ℝ = μ.real (s ∩ t) := by
+  simp [inner_indicatorConstLp_indicatorConstLp]
+
 end IndicatorConstLp
 
 end L2