OAI/Geometry/PrescribedPotential/RealNonlinearCommutator.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Real Nonlinear Commutator.

  1. lemma OAI.GlobalElliptic.GluingData.realVolumeDerivative_val line 33
  2. lemma OAI.GlobalElliptic.GluingData.nonlinearRemainder_core_real line 45
  3. lemma OAI.GlobalElliptic.GluingData.nonlinearRemainder_real line 67
  4. def OAI.GlobalElliptic.GluingData.realNonlinearRemainder line 77
  5. lemma OAI.GlobalElliptic.GluingData.realNonlinearRemainder_continuous line 82
  6. lemma OAI.GlobalElliptic.GluingData.real_commutator_core line 86
  7. def OAI.GlobalElliptic.GluingData.realCompletedDerivative line 98
  8. lemma OAI.GlobalElliptic.GluingData.realCompletedDerivative_embed line 103