OAI/MathematicalPhysics/DefocusingNLS/Profile/SlowKernelDomination.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

An integrable majorant uniform in the spatial parameter

  1. theorem OAI.DefocusingNLS.one_add_div_rpow_le line 11
  2. theorem OAI.DefocusingNLS.one_add_real_div_bounds_of_re line 30
  3. theorem OAI.DefocusingNLS.integrable_exp_neg_mul_rpow line 48
  4. theorem OAI.DefocusingNLS.slowKernelSpatialDerivative_majorant line 53
  5. theorem OAI.DefocusingNLS.exists_slowKernelSpatialDerivative_majorant line 106

    Source documentation

    Spatial derivatives have a single integrable majorant on each closed right half-plane away from zero.

    theorem exists_slowKernelSpatialDerivative_majorant (q : ℂ) (m : ℕ)
    (hq : -1 < q.re) (c : ℝ) (hc : 0 < c) :
    ∃ bound : ℝ → ℝ, IntegrableOn bound (Set.Ioi 0) ∧
      ∀ x : ℂ, c ≤ x.re → ∀ u : ℝ, 0 < u → ‖slowKernelSpatialDerivative q m x u‖ ≤ bound u := by
…

    Mentions: OAI.DefocusingNLS.slowKernelSpatialDerivative