OAI/Probability/CriticalPercolation/Entropy/BinaryStages.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.BinaryLaw.stageIndices line 19
  2. def OAI.CriticalPercolation.BinaryLaw.stage line 22
  3. lemma OAI.CriticalPercolation.BinaryLaw.stage_zero line 25
  4. lemma OAI.CriticalPercolation.BinaryLaw.stage_last line 29
  5. lemma OAI.CriticalPercolation.BinaryLaw.stageIndices_succ_active line 34
  6. lemma OAI.CriticalPercolation.BinaryLaw.stageIndices_succ_inactive line 48
  7. lemma OAI.CriticalPercolation.BinaryLaw.configuration_opened line 60
  8. lemma OAI.CriticalPercolation.BinaryLaw.supported_mark_closed line 79
  9. lemma OAI.CriticalPercolation.BinaryLaw.supported_marks_distinct line 89
  10. lemma OAI.CriticalPercolation.BinaryLaw.supported_stage_closed line 99
  11. lemma OAI.CriticalPercolation.BinaryLaw.supported_stage_close line 111
  12. lemma OAI.CriticalPercolation.BinaryLaw.supported_opening_injective line 124
  13. lemma OAI.CriticalPercolation.BinaryLaw.stage_endpointEvent line 141