SobolevPolynomialBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform polynomial bounds on Sobolev balls

theorem OAI.DefocusingNLS.norm_sobolevProduct_sub_le line 10

Source documentation

The bilinear difference estimate in the Sobolev algebra.

theorem norm_sobolevProduct_sub_le (k : ℝ) (hk : 6 < k)
    (u v u' v' : FourierL2) :
    ‖sobolevProduct k hk u v - sobolevProduct k hk u' v'‖ ≤
      ‖sobolevBilinearProduct k hk‖ *
        (‖u - u'‖ * ‖v‖ + ‖u'‖ * ‖v - v'‖) := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.sobolevBilinearProduct

theorem OAI.DefocusingNLS.exists_sobolevOddPower_ball_bounds line 28

Source documentation

Polynomial bounds are uniform on every norm ball, including in infinite dimension.

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

Mentions: OAI.DefocusingNLS.FourierL2