OAI/Analysis/NodalLength/RieszMeasure.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpNodal.Profiles.smoothCompactTests line 80
2. lemma OAI.SharpNodal.Profiles.smoothCompactTests_dominate line 97
3. def OAI.SharpNodal.Profiles.compactTestsPositiveCone line 120
4. theorem OAI.SharpNodal.Profiles.positive_smooth_tests_representable line 126
5. def OAI.SharpNodal.Profiles.localizedLaplacianFunctional line 153
6. theorem OAI.SharpNodal.Profiles.localized_laplacian_measure line 173
7. lemma OAI.SharpNodal.Profiles.integral_mul_le_norm_bound line 215
8. theorem OAI.SharpNodal.Profiles.local_positive_measure_uniform line 225
9. theorem OAI.SharpNodal.Profiles.profile_riesz_uniform line 253