`ChapterTotalVariance.within_le_variance` [Finite κ] (w : Ω → ℝ) (X : Ω → κ) (Y : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω) : within w X Y ≤ variance w Y

Initializing...

`ChapterTotalVariance.within_le_variance` [Finite κ] (w : Ω → ℝ) (X : Ω → κ) (Y : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω) : within w X Y ≤ variance w Y · Prove2Me