OAI/Analysis/NodalLength/AffineError.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpNodal.Profiles.fderiv_log_norm_apply line 120
2. lemma OAI.SharpNodal.Profiles.fderiv_smoothLog_unit line 134
3. lemma OAI.SharpNodal.Profiles.smoothLog_hessian_bounded line 144
4. lemma OAI.SharpNodal.Profiles.normalized_log_affine_error line 157
5. lemma OAI.SharpNodal.Profiles.log_far_affine_error line 178
6. lemma OAI.SharpNodal.Profiles.volume_unit_disk_real line 218
7. lemma OAI.SharpNodal.Profiles.log_scaled_kernel_ae line 221
8. lemma OAI.SharpNodal.Profiles.log_scaled_kernel_integrable line 229
9. def OAI.SharpNodal.Profiles.logDiskAverage line 237
10. lemma OAI.SharpNodal.Profiles.logDiskAverage_scale line 240
11. lemma OAI.SharpNodal.Profiles.log_near_average_lower line 252
12. lemma OAI.SharpNodal.Profiles.log_near_outer_upper line 271
13. lemma OAI.SharpNodal.Profiles.integral_linear_unitDisk line 281
14. lemma OAI.SharpNodal.Profiles.log_far_diskAverage_error line 305
15. lemma OAI.SharpNodal.Profiles.logarithmic_kernel_comparison line 341
16. instance OAI.SharpNodal.Profiles.unitDisk_volume_finite line 377
17. lemma OAI.SharpNodal.Profiles.scaled_log_kernel_norm_bound line 380
18. lemma OAI.SharpNodal.Profiles.scaled_logPotential_prod_integrable line 398
19. lemma OAI.SharpNodal.Profiles.scaled_aeLogPotential_integrableOn line 418
20. lemma OAI.SharpNodal.Profiles.logDiskAverage_integrable line 423
21. lemma OAI.SharpNodal.Profiles.integral_logDiskAverage line 428
22. lemma OAI.SharpNodal.Profiles.ae_source_ne line 438
23. def OAI.SharpNodal.Profiles.farGradient line 450
24. def OAI.SharpNodal.Profiles.farWeight line 453
25. lemma OAI.SharpNodal.Profiles.measurable_farGradient line 456
26. lemma OAI.SharpNodal.Profiles.measurable_farWeight line 460
27. lemma OAI.SharpNodal.Profiles.farGradient_inner line 464
28. lemma OAI.SharpNodal.Profiles.farGradient_norm_bound line 471
29. lemma OAI.SharpNodal.Profiles.farWeight_bounds line 484
30. lemma OAI.SharpNodal.Profiles.integrable_farGradient line 495
31. lemma OAI.SharpNodal.Profiles.integrable_farWeight line 500
32. lemma OAI.SharpNodal.Profiles.integral_inner_left line 507
33. lemma OAI.SharpNodal.Profiles.ae_potential_affine_comparison line 513
34. def OAI.SharpNodal.Profiles.diskAverage line 545
35. lemma OAI.SharpNodal.Profiles.scaled_continuous_integrable line 548
36. lemma OAI.SharpNodal.Profiles.diskAverage_linear line 553
37. lemma OAI.SharpNodal.Profiles.diskAverage_const line 560
38. lemma OAI.SharpNodal.Profiles.diskAverage_affine_error line 567
39. lemma OAI.SharpNodal.Profiles.harmonic_outer_minus_average line 601
40. lemma OAI.SharpNodal.Profiles.quasiMeasurePreserving_affine line 611
41. lemma OAI.SharpNodal.Profiles.diskAverage_le_profileSup line 615
42. lemma OAI.SharpNodal.Profiles.profile_finite_ae_D3 line 651
43. theorem OAI.SharpNodal.Profiles.potential_profile_affine_sup_bound line 667