OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousFrequencySplit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A concrete low/high frequency splitting on the Schwartz domain

The low cutoff equals one up to R and vanishes beyond 2R. Its complement does not increase any homogeneous Fourier energy.

  1. def OAI.DefocusingNLS.homogeneousFrequencyBump line 20
  2. def OAI.DefocusingNLS.homogeneousFrequencyCutoff line 26
  3. theorem OAI.DefocusingNLS.homogeneousFrequencyCutoff_apply line 31
  4. theorem OAI.DefocusingNLS.homogeneousFrequencyCutoff_one line 34
  5. theorem OAI.DefocusingNLS.homogeneousFrequencyCutoff_zero line 40
  6. theorem OAI.DefocusingNLS.homogeneousFrequencyCutoff_complement_norm line 46
  7. def OAI.DefocusingNLS.homogeneousLowFrequencyPart line 56
  8. theorem OAI.DefocusingNLS.homogeneousLowFrequencyPart_fourier line 60
  9. def OAI.DefocusingNLS.homogeneousHighFrequencyPart line 68
  10. theorem OAI.DefocusingNLS.homogeneousHighFrequencyPart_fourier line 71
  11. theorem OAI.DefocusingNLS.homogeneousHighFrequencyPart_zero line 79
  12. theorem OAI.DefocusingNLS.homogeneousHighFrequencyPart_energy_le line 84