ComplexPolynomialBounds

Quantitative complex polynomial bounds, without Choice or square roots

Open in Workbench View on GitHub

1-- Quantitative complex polynomial bounds, without Choice or square roots.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67-- Copyright (c) 2026 Grant Passmore. Apache License 2.0.8module ComplexPolynomialBoundsExample9import Grace.Cumulus.Complex.PolynomialBounds1011section Bounds12notation ring C := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)13notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)1415theorem evaluate (leading z : Set) (radius : Real) (cs : List(complexCarrier))16  requires initial : leading ∈ C17  requires element : z ∈ C18  requires nonnegative : realZero ≤ radius19  requires within : complexNormSquared(z) ≤ radius20  shows complexNormSquared(hornerAt{complexCarrier}(complexAdd, complexMul, leading, z, cs)) ≤ complexHornerBound(leading, radius, cs)21proof22  exact complexHornerBound.bounds with *2324theorem bounded (radius : Real) (cs : List(complexCarrier))25  requires nonnegative : realZero ≤ radius26  shows ∃ bound ∈ ℝ, realZero ≤ bound ∧ (∀ z ∈ C, complexNormSquared(z) ≤ radius → complexNormSquared(complexPolynomial(cs)(z)) ≤ bound)27proof28  exact complexPolynomial.bounded_on_disk with *2930-- For each fixed center a, one constant controls every x in the disk.31theorem difference (a c : Set) (radius : Real) (cs : List(complexCarrier))32  requires center : a ∈ C33  requires coefficient : c ∈ C34  requires nonnegative : realZero ≤ radius35  shows ∃ bound ∈ ℝ, realZero ≤ bound ∧ (∀ x ∈ C, complexNormSquared(x) ≤ radius → complexNormSquared(C[complexPolynomial(c :: cs)(x) - complexPolynomial(c :: cs)(a)]) ≤ R[complexNormSquared(C[x - a]) * bound])36proof37  exact complexPolynomial.difference_bound_on_disk with *3839end Bounds40