HomogeneousHarmonicWeakLaplacian.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The angular projection of the classical Laplacian, in weak radial form

The only angular assumptions are the explicit degree-zero homogeneity and spherical Laplacian eigenfunction identities. The function being projected is an arbitrary C² Cartesian function.

def OAI.DefocusingNLS.harmonicAngularCoefficient line 21
theorem OAI.DefocusingNLS.integral_eq_polar_iterated line 24

theorem OAI.DefocusingNLS.harmonicAngularCoefficient_weak_laplacian line 40

Source documentation

The weak radial Laplacian identity in dimension twelve. Squared-radius tests suffice locally, and avoid any artificial derivative at the origin.

theorem harmonicAngularCoefficient_weak_laplacian
    (Y F : E → ℂ) (lam : ℂ)
    (hY : ∀ x : E, x ≠ 0 → ContDiffAt ℝ ∞ Y x)
    (hRay : ∀ (x : E) (t : ℝ), 0 < t → Y (t • x) = Y x)
    (hEigen : ∀ x : E, x ≠ 0 → Δ Y x = -(lam / (‖x‖ ^ 2 : ℝ)) * Y x)
    (hF : ContDiff ℝ 2 F)
    (ψ : 𝓢(ℝ, ℂ)) (hc : HasCompactSupport ψ) (hs : tsupport ψ ⊆ Ioi (0 : ℝ)) :
    (∫ r : PhysicalPositiveRadius, ψ (r.1 ^ 2) *
      harmonicAngularCoefficient Y (Δ F) r ∂physicalRadiusMeasure) =
    ∫ r : PhysicalPositiveRadius,
      (((4 * r.1 ^ 2 : ℝ) : ℂ) * deriv (deriv ψ) (r.1 ^ 2) +
        24 * deriv ψ (r.1 ^ 2) - lam / (r.1 ^ 2 : ℝ) * ψ (r.1 ^ 2)) *
…

Mentions: OAI.DefocusingNLS.PhysicalPositiveRadius, OAI.DefocusingNLS.harmonicAngularCoefficient, OAI.DefocusingNLS.physicalRadiusMeasure