OAI/Probability/UnimodularPercolation/Criticality/ClusterCount.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exclusion of positive finite critical cluster counts.

  1. theorem OAI.Percolation.law_invariant_zero_one line 21
  2. theorem OAI.Percolation.unique_infinite_cluster_aut_iff line 35
  3. theorem OAI.Percolation.critical_unique_probability_zero line 54
  4. def OAI.Percolation.InfiniteCover line 66
  5. theorem OAI.Percolation.measurableSet_infiniteCover line 69
  6. theorem OAI.Percolation.unique_pos_of_cover_pos line 81
  7. theorem OAI.Percolation.critical_infiniteCover_survival_zero line 102
  8. theorem OAI.Percolation.critical_finite_count_empty_ae line 114