OAI/Probability/CriticalPercolation/Harmonic/GraphWalkProbability.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.degree_pos line 18
  2. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.averaging_mass line 25
  3. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.lazyWalk_nonnegative line 33
  4. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.lazyWalk_mass line 38
  5. def OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkFeature line 42
  6. abbrev OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkState line 43
  7. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkFeature_zero line 44
  8. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkFeature_succ line 45
  9. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkState_succ line 47
  10. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkState_nonnegative line 48
  11. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkState_mass line 52
  12. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkState_root_pos line 56
  13. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkState_support line 64
  14. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkPower_symmetric line 80
  15. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkState_double_at_root line 90
  16. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkState_norm_sq line 99
  17. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkState_norm_lower line 102
  18. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.transport_averaging line 110
  19. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.transport_lazyWalk line 118
  20. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.transport_walkFeature line 121
  21. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkFeature_norm line 126
  22. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkFeature_average line 129