OAI/Probability/CriticalPercolation/Clusters/Earlier.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.ClusterColumns.earlier line 17
  2. def OAI.CriticalPercolation.ClusterColumns.first line 18
  3. def OAI.CriticalPercolation.ClusterColumns.select line 20
  4. lemma OAI.CriticalPercolation.ClusterColumns.root_not_mem_earlier line 23
  5. lemma OAI.CriticalPercolation.ClusterColumns.earlier_mono line 28
  6. lemma OAI.CriticalPercolation.ClusterColumns.first_unique line 33
  7. lemma OAI.CriticalPercolation.ClusterColumns.exists_first line 42
  8. lemma OAI.CriticalPercolation.ClusterColumns.select_nonneg line 57
  9. lemma OAI.CriticalPercolation.ClusterColumns.select_zero_of_lt line 60
  10. lemma OAI.CriticalPercolation.ClusterColumns.select_diag line 66
  11. lemma OAI.CriticalPercolation.ClusterColumns.select_mul_sum line 70
  12. lemma OAI.CriticalPercolation.ClusterColumns.select_mass line 84
  13. lemma OAI.CriticalPercolation.ClusterColumns.cluster_partition line 89
  14. lemma OAI.CriticalPercolation.ClusterColumns.first_hit_not_mem_roots_iff line 95
  15. lemma OAI.CriticalPercolation.ClusterColumns.select_truncation line 105