OAI/Geometry/PrescribedPotential/SchwartzFamilyBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Schwartz Family Bounds.

  1. def OAI.SobolevChart.schwartzCoordCLM line 17
  2. lemma OAI.SobolevChart.schwartzCoordCLM_apply line 21
  3. lemma OAI.SobolevChart.schwartz_family_bounded line 29
  4. lemma OAI.SobolevChart.schwartzCoord_family_bound line 50