Commit 2025-05-02 17:28 846a90cb

View on Github →

chore(Probability): typeclass generalizations (#24474) These typeclass generalizations are extracted from a list generated by a linter written by @JovanGerb . See #mathlib4 > Linter for generalizing type class hypotheses @ 💬

Estimated changes

Modified Mathlib/Probability/IdentDistrib.lean

modified theorem ProbabilityTheory.IdentDistrib.aestronglyMeasurable_fst

modified theorem ProbabilityTheory.IdentDistrib.aestronglyMeasurable_iff

modified theorem ProbabilityTheory.IdentDistrib.aestronglyMeasurable_snd

Modified Mathlib/Probability/Independence/Integrable.lean

Modified Mathlib/Probability/Integration.lean

Modified Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean

modified theorem MeasureTheory.Measure.dirac_unit_compProd_const

modified theorem MeasureTheory.Measure.snd_dirac_unit_compProd_const

Modified Mathlib/Probability/Kernel/RadonNikodym.lean

modified theorem ProbabilityTheory.Kernel.singularPart_eq_zero_iff_apply_eq_zero

modified theorem ProbabilityTheory.Kernel.singularPart_of_subset_compl_mutuallySingularSetSlice

Modified Mathlib/Probability/Martingale/Basic.lean

modified theorem MeasureTheory.martingale_const_fun

modified theorem MeasureTheory.submartingale_iff_condExp_sub_nonneg

modified theorem MeasureTheory.submartingale_of_condExp_sub_nonneg

modified theorem MeasureTheory.submartingale_of_setIntegral_le

Modified Mathlib/Probability/Process/Adapted.lean

Modified Mathlib/Probability/Process/Stopping.lean

modified theorem MeasureTheory.ProgMeasurable.adapted_stoppedProcess

modified theorem MeasureTheory.ProgMeasurable.stoppedProcess

modified theorem MeasureTheory.ProgMeasurable.stronglyMeasurable_stoppedProcess

modified theorem MeasureTheory.measurable_stoppedValue

modified theorem MeasureTheory.progMeasurable_min_stopping_time