OAI/Geometry/PrescribedPotential/NonlinearSobolevGain.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Nonlinear Sobolev Gain.

  1. lemma OAI.GlobalElliptic.Localizers.realLower_lower line 26
  2. lemma OAI.GlobalElliptic.GluingData.real_sobolev_first_gain line 43
  3. lemma OAI.GlobalElliptic.GluingData.derivative_lifts_reindex line 61
  4. lemma OAI.GlobalElliptic.GluingData.derivative_lifts_gain line 79
  5. theorem OAI.GlobalElliptic.GluingData.nonlinear_sobolev_gain line 99