OAI/Geometry/PrescribedPotential/GlobalSmooth.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Global Smooth.

  1. lemma OAI.SobolevChart.schwartzCoord_order_zero line 21
  2. lemma OAI.GlobalElliptic.Localizers.allRegular_distribution line 36
  3. def OAI.GlobalElliptic.Localizers.globalizeL2 line 47
  4. lemma OAI.GlobalElliptic.Localizers.globalizeL2_schwartz line 52
  5. lemma OAI.GlobalElliptic.GluingData.cutoff_forcing line 70
  6. lemma OAI.GlobalElliptic.GluingData.cutoff_distribution line 81
  7. lemma OAI.GlobalElliptic.GluingData.allRegular_coordinate line 97
  8. def OAI.GlobalElliptic.GluingData.reconstruct line 110
  9. lemma OAI.GlobalElliptic.GluingData.reconstruct_apply line 114
  10. lemma OAI.GlobalElliptic.GluingData.reconstruct_eq line 119
  11. theorem OAI.GlobalElliptic.GluingData.allRegular_smooth line 134
  12. theorem OAI.GlobalElliptic.GluingData.exists_smooth_shifted line 145