SobolevTaylorRemainder.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The quadratic Sobolev remainder after linearization

def OAI.DefocusingNLS.sobolevNonlinearRemainder line 12
Source documentation
The actual odd-power nonlinearity with its constant and linear parts removed.
```
noncomputable def sobolevNonlinearRemainder (k : ℝ) (hk : 6 < k) (m : ℕ)
    (q v : FourierL2) : FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.sobolevNonlinearRemainder_zero line 17
theorem OAI.DefocusingNLS.hasFDerivAt_sobolevNonlinearRemainder line 21

theorem OAI.DefocusingNLS.exists_sobolevNonlinearRemainder_lipschitz line 35

Source documentation

On any bounded set of backgrounds, the linearized remainder has the manuscript's quadratic Lipschitz bound, uniformly for perturbations in the unit ball.

theorem exists_sobolevNonlinearRemainder_lipschitz (k : ℝ) (hk : 6 < k) (m : ℕ)
    (R : ℝ) (hR : 0 ≤ R) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ q v w : FourierL2, ‖q‖ ≤ R → ‖v‖ ≤ 1 → ‖w‖ ≤ 1 →
      ‖sobolevNonlinearRemainder k hk m q v - sobolevNonlinearRemainder k hk m q w‖ ≤
        C * (‖v‖ + ‖w‖) * ‖v - w‖ := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.sobolevNonlinearRemainder

theorem OAI.DefocusingNLS.exists_sobolevNonlinearRemainder_quadratic line 64

Source documentation

The remainder is quadratic, with one constant for every background in a fixed Sobolev ball.

theorem exists_sobolevNonlinearRemainder_quadratic (k : ℝ) (hk : 6 < k) (m : ℕ)
    (R : ℝ) (hR : 0 ≤ R) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ q v : FourierL2, ‖q‖ ≤ R → ‖v‖ ≤ 1 →
      ‖sobolevNonlinearRemainder k hk m q v‖ ≤ C * ‖v‖ ^ 2 := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.sobolevNonlinearRemainder