ExpandingProfilePropagator.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The finite-slab propagator for the actual linearized profile

The solution operator is real-linear and bounded in the exact expanding Sobolev coordinates. Its bound depends on the profile bound and elapsed time, and is independent of the starting radius.

def OAI.DefocusingNLS.expandingProfileTrajectory line 27
theorem OAI.DefocusingNLS.expandingProfileTrajectory_eq line 34
theorem OAI.DefocusingNLS.expandingProfileTrajectory_unique line 40
theorem OAI.DefocusingNLS.profile_history_zero line 48
theorem OAI.DefocusingNLS.profile_history_add line 57
theorem OAI.DefocusingNLS.profile_history_smul line 69
theorem OAI.DefocusingNLS.expandingProfileTrajectory_zero line 82
theorem OAI.DefocusingNLS.expandingProfileTrajectory_add line 90
theorem OAI.DefocusingNLS.expandingProfileTrajectory_smul line 103

theorem OAI.DefocusingNLS.exists_expandingProfile_propagator line 116

Source documentation

One uniform growth rate yields bounded real-linear finite-slab propagators for every permitted radius and bounded continuous profile.

theorem exists_expandingProfile_propagator (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 : C(Icc (0 : ℝ) T, FourierL2)) (_hq : ∀ t, ‖q t‖ ≤ R),
      ∃ U : FourierL2 →L[ℝ] C(Icc (0 : ℝ) T, FourierL2),
        (∀ u₀ t, U 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 0) (U u₀))) ∧
        ‖U‖ ≤ (K + 1) * Real.exp ((K + 1) * T) := by
…

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