OAI/Analysis/NodalLength/Cutoffs.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpNodal.Carleman.smooth_cutoff_mul line 15
2. lemma OAI.SharpNodal.Carleman.exists_smooth_cutoff line 26
3. lemma OAI.SharpNodal.Carleman.partial_eventuallyEq line 42
4. lemma OAI.SharpNodal.Carleman.laplacian_eventuallyEq line 47
5. lemma OAI.SharpNodal.Carleman.gradient_eq_of_eventuallyEq line 54
6. lemma OAI.SharpNodal.Carleman.young_pairing line 59
7. lemma OAI.SharpNodal.Carleman.weighted_energy_component line 71
8. lemma OAI.SharpNodal.Carleman.weighted_energy_identity line 95
9. theorem OAI.SharpNodal.Carleman.caccioppoli line 107
10. theorem OAI.SharpNodal.Carleman.local_carleman_on line 139
11. lemma OAI.SharpNodal.Carleman.l2sq_cutoff_comparison line 208
12. theorem OAI.SharpNodal.Carleman.exponential_caccioppoli line 220
13. lemma OAI.SharpNodal.Carleman.partial2_mul line 269
14. lemma OAI.SharpNodal.Carleman.laplacian_mul line 280
15. lemma OAI.SharpNodal.Carleman.cutoff_residual line 287
16. lemma OAI.SharpNodal.Carleman.weighted_cutoff_residual line 298
17. lemma OAI.SharpNodal.Carleman.cutoff_prefactor_bound line 349
18. lemma OAI.SharpNodal.Carleman.cancel_carleman_frequency line 363