OAI/Geometry/NodalSets/Elliptic/RealConvexifiedQuadraticLemmas.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Yau.Geometry.real_flux_rank_one line 12
  2. theorem OAI.Yau.Geometry.real_convexified_quadratic line 35
  3. def OAI.Yau.Geometry.realCoordinateSquare line 53
  4. lemma OAI.Yau.Geometry.realCoordinateSquare_smooth line 55
  5. lemma OAI.Yau.Geometry.realCoordinateSquare_zero line 59
  6. lemma OAI.Yau.Geometry.realCoordinateSquare_nonneg line 62
  7. lemma OAI.Yau.Geometry.realCoordinateSquare_norm line 65
  8. lemma OAI.Yau.Geometry.realCoordinateSquare_partial_center line 68
  9. def OAI.Yau.Geometry.realIndentedPhase line 80
  10. lemma OAI.Yau.Geometry.realIndentedPhase_smooth line 83
  11. lemma OAI.Yau.Geometry.realIndentedPhase_center line 87
  12. lemma OAI.Yau.Geometry.realIndentedPhase_gradient_center line 90
  13. lemma OAI.Yau.Geometry.realIndentedPhase_annulus line 101
  14. lemma OAI.Yau.Geometry.realConvexifiedPhase_negative_bound line 110