LocalizationFourierEnergy.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The exact homogeneous Fourier energy of a finite localized polynomial

The dilation identity supplies the factor L^(12-2s). The weighted mixed estimate then controls both orders of Y by the exact Y_L coefficient norm.

def OAI.DefocusingNLS.homogeneousFourierEnergy line 19
theorem OAI.DefocusingNLS.homogeneousKernel_density_scale line 22
theorem OAI.DefocusingNLS.homogeneousKernel_dilation line 38
theorem OAI.DefocusingNLS.homogeneousKernel_bessel_control line 52

theorem OAI.DefocusingNLS.integrable_localizedFourierPolynomial_energy line 78

Source documentation

Each finite physical cutoff has finite homogeneous Fourier energy.

theorem integrable_localizedFourierPolynomial_energy (s L : ℝ) (hs : 0 ≤ s) (hL : 0 < L)
    (χ : 𝓢(E, ℂ)) (S : Finset frequencyLattice) (v : frequencyLattice → ℂ) :
    Integrable (fun ξ => ‖ξ‖ ^ (2 * s) *
      ‖radianFourierIntegral (localizedFourierPolynomial L χ S v) ξ‖ ^ 2) := by
…

Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.radianFourierIntegral, OAI.DefocusingNLS.localizedFourierPolynomial

theorem OAI.DefocusingNLS.exists_localizedFourierPolynomial_energy_bound line 92

Source documentation

The finite Fourier version of the manuscript's uniform cutoff estimate. The right side is the exact Y_L coefficient density, before the common (2π)^12 normalization.

theorem exists_localizedFourierPolynomial_energy_bound (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (χ : 𝓢(E, ℂ)) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (L : ℝ), 1 ≤ L →
      ∀ (S : Finset frequencyLattice) (v : frequencyLattice → ℂ),
      homogeneousFourierEnergy (6 - a) (localizedFourierPolynomial L χ S v) +
        homogeneousFourierEnergy k (localizedFourierPolynomial L χ S v) ≤
          C * ∑ n ∈ S, expandingSobolevWeightSq a k L n * ‖v n‖ ^ 2 := by
…

Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.homogeneousFourierEnergy, OAI.DefocusingNLS.localizedFourierPolynomial, OAI.DefocusingNLS.expandingSobolevWeightSq