OAI/Geometry/SurfaceImmersion/Atlas/WeightedInverseJacobian.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Explicit polynomial bounds for the inverse Jacobian field in dimension two.

  1. def OAI.ClosedSurfaceR4.RealModes.inverseJacobianField line 15
  2. lemma OAI.ClosedSurfaceR4.RealModes.contDiffOn_coordDet line 18
  3. lemma OAI.ClosedSurfaceR4.RealModes.contDiffOn_inverseJacobianField line 24
  4. lemma OAI.ClosedSurfaceR4.RealModes.weighted_coordDet line 30
  5. def OAI.ClosedSurfaceR4.RealModes.inverseJacobianBudget line 59
  6. theorem OAI.ClosedSurfaceR4.RealModes.weighted_inverseJacobianField line 62
  7. lemma OAI.ClosedSurfaceR4.RealModes.inverseJacobianBudget_polynomial line 80