{m : ℕ} {w : Fin m → E} (hw : LinearIndependent ℂ w) : ∃ T : EuclideanSpace ℂ (Fin m) →L[ℂ] EuclideanSpace ℂ (Fin m), Function.Bijective T ∧ IsWhitening w T
ProvedBookProof.ChapterSirkGramWhitening.exists_isWhiteningsirkspectral-theorytimepiece
Lean 4 theorem BookProof.ChapterSirkGramWhitening.exists_isWhitening (module BookProof.ChapterSirkGramWhitening), source chapter BookProof/ChapterChapterSirkGramWhitening.lean.
Preamble
-- Generated from ChapterSirkGramWhitening.lean — theorem BookProof.ChapterSirkGramWhitening.exists_isWhitening
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.exists_isWhitening {m : ℕ} {w : Fin m → E} (hw : LinearIndependent ℂ w) :
∃ T : EuclideanSpace ℂ (Fin m) →L[ℂ] EuclideanSpace ℂ (Fin m),
Function.Bijective T ∧ IsWhitening w T := by sorrySource