OAI/Probability/CriticalPercolation/Exploration/AncestryForest.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CriticalPercolation.InterpolationForest.Forest line 9
  2. def OAI.CriticalPercolation.InterpolationForest.Forest.lineage line 16
  3. lemma OAI.CriticalPercolation.InterpolationForest.Forest.lineage_base line 21
  4. lemma OAI.CriticalPercolation.InterpolationForest.Forest.lineage_step line 24
  5. lemma OAI.CriticalPercolation.InterpolationForest.Forest.self_mem_lineage line 27
  6. lemma OAI.CriticalPercolation.InterpolationForest.Forest.mem_lineage_le line 31
  7. lemma OAI.CriticalPercolation.InterpolationForest.Forest.lineage_nodup line 43
  8. def OAI.CriticalPercolation.InterpolationForest.Forest.root line 52
  9. lemma OAI.CriticalPercolation.InterpolationForest.Forest.root_base line 57
  10. lemma OAI.CriticalPercolation.InterpolationForest.Forest.root_step line 60
  11. lemma OAI.CriticalPercolation.InterpolationForest.Forest.root_lt_two line 63
  12. lemma OAI.CriticalPercolation.InterpolationForest.Forest.root_mem_lineage line 71
  13. lemma OAI.CriticalPercolation.InterpolationForest.Forest.root_eq_of_mem line 79
  14. lemma OAI.CriticalPercolation.InterpolationForest.Forest.lineage_disjoint line 91
  15. lemma OAI.CriticalPercolation.InterpolationForest.Forest.lineage_subset_of_mem line 96
  16. lemma OAI.CriticalPercolation.InterpolationForest.Forest.parent_mem_lineage line 110
  17. lemma OAI.CriticalPercolation.InterpolationForest.Forest.parent_injective_lineage line 116
  18. lemma OAI.CriticalPercolation.InterpolationForest.Forest.parent_injective_two_lineages line 135
  19. def OAI.CriticalPercolation.InterpolationForest.Forest.active line 158
  20. lemma OAI.CriticalPercolation.InterpolationForest.Forest.mem_active line 161
  21. lemma OAI.CriticalPercolation.InterpolationForest.Forest.active_parent line 165
  22. lemma OAI.CriticalPercolation.InterpolationForest.Forest.parent_injOn_active line 173
  23. theorem OAI.CriticalPercolation.InterpolationForest.Forest.active_pair_multiplicity line 179
  24. lemma OAI.CriticalPercolation.InterpolationForest.Forest.previous_lineage_le_parent line 193
  25. theorem OAI.CriticalPercolation.InterpolationForest.Forest.previous_active_le_parent line 209