OAI/Analysis/NodalLength/Integration.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SharpNodal.Carleman.Smooth line 15
2. lemma OAI.SharpNodal.Carleman.smooth_partial line 17
3. lemma OAI.SharpNodal.Carleman.compact_partial line 21
4. lemma OAI.SharpNodal.Carleman.partial_mul line 25
5. lemma OAI.SharpNodal.Carleman.integrable_mul_compact_right line 35
6. lemma OAI.SharpNodal.Carleman.integral_mul_partial line 39
7. lemma OAI.SharpNodal.Carleman.partial_partial line 51
8. lemma OAI.SharpNodal.Carleman.partial_add line 67
9. lemma OAI.SharpNodal.Carleman.partial_const_mul line 76
10. lemma OAI.SharpNodal.Carleman.integral_coeff_mul_partial_square line 83
11. lemma OAI.SharpNodal.Carleman.integrable_mul_compact_left line 98
12. lemma OAI.SharpNodal.Carleman.integral_partial_mul line 102
13. lemma OAI.SharpNodal.Carleman.integral_partial_mul_mul line 107
14. lemma OAI.SharpNodal.Carleman.laplacian_transport_pair line 133
15. lemma OAI.SharpNodal.Carleman.multiplication_transport_pair line 157
16. def OAI.SharpNodal.Carleman.euclideanLaplacian line 180
17. def OAI.SharpNodal.Carleman.skewPart line 183
18. lemma OAI.SharpNodal.Carleman.smooth_laplacian line 187
19. lemma OAI.SharpNodal.Carleman.compact_laplacian line 191
20. lemma OAI.SharpNodal.Carleman.smooth_skew line 197
21. lemma OAI.SharpNodal.Carleman.compact_skew line 204
22. lemma OAI.SharpNodal.Carleman.integral_sum_mul line 211
23. lemma OAI.SharpNodal.Carleman.integral_mul_sum line 217
24. lemma OAI.SharpNodal.Carleman.integral_skew_component line 224
25. lemma OAI.SharpNodal.Carleman.integral_skew line 249
26. lemma OAI.SharpNodal.Carleman.laplacian_transport line 264
27. lemma OAI.SharpNodal.Carleman.multiplication_transport line 294
28. lemma OAI.SharpNodal.Carleman.transport_commutator line 304