OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousEnergyInterpolation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The low homogeneous energy is controlled by LĀ² and the high energy

This is the elementary frequency splitting used for the compact interior potential term. The indices are exactly 6-a and k from the manuscript.

  1. theorem OAI.DefocusingNLS.radianFourier_energy_zero line 19

    Source documentation

    Plancherel with the manuscript's radian Fourier normalization.

    theorem radianFourier_energy_zero (f : š“¢(E, ā„‚)) :
    homogeneousFrequencyEnergy 0 (radianFourierKernel f) =
      (2 * Real.pi) ^ (12 : ā„•) * homogeneousFrequencyEnergy 0 f := by
ā€¦

    Mentions: OAI.DefocusingNLS.homogeneousFrequencyEnergy, OAI.DefocusingNLS.radianFourierKernel

  2. theorem OAI.DefocusingNLS.low_weight_interpolation line 34
  3. theorem OAI.DefocusingNLS.homogeneousLowEnergy_interpolation line 65
  4. theorem OAI.DefocusingNLS.tendsto_homogeneousLowEnergy_of_L2 line 87