OAI/Geometry/PrescribedPotential/LinearizedCommutator.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Linearized Commutator.

  1. lemma OAI.GlobalElliptic.GluingData.realVolumeDerivative_eq_fderiv line 33
  2. lemma OAI.GlobalElliptic.GluingData.realVolumeDerivative_contDiff line 38
  3. def OAI.GlobalElliptic.GluingData.realVolumeSecond line 43
  4. def OAI.GlobalElliptic.GluingData.realRemainderDerivative line 51
  5. lemma OAI.GlobalElliptic.GluingData.realVolumeSecond_lower line 56
  6. lemma OAI.GlobalElliptic.GluingData.potentialDerivative_lower line 88
  7. lemma OAI.GlobalElliptic.GluingData.densityDerivative_lower line 106
  8. lemma OAI.GlobalElliptic.GluingData.nonlinear_commutator_linearization line 125
  9. lemma OAI.GlobalElliptic.GluingData.secondPotential_lower line 165
  10. lemma OAI.GlobalElliptic.GluingData.linearized_commutator_weak line 183