OAI/Geometry/Immersion/ClosedSurface/JetBounds.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ClosedSurfaceR4.SmallModes.TwoJet line 15
2. def OAI.ClosedSurfaceR4.SmallModes.twoJet line 17
3. lemma OAI.ClosedSurfaceR4.SmallModes.LowJet.contDiffAt_dot line 24
4. lemma OAI.ClosedSurfaceR4.SmallModes.LowJet.contDiffAt_cdiv line 30
5. lemma OAI.ClosedSurfaceR4.SmallModes.LowJet.contDiffAt_gramDet line 36
6. lemma OAI.ClosedSurfaceR4.SmallModes.LowJet.contDiffAt_liftX line 41
7. lemma OAI.ClosedSurfaceR4.SmallModes.LowJet.contDiffAt_liftY line 49
8. lemma OAI.ClosedSurfaceR4.SmallModes.LowJet.contDiffAt_tangentLift line 57
9. lemma OAI.ClosedSurfaceR4.SmallModes.LowJet.contDiffAt_normalPart line 64
10. structure OAI.ClosedSurfaceR4.SmallModes.LowJet.Domain line 72
11. def OAI.ClosedSurfaceR4.SmallModes.LowJet.scalarCoefficients line 78
12. def OAI.ClosedSurfaceR4.SmallModes.LowJet.vectorCoefficients line 88
13. abbrev OAI.ClosedSurfaceR4.SmallModes.LowJet.CoeffIndex line 95
14. def OAI.ClosedSurfaceR4.SmallModes.LowJet.coefficients line 97
15. lemma OAI.ClosedSurfaceR4.SmallModes.LowJet.contDiffAt_scalarCoefficients line 101
16. lemma OAI.ClosedSurfaceR4.SmallModes.LowJet.contDiffAt_vectorCoefficients line 125
17. lemma OAI.ClosedSurfaceR4.SmallModes.LowJet.Domain.smoothCoefficients line 142
18. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffOn_twoJet line 156
19. lemma OAI.ClosedSurfaceR4.SmallModes.modeDomain_of_twoJet line 170
20. theorem OAI.ClosedSurfaceR4.SmallModes.compact_reconstructionCoefficientBound line 183