OAI/Probability/BenjaminiSchramm/EventMeasurability.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Percolation.BenjaminiSchramm.volumeEvent_eq_clusterLarge line 14
  2. theorem OAI.Percolation.BenjaminiSchramm.measurableSet_volumeEvent line 35
  3. theorem OAI.Percolation.BenjaminiSchramm.measurableSet_extrinsicRadiusEvent line 40
  4. theorem OAI.Percolation.BenjaminiSchramm.along_exists_walk_length_le line 46
  5. theorem OAI.Percolation.BenjaminiSchramm.intrinsicBall_iff_distance_le line 60
  6. theorem OAI.Percolation.BenjaminiSchramm.measurableSet_mem_intrinsicBall line 75
  7. theorem OAI.Percolation.BenjaminiSchramm.intrinsicRadiusEvent_eq line 86
  8. theorem OAI.Percolation.BenjaminiSchramm.measurableSet_intrinsicRadiusEvent line 100