OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousDyadicPartition.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

A concrete smooth dyadic partition in twelve dimensions

  1. def OAI.DefocusingNLS.homogeneousCoreBump line 15
  2. def OAI.DefocusingNLS.homogeneousCoreCutoff line 21
  3. theorem OAI.DefocusingNLS.homogeneousCoreCutoff_apply line 25
  4. theorem OAI.DefocusingNLS.homogeneousCoreCutoff_hasCompactSupport line 28
  5. theorem OAI.DefocusingNLS.homogeneousCoreCutoff_one line 32
  6. theorem OAI.DefocusingNLS.homogeneousCoreCutoff_zero line 38
  7. def OAI.DefocusingNLS.homogeneousHalfScale line 44
  8. theorem OAI.DefocusingNLS.homogeneousHalfScale_apply line 47
  9. def OAI.DefocusingNLS.homogeneousAnnulusCutoff line 50
  10. theorem OAI.DefocusingNLS.homogeneousAnnulusCutoff_apply line 54
  11. theorem OAI.DefocusingNLS.homogeneousAnnulusCutoff_hasCompactSupport line 59
  12. theorem OAI.DefocusingNLS.homogeneousAnnulusCutoff_support line 64
  13. theorem OAI.DefocusingNLS.homogeneousCoreCutoff_dyadic_tendsto_one line 92
  14. theorem OAI.DefocusingNLS.homogeneousAnnulusCutoff_dyadic_eventually_zero line 101
  15. theorem OAI.DefocusingNLS.homogeneousAnnulusCutoff_dyadic_sum line 119