OAI/Probability/UnimodularPercolation/Encounter/Measurability.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Measurability of branches and finite clusters.

  1. theorem OAI.Percolation.card_image_eq_minima line 18
  2. theorem OAI.Percolation.measurable_branchCount line 41
  3. def OAI.Percolation.clusterFinset line 68
  4. theorem OAI.Percolation.clusterFinset_coe line 71
  5. theorem OAI.Percolation.measurable_clusterFinset line 75
  6. theorem OAI.Percolation.measurable_filter_finset line 98