ExpandingProfileResponse.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite-slab response to forcing in the actual linearized equation

An exponential time weight bounds the response on an arbitrary fixed slab. The constants are independent of the initial torus radius and use the actual odd-power derivative along the given bounded profile.

theorem OAI.DefocusingNLS.expandingMild_finiteSlab_residual_bound line 18

theorem OAI.DefocusingNLS.exists_expandingProfile_response_bound line 72

Source documentation

Bounded forcing in the actual profile linearization has a response bound on every finite slab, uniformly in the starting radius.

theorem exists_expandingProfile_response_bound (a b k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ) (R : ℝ) (hR : 0 ≤ R) :
    ∃ K : ℝ, 0 ≤ K ∧ ∀ (L T : ℝ) (hL : 1 ≤ L) (hT : 0 ≤ T)
      (q g : C(Icc (0 : ℝ) T, FourierL2)) (u₀ : FourierL2)
      (G : ℝ), 0 ≤ G → (∀ t, ‖q t‖ ≤ R) → (∀ t, ‖g t‖ ≤ G) →
      ∀ u v : C(Icc (0 : ℝ) T, FourierL2),
      (∀ t : Icc (0 : ℝ) T, u t =
        expandingFreeStep a b k L t ha hk hL t.2.1 u₀ +
          expandingDuhamel a b k L ha hk hL t
            (expandingReactionHistory T hT
              (expandingProfileReaction a k T ha ha1 hk m (expandingRadiusCurve L T hL) q g) u)) →
      (∀ t : Icc (0 : ℝ) T, v t =
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingFreeStep, OAI.DefocusingNLS.expandingDuhamel, OAI.DefocusingNLS.expandingReactionHistory, OAI.DefocusingNLS.expandingProfileReaction, OAI.DefocusingNLS.expandingRadiusCurve