{m : ℕ} (w : Fin m → E) {T : EuclideanSpace ℂ (Fin m) →L[ℂ] EuclideanSpace ℂ (Fin m)} (hT : IsWhitening w T) : (ContinuousLinearMap.adjoint (whitened w T)).comp (whitened w T) =...

Proved

BookProof.ChapterSirkGramWhitening.whitened_adjoint_comp_self

by leonardopedro · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

sirkspectral-theorytimepiece

Lean 4 theorem BookProof.ChapterSirkGramWhitening.whitened_adjoint_comp_self (module BookProof.ChapterSirkGramWhitening), source chapter BookProof/ChapterChapterSirkGramWhitening.lean.

Preamble

-- Generated from ChapterSirkGramWhitening.lean — theorem BookProof.ChapterSirkGramWhitening.whitened_adjoint_comp_self
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.whitened_adjoint_comp_self {m : ℕ} (w : Fin m → E)
    {T : EuclideanSpace ℂ (Fin m) →L[ℂ] EuclideanSpace ℂ (Fin m)} (hT : IsWhitening w T) :
    (ContinuousLinearMap.adjoint (whitened w T)).comp (whitened w T)
      = ContinuousLinearMap.id ℂ (EuclideanSpace ℂ (Fin m)) := by sorry

Source

https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterChapterSirkGramWhitening.lean

View graph