OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousEigenfunctionPDE.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The two classical channels of an actual semigroup eigenvector

The complexification used by the spectral argument has two physical channels. An eigenvector of the actual evolution satisfies their coupled elliptic equations; the required C² regularity follows from membership in Y with k > 8.

  1. theorem OAI.DefocusingNLS.laplacian_channel_add line 20

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousInhomogeneousChannels.lean:21 (same declaration text).

  2. theorem OAI.DefocusingNLS.fderiv_channel_add line 30

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousInhomogeneousChannels.lean:31 (same declaration text).

  3. theorem OAI.DefocusingNLS.laplacian_channel_star line 38

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousInhomogeneousChannels.lean:39 (same declaration text).

  4. theorem OAI.DefocusingNLS.fderiv_channel_star line 43

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousInhomogeneousChannels.lean:44 (same declaration text).

  5. theorem OAI.DefocusingNLS.homogeneous_eigenvector_classical_channels line 50

    Source documentation

    A semigroup eigenvector has the actual two-channel classical PDE, with coefficients obtained from the derivative of the odd-power nonlinearity.

    theorem homogeneous_eigenvector_classical_channels (a b k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ)
    (q : HomogeneousY a k) (lam : ℂ) (w : HomogeneousY a k × HomogeneousY a k)
    (hw : ∀ t : ℝ≥0, homogeneousComplexLinearizedStep a b k ha ha1 hk m q t w =
      Complex.exp (((t : ℝ) : ℂ) * lam) • w) :
    let P := fun f : HomogeneousY a k =>
…

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