OAI/Geometry/NodalSets/Elliptic/IntrinsicRealCoordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Yau.Target.intrinsicRealPrincipal line 13
  2. def OAI.Yau.Target.intrinsicRealDrift line 16
  3. def OAI.Yau.Target.intrinsicRealPotential line 19
  4. lemma OAI.Yau.Target.intrinsicRealPrincipal_smooth line 22
  5. lemma OAI.Yau.Target.intrinsicRealPrincipal_symmetric line 31
  6. lemma OAI.Yau.Target.intrinsicRealPrincipal_posDef line 36
  7. lemma OAI.Yau.Target.intrinsicRealDrift_smooth line 41
  8. lemma OAI.Yau.Target.intrinsicRealPotential_smooth line 47
  9. lemma OAI.Yau.Target.real_seedCoordPartial_pullback line 52
  10. lemma OAI.Yau.Target.intrinsicRealFlux_pullback line 59
  11. theorem OAI.Yau.Target.intrinsicRealOperator_pullback line 70
  12. theorem OAI.Yau.Target.intrinsic_real_local_equation line 85