Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-08 12:55 3478a2af

View on Github →

feat(probability/ident_distrib): identically distributed random variables (#14024)

Estimated changes

Created src/probability/ident_distrib.lean

added theorem probability_theory.ident_distrib.ae_mem_snd

added theorem probability_theory.ident_distrib.ae_snd

added theorem probability_theory.ident_distrib.ae_strongly_measurable_fst

added theorem probability_theory.ident_distrib.ae_strongly_measurable_iff

added theorem probability_theory.ident_distrib.ae_strongly_measurable_snd

added theorem probability_theory.ident_distrib.const_div

added theorem probability_theory.ident_distrib.const_mul

added theorem probability_theory.ident_distrib.div_const

added theorem probability_theory.ident_distrib.ess_sup_eq

added theorem probability_theory.ident_distrib.integrable_iff

added theorem probability_theory.ident_distrib.integrable_snd

added theorem probability_theory.ident_distrib.integral_eq

added theorem probability_theory.ident_distrib.lintegral_eq

added theorem probability_theory.ident_distrib.measure_mem_eq

added theorem probability_theory.ident_distrib.mem_ℒp_iff

added theorem probability_theory.ident_distrib.mem_ℒp_snd

added theorem probability_theory.ident_distrib.mul_const

added theorem probability_theory.ident_distrib.snorm_eq

added theorem probability_theory.ident_distrib.variance_eq

added structure probability_theory.ident_distrib