OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralScalarBoundaryNorm.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.spectralShellNorm_right_error line 11
2. theorem OAI.DefocusingNLS.spectralScalarGreen_boundary_norm line 17
3. theorem OAI.DefocusingNLS.spectralShellNorm_boundary_absorption line 42

   Source documentation

   Quantitative absorption form, with a separately bounded remote error and the small Green correction.

   theorem spectralShellNorm_boundary_absorption
       (k B eta G M : ℝ) (heta : 0≤ eta) (hM : 0≤ M)
       (q diagonal D U : ℂ × ℂ) (W error : ℂ) (correction : ℂ × ℂ)
       (hk : 0≤ k)
       (he : q-diagonal=((-U.1/W)*error) • D+correction)
       (hremote : spectralShellNorm k ((U.1/W) • D)≤ B)
       (herror : ‖error‖≤ eta*M) (hgreen : spectralShellNorm k correction≤ G*M) :
       spectralShellNorm k (q-diagonal)≤(eta*B+G)*M := by
   …

   Mentions: OAI.DefocusingNLS.spectralShellNorm