OAI/Geometry/Relativity/CKS/BendingFirstJet.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSBending.bendingV_deriv line 11
2. lemma OAI.CKSBending.bendingV_reduced_deriv line 23
3. lemma OAI.CKSBending.base_tail line 31
4. lemma OAI.CKSBending.base_tail_le_one line 39
5. lemma OAI.CKSBending.v_le_sqrt line 50
6. lemma OAI.CKSBending.one_le_sqrt line 53
7. theorem OAI.CKSBending.bendingV_first_scaled line 57