OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousFreeFourier.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Exact whole-space free evolution in Fourier variables

The similarity factor and dilation are those of (lin:free-flow). The two homogeneous energies are estimated separately before extending the action to Y.

  1. def OAI.DefocusingNLS.homogeneousFrequencyEnergy line 20
  2. theorem OAI.DefocusingNLS.frequency_density_dilation line 23
  3. theorem OAI.DefocusingNLS.homogeneousFrequencyEnergy_dilation line 36
  4. def OAI.DefocusingNLS.homogeneousFreePhase line 51
  5. theorem OAI.DefocusingNLS.homogeneousFreePhase_norm line 54
  6. theorem OAI.DefocusingNLS.homogeneousFreePhase_temperate line 57
  7. def OAI.DefocusingNLS.homogeneousFreeAmplitude line 63
  8. theorem OAI.DefocusingNLS.homogeneousFreeAmplitude_norm line 66
  9. def OAI.DefocusingNLS.homogeneousFreeFourier line 71

    Source documentation

    Fourier action of e^((-a+ib)s)e^(i(1-e^-s)Δ)v.

    noncomputable def homogeneousFreeFourier (a b s : ℝ) : 𝓢(E, ℂ) →L[ℂ] 𝓢(E, ℂ) :=
…
  10. theorem OAI.DefocusingNLS.homogeneousFreeFourier_apply line 78
  11. theorem OAI.DefocusingNLS.homogeneousFreeFourier_energy line 91

    Source documentation

    Each homogeneous order has its exact similarity exponent.

    theorem homogeneousFreeFourier_energy (a b s r : ℝ) (ψ : 𝓢(E, ℂ)) :
    homogeneousFrequencyEnergy r (homogeneousFreeFourier a b s ψ) =
      Real.exp ((6 - 2 * a - r) * s) * homogeneousFrequencyEnergy r ψ := by
…

    Mentions: OAI.DefocusingNLS.homogeneousFrequencyEnergy, OAI.DefocusingNLS.homogeneousFreeFourier