OAI/Geometry/PrescribedPotential/CommutatorSupport.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Commutator Support.

  1. lemma OAI.GlobalElliptic.hessianLocalizedError_zero line 24
  2. lemma OAI.GlobalElliptic.source_hessian_zero_of_local line 43
  3. def OAI.GlobalElliptic.GluingData.derivativeSupport line 62
  4. lemma OAI.GlobalElliptic.GluingData.localizedDerivative_tsupport line 65
  5. lemma OAI.GlobalElliptic.GluingData.derivativeSupport_source line 71
  6. lemma OAI.GlobalElliptic.GluingData.outsideDerivativeSupport_coord line 80
  7. lemma OAI.GlobalElliptic.GluingData.localizedDerivative_zero line 86
  8. lemma OAI.GlobalElliptic.GluingData.regularityError_zero line 90
  9. lemma OAI.GlobalElliptic.GluingData.nonlinearRemainder_zero line 103
  10. lemma OAI.GlobalElliptic.GluingData.localizedDerivative_source_hessian_zero line 123