OAI/Probability/CriticalPercolation/Harmonic/HomogeneousPoincare.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.getVert_mem_ball line 20
2. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.walk_square_bound line 25
3. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.averaged_path_bound line 32
4. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.pair_sum_le_aut line 79
5. theorem OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.ball_poincare line 92