ExpandingLocalizationBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform localization on the actual expanding-torus space

The finite-cutoff estimate passes to the continuous periodic Fourier series. The coefficient normalization is exactly the Y_L normalization already used for the expanding flow, and every constant is independent of L ≥ 1.

theorem OAI.DefocusingNLS.exists_localizedFourierSeries_energy_bound line 21
theorem OAI.DefocusingNLS.expanding_coefficient_localization_energy line 74

theorem OAI.DefocusingNLS.exists_expandingPhysicalLocalization_bound line 88

Source documentation

The actual physical cutoff has a uniform two-order homogeneous Fourier bound. This is the squared version of (lin:J-bound), with fixed Fourier normalization absorbed in C.

theorem exists_expandingPhysicalLocalization_bound (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (χ : 𝓢(E, ℂ)) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (L : ℝ), 1 ≤ L → ∀ (f : FourierL2),
      Integrable (fun ξ => ‖ξ‖ ^ (2 * (6 - a)) *
        ‖radianFourierIntegral (expandingPhysicalLocalization a k L χ f) ξ‖ ^ 2) ∧
      Integrable (fun ξ => ‖ξ‖ ^ (2 * k) *
        ‖radianFourierIntegral (expandingPhysicalLocalization a k L χ f) ξ‖ ^ 2) ∧
      homogeneousFourierEnergy (6 - a) (expandingPhysicalLocalization a k L χ f) +
        homogeneousFourierEnergy k (expandingPhysicalLocalization a k L χ f) ≤ C * ‖f‖ ^ 2 := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.radianFourierIntegral, OAI.DefocusingNLS.expandingPhysicalLocalization, OAI.DefocusingNLS.homogeneousFourierEnergy