SobolevLinearization.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Pointwise meaning of the Sobolev linearization

Bounded torus observation commutes with the real Fréchet derivative. Thus the operator used in the perturbation equation is exactly the scalar linearization, including its conjugate component.

theorem OAI.DefocusingNLS.sobolevOddPower_fderiv_pointwise line 15

Source documentation

At each torus point, the Sobolev derivative is the scalar real derivative.

theorem sobolevOddPower_fderiv_pointwise (k : ℝ) (hk : 6 < k) (m : ℕ)
    (q v : FourierL2) (x : SchrodingerTorus) :
    sobolevTorusFunction k (fderiv ℝ (sobolevOddPower k hk m) q v) x =
      oddPowerDerivative m (sobolevTorusFunction k q x) (sobolevTorusFunction k v x) := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.oddPowerDerivative

theorem OAI.DefocusingNLS.sobolevOddPower_fderiv_pointwise_explicit line 37

Source documentation

The two circular components of the exact linearized odd-power operator.

theorem sobolevOddPower_fderiv_pointwise_explicit (k : ℝ) (hk : 6 < k) (m : ℕ)
    (q v : FourierL2) (x : SchrodingerTorus) :
    sobolevTorusFunction k (fderiv ℝ (sobolevOddPower k hk m) q v) x =
      ((m + 1 : ℕ) : ℂ) * (sobolevTorusFunction k q x) ^ m *
        star (sobolevTorusFunction k q x) ^ m * sobolevTorusFunction k v x +
      (m : ℂ) * (sobolevTorusFunction k q x) ^ (m + 1) *
        star (sobolevTorusFunction k q x) ^ (m - 1) * star (sobolevTorusFunction k v x) := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus

theorem OAI.DefocusingNLS.sobolevNonlinearRemainder_pointwise line 48

Source documentation

The abstract remainder evaluates to the actual scalar nonlinear Taylor remainder.

theorem sobolevNonlinearRemainder_pointwise (k : ℝ) (hk : 6 < k) (m : ℕ)
    (q v : FourierL2) (x : SchrodingerTorus) :
    sobolevTorusFunction k (sobolevNonlinearRemainder k hk m q v) x =
      oddPowerNonlinearity m (sobolevTorusFunction k q x + sobolevTorusFunction k v x) -
        oddPowerNonlinearity m (sobolevTorusFunction k q x) -
          oddPowerDerivative m (sobolevTorusFunction k q x) (sobolevTorusFunction k v x) := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.sobolevNonlinearRemainder, OAI.DefocusingNLS.oddPowerNonlinearity, OAI.DefocusingNLS.oddPowerDerivative