OAI/Probability/BenjaminiSchramm/DeletionLoss.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Percolation.BenjaminiSchramm.connection_measure_symm line 14
  2. def OAI.Percolation.BenjaminiSchramm.openTriangle line 20
  3. theorem OAI.Percolation.BenjaminiSchramm.lintegral_clusterMass_conn line 24
  4. theorem OAI.Percolation.BenjaminiSchramm.three_arm_first_moment_bound line 46
  5. def OAI.Percolation.BenjaminiSchramm.clusterDeletionLoss line 66
  6. theorem OAI.Percolation.BenjaminiSchramm.measurable_clusterDeletionLoss line 70
  7. theorem OAI.Percolation.BenjaminiSchramm.lintegral_clusterDeletionLoss line 76
  8. theorem OAI.Percolation.BenjaminiSchramm.clusterDeletionLoss_openTriangle_bound line 100