Commit 2022-11-07 13:00 bea6c853

View on Github →

chore(probability/process/stopping): generalize lemmas about nat-indexed processes to generic types (#17379) We generalize several lemmas either to a type with the discrete topology, or to a locally_finite_order_bot.

Estimated changes

Modified src/probability/martingale/basic.lean

deleted theorem measure_theory.martingale.eq_zero_of_predicatable

added theorem measure_theory.martingale.eq_zero_of_predictable

Modified src/probability/martingale/borel_cantelli.lean

Modified src/probability/martingale/centering.lean

Modified src/probability/martingale/optional_stopping.lean

Modified src/probability/process/adapted.lean

added theorem measure_theory.adapted.prog_measurable_of_discrete

deleted theorem measure_theory.adapted.prog_measurable_of_nat

modified theorem measure_theory.prog_measurable_of_tendsto'

modified theorem measure_theory.prog_measurable_of_tendsto

Modified src/probability/process/stopping.lean

added theorem measure_theory.adapted.stopped_process

added theorem measure_theory.adapted.stopped_process_of_discrete

deleted theorem measure_theory.adapted.stopped_process_of_nat

added theorem measure_theory.adapted.strongly_measurable_stopped_process

added theorem measure_theory.adapted.strongly_measurable_stopped_process_of_discrete

deleted theorem measure_theory.adapted.strongly_measurable_stopped_process_of_nat

modified theorem measure_theory.integrable_stopped_process

added theorem measure_theory.integrable_stopped_process_of_mem_finset

modified theorem measure_theory.mem_ℒp_stopped_process

added theorem measure_theory.mem_ℒp_stopped_process_of_mem_finset

added theorem measure_theory.stopped_process_eq''

added theorem measure_theory.stopped_process_eq_of_mem_finset