SobolevResidualStability.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Stability near an approximate physical Schrödinger trajectory

These estimates retain the actual Fourier generator and pointwise Sobolev nonlinearity. They apply on a fixed Sobolev ball; no uniform estimate for a rescaled growing torus is asserted here.

theorem OAI.DefocusingNLS.exists_sobolevSchrodinger_residual_stability_constant line 19

Source documentation

A bounded residual gives a quantitative comparison with an exact physical solution.

theorem exists_sobolevSchrodinger_residual_stability_constant
    (k : ℝ) (hk : 6 < k) (m : ℕ) (R : ℝ) (hR : 0 ≤ R) :
    ∃ K : ℝ≥0, ∀ (u q r : ℝ → FourierL2) (a' b' a b ε : ℝ),
      Icc a b ⊆ Ioo a' b' →
      ContinuousOn u (Ioo a' b') → ContinuousOn q (Ioo a' b') →
      ContinuousOn r (Ioo a' b') →
      (∀ t ∈ Ioo a' b', HasDerivAt (fun s => lowerSobolevInclusion (u s))
        (lowerSobolevGenerator (u t) -
          Complex.I • lowerSobolevInclusion (sobolevOddPower k hk m (u t))) t) →
      (∀ t ∈ Ioo a' b', HasDerivAt (fun s => lowerSobolevInclusion (q s))
        (lowerSobolevGenerator (q t) -
          Complex.I • lowerSobolevInclusion (sobolevOddPower k hk m (q t)) +
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.lowerSobolevInclusion

theorem OAI.DefocusingNLS.hasDerivAt_sobolevProfilePerturbation line 72

Source documentation

Subtracting an approximate profile gives the actual linearized equation plus its quadratic Taylor remainder and the negative profile residual.

theorem hasDerivAt_sobolevProfilePerturbation
    (k : ℝ) (hk : 6 < k) (m : ℕ) (u q : ℝ → FourierL2) (r : FourierL2) (t : ℝ)
    (hu : HasDerivAt (fun s => lowerSobolevInclusion (u s))
      (lowerSobolevGenerator (u t) -
        Complex.I • lowerSobolevInclusion (sobolevOddPower k hk m (u t))) t)
    (hq : HasDerivAt (fun s => lowerSobolevInclusion (q s))
      (lowerSobolevGenerator (q t) -
        Complex.I • lowerSobolevInclusion (sobolevOddPower k hk m (q t)) +
          lowerSobolevInclusion r) t) :
    HasDerivAt (fun s => lowerSobolevInclusion (u s - q s))
      (lowerSobolevGenerator (u t - q t) -
        Complex.I • lowerSobolevInclusion
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.lowerSobolevInclusion