OAI/Probability/CriticalPercolation/Harmonic/ProjectedWalkFunctions.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.projectedFunction line 15
2. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.exists_large_generator_gradient line 18
3. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.projectedFunction_one line 27
4. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.projectedFunction_edge_bound line 30
5. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.projectedFunction_length_bound line 51
6. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.projectedFunction_generator_lower line 69
7. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.sum_walk_displacement line 82
8. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.projectedFunction_residual line 92
9. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.projectedFunction_residual_sq line 106