OAI/Analysis/NodalLength/Decomposition.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpNodal.Profiles.indicator_mul_laplacian line 110
2. lemma OAI.SharpNodal.Profiles.integrable_aeLogPotential_mul_compact line 120
3. lemma OAI.SharpNodal.Profiles.potential_difference_integrable line 131
4. lemma OAI.SharpNodal.Profiles.potential_difference_weakHarmonic line 136
5. lemma OAI.SharpNodal.Profiles.potential_difference_norm_bound line 149
6. lemma OAI.SharpNodal.Profiles.ae_potential_decomposition line 166
7. def OAI.SharpNodal.Profiles.normalizedRiesz line 190
8. lemma OAI.SharpNodal.Profiles.normalizedRiesz_finite line 193
9. lemma OAI.SharpNodal.Profiles.normalizedRiesz_support line 203
10. lemma OAI.SharpNodal.Profiles.normalizedRiesz_mass line 208
11. lemma OAI.SharpNodal.Profiles.normalizedRiesz_test line 217
12. theorem OAI.SharpNodal.Profiles.profile_ae_decomposition_uniform line 237
13. lemma OAI.SharpNodal.Profiles.profile_le_continuous_of_ae line 314
14. lemma OAI.SharpNodal.Profiles.profile_le_continuous_of_toReal_ae line 345
15. lemma OAI.SharpNodal.Profiles.plane_basis_expansion line 365
16. lemma OAI.SharpNodal.Profiles.plane_component_norm_le line 370
17. lemma OAI.SharpNodal.Profiles.plane_clm_norm_le_two line 373
18. lemma OAI.SharpNodal.Profiles.fderiv_norm_le_two line 388
19. lemma OAI.SharpNodal.Profiles.fderiv_sub_norm_le_two line 392
20. lemma OAI.SharpNodal.Profiles.affine_error_bound_ball line 397