OAI/Probability/CriticalPercolation/Harmonic/GraphWalkOperator.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.inverse_neighbor_sum line 18
  2. def OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.averaging line 28
  3. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.averaging_coordinate line 39
  4. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.averaging_delta line 42
  5. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.averaging_symmetric_delta line 51
  6. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.averaging_symmetric line 56
  7. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.sum_neighbor_sq_bound line 65
  8. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.averaging_norm_le line 80
  9. def OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.lazyWalk line 98
  10. def OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkEnergy line 99
  11. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.lazyWalk_apply line 100
  12. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.lazyWalk_coordinate line 102
  13. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.lazyWalk_symmetric line 105
  14. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.lazyWalk_norm_le line 109
  15. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.lazyWalk_positive line 115
  16. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkEnergy_nonneg line 121
  17. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walkEnergy_dissipation line 127