ExpandingProfileDifference.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Differences in the actual profile-linearized evolution

Subtracting two forced linearized trajectories preserves the linearized equation, with the difference of their initial data and forcing.

theorem OAI.DefocusingNLS.expandingProfileTrajectory_sub line 19
theorem OAI.DefocusingNLS.expandingProfile_mild_sub line 33

theorem OAI.DefocusingNLS.expandingPerturbation_difference_linear_mild line 78

Source documentation

The nonlinear difference is a forced trajectory of the actual profile linearization; the common profile defect cancels from its source.

theorem expandingPerturbation_difference_linear_mild (a b k L T : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (hT : 0 ≤ T) (m : ℕ)
    (q g u v : C(Icc (0 : ℝ) T, FourierL2)) (u₀ v₀ : FourierL2)
    (hu : u = expandingPicard a b k L T ha hk hL hT
      (expandingPerturbationReaction a k L T ha ha1 hk hL m q g) u₀ u)
    (hv : v = expandingPicard a b k L T ha hk hL hT
      (expandingPerturbationReaction a k L T ha ha1 hk hL m q g) v₀ v) :
    ∀ t : Icc (0 : ℝ) T, (u - v) t =
      expandingFreeStep a b k L t ha hk hL t.2.1 (u₀ - v₀) +
        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
…

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