[Merged by Bors] - feat(Analysis/InnerProductSpace): inner products on exterior powers

Mathlib.lean

@@ -2046,6 +2046,7 @@ public import Mathlib.Analysis.InnerProductSpace.Convex
 public import Mathlib.Analysis.InnerProductSpace.Defs
 public import Mathlib.Analysis.InnerProductSpace.Dual
 public import Mathlib.Analysis.InnerProductSpace.EuclideanDist
+public import Mathlib.Analysis.InnerProductSpace.ExteriorPower
 public import Mathlib.Analysis.InnerProductSpace.GramMatrix
 public import Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
 public import Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean

@@ -0,0 +1,155 @@
+/-
+Copyright (c) 2026 Justus Springer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Justus Springer
+-/
+module
+
+public import Mathlib.Analysis.InnerProductSpace.GramMatrix
+public import Mathlib.LinearAlgebra.ExteriorPower.Basis
+
+/-!
+# Inner product space structure on exterior powers
+
+Given a real inner product space `E`, we construct a canonical inner product on `⋀[ℝ]^n E`
+via the Gram determinant formula: on decomposable elements,
+`⟪v₁ ∧ ⋯ ∧ vₙ, w₁ ∧ ⋯ ∧ wₙ⟫ = det (⟪vⱼ, wᵢ⟫)ᵢⱼ`.
+
+## Main results
+
+- `exteriorPower.inner_ιMulti_ιMulti`: The inner product on decomposable elements equals the
+  Gram determinant.
+- `exteriorPower.inner_ιMulti_self`: `⟪v₁ ∧ ⋯ ∧ vₙ, v₁ ∧ ⋯ ∧ vₙ⟫ = det (gram ℝ v)`.
+- `OrthonormalBasis.exteriorPower`: An orthonormal basis of `E` induces an orthonormal basis
+  of `⋀[ℝ]^n E`.
+
+## Future work
+
+- Generalize to `RCLike 𝕜`. To define `innerProductForm` in this case, we would probably
+  want a semilinear generalization of `exteriorPower.map`, which in turn requires
+  generalizing `AlternatingMap` to the semilinear setting.
+- Remove the `FiniteDimensional` hypothesis from the `InnerProductSpace` instance.
+  Currently the proofs of `re_inner_nonneg` and `definite` require finite dimension, because
+  we need to choose an orthonormal basis of `E`. But we can reduce the general case to
+  the finite-dimensional case by noticing that any `x : ⋀[𝕜]^n E` is contained in some
+  `⋀[𝕜]^n F` for a finite-dimensional subspace `F ≤ E`.
+
+-/
+
+@[expose] public noncomputable section
+
+namespace exteriorPower
+
+open RealInnerProductSpace Matrix
+
+variable {n : ℕ} {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
+
+/-- The inner product on `⋀[ℝ]^n E` as a bilinear map. This is an implementation detail
+for constructing the `InnerProductSpace` instance and should not be used directly.
+Use `⟪·, ·⟫` instead. -/
+private def innerProductForm : ⋀[ℝ]^n E →ₗ[ℝ] ⋀[ℝ]^n E →ₗ[ℝ] ℝ :=
+  pairingDual ℝ E n ∘ₗ map n (innerₗ E)
+
+private lemma innerProductForm_ιMulti_ιMulti (x y : Fin n → E) :
+    innerProductForm (ιMulti ℝ n x) (ιMulti ℝ n y) = det (of fun i j ↦ ⟪x j, y i⟫) := by
+  simp [innerProductForm]
+
+@[simp]
+private lemma innerProductForm_ιMulti_self (x : Fin n → E) :
+    innerProductForm (ιMulti ℝ n x) (ιMulti ℝ n x) = det (gram ℝ x) := by
+  simp [gram, innerProductForm_ιMulti_ιMulti, real_inner_comm]
+
+private lemma flip_innerProductForm :
+    (innerProductForm (E := E) (n := n)).flip = innerProductForm := by
+  apply linearMap_ext
+  ext
+  simp only [LinearMap.compAlternatingMap_apply, LinearMap.flip_apply,
+    innerProductForm_ιMulti_ιMulti]
+  rw [← Matrix.det_transpose]
+  congr 1
+  ext
+  exact real_inner_comm _ _
+
+private lemma innerProductForm_symm (x y : ⋀[ℝ]^n E) :
+    innerProductForm y x = innerProductForm x y :=
+  congr($flip_innerProductForm x y)
+
+@[simp]
+private lemma innerProductForm_ιMulti_family_of_orthonormal {ι : Type*} [LinearOrder ι] {v : ι → E}
+    (hv : Orthonormal ℝ v) (s t : Set.powersetCard ι n) :
+    innerProductForm (ιMulti_family ℝ n v s) (ιMulti_family ℝ n v t) = if s = t then 1 else 0 := by
+  simp only [ιMulti_family]
+  split_ifs with h
+  · subst h
+    simp [gram_eq_one_iff_orthonormal.mpr (hv.comp _ (RelEmbedding.injective _))]
+  · rw [innerProductForm_ιMulti_ιMulti]
+    obtain ⟨x, hxt, hxs⟩ := (Set.powersetCard.exists_mem_notMem_iff_ne t s).mp (.symm h)
+    simp only [Set.mem_range, not_exists,
+      ← Set.powersetCard.mem_range_ofFinEmbEquiv_symm_iff_mem] at hxs hxt
+    obtain ⟨i, rfl⟩ := hxt
+    exact det_eq_zero_of_row_eq_zero i (fun j ↦ hv.inner_eq_zero (hxs j))
+
+private lemma innerProductForm_eq_sum {ι : Type*} [Fintype ι] [LinearOrder ι]
+    (b : OrthonormalBasis ι ℝ E) (x y : ⋀[ℝ]^n E) :
+    innerProductForm x y =
+      ∑ s, (b.toBasis.exteriorPower n).repr y s * (b.toBasis.exteriorPower n).repr x s := by
+  conv_lhs =>
+    rw [← (b.toBasis.exteriorPower n).sum_repr x, ← (b.toBasis.exteriorPower n).sum_repr y]
+  simp
+
+private lemma innerProductForm_self (x : ⋀[ℝ]^n E) {ι : Type*} [Fintype ι] [LinearOrder ι]
+    (b : OrthonormalBasis ι ℝ E) :
+    innerProductForm x x = ∑ s, (b.toBasis.exteriorPower n).repr x s ^ 2 := by
+  simp_rw [innerProductForm_eq_sum b, pow_two]
+
+@[no_expose] instance [FiniteDimensional ℝ E] : InnerProductSpace.Core ℝ (⋀[ℝ]^n E) where
+  inner x y := innerProductForm x y
+  conj_inner_symm := innerProductForm_symm
+  add_left := by simp
+  smul_left := by simp
+  re_inner_nonneg x := by
+    rw [innerProductForm_self x (stdOrthonormalBasis ℝ E)]
+    exact Finset.sum_nonneg (fun _ _ ↦ sq_nonneg _)
+  definite x h := by
+    rw [innerProductForm_self x (stdOrthonormalBasis ℝ E),
+      Finset.sum_eq_zero_iff_of_nonneg (fun _ _ ↦ sq_nonneg _)] at h
+    apply Module.Basis.ext_elem ((stdOrthonormalBasis ℝ E).toBasis.exteriorPower n)
+    simpa using h
+
+instance [FiniteDimensional ℝ E] : NormedAddCommGroup (⋀[ℝ]^n E) :=
+  InnerProductSpace.Core.toNormedAddCommGroup (𝕜 := ℝ)
+
+instance [FiniteDimensional ℝ E] : InnerProductSpace ℝ (⋀[ℝ]^n E) :=
+  InnerProductSpace.ofCore _
+
+lemma inner_ιMulti_ιMulti [FiniteDimensional ℝ E] (x y : Fin n → E) :
+    ⟪ιMulti ℝ n x, ιMulti ℝ n y⟫ = det (of fun i j ↦ ⟪x j, y i⟫) :=
+  innerProductForm_ιMulti_ιMulti x y
+
+lemma inner_ιMulti_self [FiniteDimensional ℝ E] (x : Fin n → E) :
+    ⟪ιMulti ℝ n x, ιMulti ℝ n x⟫ = det (gram ℝ x) :=
+  innerProductForm_ιMulti_self x
+
+end exteriorPower
+
+section OrthonormalBasis
+
+variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
+variable {I : Type*} [Fintype I] [LinearOrder I]
+
+/-- An orthonormal basis of a finite-dimensional real inner product space `E` induces an
+orthonormal basis of `⋀[ℝ]^n E`, indexed by `n`-element subsets of the index type. -/
+def OrthonormalBasis.exteriorPower (b : OrthonormalBasis I ℝ E) (n : ℕ) :
+    OrthonormalBasis (Set.powersetCard I n) ℝ (⋀[ℝ]^n E) :=
+  (b.toBasis.exteriorPower n).toOrthonormalBasis <| by
+    rw [orthonormal_iff_ite]
+    intro i j
+    rw [exteriorPower.coe_basis, OrthonormalBasis.coe_toBasis]
+    exact exteriorPower.innerProductForm_ιMulti_family_of_orthonormal b.orthonormal i j
+
+@[simp]
+lemma OrthonormalBasis.toBasis_exteriorPower (b : OrthonormalBasis I ℝ E) (n : ℕ) :
+    (b.exteriorPower n).toBasis = b.toBasis.exteriorPower n :=
+  (b.toBasis.exteriorPower n).toBasis_toOrthonormalBasis _
+
+end OrthonormalBasis

Mathlib/Analysis/InnerProductSpace/GramMatrix.lean

@@ -134,6 +134,11 @@ theorem gram_eq_conjTranspose_mul {ι : Type*} [Fintype ι] (b : OrthonormalBasi
   ext i j
   simp [mul_apply, b.repr_apply_apply, b.sum_inner_mul_inner]
 
+omit [Finite n] in
+@[simp]
+lemma gram_eq_one_iff_orthonormal [DecidableEq n] {v : n → E} : gram 𝕜 v = 1 ↔ Orthonormal 𝕜 v := by
+  simp [← Matrix.ext_iff, orthonormal_iff_ite, Matrix.one_apply]
+
 omit [Finite n] in
 /-- Inequality `‖f x‖ ≤ ‖f‖ * ‖x‖` lifted to Gram matrices. -/
 theorem posSemidef_opNorm_smul_gram_sub_gram {F} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F]