`ChapterTotalVariance.crossTerm_zero` [Finite κ] (w : Ω → ℝ) (X : Ω → κ) (Y : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω) : (∑ ω, w ω * (Y ω - condMean w X Y (X ω)) * (condMean w X Y...

Initializing...

`ChapterTotalVariance.crossTerm_zero` [Finite κ] (w : Ω → ℝ) (X : Ω → κ) (Y : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω) : (∑ ω, w ω * (Y ω - condMean w X Y (X ω)) * (condMean w X Y... · Prove2Me