HomogeneousSymbolBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite Schwartz-jet control for normalized profile pieces

Continuity of the actual Schwartz-to-Y embedding reduces the remaining annular estimate to finitely many weighted physical derivatives.

theorem OAI.DefocusingNLS.exists_homogeneousSymbolJet_bound line 19

theorem OAI.DefocusingNLS.exists_homogeneous_from_schwartz_annuli line 51

Source documentation

Uniform jets of the normalized annuli suffice for the dyadic Y reconstruction.

theorem exists_homogeneous_from_schwartz_annuli (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) :
    ∃ (N : ℕ) (C : ℝ), 0 ≤ C ∧ ∀ (ψ : ℕ → 𝓢(E, ℂ)) (D : ℝ), 0 ≤ D →
      (∀ j n, n ≤ N → ∀ x : E,
        (1 + ‖x‖) ^ N * ‖iteratedFDeriv ℝ n (ψ j) x‖ ≤ D) →
      ∃ q : HomogeneousY a k,
        (∀ y : E, homogeneousPhysicalCLM a k ha ha1 hk q y =
          ∑' j, (((2 : ℝ) ^ j) ^ (-2 * a) : ℝ) * ψ j (((2 : ℝ) ^ j)⁻¹ • y)) ∧
        ‖q‖ ≤ C * D / (1 - 2 ^ (-a)) := by
…

Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousPhysicalCLM