Theorem ProbabilityTheory.evariance_def'

Modification history

2024-10-13 20:13

Mathlib/Probability/Variance.lean

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

Modified ProbabilityTheory.evariance_def'View on Github →

2023-06-21 03:45

Mathlib/Probability/Variance.lean

feat: port Probability.Variance (#5200)

Added ProbabilityTheory.evariance_def'View on Github →