OAI/Geometry/PrescribedPotential/NonlinearRemainder.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Nonlinear Remainder.

  1. def OAI.GlobalElliptic.GluingData.regularityMetric line 27
  2. def OAI.GlobalElliptic.GluingData.regularityInverseDet line 32
  3. def OAI.GlobalElliptic.GluingData.regularityMatrix line 37
  4. def OAI.GlobalElliptic.GluingData.regularityErrorMatrix line 42
  5. def OAI.GlobalElliptic.GluingData.nonlinearRemainder line 48
  6. lemma OAI.GlobalElliptic.GluingData.regularityMatrix_contDiff line 56
  7. lemma OAI.GlobalElliptic.GluingData.regularityErrorMatrix_contDiff line 63
  8. lemma OAI.GlobalElliptic.GluingData.nonlinearRemainder_contDiff line 71