OAI/Geometry/PrescribedPotential/RegularityCutoffs.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Regularity Cutoffs.

  1. lemma OAI.GlobalElliptic.exists_chartCutoff_nhds line 21
  2. lemma OAI.GlobalElliptic.GluingData.exists_regularityCutoff line 48
  3. def OAI.GlobalElliptic.GluingData.regularityCutoff line 56
  4. lemma OAI.GlobalElliptic.GluingData.regularityCutoff_real line 59
  5. lemma OAI.GlobalElliptic.GluingData.regularityCutoff_one line 62
  6. lemma OAI.GlobalElliptic.GluingData.exists_regularityOuter line 67
  7. def OAI.GlobalElliptic.GluingData.regularityOuter line 75
  8. lemma OAI.GlobalElliptic.GluingData.regularityOuter_one line 78
  9. lemma OAI.GlobalElliptic.GluingData.localizedDerivative_real line 85
  10. def OAI.GlobalElliptic.GluingData.realLocalizedDerivative line 107
  11. lemma OAI.GlobalElliptic.GluingData.completedDerivative_real line 111