OAI/Geometry/SmoothYau/Smoothness/WaveJetMatrix.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.waveJetMatrix line 42
2. theorem OAI.YauCounterexamples.waveJetMatrix_det line 46
3. theorem OAI.YauCounterexamples.contDiff_matrixDet line 52
4. theorem OAI.YauCounterexamples.continuous_waveJetMatrix line 58
5. theorem OAI.YauCounterexamples.determinant_linear_lower_bound line 63
6. theorem OAI.YauCounterexamples.determinant_uniform_error_bound line 110