OAI/Probability/CriticalPercolation/Harmonic/LazyWalkHilbert.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CriticalPercolation.HarmonicAnalysis.RegularHilbert line 13
2. lemma OAI.CriticalPercolation.HarmonicAnalysis.translate_mem line 15
3. def OAI.CriticalPercolation.HarmonicAnalysis.translateVector line 22
4. def OAI.CriticalPercolation.HarmonicAnalysis.regularLinearEquiv line 25
5. def OAI.CriticalPercolation.HarmonicAnalysis.regular line 41
6. lemma OAI.CriticalPercolation.HarmonicAnalysis.regular_apply line 47
7. lemma OAI.CriticalPercolation.HarmonicAnalysis.regular_one line 49
8. lemma OAI.CriticalPercolation.HarmonicAnalysis.regular_mul line 50
9. lemma OAI.CriticalPercolation.HarmonicAnalysis.regular_inner line 53
10. def OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkAverage line 60
11. def OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.lazyWalk line 63
12. def OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkEnergy line 66
13. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.generators_card_pos line 68
14. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkAverage_apply line 71
15. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.lazyWalk_apply line 75
16. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkAverage_norm_le line 78
17. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkAverage_symmetric line 86
18. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.lazyWalk_symmetric line 102
19. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.lazyWalk_norm_le line 107
20. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.lazyWalk_positive line 114
21. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkEnergy_nonneg line 122
22. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkEnergy_dissipation line 129
23. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkEnergy_gradient line 140