OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousYNorm.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact norm in the homogeneous completion

This identifies the weighted Fourier L² norm with the manuscript's two homogeneous Sobolev energies, including the radian Plancherel constant.

  1. theorem OAI.DefocusingNLS.integral_homogeneousFourierMeasure line 19
  2. theorem OAI.DefocusingNLS.integrable_homogeneousSchwartz line 39
  3. theorem OAI.DefocusingNLS.homogeneousSchwartzEmbedding_norm_sq line 49

    Source documentation

    The norm of the dense Schwartz embedding is exactly the norm defining Y.

    theorem homogeneousSchwartzEmbedding_norm_sq (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (χ : 𝓢(E, ℂ)) :
    ‖homogeneousSchwartzEmbedding a k ha ha1 hk χ‖ ^ 2 =
      ((2 * Real.pi) ^ (12 : ℕ))⁻¹ *
        (homogeneousFourierEnergy (6 - a) χ + homogeneousFourierEnergy k χ) := by
…

    Mentions: OAI.DefocusingNLS.homogeneousSchwartzEmbedding, OAI.DefocusingNLS.homogeneousFourierEnergy