OAI/MathematicalPhysics/DefocusingNLS/Certificates/BoundaryHornerEvaluation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Degree and rational-substitution identity for the chart transform

  1. def OAI.DefocusingNLS.BoundaryCertificate.coefficientPolynomial line 12
  2. theorem OAI.DefocusingNLS.BoundaryCertificate.chartNumerator_degree line 16
  3. theorem OAI.DefocusingNLS.BoundaryCertificate.chartDenominator_degree line 21
  4. theorem OAI.DefocusingNLS.BoundaryCertificate.homogeneousHorner_cons_degree line 26
  5. theorem OAI.DefocusingNLS.BoundaryCertificate.homogeneousHorner_degree line 38
  6. theorem OAI.DefocusingNLS.BoundaryCertificate.homogeneousHorner_eval line 44
  7. theorem OAI.DefocusingNLS.BoundaryCertificate.homogeneousHorner_positive line 68

    Source documentation

    Each of the three exact certificate charts is strictly positive on its nonnegative parameter half-line, throughout the actual parameter box.

    theorem homogeneousHorner_positive (ell : Fin 4) (b Z w : ℝ)
    (hb : |100000000 * b - 33477607| ≤ 2) (hZ : |100000000 * Z - 270506819| ≤ 2)
    (hw : 0 ≤ w) (U V J : ℤ)
    (hcert : positiveFirst16 (transformed ell U V J) = true) :
    0 < ((homogeneousHorner U V J (evenValues ell b Z)).eval (w : ℂ)).re := by
…

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