Theorems · Theorem · probability
ProbabilityTheory.variance_eq_integral
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
AEMeasurable X μ → ProbabilityTheory.variance X μ = ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ- Defined in
- Mathlib.Probability.Moments.Variance
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 255 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- MeasureTheory.integralstatement and proof · cited by 1,779
- AEMeasurablestatement and proof · cited by 840
- ENorm.enormproof · cited by 715
- Filter.Eventually.of_forallproof · cited by 526
- ProbabilityTheory.variancestatement · cited by 104
- sq_absproof · cited by 49
- AEMeasurable.pow_constproof · cited by 27
- toReal_enormproof · cited by 20
- MeasureTheory.integral_toRealproof · cited by 15
Cited by10
Results whose statement or proof uses this declaration.
- ProbabilityTheory.covariance_selfproof · cited by 11
- ProbabilityTheory.variance_mapproof · cited by 11
- ProbabilityTheory.variance_add_constproof · cited by 2
- ProbabilityTheory.condVar_botproof · cited by 1
- ProbabilityTheory.variance_tilted_mulproof · cited by 1
- ProbabilityTheory.ae_eq_integral_of_variance_eq_zeroproof · cited by 1
- ProbabilityTheory.variance_fun_id_gaussianRealproof · cited by 1
- ProbabilityTheory.variance_of_integral_eq_zeroproof · cited by 0
- ProbabilityTheory.variance_diracproof · cited by 0
- ProbabilityTheory.centralMoment_two_eq_varianceproof · cited by 0