Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-09 17:00 878370b7

View on Github →

chore(measure_theory/function/condexp): split conditional_expectation into multiple files (#15714)

Estimated changes

Renamed src/measure_theory/function/conditional_expectation.lean to src/measure_theory/function/conditional_expectation/basic.lean

deleted theorem measure_theory.condexp_ae_eq_restrict_of_measurable_space_eq_on

deleted theorem measure_theory.condexp_ae_eq_restrict_zero

deleted theorem measure_theory.condexp_indicator

deleted theorem measure_theory.condexp_indicator_aux

deleted theorem measure_theory.condexp_restrict_ae_eq_restrict

deleted theorem measure_theory.condexp_strongly_measurable_mul

deleted theorem measure_theory.condexp_strongly_measurable_mul_of_bound

deleted theorem measure_theory.condexp_strongly_measurable_mul_of_bound₀

deleted theorem measure_theory.condexp_strongly_measurable_mul₀

deleted theorem measure_theory.condexp_strongly_measurable_simple_func_mul

deleted theorem measure_theory.integrable.uniform_integrable_condexp

deleted theorem measure_theory.rn_deriv_ae_eq_condexp

deleted theorem measure_theory.snorm_one_condexp_le_snorm

Created src/measure_theory/function/conditional_expectation/indicator.lean

added theorem measure_theory.condexp_ae_eq_restrict_of_measurable_space_eq_on

added theorem measure_theory.condexp_ae_eq_restrict_zero

added theorem measure_theory.condexp_indicator

added theorem measure_theory.condexp_indicator_aux

added theorem measure_theory.condexp_restrict_ae_eq_restrict

Created src/measure_theory/function/conditional_expectation/real.lean

added theorem measure_theory.condexp_strongly_measurable_mul

added theorem measure_theory.condexp_strongly_measurable_mul_of_bound

added theorem measure_theory.condexp_strongly_measurable_mul_of_bound₀

added theorem measure_theory.condexp_strongly_measurable_mul₀

added theorem measure_theory.condexp_strongly_measurable_simple_func_mul

added theorem measure_theory.integrable.uniform_integrable_condexp

added theorem measure_theory.rn_deriv_ae_eq_condexp

added theorem measure_theory.snorm_one_condexp_le_snorm

Modified src/probability/notation.lean

Modified src/probability/stopping.lean