OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousSymbolMembership.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual homogeneous-space membership from physical symbol estimates

A smooth physical profile with the manuscript's |x|^(-2a) derivative decay has a representative in the faithful Fourier completion. The proof builds the representative from a compact core and normalized dyadic annuli.

  1. theorem OAI.DefocusingNLS.exists_finite_symbol_membership_order line 18
  2. theorem OAI.DefocusingNLS.exists_homogeneous_of_symbol_decay line 60
  3. theorem OAI.DefocusingNLS.exists_homogeneous_of_symbol_decay_at_infinity line 78

    Source documentation

    Only the decay at infinity needs to be supplied; smoothness controls the core.

    theorem exists_homogeneous_of_symbol_decay_at_infinity (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k)
    (Q : E → ℂ) (hQ : ContDiff ℝ ∞ Q)
    (hsymbol : ∀ n : ℕ, ∃ D : ℝ, ∀ y : E, 1 ≤ ‖y‖ →
      ‖iteratedFDeriv ℝ n Q y‖ ≤ D * ‖y‖ ^ (-2 * a - (n : ℝ))) :
    ∃ q : HomogeneousY a k, ∀ y : E, homogeneousPhysicalCLM a k ha ha1 hk q y = Q y := by
…

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