OAI/Geometry/PrescribedPotential/WeakNonlinearCommutator.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Weak Nonlinear Commutator.

  1. lemma OAI.GlobalElliptic.GluingData.realNonlinearRemainder_lower line 31
  2. def OAI.GlobalElliptic.GluingData.potentialDerivative line 71
  3. lemma OAI.GlobalElliptic.GluingData.potentialDerivative_embed line 78
  4. def OAI.GlobalElliptic.GluingData.densityDerivative line 84
  5. lemma OAI.GlobalElliptic.GluingData.densityDerivative_embed line 89
  6. theorem OAI.GlobalElliptic.GluingData.nonlinear_commutator_weak line 97