OAI/Geometry/Relativity/CKS/ScalarJetCalculus.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSAngularGeometry.constantJet line 11
2. def OAI.CKSAngularGeometry.productJet line 13
3. def OAI.CKSAngularGeometry.sqrtJet line 17
4. lemma OAI.CKSAngularGeometry.actualScalarJet_const line 21
5. lemma OAI.CKSAngularGeometry.actualScalarJet_add line 28
6. lemma OAI.CKSAngularGeometry.actualScalarJet_smul line 46
7. lemma OAI.CKSAngularGeometry.actualScalarJet_sub line 62
8. lemma OAI.CKSAngularGeometry.actualScalarJet_mul line 70
9. lemma OAI.CKSAngularGeometry.actualScalarJet_sqrt line 81
10. lemma OAI.CKSAngularGeometry.productJet_smooth line 94
11. lemma OAI.CKSAngularGeometry.reciprocalJet_smooth line 98
12. lemma OAI.CKSAngularGeometry.sqrtJet_smooth line 115