OAI/Geometry/PrescribedPotential/ParametrixAtlas.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Parametrix Atlas.

  1. def OAI.Anticanonical.ComplexAtlas.euclideanChart line 22
  2. lemma OAI.Anticanonical.ComplexAtlas.euclideanChart_source line 25
  3. lemma OAI.Anticanonical.ComplexAtlas.euclideanChart_target line 29
  4. lemma OAI.Anticanonical.ComplexAtlas.euclideanChart_apply line 34
  5. lemma OAI.Anticanonical.ComplexAtlas.euclideanChart_symm_apply line 37
  6. lemma OAI.Anticanonical.ComplexAtlas.euclidean_transition_smooth line 40
  7. structure OAI.Anticanonical.SourceSmooth.ParametrixPatch line 59
  8. def OAI.Anticanonical.SourceSmooth.ParametrixPatch.source line 80
  9. lemma OAI.Anticanonical.SourceSmooth.ParametrixPatch.isOpen_source line 83
  10. lemma OAI.Anticanonical.SourceSmooth.ParametrixPatch.source_sub line 86
  11. lemma OAI.Anticanonical.SourceSmooth.ParametrixPatch.exists_at line 89
  12. theorem OAI.Anticanonical.SourceSmooth.ParametrixPatch.finite_cover line 123