HomogeneousHarmonicRadialEquation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The classical radial equation for an angular projection

The angular eigenfunction and its degree-zero extension are explicit data. The radial differential equation follows from Cartesian Green's identity; no completeness or spectral decomposition assumption is used.

theorem OAI.DefocusingNLS.harmonicAngularCoefficient_continuous line 22
theorem OAI.DefocusingNLS.test_and_derivatives_zero_nonpositive line 34
theorem OAI.DefocusingNLS.harmonicAngularCoefficient_weighted_laplacian line 45
theorem OAI.DefocusingNLS.compact_positive_test_integrable line 95
theorem OAI.DefocusingNLS.radial_laplacian_eq_of_weighted_tests line 104

theorem OAI.DefocusingNLS.homogeneous_harmonic_radial_laplacian line 164

Source documentation

The actual homogeneous-space physical realization satisfies the classical radial Laplacian identity in every explicit harmonic channel.

theorem homogeneous_harmonic_radial_laplacian
    (a k : ℝ) (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k)
    (u : HomogeneousY a k) (Y : 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)
    (r : ℝ) (hr : 0 < r) :
    harmonicAngularCoefficient Y (Δ (fun x : E => homogeneousPhysicalCLM a k ha ha1 hk u x)) r =
      deriv (deriv (harmonicAngularCoefficient Y (homogeneousPhysicalCLM a k ha ha1 hk u))) r +
      ((11 / r : ℝ) : ℂ) *
        deriv (harmonicAngularCoefficient Y (homogeneousPhysicalCLM a k ha ha1 hk u)) r -
      lam / (r ^ 2 : ℝ) *
…

Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.harmonicAngularCoefficient, OAI.DefocusingNLS.homogeneousPhysicalCLM