OAI/Geometry/PrescribedPotential/PatchDifferential.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Patch Differential.

  1. lemma OAI.SobolevChart.schwartz_temperate_product_distribution line 24
  2. lemma OAI.SobolevChart.schwartz_second_deriv line 36
  3. def OAI.MetricLocalization.schwartzDifferential line 48
  4. lemma OAI.MetricLocalization.schwartzDifferential_apply line 54
  5. lemma OAI.MetricLocalization.schwartzDifferential_distribution line 65
  6. lemma OAI.MetricLocalization.schwartzDifferential_tsupport line 79
  7. def OAI.MetricLocalization.schwartzCutoffError line 99
  8. lemma OAI.MetricLocalization.schwartzCutoffError_distribution line 104
  9. lemma OAI.MetricLocalization.schwartzCutoffError_tsupport line 115
  10. abbrev OAI.Anticanonical.SourceSmooth.ParametrixPatch.coefficients line 133
  11. lemma OAI.Anticanonical.SourceSmooth.ParametrixPatch.coefficients_temperate line 135
  12. def OAI.Anticanonical.SourceSmooth.ParametrixPatch.differential line 139
  13. def OAI.Anticanonical.SourceSmooth.ParametrixPatch.cutoffError line 141
  14. lemma OAI.Anticanonical.SourceSmooth.ParametrixPatch.differential_local line 144
  15. lemma OAI.Anticanonical.SourceSmooth.ParametrixPatch.localInverse_distribution line 155
  16. lemma OAI.Anticanonical.SourceSmooth.ParametrixPatch.localInverse_equation line 163
  17. lemma OAI.Anticanonical.SourceSmooth.ParametrixPatch.cutoffError_coord line 175
  18. lemma OAI.Anticanonical.SourceSmooth.ParametrixPatch.cutoffError_bound line 187