OAI/Probability/CriticalPercolation/Harmonic/HarmonicFunctionSpace.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.HarmonicAnalysis.vanishingSubspace line 12
2. lemma OAI.CriticalPercolation.HarmonicAnalysis.vanishingSubspace_antitone line 18
3. theorem OAI.CriticalPercolation.HarmonicAnalysis.exists_detecting_ball line 23
4. def OAI.CriticalPercolation.HarmonicAnalysis.squareMass line 41
5. lemma OAI.CriticalPercolation.HarmonicAnalysis.squareMass_nonneg line 43
6. lemma OAI.CriticalPercolation.HarmonicAnalysis.squareMass_eq_zero_iff line 46
7. lemma OAI.CriticalPercolation.HarmonicAnalysis.squareMass_mono line 51
8. lemma OAI.CriticalPercolation.HarmonicAnalysis.squareMass_pos line 55