`ChapterTotalVariance.within_nonneg` (w : Ω → ℝ) (X : Ω → κ) (Y : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω) : 0 ≤ within w X Y

Initializing...

`ChapterTotalVariance.within_nonneg` (w : Ω → ℝ) (X : Ω → κ) (Y : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω) : 0 ≤ within w X Y · Prove2Me