OAI/Probability/CriticalPercolation/Harmonic/GraphWalkEnergy.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.exists_ball_boundary line 19
  2. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkFeature_symmetric line 38
  3. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkEnergy_gradient line 43
  4. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.feature_neighbor_bound line 55
  5. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.feature_edge_bound line 63
  6. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.feature_walk_bound line 72
  7. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.feature_ball_bound line 84
  8. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.supported_energy_bound line 89
  9. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkState_energy_pos line 103
  10. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkState_energy_lower line 111
  11. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkState_energy_antitone line 121
  12. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walk_energy_inverse_sparse line 128
  13. theorem OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.exists_walk_small_relative_residual line 159