OAI/Probability/CriticalPercolation/Harmonic/WalkEnergyLower.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.exists_word_ball_boundary line 15
2. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.regular_word_displacement line 37
3. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.regular_energy_displacement line 58
4. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.supported_energy_bound line 70
5. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkState_energy_pos line 93
6. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.walkState_energy_lower line 102