SchrodingerForcedDuhamel.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Duhamel's identity with a Sobolev forcing term

The forcing is an actual vector in the upper Sobolev space, while the time derivative is taken after the two-order inclusion. Fourier coordinates remove the unbounded generator without assuming upper-space differentiability.

theorem OAI.DefocusingNLS.hasDerivAt_coordinate_forced_schrodinger line 17

Source documentation

The forced equation determines every physical Fourier coefficient.

theorem hasDerivAt_coordinate_forced_schrodinger
    (u j : ℝ → FourierL2) (t : ℝ) (n : frequencyLattice)
    (hu : HasDerivAt (fun s => lowerSobolevInclusion (u s))
      (lowerSobolevGenerator (u t) + lowerSobolevInclusion (j t)) t) :
    HasDerivAt (fun s => u s n)
      (-Complex.I * ((‖n‖ ^ 2 : ℝ) : ℂ) * u t n + j t n) t := by
…

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

theorem OAI.DefocusingNLS.hasDerivAt_forced_interaction_coordinate line 32

Source documentation

The inverse phase cancels the free generator in the forced equation.

theorem hasDerivAt_forced_interaction_coordinate
    (u j : ℝ → FourierL2) (t : ℝ) (n : frequencyLattice)
    (hu : HasDerivAt (fun s => lowerSobolevInclusion (u s))
      (lowerSobolevGenerator (u t) + lowerSobolevInclusion (j t)) t) :
    HasDerivAt (fun s => inverseSchrodingerCurve u s n)
      (schrodingerFlow (-t) (j t) n) t := by
…

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

theorem OAI.DefocusingNLS.continuousOn_rotatedSchrodingerForcing line 51

theorem OAI.DefocusingNLS.forcedSobolevDuhamel_identity line 62

Source documentation

The forced equation gives an upper-Sobolev Bochner integral identity.

theorem forcedSobolevDuhamel_identity
    (u j : ℝ → FourierL2) (a b t₀ t : ℝ)
    (hj : ContinuousOn j (Ioo a b))
    (hu : ∀ s ∈ Ioo a b, HasDerivAt (fun r => lowerSobolevInclusion (u r))
      (lowerSobolevGenerator (u s) + lowerSobolevInclusion (j s)) s)
    (ht₀ : t₀ ∈ Ioo a b) (ht : t ∈ Ioo a b) :
    inverseSchrodingerCurve u t = inverseSchrodingerCurve u t₀ +
      ∫ s in t₀..t, schrodingerFlow (-s) (j s) := by
…

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

theorem OAI.DefocusingNLS.forcedSobolevDuhamel_physical line 94

Source documentation

The usual variation-of-constants formula in the physical Sobolev representation.

theorem forcedSobolevDuhamel_physical
    (u j : ℝ → FourierL2) (a b t₀ t : ℝ)
    (hj : ContinuousOn j (Ioo a b))
    (hu : ∀ s ∈ Ioo a b, HasDerivAt (fun r => lowerSobolevInclusion (u r))
      (lowerSobolevGenerator (u s) + lowerSobolevInclusion (j s)) s)
    (ht₀ : t₀ ∈ Ioo a b) (ht : t ∈ Ioo a b) :
    u t = schrodingerFlow (t - t₀) (u t₀) +
      ∫ s in t₀..t, schrodingerFlow (t - s) (j s) := by
…

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

theorem OAI.DefocusingNLS.hasDerivAt_forced_inverseSchrodingerCurve line 109

Source documentation

Continuous upper-space forcing upgrades the interaction curve to a classical one.

theorem hasDerivAt_forced_inverseSchrodingerCurve
    (u j : ℝ → FourierL2) (a b t : ℝ)
    (hj : ContinuousOn j (Ioo a b))
    (hu : ∀ s ∈ Ioo a b, HasDerivAt (fun r => lowerSobolevInclusion (u r))
      (lowerSobolevGenerator (u s) + lowerSobolevInclusion (j s)) s)
    (ht : t ∈ Ioo a b) :
    HasDerivAt (inverseSchrodingerCurve u) (schrodingerFlow (-t) (j t)) t := by
…

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

theorem OAI.DefocusingNLS.hasDerivAt_residual_inverseSchrodingerCurve line 129

Source documentation

An approximate nonlinear Schrödinger trajectory has the exact rotated residual.

theorem hasDerivAt_residual_inverseSchrodingerCurve
    (k : ℝ) (hk : 6 < k) (m : ℕ) (u r : ℝ → FourierL2) (a b t : ℝ)
    (huc : ContinuousOn u (Ioo a b)) (hrc : ContinuousOn r (Ioo a b))
    (hu : ∀ s ∈ Ioo a b, HasDerivAt (fun x => lowerSobolevInclusion (u x))
      (lowerSobolevGenerator (u s) -
        Complex.I • lowerSobolevInclusion (sobolevOddPower k hk m (u s)) +
        lowerSobolevInclusion (r s)) s)
    (ht : t ∈ Ioo a b) :
    HasDerivAt (inverseSchrodingerCurve u)
      (schrodingerInteractionField k hk m t (inverseSchrodingerCurve u t) +
        schrodingerFlow (-t) (r t)) t := by
…

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