OAI/MathematicalPhysics/DefocusingNLS/Profile/SlowKernelEndpoint.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Removal of the singularity at the regularized integral's lower endpoint

  1. theorem OAI.DefocusingNLS.regularizedSlowKernel_norm_le line 14
  2. theorem OAI.DefocusingNLS.regularizedSlowKernel_isBigO_zero line 35

    Source documentation

    The regularized kernel is no worse than u ^ Re(q) at zero.

    theorem regularizedSlowKernel_isBigO_zero (q : ℂ) (m : ℕ) (x : ℂ) :
    regularizedSlowKernel q m x =O[𝓝[>] (0 : ℝ)] (fun u : ℝ => u ^ q.re) := by
…

    Mentions: OAI.DefocusingNLS.regularizedSlowKernel

  3. theorem OAI.DefocusingNLS.measurable_regularizedSlowKernel line 49
  4. theorem OAI.DefocusingNLS.regularizedSlowKernel_integrableAt_zero line 62

    Source documentation

    The lower endpoint is integrable throughout the half-plane required by the matching calculation.

    theorem regularizedSlowKernel_integrableAt_zero (q : ℂ) (m : ℕ) (x : ℂ)
    (hq : -1 < q.re) :
    IntegrableAtFilter (regularizedSlowKernel q m x) (𝓝[>] (0 : ℝ)) := by
…

    Mentions: OAI.DefocusingNLS.regularizedSlowKernel