OAI/Geometry/PrescribedRicci/UniformL2.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Uniform L2.

  1. def OAI.SobolevChart.UniformL2 line 19
  2. lemma OAI.SobolevChart.UniformSobolev.uniformL2 line 22
  3. lemma OAI.SobolevChart.UniformL2.norm line 27
  4. lemma OAI.SobolevChart.UniformL2.add line 33
  5. lemma OAI.SobolevChart.UniformL2.smul line 40
  6. lemma OAI.SobolevChart.UniformL2.zero line 49
  7. lemma OAI.SobolevChart.UniformL2.sum line 53
  8. lemma OAI.SobolevChart.UniformSobolev.zero_of_majorant line 63