Theorems · Theorem · probability

ProbabilityTheory.evariance_mul

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (c : ℝ) (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.evariance (fun ω => c * X ω) μ = ENNReal.ofReal (c ^ 2) * ProbabilityTheory.evariance X μ

Defined in

Mathlib.Probability.Moments.Variance

Cited by

1 results in Mathlib

Foundations

Depth 254 from the axioms · uses propext, Classical.choice, Quot.sound