OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousInhomogeneousChannels.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Classical inhomogeneous channels for the actual generator

The same physical differential expression acts on every strong generator vector. In particular this identifies the forcing in finite-dimensional Jordan chains, rather than only homogeneous eigenvector equations.

  1. theorem OAI.DefocusingNLS.laplacian_channel_add line 21

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousEigenfunctionPDE.lean:20 (same declaration text).

  2. theorem OAI.DefocusingNLS.fderiv_channel_add line 31

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousEigenfunctionPDE.lean:30 (same declaration text).

  3. theorem OAI.DefocusingNLS.laplacian_channel_star line 39

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousEigenfunctionPDE.lean:38 (same declaration text).

  4. theorem OAI.DefocusingNLS.fderiv_channel_star line 44

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousEigenfunctionPDE.lean:43 (same declaration text).

  5. theorem OAI.DefocusingNLS.homogeneous_generator_classical_channels line 51

    Source documentation

    The strong derivative of the actual complexified flow is precisely the two-channel physical differential expression.

    theorem homogeneous_generator_classical_channels (a b k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ)
    (q : HomogeneousY a k) (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) :
    let P := fun f : HomogeneousY a k =>
…

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