OAI/Probability/CriticalPercolation/Growth/WordLengthGeometry.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry line 14
2. abbrev OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.ball line 22
3. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.exists_mem_ball line 24
4. def OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.length line 27
5. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.mem_ball_length line 29
6. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.length_le_iff line 31
7. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.ball_mono line 37
8. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.length_mul_le line 41
9. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.length_inv line 46
10. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.length_one line 53
11. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.length_generator line 56
12. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.length_mul_generator line 59
13. def OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.cutoff line 67
14. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.cutoff_nonneg line 69
15. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.cutoff_large line 71
16. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.cutoff_eq_zero line 75
17. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.cutoff_ne_zero_length line 79
18. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.cutoff_lipschitz_generator line 84