OAI/Analysis/NodalLength/RegularWeights.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpNodal.Profiles.regularWeight line 134
2. def OAI.SharpNodal.Profiles.regularGradientWeight line 135
3. lemma OAI.SharpNodal.Profiles.continuous_regularWeight line 137
4. lemma OAI.SharpNodal.Profiles.continuous_regularGradientWeight line 141
5. lemma OAI.SharpNodal.Profiles.regularWeight_nonneg line 145
6. lemma OAI.SharpNodal.Profiles.regularGradientWeight_nonneg line 149
7. lemma OAI.SharpNodal.Profiles.regularWeight_integral line 153
8. lemma OAI.SharpNodal.Profiles.regularWeight_integral_bound line 172
9. lemma OAI.SharpNodal.Profiles.regularGradientWeight_integral_bound line 183
10. lemma OAI.SharpNodal.Profiles.translated_kernel_integral_le line 201
11. lemma OAI.SharpNodal.Profiles.separated_disks line 219
12. lemma OAI.SharpNodal.Profiles.separated_centers_integral_bound line 228
13. lemma OAI.SharpNodal.Profiles.regularWeight_center_comparison line 262
14. lemma OAI.SharpNodal.Profiles.regularGradientWeight_center_comparison line 276
15. lemma OAI.SharpNodal.Profiles.separated_regularWeight_sum line 286
16. lemma OAI.SharpNodal.Profiles.separated_regularGradientWeight_sum line 305
17. lemma OAI.SharpNodal.Profiles.farWeight_le_regularWeight line 324
18. lemma OAI.SharpNodal.Profiles.farGradient_le_regularGradientWeight line 340
19. lemma OAI.SharpNodal.Profiles.separated_farWeight_sum line 353
20. lemma OAI.SharpNodal.Profiles.separated_farGradient_sum line 366
21. lemma OAI.SharpNodal.Profiles.separated_farWeight_integrals line 376
22. lemma OAI.SharpNodal.Profiles.separated_farGradient_integrals line 388
23. theorem OAI.SharpNodal.Profiles.affine_profile_grid line 402