OAI/Geometry/PrescribedPotential/CoordinatePotential.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Coordinate Potential.

  1. lemma OAI.PotentialABP.hessian_coord_comp_at line 23
  2. lemma OAI.PotentialABP.levi_coord_pair_at line 36
  3. lemma OAI.PotentialABP.matrix_quadratic_le line 49
  4. lemma OAI.PotentialABP.matrix_quadratic_nonneg line 56
  5. def OAI.Anticanonical.SourceSmooth.CoordinateBall.bump line 70
  6. def OAI.Anticanonical.SourceSmooth.CoordinateBall.extension line 76
  7. lemma OAI.Anticanonical.SourceSmooth.CoordinateBall.extension_smooth line 79
  8. lemma OAI.Anticanonical.SourceSmooth.CoordinateBall.extension_eventuallyEq line 88
  9. lemma OAI.Anticanonical.SourceSmooth.CoordinateBall.extension_eq line 100
  10. lemma OAI.Anticanonical.SourceSmooth.CoordinateBall.metric_bound line 105
  11. lemma OAI.Anticanonical.SourceSmooth.CoordinateBall.extension_levi_lower line 131