OAI/Geometry/Relativity/CKS/LogRadiusJets.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSMixedGeometry.radiusPower line 12
2. lemma OAI.CKSMixedGeometry.radiusPower_pos line 15
3. lemma OAI.CKSMixedGeometry.radiusPower_smooth line 16
4. lemma OAI.CKSMixedGeometry.radiusPower_diff line 17
5. lemma OAI.CKSMixedGeometry.basis_rad_abs line 19
6. lemma OAI.CKSMixedGeometry.D_radiusPower line 22
7. lemma OAI.CKSMixedGeometry.actual_radiusPower line 34
8. lemma OAI.CKSMixedGeometry.radiusPower_two_norm line 47
9. lemma OAI.CKSMixedGeometry.radiusPower_three_norm line 79
10. lemma OAI.CKSMixedGeometry.inverse_radius_three_norm line 101