Theorem ProbabilityTheory.Kernel.pow_succ_apply_eq_lintegral

Modification history

2025-11-29 08:58
Mathlib/Probability/Kernel/Composition/Comp.lean
feat(Probability/Kernel): \phi-irreducibility of kernels (#29734) …
Added ProbabilityTheory.Kernel.pow_succ_apply_eq_lintegralView on Github →