OAI/Probability/CriticalPercolation/ProductMeasure/Associated.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.FiniteMarkov.Associated line 18
  2. lemma OAI.CriticalPercolation.FiniteMarkov.avg_neg line 23
  3. lemma OAI.CriticalPercolation.FiniteMarkov.Associated.antitone line 27
  4. lemma OAI.CriticalPercolation.FiniteMarkov.Associated.cross line 33
  5. lemma OAI.CriticalPercolation.FiniteMarkov.step_mono line 41
  6. lemma OAI.CriticalPercolation.FiniteMarkov.association_halfstep line 45
  7. lemma OAI.CriticalPercolation.FiniteMarkov.step_antitone_of_neg line 57
  8. lemma OAI.CriticalPercolation.FiniteMarkov.iterate_association line 64
  9. def OAI.CriticalPercolation.FiniteMarkov.compose line 85
  10. lemma OAI.CriticalPercolation.FiniteMarkov.step_compose line 89
  11. lemma OAI.CriticalPercolation.FiniteMarkov.compose_nonneg line 96
  12. lemma OAI.CriticalPercolation.FiniteMarkov.compose_mass line 101
  13. lemma OAI.CriticalPercolation.FiniteMarkov.compose_minorization line 109
  14. lemma OAI.CriticalPercolation.FiniteMarkov.compose_associated line 117
  15. lemma OAI.CriticalPercolation.FiniteMarkov.compose_monotone line 128
  16. theorem OAI.CriticalPercolation.FiniteMarkov.stationary_associated line 135