OAI/Probability/CriticalPercolation/Growth/HomogeneousAverage.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.Stab line 18
2. def OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.frame line 20
3. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.frame_root line 21
4. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.frame_smul_root line 22
5. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.action_transitive line 23
6. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.suborbit_finite line 25
7. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.suborbit_card_pos line 35
8. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.stab_ball_preserved line 39
9. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.row_image line 45
10. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.average_row line 73
11. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.average_sum_bound line 87