OAI/Probability/CriticalPercolation/Harmonic/HarmonicLinearQuotient.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.harmonic_constant_of_attained_max line 18
2. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.harmonic_constant_of_finite_range line 40
3. def OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.translateFunction line 47
4. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.translate_harmonic line 49
5. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.translate_polynomial_growth line 54
6. def OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.harmonicTranslation line 71
7. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.harmonicTranslation_apply line 82
8. def OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.harmonicRepresentation line 85
9. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.finite_range_of_finite_harmonic_image line 91
10. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.infinite_harmonic_linear_image line 100
11. theorem OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.exists_infinite_finiteDimensional_linear_image line 114