OAI/MathematicalPhysics/DefocusingNLS/Certificates/BoundaryPositiveForm.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.BoundaryCertificate.rawBoundaryEntry line 13
2. theorem OAI.DefocusingNLS.BoundaryCertificate.rawBoundaryEntry_diagonal line 17
3. theorem OAI.DefocusingNLS.BoundaryCertificate.rawBoundaryEntry_continuous line 21
4. theorem OAI.DefocusingNLS.BoundaryCertificate.rawBoundaryEntry_determinant line 26
5. theorem OAI.DefocusingNLS.BoundaryCertificate.rawBoundaryEntry_leading_pos line 36
6. theorem OAI.DefocusingNLS.BoundaryCertificate.rawBoundaryEntry_pairForm_pos line 55

   Source documentation

   The finite boundary certificate yields a strictly positive quadratic form at every real frequency, uniformly throughout the parameter box.

   theorem rawBoundaryEntry_pairForm_pos (ell : Fin 4) (b Z v : ℝ)
       (hb : |100000000 * b - 33477607| ≤ 2) (hZ : |100000000 * Z - 270506819| ≤ 2)
       (u w : ℂ) (huw : u ≠ 0 ∨ w ≠ 0) :
       0 < hermitianPairForm (rawBoundaryEntry ell b Z v 0 0).re
         (rawBoundaryEntry ell b Z v 1 1).re (rawBoundaryEntry ell b Z v 0 1) u w := by
   …

   Mentions: OAI.DefocusingNLS.hermitianPairForm, OAI.DefocusingNLS.BoundaryCertificate.rawBoundaryEntry

7. theorem OAI.DefocusingNLS.BoundaryCertificate.evaluated_boundary_cones_pos line 65

   Source documentation

   A direct positivity statement for the two actual evaluated forward forms.

   theorem evaluated_boundary_cones_pos (ell : Fin 4) (b Z v : ℝ)
       (hb : |100000000 * b - 33477607| ≤ 2) (hZ : |100000000 * Z - 270506819| ≤ 2)
       (w : Fin 2 → ℂ) (hw : w ≠ 0) :
       0 < matrixCone (scaledMass ell) (scaledShift Z)
         (fun i j => ((stateMatrix (polynomialState ell b Z 8)) i j).eval (v : ℂ)) w +
         matrixCone (scaledMass ell) (star (scaledShift Z))
         (fun i j => star (((stateMatrix (polynomialState ell b Z 8)) i j).eval
           ((-v : ℝ) : ℂ))) w := by
   …

   Mentions: OAI.DefocusingNLS.matrixCone, OAI.DefocusingNLS.BoundaryCertificate.scaledMass, OAI.DefocusingNLS.BoundaryCertificate.scaledShift, OAI.DefocusingNLS.BoundaryCertificate.stateMatrix, OAI.DefocusingNLS.BoundaryCertificate.polynomialState