OAI/Analysis/NodalLength/Isothermal.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpNodal.Geometry.IsConformal line 325
  2. theorem OAI.SharpNodal.Geometry.exists_isothermal_chart line 329
  3. def OAI.SharpNodal.Geometry.chartScalarLaplace line 403
  4. lemma OAI.SharpNodal.Geometry.laplaceBeltrami_eq_chartScalar line 409
  5. lemma OAI.SharpNodal.Geometry.chartScalarLaplace_covariant line 440
  6. lemma OAI.SharpNodal.Geometry.laplaceBeltrami_in_chart line 489
  7. def OAI.SharpNodal.Geometry.conformalFactor line 507
  8. lemma OAI.SharpNodal.Geometry.IsConformal.factor line 512
  9. lemma OAI.SharpNodal.Geometry.IsConformal.factor_smooth line 520
  10. lemma OAI.SharpNodal.Geometry.IsConformal.laplace line 523
  11. lemma OAI.SharpNodal.Geometry.IsConformal.eigenfunction line 557