OAI/Probability/CriticalPercolation/Growth/HomogeneousGeometry.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CriticalPercolation.HomogeneousAnalysis.Geometry line 12
  2. abbrev OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.Aut line 21
  3. def OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.around line 23
  4. abbrev OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.ball line 24
  5. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.mem_around line 26
  6. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.around_mono line 29
  7. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.ball_mono line 32
  8. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.self_mem_around line 34
  9. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.mem_around_symm line 36
  10. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.mem_around_add line 38
  11. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.around_subset_ball line 41
  12. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.ball_card_pos line 43
  13. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.aut_around_image line 46
  14. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.card_around line 58
  15. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.exists_mem_ball line 63
  16. def OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.length line 67
  17. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.mem_ball_length line 68
  18. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.length_le_iff line 71
  19. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.length_root line 77
  20. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.length_adj line 78
  21. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.aut_length_le line 86
  22. def OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.neighbors line 92
  23. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.mem_neighbors line 93
  24. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.neighbors_image line 94
  25. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.neighbors_card line 100
  26. abbrev OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.degree line 104
  27. def OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.energy line 106
  28. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.energy_nonneg line 107
  29. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.energy_mono line 109
  30. def OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.IsHarmonic line 113
  31. def OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.cutoff line 115
  32. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.cutoff_nonneg line 116
  33. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.cutoff_large line 117
  34. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.cutoff_eq_zero line 120
  35. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.cutoff_ne_zero_length line 123
  36. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.cutoff_lipschitz line 125