HomogeneousHarmonicTestCalculus.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Cartesian calculus for a radial test times a spherical harmonic

The degree-zero extension of the spherical harmonic is kept explicit: its Euler derivative is zero and its Cartesian Laplacian is the spherical eigenvalue divided by the squared radius. All formulas are local away from zero.

theorem OAI.DefocusingNLS.second_directional_complex_mul_at line 20
theorem OAI.DefocusingNLS.laplacian_complex_mul_at line 52
theorem OAI.DefocusingNLS.radial_basis_derivative_contraction line 62

theorem OAI.DefocusingNLS.radialSquare_harmonic_test_euler line 69

Source documentation

The dilation derivative of the same test contains no angular term.

theorem radialSquare_harmonic_test_euler (q : ℝ → ℂ) (Y : E → ℂ)
    (x : E) (hq : DifferentiableAt ℝ q (‖x‖ ^ 2))
    (hY : DifferentiableAt ℝ Y x) (hEuler : fderiv ℝ Y x x = 0) :
    fderiv ℝ (fun y : E => q (‖y‖ ^ 2) * Y y) x x =
      ((2 * ‖x‖ ^ 2 : ℝ) : ℂ) * deriv q (‖x‖ ^ 2) * Y x := by
…

theorem OAI.DefocusingNLS.radialSquare_harmonic_test_laplacian line 83

Source documentation

The Laplacian of a squared-radius test times a degree-zero harmonic extension. Here λ is the spherical eigenvalue ell(ell+10).

theorem radialSquare_harmonic_test_laplacian (q : ℝ → ℂ) (Y : E → ℂ)
    (x : E) (lam : ℂ) (hq : ContDiffAt ℝ 2 q (‖x‖ ^ 2))
    (hY : ContDiffAt ℝ 2 Y x) (hEuler : fderiv ℝ Y x x = 0)
    (hEigen : Δ Y x = -(lam / (‖x‖ ^ 2 : ℝ)) * Y x) :
    Δ (fun y : E => q (‖y‖ ^ 2) * Y y) x =
      (((4 * ‖x‖ ^ 2 : ℝ) : ℂ) * deriv (deriv q) (‖x‖ ^ 2) +
        24 * deriv q (‖x‖ ^ 2) - lam / (‖x‖ ^ 2 : ℝ) * q (‖x‖ ^ 2)) * Y x := by
…

theorem OAI.DefocusingNLS.zero_euler_of_ray_constant line 111

Source documentation

Constancy on positive rays gives the zero Euler derivative used above.

theorem zero_euler_of_ray_constant (Y : E → ℂ) (x : E)
    (hY : DifferentiableAt ℝ Y x)
    (hRay : ∀ t : ℝ, 0 < t → Y (t • x) = Y x) : fderiv ℝ Y x x = 0 := by
…