OddPowerMixedIncrement.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Mixed increments of the scalar odd-power nonlinearity

The extra factor of the increment preserves the decaying tail weight when the background profile varies at a fixed power.

theorem OAI.DefocusingNLS.exists_oddPower_derivative_lipschitz line 17

theorem OAI.DefocusingNLS.exists_oddPower_mixed_increment_bound line 49

Source documentation

For fixed power and a fixed bounded ball, varying the background changes the nonlinear increment by at most C * ‖f-g‖ * ‖h‖.

theorem exists_oddPower_mixed_increment_bound (m : ℕ) (M : ℝ) (hM : 0 ≤ M) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ f g h : ℂ, ‖f‖ ≤ M → ‖g‖ ≤ M → ‖h‖ ≤ M →
      ‖(oddPowerNonlinearity m (f + h) - oddPowerNonlinearity m f) -
        (oddPowerNonlinearity m (g + h) - oddPowerNonlinearity m g)‖ ≤
        C * ‖f - g‖ * ‖h‖ := by
…

Mentions: OAI.DefocusingNLS.oddPowerNonlinearity