Structures · Analysis
ProbabilityTheory.Kernel.IsIrreducible
A kernel κ : Kernel α α is φ-irreducible (w.r.t. a given measure φ on α),
if for every measurable set A with positive measure under φ,
and for every a : α, there exists an integer n such that (κ ^ n) a A > 0.
Ref. Meyn-Tweedie Proposition 4.2.1(ii), page 89
- Defined in
- Mathlib.Probability.Kernel.Irreducible
- Shape
- 2 explicit arguments · adds irreducible
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by3
Ancestors0
No ancestors.