Spans of orthonormal subfamilies

For an orthonormal basis b : OrthonormalBasis ι 𝕜 E and a set s : Set ι of indices, b.spanIndices s is the subspace spanned by the selected basis vectors {b i : i ∈ s}.

Main results

• OrthonormalBasis.mem_spanIndices_iff: membership is characterized by the vanishing of the coordinates outside s.
• OrthonormalBasis.finrank_spanIndices: the dimension is the number of selected indices.
• OrthonormalBasis.orthogonal_spanIndices: the orthogonal complement is the span of the complementary subfamily.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: ForMathlib/Analysis/InnerProductSpace/CourantFischer.lean (the specSubspace scaffolding), staged at ForTauCeti/Analysis/InnerProductSpace/CourantFischer.lean.
• Original authors / copyright: formalized by Claude Fable 5, golfed/polished by Claude Opus 4.8; Apache 2.0. Generalized (index type, Set selection, membership iff) by Claude Fable 5 during Tau Ceti signature polish.
• Extraction class: generalized; the Courant–Fischer module now consumes this API.
• Spectra influence: none — this module imports only Mathlib.

noncomputable def OrthonormalBasis.spanIndices {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (s : Set ι) : Submodule 𝕜 E

The subspace spanned by the orthonormal basis vectors b i for indices i ∈ s.

Equations

• b.spanIndices s = Submodule.span 𝕜 (⇑b '' s)

theorem OrthonormalBasis.spanIndices_eq_span {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (s : Set ι) : b.spanIndices s = Submodule.span 𝕜 (⇑b '' s)

spanIndices is the span of the selected basis vectors. The characteristic lemma: spanIndices is a name for a Submodule.span, and a consumer that needs to run Submodule.span_induction needs to be told so.

Written because dropping this module's blanket @[expose] broke exactly one downstream proof — LinearMap.IsSymmetric.map_mem_spanIndices in CourantFischer.lean — which was reaching through the definition instead. That is the api-design rubric's case for a missing lemma rather than an exposed body.

theorem OrthonormalBasis.spanIndices_mono {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) {s t : Set ι} (h : s ⊆ t) : b.spanIndices s ≤ b.spanIndices t

Selecting more indices spans more.

theorem OrthonormalBasis.mem_spanIndices_of_mem {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) {s : Set ι} {i : ι} (hi : i ∈ s) : b i ∈ b.spanIndices s

A selected basis vector lies in the span of its index set.

theorem OrthonormalBasis.repr_eq_zero_of_mem_spanIndices {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) {s : Set ι} {x : E} (hx : x ∈ b.spanIndices s) {i : ι} (hi : i ∉ s) : (b.repr x).ofLp i = 0

A vector in the span of a selected subfamily has zero coordinate at any index outside the selection.

theorem OrthonormalBasis.mem_spanIndices_iff {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) {s : Set ι} {x : E} : x ∈ b.spanIndices s ↔ ∀ i ∉ s, (b.repr x).ofLp i = 0

Membership in the span of a selected subfamily is exactly the vanishing of the coordinates outside the selection.

theorem OrthonormalBasis.finrank_spanIndices {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (s : Finset ι) : Module.finrank 𝕜 ↥(b.spanIndices ↑s) = s.card

The span of a selected subfamily has dimension the number of selected indices.

theorem OrthonormalBasis.finrank_spanIndices_set {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (s : Set ι) [DecidablePred fun (x : ι) => x ∈ s] : Module.finrank 𝕜 ↥(b.spanIndices s) = s.toFinset.card

Set form of OrthonormalBasis.finrank_spanIndices.

theorem OrthonormalBasis.orthogonal_spanIndices {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (s : Set ι) : (b.spanIndices s)ᗮ = b.spanIndices sᶜ

The orthogonal complement of the span of a selected subfamily is the span of the complementary subfamily.