Exact source: MathlibAnnex/Analysis/InnerProductSpace/FiniteEmbedding.lean
Pinned GitHub source · Raw UTF-8 source
Back to Realizing a finite Gram matrix in a represented CAR corner
1import Mathlib.Analysis.InnerProductSpace.l2Space23/-!4# Finite-dimensional isometric embeddings into infinite Hilbert spaces56The construction chooses finitely many members of a Hilbert basis of the7target and sends a finite orthonormal basis of the source to them.8-/910set_option autoImplicit false1112open scoped InnerProductSpace1314namespace MathlibAnnex.Analysis.InnerProductSpace1516/-- Every finite-dimensional complex inner product space embeds linearly and17isometrically into an infinite-dimensional complete complex inner product18space. -/19theorem nonempty_linearIsometry_of_finiteDimensional_of_not_finiteDimensional20 {E F : Type*}21 [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E]22 [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]23 (hF : ¬ FiniteDimensional ℂ F) : Nonempty (E →ₗᵢ[ℂ] F) := by24 classical25 obtain ⟨s, b, _⟩ := exists_hilbertBasis ℂ F26 have hs : s.Infinite := by27 intro hsfin28 letI : Fintype s := hsfin.fintype29 haveI : FiniteDimensional ℂ F :=30 b.toOrthonormalBasis.toBasis.finiteDimensional_of_finite31 exact hF inferInstance32 letI : Infinite s := hs.to_subtype33 let e : Fin (Module.finrank ℂ E) ↪ s :=34 Fin.valEmbedding.trans (Infinite.natEmbedding s)35 let u : Fin (Module.finrank ℂ E) → F := fun i => b (e i)36 have hu : Orthonormal ℂ u := b.orthonormal.comp e e.injective37 let v : OrthonormalBasis (Fin (Module.finrank ℂ E)) ℂ E :=38 stdOrthonormalBasis ℂ E39 let f : E →ₗ[ℂ] F := v.toBasis.constr ℂ u40 have hf : f ∘ v.toBasis = u := by41 funext i42 simp [f]43 exact ⟨f.isometryOfOrthonormal v.orthonormal (hf ▸ hu)⟩4445end MathlibAnnex.Analysis.InnerProductSpace