OAI/Probability/CriticalPercolation/ProductMeasure/FiniteMarkovAvg.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.FiniteMarkov.avg line 14
2. def OAI.CriticalPercolation.FiniteMarkov.step line 16
3. lemma OAI.CriticalPercolation.FiniteMarkov.avg_const line 18
4. lemma OAI.CriticalPercolation.FiniteMarkov.avg_mono line 22
5. lemma OAI.CriticalPercolation.FiniteMarkov.avg_stationary line 26
6. lemma OAI.CriticalPercolation.FiniteMarkov.avg_iterate line 35
7. def OAI.CriticalPercolation.FiniteMarkov.remainder line 43
8. lemma OAI.CriticalPercolation.FiniteMarkov.remainder_nonneg line 48
9. lemma OAI.CriticalPercolation.FiniteMarkov.remainder_mass line 58
10. lemma OAI.CriticalPercolation.FiniteMarkov.step_remainder line 63
11. lemma OAI.CriticalPercolation.FiniteMarkov.step_bounds line 68
12. lemma OAI.CriticalPercolation.FiniteMarkov.iterate_bounds line 81
13. lemma OAI.CriticalPercolation.FiniteMarkov.iterate_distance line 99
14. lemma OAI.CriticalPercolation.FiniteMarkov.tendsto_iterate line 116