{m : ℕ} (w : Fin m → E) {T : EuclideanSpace ℂ (Fin m) →L[ℂ] EuclideanSpace ℂ (Fin m)} (hT : IsWhitening w T) (c : EuclideanSpace ℂ (Fin m)) : ‖whitened w T c‖ = ‖c‖

Initializing...

{m : ℕ} (w : Fin m → E) {T : EuclideanSpace ℂ (Fin m) →L[ℂ] EuclideanSpace ℂ (Fin m)} (hT : IsWhitening w T) (c : EuclideanSpace ℂ (Fin m)) : ‖whitened w T c‖ = ‖c‖ · Prove2Me