OAI/Geometry/Relativity/CKS/BoostIntegral.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSLorentz.pullbackRate line 12
2. lemma OAI.CKSLorentz.normalizedDomain_open line 15
3. lemma OAI.CKSLorentz.pullbackRate_smooth line 18
4. lemma OAI.CKSLorentz.pullback_time_derivative line 22
5. lemma OAI.CKSLorentz.pullbackRate_transport line 31
6. lemma OAI.CKSLorentz.continuous_restrict_sphere line 38
7. lemma OAI.CKSLorentz.sphere_integrable_smooth line 50
8. lemma OAI.CKSLorentz.boostField_smooth line 54
9. lemma OAI.CKSLorentz.pullbackRate_integral_zero line 57
10. lemma OAI.CKSLorentz.normalizedIntegral_derivative_zero line 75
11. theorem OAI.CKSLorentz.flow_area_substitution line 108