OAI/Probability/CriticalPercolation/Harmonic/CoverPoincare.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.squareMass_around line 18
2. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.energy_around line 25
3. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.sum_around line 34
4. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.translated_poincare line 41
5. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.cover_mass_energy line 69
6. theorem OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.harmonic_cover_kernel_bound line 99