OAI/Geometry/PrescribedRicci/PathLocalGain.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Path Local Gain.

  1. lemma OAI.SobolevChart.UniformSobolev.cutoff_integer line 21
  2. lemma OAI.SobolevChart.UniformSobolev.cutoff_zero line 26
  3. lemma OAI.SobolevChart.UniformSobolev.cutoff_two line 31
  4. lemma OAI.GlobalElliptic.GluingData.cutoff_nested_one line 45
  5. lemma OAI.GlobalElliptic.GluingData.path_cutoff_identity line 57
  6. lemma OAI.GlobalElliptic.GluingData.path_cutoff_bound line 71
  7. lemma OAI.GlobalElliptic.GluingData.path_local_word_differential line 84
  8. lemma OAI.GlobalElliptic.GluingData.path_local_word_H2 line 173
  9. lemma OAI.GlobalElliptic.GluingData.path_local_gain line 202