OAI/Geometry/Relativity/CKS/MixedMassUniform.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSMixedGeometry.massMetricRegion line 12
  2. def OAI.CKSMixedGeometry.massDenominator line 15
  3. def OAI.CKSMixedGeometry.massRegion line 18
  4. lemma OAI.CKSMixedGeometry.massMetricRegion_open line 20
  5. lemma OAI.CKSMixedGeometry.massDenominator_continuousOn line 25
  6. lemma OAI.CKSMixedGeometry.massRegion_open line 34
  7. lemma OAI.CKSMixedGeometry.massRegion_zero line 37
  8. lemma OAI.CKSMixedGeometry.massRegion_locallyLipschitz line 43
  9. lemma OAI.CKSMixedGeometry.mass_uniform_lipschitz line 50
  10. lemma OAI.CKSMixedGeometry.parameter_lipschitz_zero_estimate line 73
  11. theorem OAI.CKSMixedGeometry.cks_mass_uniform line 92