OAI/Geometry/PrescribedPotential/CoordinateEllipticity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Coordinate Ellipticity.

  1. lemma OAI.PotentialABP.matrix_quadratic_pos line 22
  2. lemma OAI.PotentialABP.compact_matrix_lower_bound line 33
  3. lemma OAI.Anticanonical.SourceSmooth.CoordinateBall.metric_continuousOn line 90
  4. lemma OAI.Anticanonical.SourceSmooth.CoordinateBall.metric_lower_bound line 111