OAI/Geometry/NodalSets/Elliptic/SmoothCutoff.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Yau.Waves.iteratedFDeriv_dilate_translate line 14
  2. theorem OAI.Yau.Waves.compact_smooth_derivative_bound line 22
  3. theorem OAI.Yau.Waves.scaled_compact_derivative_bound line 31
  4. def OAI.Yau.Waves.baseCutoff line 50
  5. def OAI.Yau.Waves.scaledCutoff line 52
  6. lemma OAI.Yau.Waves.scaledCutoff_contDiff line 55
  7. lemma OAI.Yau.Waves.scaledCutoff_mem_Icc line 58
  8. lemma OAI.Yau.Waves.scaledCutoff_eq_one line 61
  9. theorem OAI.Yau.Waves.scaledCutoff_support line 72
  10. theorem OAI.Yau.Waves.scaledCutoff_derivative_bound line 85