OAI/Probability/BenjaminiSchramm/RadiusTransfer.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Percolation.BenjaminiSchramm.extrinsicRadiusEvent_subset_intrinsic line 16
  2. theorem OAI.Percolation.BenjaminiSchramm.intrinsicRadiusEvent_subset_extrinsic_union line 25
  3. theorem OAI.Percolation.BenjaminiSchramm.intrinsic_radius_le_extrinsic_add line 40
  4. theorem OAI.Percolation.BenjaminiSchramm.exponential_quadratic_bound line 68
  5. theorem OAI.Percolation.BenjaminiSchramm.radius_transfer_error line 76
  6. theorem OAI.Percolation.BenjaminiSchramm.extrinsic_radius_lower_of_intrinsic line 119
  7. theorem OAI.Percolation.BenjaminiSchramm.critical_radius_powerTails_of_operator line 145
  8. theorem OAI.Percolation.BenjaminiSchramm.criticalRadiiInput_of_nonamenable line 168