{d : ℕ} (S : Submodule ℂ E) [CompleteSpace S] (b : OrthonormalBasis (Fin d) ℂ S) : (ContinuousLinearMap.adjoint (onbEmbedding S b)).comp (onbEmbedding S b) = ContinuousLinearMap.id ℂ...
ProvedBookProof.ChapterSirkGramWhitening.onbEmbedding_isometrysirkspectral-theorytimepiece
Lean 4 theorem BookProof.ChapterSirkGramWhitening.onbEmbedding_isometry (module BookProof.ChapterSirkGramWhitening), source chapter BookProof/ChapterChapterSirkGramWhitening.lean.
Preamble
-- Generated from ChapterSirkGramWhitening.lean — theorem BookProof.ChapterSirkGramWhitening.onbEmbedding_isometry
import Mathlib
import Definitions.Def_ChapterSirkGramWhitening
open BookProof.ChapterSirkGramWhitening
noncomputable section
open scoped InnerProductSpace
open Matrix
open BookProof.ChapterH4 BookProof.ChapterSirkWhitening
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]Formal statement
theorem BookProof.ChapterSirkGramWhitening.onbEmbedding_isometry {d : ℕ} (S : Submodule ℂ E) [CompleteSpace S]
(b : OrthonormalBasis (Fin d) ℂ S) :
(ContinuousLinearMap.adjoint (onbEmbedding S b)).comp (onbEmbedding S b)
= ContinuousLinearMap.id ℂ (EuclideanSpace ℂ (Fin d)) := by sorrySource