OAI/Analysis/NodalLength/FrequencyGap.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpNodal.Profiles.poissonKernel_bounds line 350
2. lemma OAI.SharpNodal.Profiles.harmonic_harnack line 365
3. lemma OAI.SharpNodal.Profiles.plane_harmonic_harnack line 410
4. lemma OAI.SharpNodal.Profiles.laplacian_sub line 436
5. lemma OAI.SharpNodal.Profiles.additive_harnack_unit line 442
6. lemma OAI.SharpNodal.Geometry.no_low_energy_sequence line 521
7. lemma OAI.SharpNodal.Geometry.exists_additive_harnack line 582
8. lemma OAI.SharpNodal.Geometry.normalized_frequency_gap line 635