OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingStrongEquation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Strong derivatives for the moving-torus equation

The time-dependent Laplacian loses two Sobolev orders. After this loss, continuity of the candidate derivative upgrades the Fourier-mode equation to a strong Hilbert-space equation.

  1. def OAI.DefocusingNLS.expandingReducedField line 17
  2. theorem OAI.DefocusingNLS.continuousOn_expandingReducedField line 22
  3. theorem OAI.DefocusingNLS.hasDerivAt_expandingReducedField line 34

    Source documentation

    A continuous Fourier solution of the exact mode equations is a strong solution in the space with two fewer Sobolev derivatives.

    theorem hasDerivAt_expandingReducedField (a b L A B : ℝ) (u r : ℝ → FourierL2)
    (hu : ContinuousOn u (Ioo A B)) (hr : ContinuousOn r (Ioo A B))
    (hmode : ∀ t ∈ Ioo A B, ∀ n : frequencyLattice,
      HasDerivAt (fun s => u s n) (expandingModeRate a b L t n * u t n + r t n) t)
    (t : ℝ) (ht : t ∈ Ioo A B) :
    HasDerivAt (fun s => lowerSobolevInclusion (u s))
      (expandingReducedField a b L u r t) t := by
…

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