OAI/Geometry/PrescribedPotential/SmoothChartInverse.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Smooth Chart Inverse.

  1. lemma OAI.SobolevChart.temperateDistribution_sum line 22
  2. lemma OAI.SobolevChart.temperateDistribution_mul line 30
  3. def OAI.MetricLocalization.classicalDifferential line 43
  4. lemma OAI.MetricLocalization.classicalDifferential_temperate line 48
  5. lemma OAI.MetricLocalization.classicalDifferential_distribution line 59
  6. theorem OAI.MetricLocalization.extended_smooth_solution line 90
  7. theorem OAI.MetricLocalization.germ_smooth_solution line 120