Spans of orthonormal subfamilies

For a finite-index orthonormal basis and a set of indices, spanIndices is the subspace spanned by the corresponding basis vectors.

Main results

• OrthonormalBasis.spanIndices_eq_span: the explicit span characterization.
• OrthonormalBasis.span_range_comp_subtypeVal_eq_spanIndices: the restriction b ∘ (↑) : s → E of the basis to the coordinate block s, an orthonormal family by Orthonormal.comp, spans the selected subspace.
• OrthonormalBasis.spanIndices_mono: monotonicity under index-set inclusion.
• OrthonormalBasis.mem_spanIndices_of_mem: selected basis vectors belong to the span.
• OrthonormalBasis.mem_spanIndices_iff: membership means coordinates vanish outside the selected indices.
• OrthonormalBasis.finrank_spanIndices: the dimension of a selected finite span.
• OrthonormalBasis.finrank_spanIndices_set: dimension as set cardinality.
• OrthonormalBasis.orthogonal_spanIndices: orthogonal complement by index complement.

Source

Adapted from ForTauCeti/Analysis/InnerProductSpace/BasisSpan.lean in the AIQ-Kitware DKPS formalization (Kitware, Inc.; Apache-2.0). The selected-span construction originates in the Courant--Fischer development.

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.

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)

The selected subspace is the span of its basis vectors. Use this identity to apply Submodule.span's induction or universal property.

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

The basis vectors indexed by the coordinate block s, as a family indexed by s, span the selected subspace.

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.

@[simp]

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.rank_spanIndices_val_lt_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {m : ℕ} (b : OrthonormalBasis (Fin m) 𝕜 E) (n : ℕ) : Module.rank 𝕜 ↥(b.spanIndices ↑{i : Fin m | ↑i < n}) ≤ ↑n

The span of the basis vectors with index below n has rank at most n.

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 ι) : Module.finrank 𝕜 ↥(b.spanIndices s) = s.ncard

The span of a selected set of basis vectors has dimension equal to the number of selected indices.

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.

theorem OrthonormalBasis.mem_spanIndices_le_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {m : ℕ} (b : OrthonormalBasis (Fin m) 𝕜 E) {n : ℕ} {x : E} (hx : x ∈ (b.spanIndices ↑{i : Fin m | ↑i < n})ᗮ) : x ∈ b.spanIndices {i : Fin m | n ≤ ↑i}

A vector orthogonal to the first n basis vectors lies in the remaining span.