OAI/Geometry/Relativity/CKS/CollarAngularMetric.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSAngularGeometry.actualJet_add line 11
2. lemma OAI.CKSAngularGeometry.actualJet_smul line 33
3. def OAI.CKSAngularGeometry.interpolate line 55
4. lemma OAI.CKSAngularGeometry.actualJet_interpolate line 57
5. lemma OAI.CKSAngularGeometry.interpolation_weight line 64
6. lemma OAI.CKSAngularGeometry.interpolation_reference line 74
7. def OAI.CKSAngularGeometry.cksLeaf line 80
8. lemma OAI.CKSAngularGeometry.normalized_cksLeaf line 83
9. lemma OAI.CKSAngularGeometry.cks_normalized_jet_bound line 90