Commit 2025-11-29 08:58 7408ee7f

View on Github →

feat(Probability/Kernel): \phi-irreducibility of kernels (#29734) Define powers of kernels, the Chapman-Kolmogorov equations, as well as \phi-irreducibility of kernels, following Robert-Casella, "Monte Carlo Statistical Methods", Definition 6.13.

Estimated changes

Modified Mathlib.lean

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

added theorem ProbabilityTheory.Kernel.comp_id

added theorem ProbabilityTheory.Kernel.id_comp

added theorem ProbabilityTheory.Kernel.pow_add

added theorem ProbabilityTheory.Kernel.pow_add_apply_eq_lintegral

added theorem ProbabilityTheory.Kernel.pow_succ_apply_eq_lintegral

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

deleted theorem ProbabilityTheory.Kernel.comp_id

deleted theorem ProbabilityTheory.Kernel.id_comp

Created Mathlib/Probability/Kernel/Irreducible.lean

added theorem ProbabilityTheory.Kernel.isIrreducible_of_le_measure

Modified docs/references.bib