SobolevSecondDerivativeBounds.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform second-derivative bounds for the actual Sobolev nonlinearity

theorem OAI.DefocusingNLS.linear_two_jet_bound line 13
theorem OAI.DefocusingNLS.bilinear_two_jet_bound line 34

theorem OAI.DefocusingNLS.exists_sobolevOddPower_two_jet_bound line 66

Source documentation

All derivatives of order at most two are uniformly bounded on a Sobolev ball. The proof uses the polynomial's actual bounded bilinear operations.

theorem exists_sobolevOddPower_two_jet_bound (k : ℝ) (hk : 6 < k) (m : ℕ)
    (R : ℝ) (hR : 0 ≤ R) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ f : FourierL2, ‖f‖ ≤ R → ∀ n : ℕ, n ≤ 2 →
      ‖iteratedFDeriv ℝ n (sobolevOddPower k hk m) f‖ ≤ C := by
…

Mentions: OAI.DefocusingNLS.FourierL2

theorem OAI.DefocusingNLS.exists_sobolevOddPower_derivative_lipschitz line 90

Source documentation

The real Fréchet derivative of the Sobolev odd-power map is uniformly Lipschitz on balls.

theorem exists_sobolevOddPower_derivative_lipschitz (k : ℝ) (hk : 6 < k) (m : ℕ)
    (R : ℝ) (hR : 0 ≤ R) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ f g : FourierL2, ‖f‖ ≤ R → ‖g‖ ≤ R →
      ‖fderiv ℝ (sobolevOddPower k hk m) f - fderiv ℝ (sobolevOddPower k hk m) g‖ ≤
        C * ‖f - g‖ := by
…

Mentions: OAI.DefocusingNLS.FourierL2