feat(Analysis/InnerProductSpace): Gram completeness — equal Gram matrices give a unitary

[ibarrajo]

Adds Mathlib/Analysis/InnerProductSpace/GramUnitary.lean proving Gram completeness: in a finite-dimensional inner product space over an RCLike field, two finite families of vectors with equal Gram matrices ⟪vᵢ, vⱼ⟫ = ⟪wᵢ, wⱼ⟫ are related by a single global unitary U : E ≃ₗᵢ[𝕜] E with U (v i) = w i. This is the geometric core of the First Fundamental Theorem of classical invariant theory for the unitary group U(n) (and GL(n, ℂ)): the Gram entries are a complete invariant of a family of vectors up to the diagonal unitary action.

Main results

• LinearIsometryEquiv.exists_of_gram_eq — equal Gram entries ⟪v i, v j⟫ = ⟪w i, w j⟫ produce a U : E ≃ₗᵢ[𝕜] E with U (v i) = w i for all i.
• LinearIsometryEquiv.exists_of_gram_matrix_eq — the same statement phrased through the existing Matrix.gram.
• eq_of_isometryInvariant_of_gram_eq — the function-level First Fundamental Theorem (separation): any function of a family invariant under the diagonal unitary action factors through the Gram matrix.

Supporting reusable lemmas in the same file: LinearIsometryEquiv.inner_linearCombination_linearCombination, inner_linearCombination_eq_of_gram_eq, linearCombination_eq_zero_of_gram_eq, ker_linearCombination_le_of_gram_eq, and gramFactor / gramIsometry (the Gram-preserving map span 𝕜 (range v) →ₗᵢ[𝕜] E sending v i ↦ w i).

Generality: arbitrary RCLike field 𝕜, any finite-dimensional inner product space E, and any Finite index type ι.

Why it is not already in mathlib

mathlib has the Gram matrix and its positive (semi)definiteness (Matrix.posDef_gram_iff_linearIndependent) and the geometric primitive LinearIsometry.extend, but no statement that equal Gram matrices are realized by a unitary, and no classical-invariant-theory First Fundamental Theorem. This supplies the missing geometric bridge, built directly on LinearIsometry.extend and the existing Matrix.gram.

Implementation notes

The proof factors Finsupp.linearCombination 𝕜 v through its range. Equal Gram matrices make ⟪∑ cᵢ vᵢ, ∑ dⱼ vⱼ⟫ depend only on the Gram entries, so the two linear-combination maps share a kernel and the assignment v i ↦ w i is a well-defined isometry on span 𝕜 (range v). LinearIsometry.extend promotes it to a global isometry of E, which is surjective (hence a LinearIsometryEquiv) by finite-dimensionality. #print axioms on the three main theorems gives [propext, Classical.choice, Quot.sound] only.

Out of scope (possible follow-up)

A degree-two Schur–Weyl commutant fact (End_{U(2)}(ℂ² ⊗ ℂ²) = span{id, swap}) was developed alongside this material but is not included: the available proof is an explicit n = 2 coordinate solve and would need a representation-theoretic generalization (e.g. the V ⊗ V ≅ Sym²V ⊕ Λ²V decomposition) before it is mathlib-worthy. It is left for a separate PR.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary 3d7c73681b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.InnerProductSpace.GramUnitary (new file)	2491

---

Declarations diff (regex)

+ eq_of_isometryInvariant_of_gram_eq
+ exists_of_gram_eq
+ exists_of_gram_matrix_eq
+ gramFactor
+ gramFactor_apply_gen
+ gramFactor_linearCombination
+ gramIsometry
+ inner_gramFactor
+ inner_linearCombination_eq_of_gram_eq
+ inner_linearCombination_linearCombination
+ ker_linearCombination_le_of_gram_eq
+ linearCombination_eq_zero_of_gram_eq

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 3d7c736).

• +12 new declarations
• −0 removed declarations

+LinearIsometryEquiv.exists_of_gram_eq
+LinearIsometryEquiv.exists_of_gram_matrix_eq
+LinearIsometryEquiv.gramFactor
+LinearIsometryEquiv.gramFactor_apply_gen
+LinearIsometryEquiv.gramFactor_linearCombination
+LinearIsometryEquiv.gramIsometry
+LinearIsometryEquiv.inner_gramFactor
+LinearIsometryEquiv.inner_linearCombination_eq_of_gram_eq
+LinearIsometryEquiv.inner_linearCombination_linearCombination
+LinearIsometryEquiv.ker_linearCombination_le_of_gram_eq
+LinearIsometryEquiv.linearCombination_eq_zero_of_gram_eq
+eq_of_isometryInvariant_of_gram_eq

---

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
4942	1	exposed public sections

Current commit 3d7c73681b
Reference commit 9e7b1c1166

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[wwylele]

Does this overlap with #40567 ?