OAI/Geometry/PrescribedPotential/SobolevFirstGain.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Sobolev First Gain.

  1. lemma OAI.GlobalElliptic.GluingData.completedLocalize_plus_one_embed line 23
  2. lemma OAI.GlobalElliptic.GluingData.completedLocalize_lower_one line 31
  3. lemma OAI.GlobalElliptic.GluingData.local_mem_of_derivative_lifts line 47
  4. theorem OAI.GlobalElliptic.GluingData.sobolev_first_gain line 65