HomogeneousTaylorRemainder.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The quadratic homogeneous remainder after linearization

def OAI.DefocusingNLS.homogeneousNonlinearRemainder line 16
Source documentation
The actual odd-power nonlinearity with its constant and linear parts removed.
```
noncomputable def homogeneousNonlinearRemainder (a k : ℝ) (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ)
    (q v : (HomogeneousY a k)) : (HomogeneousY a k) :=
…
```
Mentions: OAI.DefocusingNLS.HomogeneousY
theorem OAI.DefocusingNLS.homogeneousNonlinearRemainder_zero line 21

theorem OAI.DefocusingNLS.homogeneousNonlinearRemainder_physical line 26

Source documentation

The completed-space remainder is exactly the pointwise physical remainder.

theorem homogeneousNonlinearRemainder_physical (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ)
    (q v : HomogeneousY a k) (y : E) :
    homogeneousPhysicalCLM a k ha ha1 hk (homogeneousNonlinearRemainder a k ha ha1 hk m q v) y =
      oddPowerNonlinearity m
          (homogeneousPhysicalCLM a k ha ha1 hk q y + homogeneousPhysicalCLM a k ha ha1 hk v y) -
        oddPowerNonlinearity m (homogeneousPhysicalCLM a k ha ha1 hk q y) -
          oddPowerDerivative m (homogeneousPhysicalCLM a k ha ha1 hk q y)
            (homogeneousPhysicalCLM a k ha ha1 hk v y) := by
…

Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousPhysicalCLM, OAI.DefocusingNLS.homogeneousNonlinearRemainder, OAI.DefocusingNLS.oddPowerNonlinearity, OAI.DefocusingNLS.oddPowerDerivative

theorem OAI.DefocusingNLS.hasFDerivAt_homogeneousNonlinearRemainder line 39

theorem OAI.DefocusingNLS.exists_homogeneousNonlinearRemainder_lipschitz line 53

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_homogeneousNonlinearRemainder_lipschitz (a k : ℝ) (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ)
    (R : ℝ) (hR : 0 ≤ R) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ q v w : (HomogeneousY a k), ‖q‖ ≤ R → ‖v‖ ≤ 1 → ‖w‖ ≤ 1 →
      ‖homogeneousNonlinearRemainder a k ha ha1 hk m q v - homogeneousNonlinearRemainder a k ha ha1 hk m q w‖ ≤
        C * (‖v‖ + ‖w‖) * ‖v - w‖ := by
…

Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousNonlinearRemainder

theorem OAI.DefocusingNLS.exists_homogeneousNonlinearRemainder_quadratic line 82

Source documentation

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

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

Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousNonlinearRemainder