OAI/Analysis/Triangular/Construction/FarCurvature.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AtomicTriangular.Construction.transformedP line 13
2. lemma OAI.AtomicTriangular.Construction.hasDerivAt_spectralP_wave line 14
3. lemma OAI.AtomicTriangular.Construction.transformedP_contDiff line 18
4. lemma OAI.AtomicTriangular.Construction.transformedP_jet line 21
5. lemma OAI.AtomicTriangular.Construction.realP_contDiff line 28
6. lemma OAI.AtomicTriangular.Construction.realP_jet_zero line 29
7. lemma OAI.AtomicTriangular.Construction.rawConstantCurvature_antitone line 41
8. lemma OAI.AtomicTriangular.Construction.transformedP_curvature line 48
9. lemma OAI.AtomicTriangular.Construction.inputJJet_constant line 64
10. def OAI.AtomicTriangular.Construction.sideConstant line 72
11. def OAI.AtomicTriangular.Construction.actualJ0 line 73
12. lemma OAI.AtomicTriangular.Construction.actualJ0_contDiff line 77
13. lemma OAI.AtomicTriangular.Construction.actualJ_decompose line 82
14. lemma OAI.AtomicTriangular.Construction.actualJ0_curvature line 93