OAI/Analysis/NodalLength/Subharmonic.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpNodal.Profiles.full_test_local line 38
2. lemma OAI.SharpNodal.Profiles.laplacian_add_local line 52
3. lemma OAI.SharpNodal.Profiles.laplacian_radiusSquare line 62
4. lemma OAI.SharpNodal.Profiles.laplacian_quadraticBarrier line 74
5. theorem OAI.SharpNodal.Profiles.harmonic_comparison_of_full_test line 84
6. theorem OAI.SharpNodal.Profiles.extract_normalized_parameters line 162
7. lemma OAI.SharpNodal.Profiles.WeightedProfileBounds.subseq line 205
8. theorem OAI.SharpNodal.Profiles.full_test_of_profile line 215
9. theorem OAI.SharpNodal.Profiles.harmonic_comparison_of_profile line 240
10. def OAI.SharpNodal.Profiles.planeComplex line 271
11. lemma OAI.SharpNodal.Profiles.plane_laplacian_eq_mathlib line 273
12. lemma OAI.SharpNodal.Profiles.laplacian_comp_isometry line 283
13. lemma OAI.SharpNodal.Profiles.plane_laplacian_comp_complex line 304
14. lemma OAI.SharpNodal.Profiles.compare_complex_harmonic line 311
15. lemma OAI.SharpNodal.Profiles.harmonic_extension_fourier_span line 330
16. lemma OAI.SharpNodal.Profiles.exists_circle_param line 376
17. lemma OAI.SharpNodal.Profiles.approximate_circle_by_harmonic line 390
18. theorem OAI.SharpNodal.Profiles.submean_continuous_majorant line 411