{m : ℕ} (w : Fin m → E) (T : EuclideanSpace ℂ (Fin m) →L[ℂ] EuclideanSpace ℂ (Fin m)) : LinearMap.range (whitened w T : EuclideanSpace ℂ (Fin m) →ₗ[ℂ] E) ≤ Submodule.span ℂ (Set.range w)
ProvedBookProof.ChapterSirkGramWhitening.range_whitened_lesirkspectral-theorytimepiece
Lean 4 theorem BookProof.ChapterSirkGramWhitening.range_whitened_le (module BookProof.ChapterSirkGramWhitening), source chapter BookProof/ChapterChapterSirkGramWhitening.lean.
Preamble
-- Generated from ChapterSirkGramWhitening.lean — theorem BookProof.ChapterSirkGramWhitening.range_whitened_le
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.range_whitened_le {m : ℕ} (w : Fin m → E)
(T : EuclideanSpace ℂ (Fin m) →L[ℂ] EuclideanSpace ℂ (Fin m)) :
LinearMap.range (whitened w T : EuclideanSpace ℂ (Fin m) →ₗ[ℂ] E)
≤ Submodule.span ℂ (Set.range w) := by sorrySource