OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialGreenEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The exact radial weighted Green identity for the matched profile.

  1. def OAI.DefocusingNLS.radialMassLaplacian line 15

    Source documentation

    The mass density times the scalar weighted Laplace operator, in its nonsingular divergence form.

    noncomputable def radialMassLaplacian (n : ℕ) (z : ProfileMatchingBall)
    (f : ℝ → ℝ) (r : ℝ) : ℝ :=
…
  2. theorem OAI.DefocusingNLS.radialMassLaplacian_logarithmic line 19
  3. theorem OAI.DefocusingNLS.radialMatched_Green_bilinear line 30
  4. theorem OAI.DefocusingNLS.radialMatched_Green_energy line 67