OAI/Geometry/NodalSets/Elliptic/LocalizedCorrugation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Yau.Geometry.corrugationSlowMap line 12
  2. def OAI.Yau.Geometry.corrugationFastMap line 15
  3. def OAI.Yau.Geometry.localizedCorrugation line 18
  4. lemma OAI.Yau.Geometry.localizedCorrugation_formula line 22
  5. lemma OAI.Yau.Geometry.localizedCorrugation_smooth line 27
  6. lemma OAI.Yau.Geometry.localizedCorrugation_support line 35
  7. lemma OAI.Yau.Geometry.localizedCorrugation_cube line 46
  8. lemma OAI.Yau.Geometry.localizedCorrugation_compact line 57
  9. lemma OAI.Yau.Geometry.localizedCorrugation_collar line 64
  10. lemma OAI.Yau.Geometry.localizedCorrugation_bound line 72