OAI/Analysis/NodalLength/Distributional.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SharpNodal.Profiles.uniform_secondTaylor_remainder line 64
2. def OAI.SharpNodal.Profiles.planeCircleAverage line 109
3. lemma OAI.SharpNodal.Profiles.planeCircleAverage_harmonic line 112
4. lemma OAI.SharpNodal.Profiles.planeCircleAverage_radiusSquare line 126
5. lemma OAI.SharpNodal.Profiles.planeCircleAverage_secondTaylor line 134
6. lemma OAI.SharpNodal.Profiles.planeCircleAverage_uniform_second_order line 182
7. lemma OAI.SharpNodal.Profiles.submean_dual_lintegral line 218
8. def OAI.SharpNodal.Profiles.circleVector line 257
9. lemma OAI.SharpNodal.Profiles.circleVector_continuous line 259
10. lemma OAI.SharpNodal.Profiles.circleVector_norm line 262
11. lemma OAI.SharpNodal.Profiles.planeCircleAverage_eq_integral line 266
12. instance OAI.SharpNodal.Profiles.circleParameter_isProbability line 275
13. lemma OAI.SharpNodal.Profiles.planeCircleAverage_continuous line 281
14. lemma OAI.SharpNodal.Profiles.planeCircleAverage_abs_le line 289
15. lemma OAI.SharpNodal.Profiles.integrable_mul_continuous_compact line 297
16. lemma OAI.SharpNodal.Profiles.integrable_mul_planeCircleAverage line 302
17. theorem OAI.SharpNodal.Profiles.distributional_laplacian_nonpos_of_dual line 318
18. lemma OAI.SharpNodal.Profiles.circleVector_neg line 361
19. lemma OAI.SharpNodal.Profiles.planeCircleAverage_eq_integral_sub line 364
20. lemma OAI.SharpNodal.Profiles.lintegral_mul_ofReal_toReal line 371
21. lemma OAI.SharpNodal.Profiles.submean_dual_real line 380
22. lemma OAI.SharpNodal.Profiles.usc_density_indicator_measurable line 413
23. theorem OAI.SharpNodal.Profiles.profile_distribution_D6 line 432