OAI/Probability/BenjaminiSchramm/IntrinsicBallGrowth.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Percolation.BenjaminiSchramm.intrinsicBall_small_witness line 15
  2. def OAI.Percolation.BenjaminiSchramm.intrinsicBallPolynomial line 27
  3. theorem OAI.Percolation.BenjaminiSchramm.intrinsicBallPolynomial_eq line 32
  4. theorem OAI.Percolation.BenjaminiSchramm.intrinsicBall_probability_transfer line 46
  5. def OAI.Percolation.BenjaminiSchramm.intrinsicBallMoment line 59
  6. theorem OAI.Percolation.BenjaminiSchramm.intrinsicBallMoment_le_susceptibility line 63
  7. theorem OAI.Percolation.BenjaminiSchramm.intrinsicBallMoment_transfer line 76
  8. theorem OAI.Percolation.BenjaminiSchramm.intrinsicBall_ncard_eq_sum line 86
  9. theorem OAI.Percolation.BenjaminiSchramm.measurableSet_mem_intrinsicBall_domain line 103
  10. theorem OAI.Percolation.BenjaminiSchramm.integral_intrinsicBall_ncard_eq line 118
  11. theorem OAI.Percolation.BenjaminiSchramm.integrable_intrinsicBall_ncard line 142
  12. theorem OAI.Percolation.BenjaminiSchramm.critical_intrinsicBallMoment_linear line 155