OAI/MathematicalPhysics/DefocusingNLS/Certificates/RegularizedSlowSolution.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The regularized integral defining the outgoing slow solution

The integral in Lemma free:slow, specialized to integer m, subtracts a constant from the bracket to remove one order of the endpoint singularity.

  1. def OAI.DefocusingNLS.regularizingBracket line 19
  2. theorem OAI.DefocusingNLS.hasDerivAt_regularizingBracket line 21
  3. theorem OAI.DefocusingNLS.regularizingBracket_isBigO line 32

    Source documentation

    The precise endpoint cancellation needed before proving integrability.

    theorem regularizingBracket_isBigO (r x : ℂ) :
    regularizingBracket r x =O[𝓝 0] (fun u : ℂ => u) := by
…

    Mentions: OAI.DefocusingNLS.regularizingBracket

  4. def OAI.DefocusingNLS.regularizedSlowKernel line 39

    Source documentation

    The manuscript's regularized Laplace representation.

    def regularizedSlowKernel (q : ℂ) (m : ℕ) (x : ℂ) (u : ℝ) : ℂ :=
…
  5. def OAI.DefocusingNLS.regularizedSlowSolution line 43
  6. theorem OAI.DefocusingNLS.regularizedSlowSolution_zero line 47
  7. theorem OAI.DefocusingNLS.hasDerivAt_regularizedSlowSolution_zero line 51