Theorem ProbabilityTheory.variance_def'

Modification history

2025-08-07 12:26

Mathlib/Probability/Moments/Variance.lean

chore: simplify the proof that the variance of independent random variables is the sum of the variances (#27989) …

Deleted ProbabilityTheory.variance_def'View on Github →

2025-02-21 20:26

Mathlib/Probability/Variance.lean

Rename `Mem𝓛p` to `MemLp` (#22164) …

Modified ProbabilityTheory.variance_def'View on Github →

2024-10-13 20:13

Mathlib/Probability/Variance.lean

chore(Probability/Variance): generalize assumptions from `MeasureSpace` to `MeasurableSpace` (#17702) …

Modified ProbabilityTheory.variance_def'View on Github →

2023-06-21 03:45

Mathlib/Probability/Variance.lean

feat: port Probability.Variance (#5200)

Added ProbabilityTheory.variance_def'View on Github →