Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-06 07:46 a95b4427

View on Github →

feat(probability/martingale): Doob's maximal inequality (#14737)

Estimated changes

Modified src/measure_theory/integral/set_integral.lean

added theorem measure_theory.set_integral_ge_of_const_le

Modified src/measure_theory/lattice.lean

added theorem finset.measurable_range_sup''

added theorem finset.measurable_range_sup'

added theorem finset.measurable_sup'

Modified src/probability/hitting_time.lean

added theorem measure_theory.stopped_value_hitting_mem

Modified src/probability/martingale.lean

added theorem measure_theory.maximal_ineq

added theorem measure_theory.smul_le_stopped_value_hitting