OAI/Probability/UnimodularPercolation/Encounter/Counts.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Counting encounter vertices by mass transport.

  1. def OAI.Percolation.cutIso line 19
  2. theorem OAI.Percolation.branchCount_iso line 28
  3. theorem OAI.Percolation.clusterFinset_aut line 42
  4. theorem OAI.Percolation.measurable_branchCount_pair line 58
  5. def OAI.Percolation.markedCluster line 63
  6. def OAI.Percolation.encounterCount line 66
  7. theorem OAI.Percolation.markedCluster_aut line 69
  8. theorem OAI.Percolation.encounterCount_aut line 76
  9. theorem OAI.Percolation.measurable_markedCluster line 84
  10. theorem OAI.Percolation.measurable_encounterCount line 90
  11. theorem OAI.Percolation.cluster_induce_connected line 97
  12. theorem OAI.Percolation.markedCluster_eq_of_conn line 110
  13. theorem OAI.Percolation.sum_encounterCount_le line 115
  14. theorem OAI.Percolation.cluster_average_eq_sum line 152
  15. theorem OAI.Percolation.average_encounterCount_le line 173
  16. theorem OAI.Percolation.expected_encounterCount_le line 188