OAI/Analysis/NodalLength/Commutator.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpNodal.Carleman.partial_finset_sum line 15
2. def OAI.SharpNodal.Carleman.gradientSquared line 22
3. lemma OAI.SharpNodal.Carleman.smooth_gradientSquared line 25
4. lemma OAI.SharpNodal.Carleman.partial_gradientSquared line 29
5. lemma OAI.SharpNodal.Carleman.potential_transport_component line 40
6. theorem OAI.SharpNodal.Carleman.carleman_commutator line 84
7. lemma OAI.SharpNodal.Carleman.partial_exp line 104
8. lemma OAI.SharpNodal.Carleman.partial_exp_mul line 110
9. lemma OAI.SharpNodal.Carleman.partial2_exp_mul line 117
10. lemma OAI.SharpNodal.Carleman.conjugation_component line 131
11. lemma OAI.SharpNodal.Carleman.conjugation line 141
12. lemma OAI.SharpNodal.Carleman.integral_laplacian_mul line 153
13. def OAI.SharpNodal.Carleman.l2sq line 163
14. lemma OAI.SharpNodal.Carleman.l2sq_nonneg line 165
15. lemma OAI.SharpNodal.Carleman.l2sq_add line 168
16. lemma OAI.SharpNodal.Carleman.pairing_le_l2sq_add line 184
17. lemma OAI.SharpNodal.Carleman.l2sq_const_mul line 190
18. lemma OAI.SharpNodal.Carleman.pairing_sq_le line 198
19. lemma OAI.SharpNodal.Carleman.plane_trace_identity line 211
20. lemma OAI.SharpNodal.Carleman.plane_trace_sum line 219
21. lemma OAI.SharpNodal.Carleman.l2sq_linearCombination_le line 225
22. lemma OAI.SharpNodal.Carleman.integral_quadratic line 245
23. lemma OAI.SharpNodal.Carleman.l2sq_linearCombination line 256
24. lemma OAI.SharpNodal.Carleman.pairing_linearCombination line 267
25. def OAI.SharpNodal.Carleman.quadraticEnergy line 279
26. lemma OAI.SharpNodal.Carleman.plane_trace_energy_identity line 282
27. lemma OAI.SharpNodal.Carleman.pairing_tendsto_zero_of_bound line 294
28. lemma OAI.SharpNodal.Carleman.plane_trace_energy_limit line 312