ComplexPolynomialContinuity

Complex polynomial continuity with no admitted analytic premises

Open in Workbench View on GitHub

1-- Complex polynomial continuity with no admitted analytic premises.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 ComplexPolynomialContinuityExample9import Grace.Cumulus.Complex.Continuity1011theorem everywhere (cs : List(complexCarrier))12  shows ComplexContinuous(complexPolynomial(cs))13proof14  exact complexPolynomial.continuous with *1516theorem at_point (a : Set) (cs : List(complexCarrier))17  requires center : a ∈ complexCarrier18  shows ComplexContinuousAt(complexPolynomial(cs), a)19proof20  exact complexPolynomial.continuous_at with *2122theorem small_product (e b t : Real)23  requires epsilon : 0 < e24  requires nonnegative : 0 ≤ t25  requires small : t < scaledRadius(e, limitScale(b))26  shows t * b < e27proof28  exact scaledRadius.product_control with *2930section Geometry31notation ring C := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)3233theorem distance (z w : Set)34  requires first : z ∈ C35  requires second : w ∈ C36  shows complexNormSquared(C[z - w]) = Euclidean.distanceSquared(z, w)37proof38  exact complexNormSquared.difference_distance with *3940end Geometry41