ExpandingLinearization.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Pointwise meaning of the uniform expanding-torus linearization

theorem OAI.DefocusingNLS.expandingOddPower_fderiv_pointwise line 11

Source documentation

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

theorem expandingOddPower_fderiv_pointwise (a k L : ℝ) (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (m : ℕ)
    (q v : FourierL2) (x : SchrodingerTorus) :
    expandingTorusFunction a k L (fderiv ℝ (expandingOddPower a k L ha ha1 hk hL m) q v) x =
      oddPowerDerivative m (expandingTorusFunction a k L q x) (expandingTorusFunction a k L v x) := by
…

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

theorem OAI.DefocusingNLS.expandingOddPower_fderiv_pointwise_explicit line 33

Source documentation

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

theorem expandingOddPower_fderiv_pointwise_explicit (a k L : ℝ) (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (m : ℕ)
    (q v : FourierL2) (x : SchrodingerTorus) :
    expandingTorusFunction a k L (fderiv ℝ (expandingOddPower a k L ha ha1 hk hL m) q v) x =
      ((m + 1 : ℕ) : ℂ) * (expandingTorusFunction a k L q x) ^ m *
        star (expandingTorusFunction a k L q x) ^ m * expandingTorusFunction a k L v x +
      (m : ℂ) * (expandingTorusFunction a k L q x) ^ (m + 1) *
        star (expandingTorusFunction a k L q x) ^ (m - 1) * star (expandingTorusFunction a k L v x) := by
…

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

theorem OAI.DefocusingNLS.expandingNonlinearRemainder_pointwise line 44

Source documentation

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

theorem expandingNonlinearRemainder_pointwise (a k L : ℝ) (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (m : ℕ)
    (q v : FourierL2) (x : SchrodingerTorus) :
    expandingTorusFunction a k L (expandingNonlinearRemainder a k L ha ha1 hk hL m q v) x =
      oddPowerNonlinearity m (expandingTorusFunction a k L q x + expandingTorusFunction a k L v x) -
        oddPowerNonlinearity m (expandingTorusFunction a k L q x) -
          oddPowerDerivative m (expandingTorusFunction a k L q x) (expandingTorusFunction a k L v x) := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.expandingTorusFunction, OAI.DefocusingNLS.expandingNonlinearRemainder, OAI.DefocusingNLS.oddPowerNonlinearity, OAI.DefocusingNLS.oddPowerDerivative