OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralScalarGreen.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The scalar Dirichlet/outgoing Green formula used on the high-frequency shell. The sign of its diagonal jump is recorded explicitly.

  1. def OAI.DefocusingNLS.spectralScalarWronskian line 13
  2. def OAI.DefocusingNLS.spectralScalarField line 16
  3. def OAI.DefocusingNLS.spectralScalarGreenState line 19
  4. theorem OAI.DefocusingNLS.spectralScalarWronskian_hasDerivAt line 23
  5. theorem OAI.DefocusingNLS.spectralScalarGreenState_jump line 40
  6. theorem OAI.DefocusingNLS.spectralScalarGreenState_left line 49
  7. theorem OAI.DefocusingNLS.spectralScalarGreenState_right line 54
  8. theorem OAI.DefocusingNLS.spectralScalarGreen_variation line 64

    Source documentation

    Variation of constants with the Dirichlet and outgoing scalar solutions. The two derivatives of the scalar primitives cancel in the value component.

    theorem spectralScalarGreen_variation
    (D U : ℝ → ℂ × ℂ) (A B : ℝ → ℂ) (V W f : ℂ) (r : ℝ)
    (hW : W ≠ 0) (hdet : spectralScalarWronskian (D r) (U r)=W)
    (hD : HasDerivAt D (spectralScalarField V (D r)) r)
    (hU : HasDerivAt U (spectralScalarField V (U r)) r)
    (hA : HasDerivAt A ((D r).1*f/W) r)
    (hB : HasDerivAt B (-((U r).1*f/W)) r) :
    HasDerivAt (fun t => A t • U t + B t • D t)
      (spectralScalarField V (A r • U r + B r • D r) + (0,f)) r := by
…

    Mentions: OAI.DefocusingNLS.spectralScalarWronskian, OAI.DefocusingNLS.spectralScalarField