diff --git a/Mathlib.lean b/Mathlib.lean index 624f35d65fc813..9d8fe07ded62af 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean b/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean new file mode 100644 index 00000000000000..1bb7d526df2960 --- /dev/null +++ b/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 diff --git a/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean b/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean index 5137d3a797bf6b..7bc693a2ddb34c 100644 --- a/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean +++ b/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]