Commit 2023-06-21 09:25 3d3810ea

View on Github →

feat: port Probability.IdentDistrib (#5331)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/IdentDistrib.lean

added theorem ProbabilityTheory.IdentDistrib.ae_mem_snd

added theorem ProbabilityTheory.IdentDistrib.ae_snd

added theorem ProbabilityTheory.IdentDistrib.aestronglyMeasurable_fst

added theorem ProbabilityTheory.IdentDistrib.aestronglyMeasurable_iff

added theorem ProbabilityTheory.IdentDistrib.aestronglyMeasurable_snd

added theorem ProbabilityTheory.IdentDistrib.const_div

added theorem ProbabilityTheory.IdentDistrib.const_mul

added theorem ProbabilityTheory.IdentDistrib.div_const

added theorem ProbabilityTheory.IdentDistrib.essSup_eq

added theorem ProbabilityTheory.IdentDistrib.evariance_eq

added theorem ProbabilityTheory.IdentDistrib.integrable_iff

added theorem ProbabilityTheory.IdentDistrib.integrable_snd

added theorem ProbabilityTheory.IdentDistrib.integral_eq

added theorem ProbabilityTheory.IdentDistrib.lintegral_eq

added theorem ProbabilityTheory.IdentDistrib.measure_mem_eq

added theorem ProbabilityTheory.IdentDistrib.memℒp_iff

added theorem ProbabilityTheory.IdentDistrib.memℒp_snd

added theorem ProbabilityTheory.IdentDistrib.mul_const

added theorem ProbabilityTheory.IdentDistrib.snorm_eq

added theorem ProbabilityTheory.IdentDistrib.variance_eq

added structure ProbabilityTheory.IdentDistrib

added theorem ProbabilityTheory.Memℒp.uniformIntegrable_of_identDistrib

added theorem ProbabilityTheory.Memℒp.uniformIntegrable_of_identDistrib_aux