Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-07 14:57 a97d85de

View on Github →

feat(measure_theory/function/ae_eq_of_integral): remove a finite_measure assumption (#15899)

Estimated changes

Modified src/measure_theory/function/ae_eq_of_integral.lean

added theorem measure_theory.ae_nonneg_of_forall_set_integral_nonneg

deleted theorem measure_theory.ae_nonneg_of_forall_set_integral_nonneg_of_finite_measure

deleted theorem measure_theory.ae_nonneg_of_forall_set_integral_nonneg_of_finite_measure_of_strongly_measurable

added theorem measure_theory.ae_nonneg_of_forall_set_integral_nonneg_of_strongly_measurable

modified theorem measure_theory.ae_nonneg_restrict_of_forall_set_integral_nonneg_inter

deleted theorem measure_theory.integrable.ae_nonneg_of_forall_set_integral_nonneg

Modified src/probability/martingale.lean

modified theorem measure_theory.submartingale.condexp_sub_nonneg