ExpandingDerivativeBounds.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Scale-uniform derivatives of the actual expanding-torus nonlinearity

theorem OAI.DefocusingNLS.expanding_linear_two_jet_bound line 13
theorem OAI.DefocusingNLS.expanding_bilinear_two_jet_bound line 34

theorem OAI.DefocusingNLS.exists_expandingOddPower_two_jet_bound line 68

Source documentation

Derivatives through order two are bounded uniformly for every L ≥ 1.

theorem exists_expandingOddPower_two_jet_bound (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ) (R : ℝ) (hR : 0 ≤ R) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (L : ℝ) (hL : 1 ≤ L) (f : FourierL2), ‖f‖ ≤ R →
      ∀ n : ℕ, n ≤ 2 → ‖iteratedFDeriv ℝ n (expandingOddPower a k L ha ha1 hk hL m) f‖ ≤ C := by
…

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

theorem OAI.DefocusingNLS.exists_expandingOddPower_derivative_lipschitz line 99

Source documentation

The derivative is Lipschitz on each ball, uniformly in the torus radius.

theorem exists_expandingOddPower_derivative_lipschitz (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ) (R : ℝ) (hR : 0 ≤ R) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (L : ℝ) (hL : 1 ≤ L) (f g : FourierL2),
      ‖f‖ ≤ R → ‖g‖ ≤ R →
      ‖fderiv ℝ (expandingOddPower a k L ha ha1 hk hL m) f -
        fderiv ℝ (expandingOddPower a k L ha ha1 hk hL m) g‖ ≤ C * ‖f - g‖ := by
…

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