Operator norm of the exterior power: trivializations and the compound matrix #
For finite-dimensional real inner product spaces E, F, this module builds the operator-norm
theory of the k-th exterior power ⋀^k f of a linear map f : E →ₗ[ℝ] F: the submultiplicativity
engine, the Hodge and orthonormal-basis trivializations, and the compound matrix with its
Cauchy–Binet multiplicativity. The Plücker eigenvalue ceilings and the Weyl perturbation theory
that build on this layer live in Oseledets.Lyapunov.ExteriorNorm.Plucker and
Oseledets.Lyapunov.ExteriorNorm.Weyl.
Main definitions #
Oseledets.ExteriorNorm.compoundMatrix— thek-th compound matrix, whose entries are thek × kminors.
Main results #
Oseledets.ExteriorNorm.exteriorOpNorm_comp_le— submultiplicativity of the exterior-power operator norm under composition.Oseledets.ExteriorNorm.exteriorOpNorm_hodge_eq_prod_singularValues— the bridge identifying the exterior operator norm with the product of the top-ksingular values∏_{i<k} σᵢ(f).Oseledets.ExteriorNorm.compoundMatrix_mul,Oseledets.ExteriorNorm.prod_singularValues_eq_l2_opNorm_compound— Cauchy–Binet multiplicativity and the operator-norm identity of the compound matrix.
Implementation notes #
The type ⋀[ℝ]^k E is definitionally ↥(Submodule …) and already carries an AddCommGroup
instance coming from the ambient submodule. Asserting or installing a fresh
NormedAddCommGroup (⋀[ℝ]^k E) would create an AddCommGroup/topology diamond that breaks
even IsTopologicalAddGroup synthesis on ⋀^k E.
To stay diamond-free we never put a normed structure on ⋀^k E. Instead we carry an explicit
linear trivialization ε : ⋀^k E ≃ₗ[ℝ] EuclideanSpace ℝ (Fin n) as data and measure the
operator norm of the conjugated map in the genuine Euclidean target. The canonical such
trivialization (exteriorTrivialization) exists because ⋀^k E is a finite free ℝ-module.
A small set of trivialization/ordering helper lemmas in this file are not private because the
Plucker layer downstream reuses them; they are internal infrastructure, not public API.
The submultiplicativity engine #
We carry explicit linear trivializations ε : ⋀^k · ≃ₗ EuclideanSpace ℝ (Fin n) as data and
take the operator norm of the conjugated exterior map in the genuine Euclidean target.
The k-th exterior map ⋀^k f, conjugated through trivializations of source and target
exterior powers into genuine Euclidean spaces.
Equations
- Oseledets.ExteriorNorm.conjExteriorMap k εE εF f = ↑εF ∘ₗ exteriorPower.map k f ∘ₗ ↑εE.symm
Instances For
The exterior-power operator norm of f, measured through the trivializations εE, εF.
When εE, εF are the orthonormal-wedge isometries for the Hodge inner product, this is the
genuine ‖⋀^k f‖.
Equations
Instances For
Submultiplicativity of the exterior-power operator norm. Pure functoriality
(exteriorPower.map_comp, with the middle trivialization telescoping) together with the
submultiplicativity of the continuous-linear-map operator norm (opNorm_comp_le).
Existence of trivializations #
Every ⋀^k E (a finite free ℝ-module) admits a linear equiv to a Euclidean space, via its
finrank basis.
A canonical linear trivialization of ⋀^k E into a Euclidean space, via the finrank basis.
Equations
- Oseledets.ExteriorNorm.exteriorTrivialization k = (Module.finBasis ℝ ↥(⋀[ℝ]^k E)).equivFun ≪≫ₗ (EuclideanSpace.equiv (Fin (Module.finrank ℝ ↥(⋀[ℝ]^k E))) ℝ).symm.toLinearEquiv
Instances For
The Hodge trivialization #
For an inner product space E, the Hodge trivialization of ⋀^k E is the linear equiv to
EuclideanSpace that sends the orthonormal wedge basis — the k-fold wedges
e_{i₁} ∧ ⋯ ∧ e_{i_k} of the standard orthonormal basis {eᵢ} of E — to the standard
Euclidean basis. It is a concrete piece of data (no inner product is installed on ⋀^k E,
avoiding the AddCommGroup/topology diamond). Measuring the exterior operator norm through this
trivialization gives the genuine ‖⋀^k f‖ for the Hodge inner product.
The wedge basis of ⋀^k E induced by the standard orthonormal basis of E: its elements are
the k-fold wedge products of distinct standard basis vectors. As a Basis it is data, and
under the Hodge inner product it is orthonormal.
Equations
Instances For
The reindexing equiv powersetCard (Fin (finrank E)) k ≃ Fin (finrank (⋀^k E)) witnessing
that both index sets have the same cardinality (finrank E).choose k.
Instances For
The Hodge trivialization of ⋀^k E: the linear equiv to a Euclidean space sending the
orthonormal wedge basis to the standard Euclidean basis.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The bridge to singular values #
‖⋀^k f‖ = ∏_{i<k} σᵢ(f), measured through the Hodge trivializations of source and target.
Mathematically: an SVD of f diagonalizes ⋀^k f on the orthonormal bases of k-fold wedges of
singular vectors; the operator norm is attained on the top wedge u₀ ∧ ⋯ ∧ u_{k-1}, whose image
has norm ∏_{i<k} σᵢ(f) (the largest wedge product, since σ is antitone). This requires the
SVD-decomposition packaging, the orthonormality of the wedge basis for the Hodge inner product,
and a diagonal-operator-norm computation, none of which are currently in Mathlib.
The det-Gram (Hodge) bilinear form and orthonormal-wedge trivializations #
We carry the Hodge inner product on ⋀^k E as a plain bilinear form hodgeForm (never as a
typeclass instance, to avoid the AddCommGroup/topology diamond). It is defined by reusing the
exterior-power dual pairing composed with the inner-product-to-dual map innerₗ, so on ιMulti
families it is the determinant of the Gram matrix det ⟪vᵢ, wⱼ⟫.
On ιMulti families, the Hodge form is the determinant of the Gram matrix ⟪vⱼ, wᵢ⟫.
Reindexing powersetCard ι k ≃ Fin (finrank (⋀^k E)) for an o.n. basis b indexed by ι.
Equations
Instances For
The wedge trivialization attached to an arbitrary orthonormal basis b of E.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The trivialization is a Hodge isometry: the L2 inner product of trivialized vectors equals the Hodge form.
Change of coordinates between two o.n.-basis wedge trivializations of the same space is
an L2 isometry (the compound ⋀^k Q of the orthogonal change of basis). The two bases may be
indexed differently; only the space E (hence finrank (⋀^k E)) matters.
Equations
- Oseledets.ExteriorNorm.onbChange b b' k = ((Oseledets.ExteriorNorm.onbTriv b k).symm.trans (Oseledets.ExteriorNorm.onbTriv b' k)).isometryOfInner ⋯
Instances For
Operator norm of a map with orthogonal images of an orthonormal basis #
The Gram determinant and the top-k product maximization #
Top-k prefix maximizes the product of antitone nonnegative weights. For antitone
nonnegative σ : Fin n → ℝ, the product over any k-subset is at most the product over the
top-k prefix indices (any top with (top i : ℕ) = i).
The top element of a non-top k-subset is ≥ k. If the ordered enumeration e of a
k-subset S of Fin n does not enumerate the top prefix {0,…,k-1}, then its largest element
e ⟨k-1⟩ has value ≥ k. (Otherwise all of S lies in {0,…,k-1}, forcing S = top prefix.)
The second-largest k-subset product bound. For antitone nonnegative lam, the product of
lam over the ordered enumeration e of a k-subset whose top element is ≥ k (i.e. a non-top
subset) is at most the second-largest product (∏_{i<k-1} lam i)·lam k. The top factor drops from
lam (k-1) to lam k; the remaining k-1 factors are bounded by the prefix {0,…,k-2}.
The bridge. Through the Hodge trivializations of source and target, the exterior operator
norm equals the product of the top-k singular values:
exteriorOpNorm k (hodgeTrivialization k) (hodgeTrivialization k) f = ∏_{i<k} σᵢ(f).
The Plücker bridge: eigen-diagonalization of the compound #
For a symmetric map f with orthonormal eigenbasis u and eigenvalues lam, the compound
⋀^k f is diagonal in the wedge basis of u: it scales the wedge u_S by ∏_{a ∈ S} lam a.
This is the abstract spectral core behind the Plücker top eigenpair and the second-eigenvalue
ceiling established below.
Product reindexing. A product of lam over the ordered enumeration of a k-subset S
equals the product of lam over S.
Eigen-diagonalization of the compound (abstract). For a linear map f with an orthonormal
eigenbasis u (f (u i) = lam i • u i), the compound ⋀^k f scales each wedge basis vector
u_S by the subset product ∏_{a ∈ S} lam a.
The compound matrix and the operator-norm/compound bridge #
For a square matrix M, the conjugated exterior map ⋀^k (toEuclideanLin M) through the
orthonormal-wedge trivialization of the standard basis EuclideanSpace.basisFun is itself
toEuclideanLin of an explicit compound matrix compoundMatrix k M, whose entries are the
k × k minors of M. This converts the (analytically delicate) exterior operator norm into the
L2 operator norm of a concrete matrix of determinants — the form needed for measurability.
onbTriv sends the i-th wedge basis vector (under (wIndexEquiv b k).symm) to the i-th
standard Euclidean basis vector.
The compound matrix C_k(M): its (t, s) entry is the k × k minor of M obtained by
selecting the rows enumerated by the t-th k-subset and the columns enumerated by the s-th
k-subset (under the standard orthonormal-wedge index equivalence).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The compound bridge. Through the orthonormal-wedge trivializations of the standard basis,
⋀^k (toEuclideanLin M) is toEuclideanLin of the compound matrix C_k(M).
Matrix-level Cauchy–Binet. The k-th compound of a matrix product is the
product of the compounds: C_k(B * M) = C_k(B) * C_k(M). This is the multiplicativity of the
compound matrix, proved via the functoriality ⋀^k(B ∘ M) = ⋀^k B ∘ ⋀^k M
(exteriorPower.map_comp) transported through the standard orthonormal-wedge trivialization by
the compound bridge conjExteriorMap_eq_toEuclideanLin_compound.
Compound of a transpose. The k-th compound matrix of Mᵀ is the transpose of the k-th
compound of M: C_k(Mᵀ) = C_k(M)ᵀ. Entrywise this is det(Mᵀ.minor) = det(M.minorᵀ)
(Matrix.det_transpose), since the row/column enumerators at index t, s coincide.
The k-th compound of the Gram matrix Mᵀ M is (C_k M)ᵀ (C_k M), i.e. the Gram matrix of the
compound. Combines compoundMatrix_mul with compoundMatrix_transpose.
Cauchy–Binet, linear-map form. toEuclideanLin of the k-th compound of a product is
the composition of the compounds. This is the form consumed by the rank-1 exterior
Rayleigh-deficit chain below, where the right-hand factor is post-composed with the inverse
compound.
Top singular value vs. the sum of squared singular values (Frobenius) #
The Frobenius back-transport below needs ‖M‖_op ≤ ‖M‖_F. Stated through the
singular-value bridge (toEuclideanLin) to avoid the L2-operator vs. Frobenius
NormedAddCommGroup-instance diamond on Matrix. The core inequality is that the top squared
singular value is at most the sum of all squared singular values; the sum equals
tr(MᵀM) = ‖M‖_F².
The top squared singular value of toEuclideanLin M is at most the sum of
all squared singular values. The sum over Fin d equals tr(MᵀM) = ‖M‖_F² (the Hilbert–Schmidt
norm squared); combined with ‖M‖_op = σ₀ this yields ‖M‖_op ≤ ‖M‖_F.
The top singular value of toEuclideanLin M is at most the Frobenius norm
√(∑ σᵢ²). Immediate from singularValues_zero_sq_le_sum and Real.sqrt.
The L2 operator-norm/Frobenius bridge. The squared L2 operator norm ‖M‖² of a
matrix is at most the sum of the squared singular values of toEuclideanLin M (the squared
Frobenius norm). The L2 matrix norm ‖M‖ is by definition the operator norm of toEuclideanLin M
on EuclideanSpace; expanding any vector in the singular-value eigenbasis u of
adjoint f ∘ₗ f (with f = toEuclideanLin M), the images f uⱼ are pairwise orthogonal with
‖f uⱼ‖ = σⱼ, so ‖f v‖² = ∑ⱼ ⟪uⱼ, v⟫² σⱼ² ≤ (∑ σᵢ²) ‖v‖².
The sum of the squared singular values of toEuclideanLin N equals the trace of the Gram
matrix tr(Nᵀ N) (the squared Frobenius norm). Both sides are the trace of the self-adjoint
operator adjoint f ∘ₗ f = toEuclideanLin (Nᵀ N): in the singular-value eigenbasis its diagonal
entries are the eigenvalues σᵢ², while as a matrix its trace is tr(Nᵀ N).
The eigenvalues of the Gram matrix Wᵀ W are bounded by the squared L2 operator norm ‖W‖².
Each eigenvalue μᵢ of the Hermitian matrix G = Wᵀ W, with unit eigenvector bᵢ, equals
‖toEuclideanLin W (bᵢ)‖² ≤ ‖W‖².
The Frobenius back-transport. For matrices U, V with orthonormal columns
(Uᵀ U = 1, Vᵀ V = 1), the squared L2 operator norm of the difference of the orthogonal
projectors U Uᵀ and V Vᵀ is bounded by 2 k (1 - det(Uᵀ V)²). Chain: self-adjoint idempotents
of trace k; ‖P − P'‖²_op ≤ ∑σᵢ² = tr((P−P')²) = 2k − 2 tr(P P'); tr(P P') = ‖Uᵀ V‖_F² = tr(G)
for the Gram G = (Uᵀ V)ᵀ (Uᵀ V); then the elementary AM-GM k ∏ tᵢ ≤ ∑ tᵢ over the eigenvalues
tᵢ ∈ [0, 1] of G, with ∏ tᵢ = det G = det(Uᵀ V)².
The product of singular values is the L2 operator norm of the compound matrix. Combining
the singular-value bridge with the compound identity: ∏_{i<k} σᵢ(toEuclideanLin M) = ‖C_k(M)‖.