OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialDirichletKernel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The nonsingular radial Green kernel in dimension twelve.

  1. def OAI.DefocusingNLS.radialAverage line 11
  2. def OAI.DefocusingNLS.radialDirichletKernel line 16

    Source documentation

    This is the regular form of ∫ t in r..R, t⁻¹¹ * ∫ s in 0..t, s¹¹*f s.

    noncomputable def radialDirichletKernel (R : ℝ) (f : ℝ → ℝ) (r : ℝ) : ℝ :=
…
  3. theorem OAI.DefocusingNLS.radialAverage_nonneg line 19
  4. theorem OAI.DefocusingNLS.radialAverage_norm_le line 25
  5. theorem OAI.DefocusingNLS.radialDirichletKernel_norm_le line 44
  6. theorem OAI.DefocusingNLS.radialDirichletKernel_boundary line 64