OAI/Geometry/NodalSets/Waves/SmoothWaveOperator.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Yau.Jets.coordPartial_add line 10
2. lemma OAI.Yau.Jets.coordPartial_mul line 18
3. lemma OAI.Yau.Jets.coordPartial_const_mul line 27
4. lemma OAI.Yau.Jets.coordPartial_exp line 33
5. lemma OAI.Yau.Jets.coordPartial_twice_mul line 41
6. theorem OAI.Yau.Jets.smoothSecondOrder_mul line 54
7. def OAI.Yau.Jets.waveExp line 67
8. lemma OAI.Yau.Jets.waveExp_contDiff line 70
9. lemma OAI.Yau.Jets.coordPartial_waveExp line 73
10. lemma OAI.Yau.Jets.coordPartial_twice_waveExp line 79
11. theorem OAI.Yau.Jets.smoothSecondOrder_waveExp line 89
12. lemma OAI.Yau.Jets.symmetric_cross_sum line 102
13. theorem OAI.Yau.Jets.smooth_wave_residual_identity line 125