Exact source: MathlibAnnex/Analysis/InnerProductSpace/FiniteEmbedding.lean, lines 19–41.
Back to Realizing a finite Gram matrix in a represented CAR corner
1import Mathlib.Analysis.InnerProductSpace.l2Space 2 3/-! 4# Finite-dimensional isometric embeddings into infinite Hilbert spaces 5 6The construction chooses finitely many members of a Hilbert basis of the 7target and sends a finite orthonormal basis of the source to them. 8-/ 9 10set_option autoImplicit false 11 12open scoped InnerProductSpace 13 14namespace MathlibAnnex.Analysis.InnerProductSpace 15 16/-- Every finite-dimensional complex inner product space embeds linearly and 17isometrically into an infinite-dimensional complete complex inner product 18space. -/ 19theorem nonempty_linearIsometry_of_finiteDimensional_of_not_finiteDimensional 20 {E F : Type*} 21 [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] 22 [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] 23 (hF : ¬ FiniteDimensional ℂ F) : Nonempty (E →ₗᵢ[ℂ] F) := by 24 classical 25 obtain ⟨s, b, _⟩ := exists_hilbertBasis ℂ F 26 have hs : s.Infinite := by 27 intro hsfin 28 letI : Fintype s := hsfin.fintype 29 haveI : FiniteDimensional ℂ F := 30 b.toOrthonormalBasis.toBasis.finiteDimensional_of_finite 31 exact hF inferInstance 32 letI : Infinite s := hs.to_subtype 33 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.injective 37 let v : OrthonormalBasis (Fin (Module.finrank ℂ E)) ℂ E := 38 stdOrthonormalBasis ℂ E 39 let f : E →ₗ[ℂ] F := v.toBasis.constr ℂ u 40 have hf : f ∘ v.toBasis = u := by 41 funext i 42 simp [f] 43 exact ⟨f.isometryOfOrthonormal v.orthonormal (hf ▸ hu)⟩ 44 45end MathlibAnnex.Analysis.InnerProductSpace