OAI/Geometry/PrescribedRicci/UniformSchwartz.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Uniform Schwartz.

  1. def OAI.SobolevChart.UniformSobolev line 22
  2. lemma OAI.SobolevChart.UniformSobolev.of_coreBound line 25
  3. lemma OAI.SobolevChart.UniformSobolev.mono line 32
  4. lemma OAI.SobolevChart.UniformSobolev.add line 36
  5. lemma OAI.SobolevChart.UniformSobolev.const line 44
  6. lemma OAI.SobolevChart.UniformSobolev.sum line 47
  7. lemma OAI.SobolevChart.UniformSobolev.deriv line 56
  8. lemma OAI.SobolevChart.UniformSobolev.word line 60
  9. lemma OAI.SobolevChart.uniformSobolev_zero_iff line 64
  10. lemma OAI.SobolevChart.uniformSobolev_raise_two line 68
  11. theorem OAI.FrozenPoisson.uniform_schwartz_H2 line 85