OAI/Geometry/PrescribedPotential/LocalizedDerivations.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Localized Derivations.

  1. def OAI.GlobalElliptic.ChartCutoff.realPart line 22
  2. lemma OAI.GlobalElliptic.ChartCutoff.realPart_apply line 36
  3. lemma OAI.GlobalElliptic.ChartCutoff.realPart_support line 38
  4. def OAI.GlobalElliptic.GluingData.localizedDerivative line 50
  5. lemma OAI.GlobalElliptic.GluingData.localizedDerivative_bound line 56
  6. lemma OAI.GlobalElliptic.GluingData.localizedDerivative_apply line 75
  7. lemma OAI.GlobalElliptic.GluingData.localizedDerivative_mul line 99
  8. lemma OAI.GlobalElliptic.GluingData.localizedDerivative_const line 125
  9. def OAI.GlobalElliptic.GluingData.completedDerivative line 135
  10. lemma OAI.GlobalElliptic.GluingData.completedDerivative_embed line 139