OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingSobolevStrong.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.hasDerivAt_expandingSobolev_reduced line 13

   Source documentation

   Changing the fixed Fourier weight preserves the reduced strong equation.

   theorem hasDerivAt_expandingSobolev_reduced (a b k L : ℝ)
       (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k)
       (m : ℕ) (w : ℝ → FourierL2) (t : ℝ)
       (hw : HasDerivAt (fun s => lowerSobolevInclusion (w s))
         ((-(a : ℂ) + Complex.I * b) • lowerSobolevInclusion (w t) +
           (L ^ (-2 : ℝ) * Real.exp (-t)) • lowerSobolevGenerator (w t) +
           (-Complex.I) • lowerSobolevInclusion
             (expandingOddPower a k 1 ha ha1 hk le_rfl m (w t))) t) :
       let v := fun s => expandingToSobolev a k ha1 hk (w s)
   …

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

2. theorem OAI.DefocusingNLS.hasDerivAt_expandingNonlinearMild_sobolev line 42

   Source documentation

   Every constructed nonlinear Picard fixed point has the standard Sobolev strong equation.

   theorem hasDerivAt_expandingNonlinearMild_sobolev (a b k L T : ℝ)
       (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (hT : 0 ≤ T)
       (m : ℕ) (u : C(Icc (0 : ℝ) T, FourierL2)) (u₀ : FourierL2)
       (hu : u = expandingPicard a b k L T ha hk hL hT
         (expandingNonlinearReaction a k L T ha ha1 hk hL m) u₀ u)
       (t : ℝ) (ht : t ∈ Ioo 0 T) :
       let v := fun s => expandingToSobolev a k ha1 hk
   …

   Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingPicard, OAI.DefocusingNLS.expandingNonlinearReaction, OAI.DefocusingNLS.expandingToSobolev