Grace/Cumulus/Complex/PolynomialBounds.g17

Open in Workbench Download source

Imports

PolynomialMinimum

Declarations

Source

1-- Explicit squared-modulus bounds for complex Horner evaluation, in ZF.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 Passmore67module Grace.Cumulus.Complex.PolynomialBounds8import PolynomialMinimum910def complexBoundStep (c : Euclidean.Point) (radius bound : Real) : Real :=11  (2:R) * (complexNormSquared(c) + radius * bound)1213-- The radius bounds squared modulus, so no square-root construction is needed.14def complexHornerBound (leading radius : Set) (cs : List(complexCarrier)) → Set15  | leading, radius, List.nil => complexNormSquared(leading)16  | leading, radius, List.cons(c, tail) => complexBoundStep(c, radius, complexHornerBound(leading, radius, tail))17  descends cs1819theorem realLe.double_bound (a b : Real)20  requires bound : a ≤ b21  shows ((2:R) * a) ≤ ((2:R) * b)22proof23  have doubled := realLe.add with *24  have left : (a + a) = ((2:R) * a) by ring25  have right : (b + b) = ((2:R) * b) by ring26  rwa [left, right] at doubled2728theorem realLe.two_sum_nonnegative (a b : Real)29  requires first : realZero ≤ a30  requires second : realZero ≤ b31  shows realZero ≤ ((2:R) * (a + b))32proof33  have sum := realLe.add at realZero, a, realZero, b with *34  rw realAddValue.zero_left at sum35  have doubled := realLe.double_bound at realZero, (a + b) with *36  rwa realMulValue.zero_right at doubled3738section Estimates39notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)40notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)414243theorem complexHornerBound.data (leading : Set) (radius : Real) (cs : List(complexCarrier))44  requires initial : leading ∈ ℂ45  requires radiusNonnegative : realZero ≤ radius46  shows Real(complexHornerBound(leading, radius, cs)) ∧ realZero ≤ complexHornerBound(leading, radius, cs)47proof48  induction cs49  | List.nil =>50    rw complexHornerBound51    have real := complexNormSquared.real with *52    have nonnegative := complexNormSquared.nonnegative with *53    refine ⟨real, nonnegative⟩54  | List.cons(c, tail) using ih =>55    have member : c ∈ ℂ by assumption56    have nonnegative := complexNormSquared.nonnegative with member57    have product := realMulValue.nonnegative at radius, complexHornerBound(leading, radius, tail) with *58    rw complexHornerBound59    constructor60    . unfold complexBoundStep61      typecheck62    . unfold complexBoundStep63      exact realLe.two_sum_nonnegative at complexNormSquared(c), R[radius * complexHornerBound(leading, radius, tail)] with *6465theorem complexNormSquared.mul_bound (z w : Set) (radius bound : Real)66  requires first : z ∈ ℂ67  requires second : w ∈ ℂ68  requires radiusNonnegative : realZero ≤ radius69  requires zBound : complexNormSquared(z) ≤ radius70  requires wBound : complexNormSquared(w) ≤ bound71  shows complexNormSquared(ℂ[z * w]) ≤ R[radius * bound]72proof73  have wNonnegative := complexNormSquared.nonnegative at w with *74  have firstBound := realLe.mul_right_of_nonnegative at complexNormSquared(z), radius, complexNormSquared(w) with *75  have secondBound := realLe.mul_left_of_nonnegative at complexNormSquared(w), bound, radius with *76  rw complexNormSquared.mul77  exact realLe.transitive with *7879theorem complexNormSquared.horner_step_bound (c z w : Set) (radius bound : Real)80  requires coefficient : c ∈ ℂ81  requires first : z ∈ ℂ82  requires second : w ∈ ℂ83  requires radiusNonnegative : realZero ≤ radius84  requires zBound : complexNormSquared(z) ≤ radius85  requires wBound : complexNormSquared(w) ≤ bound86  shows complexNormSquared(ℂ[c + z * w]) ≤ R[2 * (complexNormSquared(c) + radius * bound)]87proof88  have field := complexes.is_field89  have ring := IsField.comm_ring with field90  have ordinary := IsCommRing.ring with ring91  have product := IsRing.mul_closed with ordinary, first, second92  have sum := IsRing.add_closed with ordinary, coefficient, product93  have estimate := complexNormSquared.mul_bound at z, w, radius, bound with *94  have addition := complexNormSquared.add_bound at c, ℂ[z * w] with *95  have translated := realLe.add_left at complexNormSquared(ℂ[z * w]), R[radius * bound], complexNormSquared(c) with *96  have doubled := realLe.double_bound at R[complexNormSquared(c) + complexNormSquared(ℂ[z * w])], R[complexNormSquared(c) + radius * bound] with *97  exact realLe.transitive with *9899theorem complexHornerBound.bounds (leading z : Set) (radius : Real) (cs : List(complexCarrier))100  requires initial : leading ∈ ℂ101  requires element : z ∈ ℂ102  requires radiusNonnegative : realZero ≤ radius103  requires within : complexNormSquared(z) ≤ radius104  shows complexNormSquared(hornerAt{complexCarrier}(complexAdd, complexMul, leading, z, cs)) ≤ complexHornerBound(leading, radius, cs)105proof106  have field := complexes.is_field107  have ring := IsField.comm_ring with field108  induction cs109  | List.nil =>110    rw [hornerAt.nil, complexHornerBound]111    exact realLe.reflexive with *112  | List.cons(c, tail) using ih =>113    have coefficient : c ∈ ℂ by assumption114    have value := hornerAt.closed at complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne, leading, z, tail with *115    have data := complexHornerBound.data at leading, radius, tail with *116    have bound := complexNormSquared.horner_step_bound at c, z, hornerAt{complexCarrier}(complexAdd, complexMul, leading, z, tail), radius, complexHornerBound(leading, radius, tail) with *117    rw [hornerAt.cons, complexHornerBound]118    unfold complexBoundStep119    exact bound120121theorem complexPolynomial.bounded_on_disk (radius : Real) (cs : List(complexCarrier))122  requires radiusNonnegative : realZero ≤ radius123  shows ∃ bound ∈ ℝ, realZero ≤ bound ∧ (∀ z ∈ ℂ, complexNormSquared(z) ≤ radius → complexNormSquared(complexPolynomial(cs)(z)) ≤ bound)124proof125  have field := complexes.is_field126  have ring := IsField.comm_ring with field127  have data := complexHornerBound.data at complexOne, radius, cs with *128  have boundIn : complexHornerBound(complexOne, radius, cs) ∈ ℝ by typecheck129  refine ⟨complexHornerBound(complexOne, radius, cs), boundIn, data.right, ?_⟩130  intros z member within131  have estimate := complexHornerBound.bounds at complexOne, z, radius, cs with *132  have value := complexPolynomial.value at cs, z with *133  rw value134  unfold hornerAt at estimate135  exact estimate136137-- Synthetic division turns the disk bound into a quantitative continuity estimate.138theorem complexHornerBound.difference (leading a x c : Set) (radius : Real) (cs : List(complexCarrier))139  requires initial : leading ∈ ℂ140  requires center : a ∈ ℂ141  requires element : x ∈ ℂ142  requires coefficient : c ∈ ℂ143  requires radiusNonnegative : realZero ≤ radius144  requires within : complexNormSquared(x) ≤ radius145  shows complexNormSquared(ℂ[hornerAt{complexCarrier}(complexAdd, complexMul, leading, x, c :: cs) - hornerAt{complexCarrier}(complexAdd, complexMul, leading, a, c :: cs)]) ≤ R[complexNormSquared(ℂ[x - a]) * complexHornerBound(leading, radius, hornerQuotient{complexCarrier}(complexAdd, complexMul, leading, a, cs))]146proof147  have field := complexes.is_field148  have ring := IsField.comm_ring with field149  have ordinary := IsCommRing.ring with ring150  have quotient := hornerQuotient.closed at complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne, leading, a, cs with *151  have aValue := hornerAt.closed at complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne, leading, a, c :: cs with *152  have qValue := hornerAt.closed at complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne, leading, x, hornerQuotient{complexCarrier}(complexAdd, complexMul, leading, a, cs) with *153  have negated := IsRing.neg_closed with ordinary, center154  have displacement := IsRing.add_closed with ordinary, element, negated155  have displacementNonnegative := complexNormSquared.nonnegative with displacement156  have reflexive := realLe.reflexive with *157  have data := complexHornerBound.data at leading, radius, hornerQuotient{complexCarrier}(complexAdd, complexMul, leading, a, cs) with *158  have bounded := complexHornerBound.bounds at leading, x, radius, hornerQuotient{complexCarrier}(complexAdd, complexMul, leading, a, cs) with *159  have division := hornerAt.synthetic_division at complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne, leading, a, x, c, cs with *160  have factorization : ℂ[hornerAt{complexCarrier}(complexAdd, complexMul, leading, x, c :: cs) - hornerAt{complexCarrier}(complexAdd, complexMul, leading, a, c :: cs)] = ℂ[(x - a) * hornerAt{complexCarrier}(complexAdd, complexMul, leading, x, hornerQuotient{complexCarrier}(complexAdd, complexMul, leading, a, cs))]161    rw division162    ring163  rw factorization164  exact complexNormSquared.mul_bound with *165166theorem complexPolynomial.difference_bound_on_disk (a c : Set) (radius : Real) (cs : List(complexCarrier))167  requires center : a ∈ ℂ168  requires coefficient : c ∈ ℂ169  requires radiusNonnegative : realZero ≤ radius170  shows ∃ bound ∈ ℝ, realZero ≤ bound ∧ (∀ x ∈ ℂ, complexNormSquared(x) ≤ radius → complexNormSquared(ℂ[complexPolynomial(c :: cs)(x) - complexPolynomial(c :: cs)(a)]) ≤ R[complexNormSquared(ℂ[x - a]) * bound])171proof172  have field := complexes.is_field173  have ring := IsField.comm_ring with field174  have quotient := hornerQuotient.closed at complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne, complexOne, a, cs with *175  have data := complexHornerBound.data at complexOne, radius, hornerQuotient{complexCarrier}(complexAdd, complexMul, complexOne, a, cs) with *176  have boundIn : complexHornerBound(complexOne, radius, hornerQuotient{complexCarrier}(complexAdd, complexMul, complexOne, a, cs)) ∈ ℝ177    typecheck178  refine ⟨complexHornerBound(complexOne, radius, hornerQuotient{complexCarrier}(complexAdd, complexMul, complexOne, a, cs)), boundIn, data.right, ?_⟩179  intros x member within180  have estimate := complexHornerBound.difference at complexOne, a, x, c, radius, cs with *181  have xValue := complexPolynomial.value at c :: cs, x with *182  have aValue := complexPolynomial.value at c :: cs, a with *183  rw [xValue, aValue]184  simpa [hornerAt] using estimate185186end Estimates187