Commit 2025-01-30 12:07 b848c8d0

View on Github →

chore(Variance): golf API (#20814)

Estimated changes

Modified Mathlib/MeasureTheory/Function/L1Space/Integrable.lean

added theorem MeasureTheory.Memℒp.integrable_norm_pow'

added theorem MeasureTheory.Memℒp.integrable_norm_pow

Modified Mathlib/Probability/Moments/Basic.lean

modified theorem ProbabilityTheory.centralMoment_two_eq_variance

Modified Mathlib/Probability/Variance.lean

deleted theorem MeasureTheory.Memℒp.evariance_lt_top

deleted theorem MeasureTheory.Memℒp.ofReal_variance_eq

deleted theorem MeasureTheory.Memℒp.variance_eq

deleted theorem MeasureTheory.Memℒp.variance_eq_of_integral_eq_zero

modified def ProbabilityTheory.evariance

modified theorem ProbabilityTheory.evariance_eq_lintegral_ofReal

added theorem ProbabilityTheory.evariance_eq_top_iff

added theorem ProbabilityTheory.evariance_lt_top

added theorem ProbabilityTheory.evariance_ne_top

added theorem ProbabilityTheory.ofReal_variance

modified def ProbabilityTheory.variance

added theorem ProbabilityTheory.variance_eq_integral

added theorem ProbabilityTheory.variance_of_integral_eq_zero