OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousRadialSquareTest.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Every annular test is a smooth test of the squared radius

The scalar test vanishes near zero, so its square-root pullback is smooth on the whole line. This removes the squared-radius restriction in the Cartesian-to-radial weak Laplacian identity.

  1. def OAI.DefocusingNLS.radialSquarePullback line 19
  2. theorem OAI.DefocusingNLS.radialSquarePullback_contDiff line 22
  3. theorem OAI.DefocusingNLS.tsupport_radialSquarePullback line 38
  4. theorem OAI.DefocusingNLS.radialSquarePullback_hasCompactSupport line 46
  5. def OAI.DefocusingNLS.radialSquareSchwartz line 64
  6. theorem OAI.DefocusingNLS.radialSquareSchwartz_apply line 69
  7. theorem OAI.DefocusingNLS.radialSquareSchwartz_square line 73
  8. theorem OAI.DefocusingNLS.radialSquareSchwartz_derivatives line 79

    Source documentation

    Exact derivative conversion, without dividing at the origin.

    theorem radialSquareSchwartz_derivatives (φ : 𝓢(ℝ, ℂ))
    (hc : HasCompactSupport φ) (hs : tsupport φ ⊆ Ioi (0 : ℝ))
    (r : ℝ) (hr : 0 < r) :
    deriv φ r = ((2 * r : ℝ) : ℂ) * deriv (radialSquareSchwartz φ hc hs) (r ^ 2) ∧
    deriv (deriv φ) r = ((4 * r ^ 2 : ℝ) : ℂ) *
      deriv (deriv (radialSquareSchwartz φ hc hs)) (r ^ 2) +
        2 * deriv (radialSquareSchwartz φ hc hs) (r ^ 2) := by
…

    Mentions: OAI.DefocusingNLS.radialSquareSchwartz

  9. theorem OAI.DefocusingNLS.radialSquareSchwartz_laplacian_test line 111