OAI/Probability/CriticalPercolation/Harmonic/PolynomialHarmonicSpace.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.harmonicSpace line 14
2. def OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.HasPolynomialGrowth line 28
3. def OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.polynomialGrowthSpace line 31
4. def OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.polynomialHarmonicSpace line 51
5. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.mem_polynomialHarmonicSpace line 54
6. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.polynomial_growth_iff_length line 57
7. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.finite_family_growth_bound line 71