From df41e0f533f6a337d9ede97824c751f102ba4acf Mon Sep 17 00:00:00 2001 From: Justus Springer Date: Sun, 14 Jun 2026 16:24:16 +0100 Subject: [PATCH 01/15] first draft --- .../ExteriorPower/InnerProductSpace.lean | 89 +++++++++++++++++++ 1 file changed, 89 insertions(+) create mode 100644 Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean diff --git a/Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean b/Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean new file mode 100644 index 00000000000000..559ef56dfa36d3 --- /dev/null +++ b/Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean @@ -0,0 +1,89 @@ +/- +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.LinearAlgebra.ExteriorPower.Pairing +public import Mathlib.LinearAlgebra.ExteriorPower.Basis +public import Mathlib.Analysis.InnerProductSpace.Basic +public import Mathlib.Analysis.InnerProductSpace.GramMatrix +public import Mathlib.Analysis.InnerProductSpace.PiL2 +public import Mathlib.Analysis.Matrix.PosDef + +/-! +# TODO + +-/ + +@[expose] public noncomputable section + +namespace exteriorPower + +open RealInnerProductSpace Matrix + +def bilinForm (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] (n : ℕ) : + ⋀[ℝ]^n E →ₗ[ℝ] ⋀[ℝ]^n E →ₗ[ℝ] ℝ := + pairingDual ℝ E n ∘ₗ map n (innerₗ E) + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} + +@[simp] +lemma bilinForm_ιMulti_ιMulti (x y : Fin n → E) : + bilinForm E n (ιMulti ℝ n x) (ιMulti ℝ n y) = det (of fun i j ↦ ⟪x j, y i⟫) := by + simp [bilinForm] + +@[simp] +lemma bilinForm_ιMulti_self (x : Fin n → E) : + bilinForm E n (ιMulti ℝ n x) (ιMulti ℝ n x) = det (gram ℝ x) := by + simp_rw [bilinForm_ιMulti_ιMulti, gram, real_inner_comm] + + +lemma bilinForm_flip : LinearMap.flip (bilinForm E n) = bilinForm E n := by + apply linearMap_ext + ext + simp only [LinearMap.compAlternatingMap_apply, LinearMap.flip_apply, bilinForm_ιMulti_ιMulti] + rw [← Matrix.det_transpose] + congr 1 + ext + exact real_inner_comm _ _ + +lemma bilinForm_symm (x y : ⋀[ℝ]^n E) : bilinForm E n x y = bilinForm E n y x := + congr($(bilinForm_flip) y x) + +variable (ι : Type*) [Fintype ι] [LinearOrder ι] (b : OrthonormalBasis ι ℝ E) +variable (σ τ : Set.powersetCard ι n) + +#check pairingDual_ιMulti_ιMulti +#check ιMulti_family_apply_coe +#check ExteriorAlgebra.ιMulti_family +#check gram +lemma bilinForm_basis_orthonormal (s t : Set.powersetCard ι n) : + bilinForm E n (b.toBasis.exteriorPower n s) (b.toBasis.exteriorPower n t) = + if s = t then 1 else 0 := by + simp [bilinForm, ιMulti_family] + #check b.orthonormal + sorry + +#check b.toBasis.exteriorPower n σ + +variable (v : Fin n → E) +#check (Matrix.posSemidef_gram ℝ v).det_nonneg +#check Matrix.PosSemidef.det_nonneg +#check OrthonormalBasis + +noncomputable instance : InnerProductSpace.Core ℝ (⋀[ℝ]^n E) where + inner x y := bilinForm E n x y + conj_inner_symm x y := bilinForm_symm y x + add_left := by simp + smul_left := by simp + re_inner_nonneg x := by + simp + sorry + definite x h := by + sorry + + +#check innerₗ + From 245e41618812fbdcb17a6bbe0cb7bb0c0c124c4a Mon Sep 17 00:00:00 2001 From: Justus Springer Date: Wed, 17 Jun 2026 17:11:55 +0100 Subject: [PATCH 02/15] progress --- .../InnerProductSpace/GramMatrix.lean | 5 + .../ExteriorPower/InnerProductSpace.lean | 157 +++++++++++++----- 2 files changed, 119 insertions(+), 43 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean b/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean index 5137d3a797bf6b..c59def5e2090a7 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_orthonormal [DecidableEq n] {v : n → E} (h : Orthonormal 𝕜 v) : gram 𝕜 v = 1 := by + ext; simp [orthonormal_iff_ite.mp h, 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] diff --git a/Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean b/Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean index 559ef56dfa36d3..3db013d527cf95 100644 --- a/Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean +++ b/Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean @@ -13,7 +13,25 @@ public import Mathlib.Analysis.InnerProductSpace.PiL2 public import Mathlib.Analysis.Matrix.PosDef /-! -# TODO +# 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 ℝ d)`. +- `OrthonormalBasis.exteriorPower`: An orthonormal basis of `E` induces an orthonormal basis + of `⋀[ℝ]^n E`. + +## Future work + +Generalize to `[RCLike 𝕜]`. To define `innerProductForm`, we would probably +want a semilinear generalization of `exteriorPower.map`, which in turn requires +generalizing `AlternatingMap` to the semilinear setting. -/ @@ -23,67 +41,120 @@ namespace exteriorPower open RealInnerProductSpace Matrix -def bilinForm (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] (n : ℕ) : +/-- The inner product on `⋀[ℝ]^n E` as a bilinear map. This is an implementation detail +for constructing the `InnerProductSpace` instance. Do not use this directly; use `⟪·, ·⟫_ℝ` +(or `⟪·, ·⟫` with `open RealInnerProductSpace`) instead. -/ +def innerProductForm {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} : ⋀[ℝ]^n E →ₗ[ℝ] ⋀[ℝ]^n E →ₗ[ℝ] ℝ := pairingDual ℝ E n ∘ₗ map n (innerₗ E) variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} -@[simp] -lemma bilinForm_ιMulti_ιMulti (x y : Fin n → E) : - bilinForm E n (ιMulti ℝ n x) (ιMulti ℝ n y) = det (of fun i j ↦ ⟪x j, y i⟫) := by - simp [bilinForm] +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] -lemma bilinForm_ιMulti_self (x : Fin n → E) : - bilinForm E n (ιMulti ℝ n x) (ιMulti ℝ n x) = det (gram ℝ x) := by - simp_rw [bilinForm_ιMulti_ιMulti, gram, real_inner_comm] - +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] -lemma bilinForm_flip : LinearMap.flip (bilinForm E n) = bilinForm E n := by +lemma flip_innerProductForm : + LinearMap.flip (innerProductForm (E := E) (n := n)) = innerProductForm := by apply linearMap_ext ext - simp only [LinearMap.compAlternatingMap_apply, LinearMap.flip_apply, bilinForm_ιMulti_ιMulti] + simp only [LinearMap.compAlternatingMap_apply, LinearMap.flip_apply, + innerProductForm_ιMulti_ιMulti] rw [← Matrix.det_transpose] congr 1 ext exact real_inner_comm _ _ -lemma bilinForm_symm (x y : ⋀[ℝ]^n E) : bilinForm E n x y = bilinForm E n y x := - congr($(bilinForm_flip) y x) - -variable (ι : Type*) [Fintype ι] [LinearOrder ι] (b : OrthonormalBasis ι ℝ E) -variable (σ τ : Set.powersetCard ι n) - -#check pairingDual_ιMulti_ιMulti -#check ιMulti_family_apply_coe -#check ExteriorAlgebra.ιMulti_family -#check gram -lemma bilinForm_basis_orthonormal (s t : Set.powersetCard ι n) : - bilinForm E n (b.toBasis.exteriorPower n s) (b.toBasis.exteriorPower n t) = - if s = t then 1 else 0 := by - simp [bilinForm, ιMulti_family] - #check b.orthonormal - sorry - -#check b.toBasis.exteriorPower n σ - -variable (v : Fin n → E) -#check (Matrix.posSemidef_gram ℝ v).det_nonneg -#check Matrix.PosSemidef.det_nonneg -#check OrthonormalBasis - -noncomputable instance : InnerProductSpace.Core ℝ (⋀[ℝ]^n E) where - inner x y := bilinForm E n x y - conj_inner_symm x y := bilinForm_symm y x +lemma innerProductForm_symm (x y : ⋀[ℝ]^n E) : innerProductForm x y = innerProductForm y x := + congr($flip_innerProductForm y x) + +@[simp] +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_orthonormal (hv.comp _ (RelEmbedding.injective _))] + · rw [innerProductForm_ιMulti_ιMulti] + have : ¬t.1 ⊆ s.1 := fun H ↦ Ne.symm h <| + Subtype.val_injective (Finset.eq_of_subset_of_card_le H (s.2.le.trans t.2.ge)) + rw [Finset.not_subset] at this + obtain ⟨x, hxt, hxs⟩ := this + simp only [Set.powersetCard.mem_coe_iff, Set.mem_range, not_exists, + ← Set.powersetCard.mem_range_ofFinEmbEquiv_symm_iff_mem] at hxs hxt + obtain ⟨i, hi⟩ := hxt + exact det_eq_zero_of_row_eq_zero i (fun j ↦ hv.inner_eq_zero (hi ▸ hxs j)) + +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 + +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] + +instance [FiniteDimensional ℝ E] : InnerProductSpace.Core ℝ (⋀[ℝ]^n E) where + inner x y := innerProductForm x y + conj_inner_symm x y := innerProductForm_symm y x add_left := by simp smul_left := by simp re_inner_nonneg x := by - simp - sorry + rw [RCLike.re_to_real, innerProductForm_self x (stdOrthonormalBasis ℝ E)] + exact Finset.sum_nonneg (fun _ _ ↦ sq_nonneg _) definite x h := by - sorry + 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 (𝕜 := ℝ) -#check innerₗ +instance [FiniteDimensional ℝ E] : InnerProductSpace ℝ (⋀[ℝ]^n E) := + InnerProductSpace.ofCore _ + +/-- The inner product on `⋀[ℝ]^n E` equals the Gram determinant on decomposable elements. -/ +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 + +/-- The self-inner-product on `⋀[ℝ]^n E` equals `det (gram ℝ v)` on decomposable elements. -/ +@[simp] +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 From 176f3969c37ee2321d0d201dc966ebdab892302b Mon Sep 17 00:00:00 2001 From: Justus Springer Date: Wed, 17 Jun 2026 18:29:16 +0100 Subject: [PATCH 03/15] cleanup --- Mathlib.lean | 1 + .../ExteriorPower/InnerProductSpace.lean | 29 ++++++++++--------- 2 files changed, 17 insertions(+), 13 deletions(-) diff --git a/Mathlib.lean b/Mathlib.lean index 3231bbedb8ef7a..eac96c928f3e6b 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5009,6 +5009,7 @@ public import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading public import Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating public import Mathlib.LinearAlgebra.ExteriorPower.Basic public import Mathlib.LinearAlgebra.ExteriorPower.Basis +public import Mathlib.LinearAlgebra.ExteriorPower.InnerProductSpace public import Mathlib.LinearAlgebra.ExteriorPower.Pairing public import Mathlib.LinearAlgebra.FiniteDimensional.Basic public import Mathlib.LinearAlgebra.FiniteDimensional.Defs diff --git a/Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean b/Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean index 3db013d527cf95..7ca69b9f97ebb6 100644 --- a/Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean +++ b/Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean @@ -23,15 +23,20 @@ via the Gram determinant formula: on decomposable elements, - `exteriorPower.inner_ιMulti_ιMulti`: The inner product on decomposable elements equals the Gram determinant. -- `exteriorPower.inner_ιMulti_self`: `⟪v₁ ∧ ⋯ ∧ vₙ, v₁ ∧ ⋯ ∧ vₙ⟫ = det (gram ℝ d)`. +- `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`, we would probably -want a semilinear generalization of `exteriorPower.map`, which in turn requires -generalizing `AlternatingMap` to the semilinear setting. +- 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`. -/ @@ -42,13 +47,13 @@ namespace exteriorPower open RealInnerProductSpace Matrix /-- The inner product on `⋀[ℝ]^n E` as a bilinear map. This is an implementation detail -for constructing the `InnerProductSpace` instance. Do not use this directly; use `⟪·, ·⟫_ℝ` -(or `⟪·, ·⟫` with `open RealInnerProductSpace`) instead. -/ +for constructing the `InnerProductSpace` instance and should not be used directly. +Use `⟪·, ·⟫` instead. -/ def innerProductForm {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} : ⋀[ℝ]^n E →ₗ[ℝ] ⋀[ℝ]^n E →ₗ[ℝ] ℝ := pairingDual ℝ E n ∘ₗ map n (innerₗ E) -variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} +variable {n : ℕ} {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] 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 @@ -70,8 +75,8 @@ lemma flip_innerProductForm : ext exact real_inner_comm _ _ -lemma innerProductForm_symm (x y : ⋀[ℝ]^n E) : innerProductForm x y = innerProductForm y x := - congr($flip_innerProductForm y x) +lemma innerProductForm_symm (x y : ⋀[ℝ]^n E) : innerProductForm y x = innerProductForm x y := + congr($flip_innerProductForm x y) @[simp] lemma innerProductForm_ιMulti_family_of_orthonormal {ι : Type*} [LinearOrder ι] {v : ι → E} @@ -106,11 +111,11 @@ lemma innerProductForm_self (x : ⋀[ℝ]^n E) {ι : Type*} [Fintype ι] [Linear instance [FiniteDimensional ℝ E] : InnerProductSpace.Core ℝ (⋀[ℝ]^n E) where inner x y := innerProductForm x y - conj_inner_symm x y := innerProductForm_symm y x + conj_inner_symm := innerProductForm_symm add_left := by simp smul_left := by simp re_inner_nonneg x := by - rw [RCLike.re_to_real, innerProductForm_self x (stdOrthonormalBasis ℝ E)] + rw [innerProductForm_self x (stdOrthonormalBasis ℝ E)] exact Finset.sum_nonneg (fun _ _ ↦ sq_nonneg _) definite x h := by rw [innerProductForm_self x (stdOrthonormalBasis ℝ E), @@ -124,12 +129,10 @@ instance [FiniteDimensional ℝ E] : NormedAddCommGroup (⋀[ℝ]^n E) := instance [FiniteDimensional ℝ E] : InnerProductSpace ℝ (⋀[ℝ]^n E) := InnerProductSpace.ofCore _ -/-- The inner product on `⋀[ℝ]^n E` equals the Gram determinant on decomposable elements. -/ 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 -/-- The self-inner-product on `⋀[ℝ]^n E` equals `det (gram ℝ v)` on decomposable elements. -/ @[simp] lemma inner_ιMulti_self [FiniteDimensional ℝ E] (x : Fin n → E) : ⟪ιMulti ℝ n x, ιMulti ℝ n x⟫ = det (gram ℝ x) := From 219b98236f1690d59652e19b8eea5b9d9aba8eb8 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci-lite[bot]" <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Date: Wed, 17 Jun 2026 17:32:02 +0000 Subject: [PATCH 04/15] [pre-commit.ci lite] apply automatic fixes --- Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean b/Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean index 7ca69b9f97ebb6..394df970307e2c 100644 --- a/Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean +++ b/Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean @@ -53,7 +53,7 @@ def innerProductForm {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E ⋀[ℝ]^n E →ₗ[ℝ] ⋀[ℝ]^n E →ₗ[ℝ] ℝ := pairingDual ℝ E n ∘ₗ map n (innerₗ E) -variable {n : ℕ} {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] +variable {n : ℕ} {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] 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 From 22c8f290599645c5d2260f923004a85ea44463df Mon Sep 17 00:00:00 2001 From: Justus Springer Date: Wed, 17 Jun 2026 18:54:04 +0100 Subject: [PATCH 05/15] remove @[simp] --- Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean b/Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean index 7ca69b9f97ebb6..ef152c7b262156 100644 --- a/Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean +++ b/Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean @@ -133,7 +133,6 @@ 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 -@[simp] lemma inner_ιMulti_self [FiniteDimensional ℝ E] (x : Fin n → E) : ⟪ιMulti ℝ n x, ιMulti ℝ n x⟫ = det (gram ℝ x) := innerProductForm_ιMulti_self x From 8d6a3e7e75841c7548bae93fc6e9f747470cdf59 Mon Sep 17 00:00:00 2001 From: Justus Springer Date: Thu, 18 Jun 2026 13:37:53 +0100 Subject: [PATCH 06/15] move file --- Mathlib.lean | 2 +- .../InnerProductSpace/ExteriorPower.lean} | 0 2 files changed, 1 insertion(+), 1 deletion(-) rename Mathlib/{LinearAlgebra/ExteriorPower/InnerProductSpace.lean => Analysis/InnerProductSpace/ExteriorPower.lean} (100%) diff --git a/Mathlib.lean b/Mathlib.lean index eac96c928f3e6b..b98ff2dd53b836 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2027,6 +2027,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 @@ -5009,7 +5010,6 @@ public import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading public import Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating public import Mathlib.LinearAlgebra.ExteriorPower.Basic public import Mathlib.LinearAlgebra.ExteriorPower.Basis -public import Mathlib.LinearAlgebra.ExteriorPower.InnerProductSpace public import Mathlib.LinearAlgebra.ExteriorPower.Pairing public import Mathlib.LinearAlgebra.FiniteDimensional.Basic public import Mathlib.LinearAlgebra.FiniteDimensional.Defs diff --git a/Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean b/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean similarity index 100% rename from Mathlib/LinearAlgebra/ExteriorPower/InnerProductSpace.lean rename to Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean From edf6b86803219b03ed817ca59ad1e5e5b6251c58 Mon Sep 17 00:00:00 2001 From: Justus Springer Date: Wed, 22 Jul 2026 17:11:11 +0100 Subject: [PATCH 07/15] min imports --- Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean b/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean index 6ba28ac9019b54..9c46238a84246a 100644 --- a/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean +++ b/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean @@ -5,12 +5,8 @@ Authors: Justus Springer -/ module -public import Mathlib.LinearAlgebra.ExteriorPower.Pairing -public import Mathlib.LinearAlgebra.ExteriorPower.Basis -public import Mathlib.Analysis.InnerProductSpace.Basic public import Mathlib.Analysis.InnerProductSpace.GramMatrix -public import Mathlib.Analysis.InnerProductSpace.PiL2 -public import Mathlib.Analysis.Matrix.PosDef +public import Mathlib.LinearAlgebra.ExteriorPower.Basis /-! # Inner product space structure on exterior powers From fd99bff5c7cb323f406ff29c613d318d67b3147c Mon Sep 17 00:00:00 2001 From: Justus Springer <50165510+justus-springer@users.noreply.github.com> Date: Thu, 23 Jul 2026 16:36:22 +0100 Subject: [PATCH 08/15] Update Mathlib/Analysis/InnerProductSpace/GramMatrix.lean Co-authored-by: Thomas Browning --- Mathlib/Analysis/InnerProductSpace/GramMatrix.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean b/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean index c59def5e2090a7..7bc693a2ddb34c 100644 --- a/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean +++ b/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean @@ -136,8 +136,8 @@ theorem gram_eq_conjTranspose_mul {ι : Type*} [Fintype ι] (b : OrthonormalBasi omit [Finite n] in @[simp] -lemma gram_orthonormal [DecidableEq n] {v : n → E} (h : Orthonormal 𝕜 v) : gram 𝕜 v = 1 := by - ext; simp [orthonormal_iff_ite.mp h, Matrix.one_apply] +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. -/ From 1ec94048edf98dc7bde767941a4522deb1f69c4b Mon Sep 17 00:00:00 2001 From: Justus Springer Date: Thu, 23 Jul 2026 16:36:48 +0100 Subject: [PATCH 09/15] move variables --- Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean b/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean index 9c46238a84246a..60cecbb4466708 100644 --- a/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean +++ b/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean @@ -42,15 +42,14 @@ 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. -/ -def innerProductForm {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} : - ⋀[ℝ]^n E →ₗ[ℝ] ⋀[ℝ]^n E →ₗ[ℝ] ℝ := +def innerProductForm : ⋀[ℝ]^n E →ₗ[ℝ] ⋀[ℝ]^n E →ₗ[ℝ] ℝ := pairingDual ℝ E n ∘ₗ map n (innerₗ E) -variable {n : ℕ} {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] - 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] From 79c83b426b68c0d43af1a4b46bdf921f7fe825c0 Mon Sep 17 00:00:00 2001 From: Justus Springer Date: Thu, 23 Jul 2026 16:47:13 +0100 Subject: [PATCH 10/15] fix --- Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean b/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean index 60cecbb4466708..25008db7cbeb15 100644 --- a/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean +++ b/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean @@ -80,7 +80,7 @@ lemma innerProductForm_ιMulti_family_of_orthonormal {ι : Type*} [LinearOrder simp only [ιMulti_family] split_ifs with h · subst h - simp [gram_orthonormal (hv.comp _ (RelEmbedding.injective _))] + simp [gram_eq_one_iff_orthonormal.mpr (hv.comp _ (RelEmbedding.injective _))] · rw [innerProductForm_ιMulti_ιMulti] have : ¬t.1 ⊆ s.1 := fun H ↦ Ne.symm h <| Subtype.val_injective (Finset.eq_of_subset_of_card_le H (s.2.le.trans t.2.ge)) From 80da7d0ddd50c5bb61a49fb1809b1cb0ce1d2ae8 Mon Sep 17 00:00:00 2001 From: Justus Springer Date: Thu, 23 Jul 2026 16:47:24 +0100 Subject: [PATCH 11/15] golf --- Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean b/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean index 25008db7cbeb15..21009e5e110cbf 100644 --- a/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean +++ b/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean @@ -82,8 +82,7 @@ lemma innerProductForm_ιMulti_family_of_orthonormal {ι : Type*} [LinearOrder · subst h simp [gram_eq_one_iff_orthonormal.mpr (hv.comp _ (RelEmbedding.injective _))] · rw [innerProductForm_ιMulti_ιMulti] - have : ¬t.1 ⊆ s.1 := fun H ↦ Ne.symm h <| - Subtype.val_injective (Finset.eq_of_subset_of_card_le H (s.2.le.trans t.2.ge)) + have : ¬t.1 ⊆ s.1 := Set.powersetCard.eq_iff_subset.not.mp (Ne.symm h) rw [Finset.not_subset] at this obtain ⟨x, hxt, hxs⟩ := this simp only [Set.powersetCard.mem_coe_iff, Set.mem_range, not_exists, From e6ef791d89ddc1f5ef7ce34cbc00d9974c121951 Mon Sep 17 00:00:00 2001 From: Justus Springer <50165510+justus-springer@users.noreply.github.com> Date: Thu, 23 Jul 2026 17:39:56 +0100 Subject: [PATCH 12/15] Update Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean Co-authored-by: Thomas Browning --- Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean b/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean index 21009e5e110cbf..a6e5621b996b30 100644 --- a/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean +++ b/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean @@ -82,13 +82,11 @@ lemma innerProductForm_ιMulti_family_of_orthonormal {ι : Type*} [LinearOrder · subst h simp [gram_eq_one_iff_orthonormal.mpr (hv.comp _ (RelEmbedding.injective _))] · rw [innerProductForm_ιMulti_ιMulti] - have : ¬t.1 ⊆ s.1 := Set.powersetCard.eq_iff_subset.not.mp (Ne.symm h) - rw [Finset.not_subset] at this - obtain ⟨x, hxt, hxs⟩ := this - simp only [Set.powersetCard.mem_coe_iff, Set.mem_range, not_exists, + 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, hi⟩ := hxt - exact det_eq_zero_of_row_eq_zero i (fun j ↦ hv.inner_eq_zero (hi ▸ hxs j)) + obtain ⟨i, rfl⟩ := hxt + exact det_eq_zero_of_row_eq_zero i (fun j ↦ hv.inner_eq_zero (hxs j)) lemma innerProductForm_eq_sum {ι : Type*} [Fintype ι] [LinearOrder ι] (b : OrthonormalBasis ι ℝ E) (x y : ⋀[ℝ]^n E) : From 25c749c6d40c121035e5cf523ebf2ba57393dbc7 Mon Sep 17 00:00:00 2001 From: Justus Springer <50165510+justus-springer@users.noreply.github.com> Date: Thu, 23 Jul 2026 17:40:25 +0100 Subject: [PATCH 13/15] Update Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean Co-authored-by: Thomas Browning --- Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean b/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean index a6e5621b996b30..668600a945f17c 100644 --- a/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean +++ b/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean @@ -59,8 +59,7 @@ 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] -lemma flip_innerProductForm : - LinearMap.flip (innerProductForm (E := E) (n := n)) = innerProductForm := by +lemma flip_innerProductForm : (innerProductForm (E := E) (n := n)).flip = innerProductForm := by apply linearMap_ext ext simp only [LinearMap.compAlternatingMap_apply, LinearMap.flip_apply, From 1bb3f47b666b3a2a48a306e8e7174900f8dcb865 Mon Sep 17 00:00:00 2001 From: Justus Springer Date: Mon, 27 Jul 2026 08:05:20 +0100 Subject: [PATCH 14/15] privatize --- .../InnerProductSpace/ExteriorPower.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean b/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean index 668600a945f17c..7d5fa0a149497c 100644 --- a/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean +++ b/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean @@ -47,19 +47,19 @@ 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. -/ -def innerProductForm : ⋀[ℝ]^n E →ₗ[ℝ] ⋀[ℝ]^n E →ₗ[ℝ] ℝ := +private def innerProductForm : ⋀[ℝ]^n E →ₗ[ℝ] ⋀[ℝ]^n E →ₗ[ℝ] ℝ := pairingDual ℝ E n ∘ₗ map n (innerₗ E) -lemma innerProductForm_ιMulti_ιMulti (x y : Fin n → 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] -lemma innerProductForm_ιMulti_self (x : Fin n → E) : +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] -lemma flip_innerProductForm : (innerProductForm (E := E) (n := n)).flip = innerProductForm := by +private lemma flip_innerProductForm : (innerProductForm (E := E) (n := n)).flip = innerProductForm := by apply linearMap_ext ext simp only [LinearMap.compAlternatingMap_apply, LinearMap.flip_apply, @@ -69,11 +69,11 @@ lemma flip_innerProductForm : (innerProductForm (E := E) (n := n)).flip = innerP ext exact real_inner_comm _ _ -lemma innerProductForm_symm (x y : ⋀[ℝ]^n E) : innerProductForm y x = innerProductForm x y := +private lemma innerProductForm_symm (x y : ⋀[ℝ]^n E) : innerProductForm y x = innerProductForm x y := congr($flip_innerProductForm x y) @[simp] -lemma innerProductForm_ιMulti_family_of_orthonormal {ι : Type*} [LinearOrder ι] {v : ι → E} +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] @@ -87,7 +87,7 @@ lemma innerProductForm_ιMulti_family_of_orthonormal {ι : Type*} [LinearOrder obtain ⟨i, rfl⟩ := hxt exact det_eq_zero_of_row_eq_zero i (fun j ↦ hv.inner_eq_zero (hxs j)) -lemma innerProductForm_eq_sum {ι : Type*} [Fintype ι] [LinearOrder ι] +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 @@ -95,12 +95,12 @@ lemma innerProductForm_eq_sum {ι : Type*} [Fintype ι] [LinearOrder ι] rw [← (b.toBasis.exteriorPower n).sum_repr x, ← (b.toBasis.exteriorPower n).sum_repr y] simp -lemma innerProductForm_self (x : ⋀[ℝ]^n E) {ι : Type*} [Fintype ι] [LinearOrder ι] +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] -instance [FiniteDimensional ℝ E] : InnerProductSpace.Core ℝ (⋀[ℝ]^n E) where +@[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 From 1935330e30a1c80fcb21a3d68c7cffaa23f67c9f Mon Sep 17 00:00:00 2001 From: tb65536 Date: Mon, 27 Jul 2026 09:06:43 +0100 Subject: [PATCH 15/15] fix long lines --- Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean b/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean index 7d5fa0a149497c..1bb7d526df2960 100644 --- a/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean +++ b/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean @@ -59,7 +59,8 @@ 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 +private lemma flip_innerProductForm : + (innerProductForm (E := E) (n := n)).flip = innerProductForm := by apply linearMap_ext ext simp only [LinearMap.compAlternatingMap_apply, LinearMap.flip_apply, @@ -69,7 +70,8 @@ private lemma flip_innerProductForm : (innerProductForm (E := E) (n := n)).flip ext exact real_inner_comm _ _ -private lemma innerProductForm_symm (x y : ⋀[ℝ]^n E) : innerProductForm y x = innerProductForm x y := +private lemma innerProductForm_symm (x y : ⋀[ℝ]^n E) : + innerProductForm y x = innerProductForm x y := congr($flip_innerProductForm x y) @[simp]