OAI/MathematicalPhysics/DefocusingNLS/Certificates/BoundaryEnclosureState.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DefocusingNLS.BoundaryCertificate.PolynomialState line 12
2. def OAI.DefocusingNLS.BoundaryCertificate.polynomialStep line 14
3. def OAI.DefocusingNLS.BoundaryCertificate.polynomialState line 19
4. def OAI.DefocusingNLS.BoundaryCertificate.EnclosesState line 24
5. theorem OAI.DefocusingNLS.BoundaryCertificate.step_sound line 28
6. theorem OAI.DefocusingNLS.BoundaryCertificate.state_sound line 44

   Source documentation

   Every coefficient enclosure is valid for the same actual parameter pair.

   theorem state_sound (ell : ℕ) (b Z : ℝ)
       (hb : |100000000 * b - 33477607| ≤ 2) (hZ : |100000000 * Z - 270506819| ≤ 2)
       (n : ℕ) : EnclosesState (state ell n) (polynomialState ell b Z n) := by
   …

   Mentions: OAI.DefocusingNLS.BoundaryCertificate.EnclosesState, OAI.DefocusingNLS.BoundaryCertificate.state, OAI.DefocusingNLS.BoundaryCertificate.polynomialState

7. theorem OAI.DefocusingNLS.BoundaryCertificate.determinant_sound line 59

   Source documentation

   The raw determinant enclosure bounds the coherent determinant before any reality, parity or degree truncation is applied.

   theorem determinant_sound (ell : ℕ) (b Z : ℝ)
       (hb : |100000000 * b - 33477607| ≤ 2) (hZ : |100000000 * Z - 270506819| ≤ 2) :
       let pq := polynomialState ell b Z 8
   …

   Mentions: OAI.DefocusingNLS.BoundaryCertificate.polynomialState