Commit 2022-10-08 03:03 85453a2a

View on Github →

feat(probability/variance): introduce ℝ≥0∞-valued variance (#16730) This PR introduces ℝ≥0∞-valued variance and define the real-valued variance in terms of it.

Estimated changes

Modified src/analysis/normed/field/basic.lean

added theorem real.to_nnreal_mul_nnnorm

Modified src/analysis/normed/group/basic.lean

added theorem real.to_nnreal_eq_nnnorm_of_nonneg

Modified src/data/real/nnreal.lean

added theorem real.to_nnreal_of_nonneg

Modified src/probability/ident_distrib.lean

added theorem probability_theory.ident_distrib.evariance_eq

Modified src/probability/moments.lean

modified theorem probability_theory.central_moment_two_eq_variance

Modified src/probability/strong_law.lean

Modified src/probability/variance.lean

added theorem measure_theory.mem_ℒp.evariance_lt_top

added theorem measure_theory.mem_ℒp.of_real_variance_eq

added theorem measure_theory.mem_ℒp.variance_eq

added theorem measure_theory.mem_ℒp.variance_eq_of_integral_eq_zero

added def probability_theory.evariance

added theorem probability_theory.evariance_def'

added theorem probability_theory.evariance_eq_lintegral_of_real

added theorem probability_theory.evariance_eq_top

added theorem probability_theory.evariance_eq_zero_iff

added theorem probability_theory.evariance_lt_top_iff_mem_ℒp

added theorem probability_theory.evariance_mul

added theorem probability_theory.evariance_zero

modified theorem probability_theory.indep_fun.variance_add

modified theorem probability_theory.indep_fun.variance_sum

added theorem probability_theory.meas_ge_le_evariance_div_sq

modified theorem probability_theory.meas_ge_le_variance_div_sq

modified def probability_theory.variance

modified theorem probability_theory.variance_def'

modified theorem probability_theory.variance_le_expectation_sq

modified theorem probability_theory.variance_mul

modified theorem probability_theory.variance_nonneg

modified theorem probability_theory.variance_smul

modified theorem probability_theory.variance_zero