ExpandingTaylorRemainder.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The quadratic remainder with constants uniform on expanding tori

def OAI.DefocusingNLS.expandingNonlinearRemainder line 11
theorem OAI.DefocusingNLS.expandingNonlinearRemainder_zero line 18
theorem OAI.DefocusingNLS.hasFDerivAt_expandingNonlinearRemainder line 23

theorem OAI.DefocusingNLS.exists_expandingNonlinearRemainder_lipschitz line 37

Source documentation

One quadratic Lipschitz constant works on every torus with L ≥ 1.

theorem exists_expandingNonlinearRemainder_lipschitz (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ) (R : ℝ) (hR : 0 ≤ R) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (L : ℝ) (hL : 1 ≤ L) (q v w : FourierL2),
      ‖q‖ ≤ R → ‖v‖ ≤ 1 → ‖w‖ ≤ 1 →
      ‖expandingNonlinearRemainder a k L ha ha1 hk hL m q v -
        expandingNonlinearRemainder a k L ha ha1 hk hL m q w‖ ≤
          C * (‖v‖ + ‖w‖) * ‖v - w‖ := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingNonlinearRemainder

theorem OAI.DefocusingNLS.exists_expandingNonlinearRemainder_quadratic line 69

Source documentation

The quadratic remainder estimate has no dependence on the expanding scale.

theorem exists_expandingNonlinearRemainder_quadratic (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ) (R : ℝ) (hR : 0 ≤ R) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (L : ℝ) (hL : 1 ≤ L) (q v : FourierL2),
      ‖q‖ ≤ R → ‖v‖ ≤ 1 →
      ‖expandingNonlinearRemainder a k L ha ha1 hk hL m q v‖ ≤ C * ‖v‖ ^ 2 := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingNonlinearRemainder