OAI/Probability/CriticalPercolation/Harmonic/LazyWalkProbability.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.lazyWalk_coordinate line 14
2. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.lazyWalk_nonnegative line 20
3. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.lazyWalk_mass line 27
4. def OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkState line 41
5. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkState_zero line 44
6. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkState_succ line 46
7. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkState_nonnegative line 49
8. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkState_mass line 54
9. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkState_one_pos line 60
10. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkState_support line 70
11. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkPower_symmetric line 90
12. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkState_double_at_one line 102
13. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkState_norm_sq line 111
14. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkState_norm_lower line 120