OAI/MathematicalPhysics/DefocusingNLS/Certificates/BoundaryCertificatePositivity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.BoundaryCertificate.row_zero_first_positive line 8

   Source documentation

   Exact positivity of the first transformed boundary enclosure.

   theorem row_zero_first_positive : positiveFirst16 (transformed 0 0 1 1) = true := by
   …

   Mentions: OAI.DefocusingNLS.BoundaryCertificate.positiveFirst16, OAI.DefocusingNLS.BoundaryCertificate.transformed

2. theorem OAI.DefocusingNLS.BoundaryCertificate.row_zero_second_positive line 11
3. theorem OAI.DefocusingNLS.BoundaryCertificate.row_zero_third_positive line 12
4. theorem OAI.DefocusingNLS.BoundaryCertificate.row_one_first_positive line 14
5. theorem OAI.DefocusingNLS.BoundaryCertificate.row_one_second_positive line 15
6. theorem OAI.DefocusingNLS.BoundaryCertificate.row_one_third_positive line 16
7. theorem OAI.DefocusingNLS.BoundaryCertificate.row_two_first_positive line 18
8. theorem OAI.DefocusingNLS.BoundaryCertificate.row_two_second_positive line 19
9. theorem OAI.DefocusingNLS.BoundaryCertificate.row_two_third_positive line 20
10. theorem OAI.DefocusingNLS.BoundaryCertificate.row_three_first_positive line 22
11. theorem OAI.DefocusingNLS.BoundaryCertificate.row_three_second_positive line 23
12. theorem OAI.DefocusingNLS.BoundaryCertificate.row_three_third_positive line 24