OAI/Geometry/CylinderCovering/Rational/CostDictionary.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalDictionary.labelDerivative line 9
  2. theorem OAI.RationalDictionary.labelDerivative_apply line 12
  3. theorem OAI.RationalDictionary.labelMap_eq_affine line 19
  4. theorem OAI.RationalDictionary.labelMap_hasFDerivAt line 26
  5. theorem OAI.RationalDictionary.labelDerivative_det line 32
  6. theorem OAI.RationalDictionary.labelMap_injective line 38
  7. theorem OAI.RationalDictionary.uncenteredDomain_measurable line 41
  8. theorem OAI.RationalDictionary.labelMap_image_domain line 46
  9. theorem OAI.RationalDictionary.cost_dictionary line 58
  10. theorem OAI.RationalDictionary.uncenteredWeight_eq_norm line 87