OAI/Probability/CriticalPercolation/Entropy/BinaryLaw.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.BinaryLaw.History line 16
  2. instance OAI.CriticalPercolation.BinaryLaw.historyFintype line 20
  3. def OAI.CriticalPercolation.BinaryLaw.interval line 26
  4. lemma OAI.CriticalPercolation.BinaryLaw.interval_bounds line 30
  5. def OAI.CriticalPercolation.BinaryLaw.nextIndex line 39
  6. lemma OAI.CriticalPercolation.BinaryLaw.nextIndex_bounds line 43
  7. def OAI.CriticalPercolation.BinaryLaw.anchors line 52
  8. def OAI.CriticalPercolation.BinaryLaw.anchorSet line 56
  9. lemma OAI.CriticalPercolation.BinaryLaw.anchors_length line 59
  10. lemma OAI.CriticalPercolation.BinaryLaw.anchorSet_step line 65
  11. lemma OAI.CriticalPercolation.BinaryLaw.endpoint_mem line 77
  12. def OAI.CriticalPercolation.BinaryLaw.firstIndex line 96
  13. lemma OAI.CriticalPercolation.BinaryLaw.firstIndex_spec line 99
  14. lemma OAI.CriticalPercolation.BinaryLaw.firstIndex_le line 103
  15. def OAI.CriticalPercolation.BinaryLaw.parentPredicate line 109
  16. def OAI.CriticalPercolation.BinaryLaw.parent line 114
  17. def OAI.CriticalPercolation.BinaryLaw.side line 117
  18. lemma OAI.CriticalPercolation.BinaryLaw.parentPredicate_congr line 120
  19. lemma OAI.CriticalPercolation.BinaryLaw.side_record line 145
  20. def OAI.CriticalPercolation.BinaryLaw.density line 158
  21. lemma OAI.CriticalPercolation.BinaryLaw.density_nonneg line 166
  22. lemma OAI.CriticalPercolation.BinaryLaw.density_record line 177
  23. theorem OAI.CriticalPercolation.BinaryLaw.density_normalized line 202
  24. lemma OAI.CriticalPercolation.BinaryLaw.base_left_mem line 239
  25. lemma OAI.CriticalPercolation.BinaryLaw.root_bound line 245
  26. lemma OAI.CriticalPercolation.BinaryLaw.reachable_record line 265
  27. lemma OAI.CriticalPercolation.BinaryLaw.cluster_record line 274
  28. def OAI.CriticalPercolation.BinaryLaw.endpointEvent line 282
  29. def OAI.CriticalPercolation.BinaryLaw.seed line 286
  30. lemma OAI.CriticalPercolation.BinaryLaw.endpointEvent_record line 290
  31. lemma OAI.CriticalPercolation.BinaryLaw.seed_record line 298
  32. lemma OAI.CriticalPercolation.BinaryLaw.seed_normalized line 303
  33. lemma OAI.CriticalPercolation.BinaryLaw.seed_nonneg line 310
  34. theorem OAI.CriticalPercolation.BinaryLaw.endpoint_density_normalized line 321
  35. lemma OAI.CriticalPercolation.BinaryLaw.kernel_parent_exists line 341
  36. lemma OAI.CriticalPercolation.BinaryLaw.parent_lt_of_exists line 369
  37. lemma OAI.CriticalPercolation.BinaryLaw.density_step_support line 374