OAI/MathematicalPhysics/DefocusingNLS/Certificates/BoundaryPositiveEvaluation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Positive evaluation from the exact coefficient checks

  1. theorem OAI.DefocusingNLS.BoundaryCertificate.positiveFirst16_spec line 13
  2. theorem OAI.DefocusingNLS.BoundaryCertificate.positiveFirst16_coefficients line 20
  3. theorem OAI.DefocusingNLS.BoundaryCertificate.eval_re_eq_sum16 line 25
  4. theorem OAI.DefocusingNLS.BoundaryCertificate.positive_eval_of_positiveFirst16 line 41

    Source documentation

    Every nonnegative evaluation is positive, including the constant endpoint.

    theorem positive_eval_of_positiveFirst16 (as : EnclosurePolynomial) (p : Polynomial ℂ)
    (h : positiveFirst16 as = true) (hp : EnclosesPolynomial as p)
    (hdeg : p.natDegree ≤ 15) (w : ℝ) (hw : 0 ≤ w) : 0 < (p.eval (w : ℂ)).re := by
…

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