OAI/Probability/BenjaminiSchramm/TiltedGhost.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Percolation.BenjaminiSchramm.ghostKernel line 11
  2. lemma OAI.Percolation.BenjaminiSchramm.ghostKernel_nonneg line 13
  3. lemma OAI.Percolation.BenjaminiSchramm.ghostKernel_le_one line 18
  4. lemma OAI.Percolation.BenjaminiSchramm.ghostKernel_le_product line 21
  5. lemma OAI.Percolation.BenjaminiSchramm.ghostKernel_scaled_derivative_le line 26
  6. lemma OAI.Percolation.BenjaminiSchramm.hasDerivAt_ghostKernel line 37
  7. lemma OAI.Percolation.BenjaminiSchramm.ghostKernel_le_threeQuarter line 50
  8. lemma OAI.Percolation.BenjaminiSchramm.ghostKernel_quartic_moment line 58
  9. def OAI.Percolation.BenjaminiSchramm.ghostMagnetization line 69
  10. def OAI.Percolation.BenjaminiSchramm.ghostMagnetizationDerivative line 71
  11. lemma OAI.Percolation.BenjaminiSchramm.measurable_ghostKernel line 74
  12. lemma OAI.Percolation.BenjaminiSchramm.integrable_ghostKernel line 78
  13. theorem OAI.Percolation.BenjaminiSchramm.hasDerivAt_ghostMagnetization line 85
  14. lemma OAI.Percolation.BenjaminiSchramm.ghostMagnetization_nonneg line 109
  15. lemma OAI.Percolation.BenjaminiSchramm.ghostMagnetization_concave_bound line 113
  16. lemma OAI.Percolation.BenjaminiSchramm.ghostMagnetization_quartic_moment line 122
  17. theorem OAI.Percolation.BenjaminiSchramm.firstMoment_le_of_ghost_quartic_ratio line 132
  18. theorem OAI.Percolation.BenjaminiSchramm.firstMoment_lt_top_of_threeQuarter_and_differential line 175