OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousHarmonicTestSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Compact annular harmonic tests

A compact scalar test in the positive squared radius removes the apparent singularity of a degree-zero angular extension at the origin.

  1. def OAI.DefocusingNLS.squaredHarmonicTest line 19
  2. theorem OAI.DefocusingNLS.squaredHarmonicTest_contDiff line 22
  3. theorem OAI.DefocusingNLS.squaredHarmonicTest_hasCompactSupport line 44
  4. def OAI.DefocusingNLS.squaredHarmonicSchwartz line 63

    Source documentation

    The actual Schwartz test used in the Cartesian weak equation.

    noncomputable def squaredHarmonicSchwartz (ψ : 𝓢(ℝ, ℂ)) (Y : E → ℂ)
    (hc : HasCompactSupport ψ) (hs : tsupport ψ ⊆ Ioi (0 : ℝ))
    (hY : ∀ x : E, x ≠ 0 → ContDiffAt ℝ ∞ Y x) : 𝓢(E, ℂ) :=
…
  5. theorem OAI.DefocusingNLS.squaredHarmonicSchwartz_apply line 69