OAI/Geometry/Relativity/CKS/MixedInputBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSMixedGeometry.radiusPower_nat line 14
  2. lemma OAI.CKSMixedGeometry.normalize_two_bound line 17
  3. lemma OAI.CKSMixedGeometry.normalize_three_bound line 27
  4. lemma OAI.CKSMixedGeometry.normalize_matrix_three line 37
  5. lemma OAI.CKSMixedGeometry.normalize_matrix_two line 47
  6. def OAI.CKSMixedGeometry.radialMatrixD line 57
  7. lemma OAI.CKSMixedGeometry.radialMatrixD_regular line 59
  8. lemma OAI.CKSMixedGeometry.radialMatrixD_bound line 67
  9. def OAI.CKSMixedGeometry.normalizeMassLogFields line 78
  10. lemma OAI.CKSMixedGeometry.normalizeMassLogFields_regular line 89
  11. lemma OAI.CKSMixedGeometry.massInputOf_norm line 96
  12. theorem OAI.CKSMixedGeometry.normalized_log_mass_input_bound line 119