OAI/Probability/CriticalPercolation/Harmonic/CayleyCaccioppoli.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.HarmonicAnalysis.sum_subtype_pair line 18
2. lemma OAI.CriticalPercolation.HarmonicAnalysis.sum_neighbor_rows line 23
3. lemma OAI.CriticalPercolation.HarmonicAnalysis.sum_neighbor_rows_le line 38
4. def OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.IsHarmonic line 53
5. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.inv_mem_generators_iff line 55
6. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.neighbor_symm line 64
7. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.cutoff_neighbor_mem_ball line 68
8. theorem OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.caccioppoli line 75