HomogeneousHarmonicChannels.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual generator vectors satisfy the projected radial system

The source is the actual strong generator derivative. Thus the same result applies both to eigenvectors and to the inhomogeneous vectors in Jordan chains.

theorem OAI.DefocusingNLS.homogeneous_harmonic_project_equation line 19

theorem OAI.DefocusingNLS.homogeneous_generator_harmonic_channels line 63

Source documentation

The strong generator equation becomes the exact two-channel radial system under every explicit spherical harmonic test.

theorem homogeneous_generator_harmonic_channels (a b k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ)
    (q : HomogeneousY a k) (Q : ℝ → ℂ)
    (hq : ∀ x : E, homogeneousPhysicalCLM a k ha ha1 hk q x = Q ‖x‖)
    (w z : HomogeneousY a k × HomogeneousY a k)
    (hw : HasDerivWithinAt (fun t : ℝ =>
      homogeneousComplexLinearizedStep a b k ha ha1 hk m q t.toNNReal w) z (Ici 0) 0)
    (Y : E → ℂ) (eta : ℂ)
    (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 = -(eta / (‖x‖ ^ 2 : ℝ)) * Y x) :
    let P := fun f : HomogeneousY a k => fun x : E => homogeneousPhysicalCLM a k ha ha1 hk f x
…

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