OAI/MathematicalPhysics/DefocusingNLS/Certificates/PolynomialEnclosure.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Polynomial semantics for integer coefficient enclosures

Lists are in ascending coefficient order. The recursive semantics keeps all roundoff radii, including those of coefficients whose centers cancel.

  1. def OAI.DefocusingNLS.GaussianEnclosure.zero line 17
  2. theorem OAI.DefocusingNLS.GaussianEnclosure.zero_sound line 19
  3. theorem OAI.DefocusingNLS.GaussianEnclosure.zero_encloses_iff line 21
  4. def OAI.DefocusingNLS.GaussianEnclosure.EnclosesPolynomial line 25

    Source documentation

    An enclosure for every coefficient, with exact zero beyond the list.

    def EnclosesPolynomial : List GaussianEnclosure → Polynomial ℂ → Prop
  | [], p => p = 0
  | a :: as, p => ∃ z q, a.Encloses z ∧ EnclosesPolynomial as q ∧ p = C z + X * q

    Mentions: OAI.DefocusingNLS.GaussianEnclosure

  5. def OAI.DefocusingNLS.GaussianEnclosure.addPolynomial line 29
  6. def OAI.DefocusingNLS.GaussianEnclosure.scalePolynomial line 34
  7. def OAI.DefocusingNLS.GaussianEnclosure.mulPolynomial line 37
  8. def OAI.DefocusingNLS.GaussianEnclosure.negPolynomial line 41
  9. def OAI.DefocusingNLS.GaussianEnclosure.subPolynomial line 43
  10. def OAI.DefocusingNLS.GaussianEnclosure.conjPolynomial line 46
  11. theorem OAI.DefocusingNLS.GaussianEnclosure.addPolynomial_sound line 48
  12. theorem OAI.DefocusingNLS.GaussianEnclosure.scalePolynomial_sound line 69
  13. theorem OAI.DefocusingNLS.GaussianEnclosure.shiftPolynomial_sound line 83
  14. theorem OAI.DefocusingNLS.GaussianEnclosure.mulPolynomial_sound line 87
  15. theorem OAI.DefocusingNLS.GaussianEnclosure.negPolynomial_sound line 103
  16. theorem OAI.DefocusingNLS.GaussianEnclosure.subPolynomial_sound line 116
  17. theorem OAI.DefocusingNLS.GaussianEnclosure.conjPolynomial_sound line 121
  18. theorem OAI.DefocusingNLS.GaussianEnclosure.coefficient_sound line 133
  19. theorem OAI.DefocusingNLS.GaussianEnclosure.enclosesPolynomial_of_coefficients line 149

    Source documentation

    Coefficientwise semantics permits truncation only when the actual discarded coefficients vanish, regardless of the size of their computed radii.

    theorem enclosesPolynomial_of_coefficients (as : List GaussianEnclosure) (p : Polynomial ℂ)
    (h : ∀ n, (as[n]?.getD zero).Encloses (p.coeff n)) : EnclosesPolynomial as p := by
…

    Mentions: OAI.DefocusingNLS.GaussianEnclosure, OAI.DefocusingNLS.GaussianEnclosure.zero, OAI.DefocusingNLS.GaussianEnclosure.Encloses, OAI.DefocusingNLS.GaussianEnclosure.EnclosesPolynomial

  20. theorem OAI.DefocusingNLS.GaussianEnclosure.enclosesPolynomial_iff_coefficients line 164
  21. theorem OAI.DefocusingNLS.GaussianEnclosure.truncatePolynomial_sound line 168