OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousYLocalization.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The actual localization operator into the homogeneous completion

The operator is the Fourier realization of χ(y/L)v(y). Its norm has a bound independent of L ≥ 1, with the exact manuscript Y and Y_L norms.

  1. theorem OAI.DefocusingNLS.norm_toLp_two_sq line 21
  2. theorem OAI.DefocusingNLS.memLp_expandingPhysicalLocalization_fourier line 29
  3. def OAI.DefocusingNLS.homogeneousLocalization line 51

    Source documentation

    The Fourier representative of the actual physical localization.

    noncomputable def homogeneousLocalization (a k L : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L)
    (χ : 𝓢(E, ℂ)) (f : FourierL2) : HomogeneousY a k :=
…

    Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.HomogeneousY

  4. theorem OAI.DefocusingNLS.homogeneousLocalization_ae line 57
  5. theorem OAI.DefocusingNLS.homogeneousLocalization_norm_sq line 64
  6. theorem OAI.DefocusingNLS.expandingPhysicalLocalization_add line 75
  7. theorem OAI.DefocusingNLS.expandingPhysicalLocalization_smul line 84
  8. def OAI.DefocusingNLS.homogeneousLocalizationLinearMap line 95
  9. theorem OAI.DefocusingNLS.exists_homogeneousLocalization_bound line 118

    Source documentation

    One constant controls the actual localization operator on every expanding torus.

    theorem exists_homogeneousLocalization_bound (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (χ : 𝓢(E, ℂ)) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (L : ℝ) (hL : 1 ≤ L) (f : FourierL2),
      ‖homogeneousLocalization a k L ha ha1 hk hL χ f‖ ≤ C * ‖f‖ := by
…

    Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.homogeneousLocalization

  10. def OAI.DefocusingNLS.homogeneousLocalizationCLM line 134
  11. theorem OAI.DefocusingNLS.homogeneousLocalizationCLM_apply line 141