OAI/Geometry/Relativity/CKS/CKSLeadingBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSMixedGeometry.leadingMassJet_continuousAt line 16
2. lemma OAI.CKSMixedGeometry.leading_mass_uniform_bounded line 27
3. lemma OAI.CKSMixedGeometry.cks_leading_mixed_bounded line 34
4. def OAI.CKSMixedGeometry.logQError line 56
5. lemma OAI.CKSMixedGeometry.logQError_diff line 59
6. lemma OAI.CKSMixedGeometry.logQError_three_bound line 63