English
An orthonormal set is maximal iff the orthogonal complement of its span is zero.
Русский
Ортонормальный набор максимален тогда и только тогда, когда ортогональное дополнение его линзы оказывается нулём.
LaTeX
$$$\\text{maximal\\_orthonormal\_iff\_orthogonalComplement\_eq\_bot}$$$
Lean4
/-- An orthonormal set in an `InnerProductSpace` is maximal, if and only if the orthogonal
complement of its span is empty. -/
theorem maximal_orthonormal_iff_orthogonalComplement_eq_bot (hv : Orthonormal 𝕜 ((↑) : v → E)) :
(∀ u ⊇ v, Orthonormal 𝕜 ((↑) : u → E) → u = v) ↔ (span 𝕜 v)ᗮ = ⊥ :=
by
rw [Submodule.eq_bot_iff]
constructor
· contrapose!
-- ** direction 1: nonempty orthogonal complement implies nonmaximal
rintro
⟨x, hx', hx⟩
-- take a nonzero vector and normalize it
let e := (‖x‖⁻¹ : 𝕜) • x
have he : ‖e‖ = 1 := by simp [e, norm_smul_inv_norm hx]
have he' : e ∈ (span 𝕜 v)ᗮ := smul_mem' _ _ hx'
have he'' : e ∉ v := by
intro hev
have : e = 0 := by
have : e ∈ span 𝕜 v ⊓ (span 𝕜 v)ᗮ := ⟨subset_span hev, he'⟩
simpa [(span 𝕜 v).inf_orthogonal_eq_bot] using this
have : e ≠ 0 := hv.ne_zero ⟨e, hev⟩
contradiction
-- put this together with `v` to provide a candidate orthonormal basis for the whole space
refine ⟨insert e v, v.subset_insert e, ⟨?_, ?_⟩, (ne_insert_of_notMem v he'').symm⟩
· -- show that the elements of `insert e v` have unit length
rintro ⟨a, ha'⟩
rcases eq_or_mem_of_mem_insert ha' with ha | ha
· simp [ha, he]
· exact hv.1 ⟨a, ha⟩
· -- show that the elements of `insert e v` are orthogonal
have h_end : ∀ a ∈ v, ⟪a, e⟫ = 0 := by
intro a ha
exact he' a (Submodule.subset_span ha)
rintro ⟨a, ha'⟩
rcases eq_or_mem_of_mem_insert ha' with ha | ha
· rintro ⟨b, hb'⟩ hab'
have hb : b ∈ v := by grind
rw [inner_eq_zero_symm]
simpa [ha] using h_end b hb
rintro ⟨b, hb'⟩ hab'
rcases eq_or_mem_of_mem_insert hb' with hb | hb
· simpa [hb] using h_end a ha
have : (⟨a, ha⟩ : v) ≠ ⟨b, hb⟩ := by
intro hab''
apply hab'
simpa using hab''
exact hv.2 this
· -- ** direction 2: empty orthogonal complement implies maximal
simp only [Subset.antisymm_iff]
rintro h u (huv : v ⊆ u) hu
refine ⟨?_, huv⟩
intro x hxu
refine ((mt (h x)) (hu.ne_zero ⟨x, hxu⟩)).imp_symm ?_
intro hxv y hy
have hxv' : (⟨x, hxu⟩ : u) ∉ ((↑) ⁻¹' v : Set u) := by simp [hxv]
obtain ⟨l, hl, rfl⟩ : ∃ l ∈ supported 𝕜 𝕜 ((↑) ⁻¹' v : Set u), (linearCombination 𝕜 ((↑) : u → E)) l = y :=
by
rw [← Finsupp.mem_span_image_iff_linearCombination]
simp [huv, inter_eq_self_of_subset_right, hy]
exact hu.inner_finsupp_eq_zero hxv' hl