Grace/Cumulus/Complex/PolynomialGrowth.g17

Open in Workbench Download source

Imports

Continuity

Declarations

Source

1-- Constructive growth at infinity for monic complex Horner polynomials.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.PolynomialGrowth8import Continuity910predicate ComplexDiskMinimum (p radius : Set) :=11  ∃ a ∈ complexCarrier, complexNormSquared(a) ≤ radius ∧12    (∀ z ∈ complexCarrier, complexNormSquared(z) ≤ radius → complexNormSquared(p(a)) ≤ complexNormSquared(p(z)))1314theorem realLe.two_sum_cancel (a b c : Real)15  requires bound : (2:R) * (a + c) ≤ (2:R) * (b + c)16  shows a ≤ b17proof18  have onePositive := realZero.lt_one19  have twoPositive : (0:R) < 2 by linarith20  have first : (2:R) * (a + c) = (a + c) * (2:R) by ring21  have second : (2:R) * (b + c) = (b + c) * (2:R) by ring22  rw [first, second] at bound23  have sums := realLe.mul_right_cancel_positive with *24  have translated := realLe.add_right at a + c, b + c, -c with *25  have left : (a + c) + (-c) = a by ring26  have right : (b + c) + (-c) = b by ring27  rwa [left, right] at translated2829theorem realLe.nonnegative_sum_bounds (a b : Real)30  requires first : realZero ≤ a31  requires second : realZero ≤ b32  shows realZero ≤ a + b ∧ a ≤ a + b ∧ b ≤ a + b33proof34  have sum := realLe.add at realZero, a, realZero, b with *35  rw realAddValue.zero_left at sum36  have left := realLe.add_left at realZero, b, a with *37  rw realAddValue.zero_right at left38  have right := realLe.add_right at realZero, a, b with *39  rw realAddValue.zero_left at right40  refine ⟨sum, left, right⟩4142section Complexes43notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)44notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)4546theorem complexNormSquared.horner_step_lower_bound (c z w : Set) (target : Real)47  requires coefficient : c ∈ ℂ48  requires first : z ∈ ℂ49  requires second : w ∈ ℂ50  requires unitBound : R[1] ≤ complexNormSquared(w)51  requires large : R[2 * (target + complexNormSquared(c))] ≤ complexNormSquared(z)52  shows target ≤ complexNormSquared(ℂ[c + z * w])53proof54  have field := complexes.is_field55  have ring := IsField.comm_ring with field56  have ordinary := IsCommRing.ring with ring57  have product := IsRing.mul_closed with ordinary, first, second58  have sum := IsRing.add_closed with ordinary, coefficient, product59  have negated := IsRing.neg_closed with ordinary, coefficient60  have productReal := complexNormSquared.real with product61  have zNonnegative := complexNormSquared.nonnegative with first62  have multiplied := realLe.mul_left_of_nonnegative at realOne, complexNormSquared(w), complexNormSquared(z) with *63  rw realMulValue.one_right at multiplied64  have normProduct := complexNormSquared.mul at z, w with *65  rw ← normProduct at multiplied66  have reverse := complexNormSquared.add_bound at ℂ[c + z * w], ℂ[-c] with *67  have cancel : ℂ[(c + z * w) + (-c)] = ℂ[z * w] by ring68  rw [cancel, complexNormSquared.neg] at reverse69  have lower := realLe.transitive at R[2 * (target + complexNormSquared(c))], complexNormSquared(z), complexNormSquared(ℂ[z * w]) with *70  have sandwich := realLe.transitive at R[2 * (target + complexNormSquared(c))], complexNormSquared(ℂ[z * w]), R[2 * (complexNormSquared(ℂ[c + z * w]) + complexNormSquared(c))] with *71  exact realLe.two_sum_cancel with *7273theorem complexPolynomial.eventually_unit_bound (cs : List(complexCarrier))74  shows ∃ radius ∈ ℝ, realZero ≤ radius ∧ (∀ z ∈ ℂ, radius ≤ complexNormSquared(z) → R[1] ≤ complexNormSquared(hornerAt{complexCarrier}(complexAdd, complexMul, complexOne, z, cs)))75proof76  have field := complexes.is_field77  have ring := IsField.comm_ring with field78  have oneNonnegative := realLess.implies_le with realZero.real, realOne.real, realZero.lt_one79  induction cs80  | List.nil =>81    have zeroIn : realZero ∈ ℝ by typecheck82    have zeroReflexive := realLe.reflexive at realZero with *83    refine ⟨realZero, zeroIn, zeroReflexive, ?_⟩84    intros z member outside85    rw [hornerAt.nil, complexNormSquared.one]86    exact realLe.reflexive with *87  | List.cons(c, tail) using ih =>88    have coefficient : c ∈ ℂ by assumption89    obtain ⟨r, rIn, rNonnegative, tailBound⟩ := ih90    have cNonnegative := complexNormSquared.nonnegative with coefficient91    have thresholdNonnegative := realLe.two_sum_nonnegative at realOne, complexNormSquared(c) with *92    have bounds := realLe.nonnegative_sum_bounds at r, R[2 * (1 + complexNormSquared(c))] with *93    have radiusIn : R[r + 2 * (1 + complexNormSquared(c))] ∈ ℝ by typecheck94    refine ⟨R[r + 2 * (1 + complexNormSquared(c))], radiusIn, bounds.left, ?_⟩95    intros z member outside96    have beyondTail := realLe.transitive at r, R[r + 2 * (1 + complexNormSquared(c))], complexNormSquared(z) with *97    have beyondThreshold := realLe.transitive at R[2 * (1 + complexNormSquared(c))], R[r + 2 * (1 + complexNormSquared(c))], complexNormSquared(z) with *98    have tailLarge := tailBound with z, member, beyondTail99    have tailValue := hornerAt.closed at complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne, complexOne, z, tail with *100    have bound := complexNormSquared.horner_step_lower_bound with *101    rwa hornerAt.cons102103theorem complexPolynomial.eventually_above (c : Set) (target : Real) (cs : List(complexCarrier))104  requires coefficient : c ∈ ℂ105  requires targetNonnegative : realZero ≤ target106  shows ∃ radius ∈ ℝ, realZero ≤ radius ∧ (∀ z ∈ ℂ, radius ≤ complexNormSquared(z) → target ≤ complexNormSquared(complexPolynomial(c :: cs)(z)))107proof108  have field := complexes.is_field109  have ring := IsField.comm_ring with field110  obtain ⟨r, rIn, rNonnegative, tailBound⟩ := complexPolynomial.eventually_unit_bound at cs with *111  have cNonnegative := complexNormSquared.nonnegative with coefficient112  have thresholdNonnegative := realLe.two_sum_nonnegative at target, complexNormSquared(c) with *113  have bounds := realLe.nonnegative_sum_bounds at r, R[2 * (target + complexNormSquared(c))] with *114  have radiusIn : R[r + 2 * (target + complexNormSquared(c))] ∈ ℝ by typecheck115  refine ⟨R[r + 2 * (target + complexNormSquared(c))], radiusIn, bounds.left, ?_⟩116  intros z member outside117  have beyondTail := realLe.transitive at r, R[r + 2 * (target + complexNormSquared(c))], complexNormSquared(z) with *118  have beyondThreshold := realLe.transitive at R[2 * (target + complexNormSquared(c))], R[r + 2 * (target + complexNormSquared(c))], complexNormSquared(z) with *119  have tailLarge := tailBound with z, member, beyondTail120  have tailValue := hornerAt.closed at complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne, complexOne, z, cs with *121  have bound := complexNormSquared.horner_step_lower_bound at c, z, hornerAt{complexCarrier}(complexAdd, complexMul, complexOne, z, cs), target with *122  have evaluation := complexPolynomial.value at c :: cs, z with *123  rw evaluation124  have expansion := hornerAt.cons at complexCarrier, complexAdd, complexMul, complexOne, z, c, cs with *125  unfold hornerAt at expansion126  unfold hornerAt at bound127  rw expansion128  exact bound129130theorem complexPolynomial.grows_at_infinity (c : Set) (target : Real) (cs : List(complexCarrier))131  requires coefficient : c ∈ ℂ132  shows ∃ radius ∈ ℝ, realZero ≤ radius ∧ (∀ z ∈ ℂ, radius ≤ complexNormSquared(z) → target < complexNormSquared(complexPolynomial(c :: cs)(z)))133proof134  have scaleReal := limitScale.real with *135  have positive := limitScale.positive at target with *136  have nonnegative := realLess.implies_le with *137  have absoluteBound := abs.upper at target with *138  have scaleBound := abs.lt_limitScale at target with *139  have targetLess := realLe.transitive_less at target, abs(target), limitScale(target) with *140  obtain ⟨radius, radiusIn, radiusNonnegative, grows⟩ := complexPolynomial.eventually_above at c, limitScale(target), cs with *141  refine ⟨radius, radiusIn, radiusNonnegative, ?_⟩142  intros z member outside143  have lower := grows with z, member, outside144  have function := complexPolynomial.function at c :: cs with *145  have image := FunctionBetween.apply_closed at complexPolynomial(c :: cs), complexCarrier, complexCarrier, z with *146  exact realLess.transitive_le with *147148theorem complexFunction.global_minimum_of_disk_minimum (p : Set) (radius : Real)149  requires function : p : ℂ → ℂ150  requires nonnegative : realZero ≤ radius151  requires escape : ∀ z ∈ ℂ, radius ≤ complexNormSquared(z) → complexNormSquared(p(ℂ[0])) < complexNormSquared(p(z))152  requires diskMinimum : ComplexDiskMinimum(p, radius)153  shows ∃ a ∈ ℂ, ∀ z ∈ ℂ, complexNormSquared(p(a)) ≤ complexNormSquared(p(z))154proof155  obtain ⟨a, member, inside, least⟩ := diskMinimum156  have field := complexes.is_field157  have ring := IsField.comm_ring with field158  have zeroInside : complexNormSquared(ℂ[0]) ≤ radius by rwa complexNormSquared.zero159  have atZero := least with complexZero, zeroInside160  have imageA := FunctionBetween.apply_closed with *161  have imageZero := FunctionBetween.apply_closed at p, complexCarrier, complexCarrier, complexZero with *162  refine ⟨a, member, ?_⟩163  intros z zIn164  have imageZ := FunctionBetween.apply_closed at p, complexCarrier, complexCarrier, z with *165  have location : complexNormSquared(z) ≤ radius ∨ ¬ (complexNormSquared(z) ≤ radius) by tauto166  cases location with within | outside167  . exact least with z, zIn, within168  . have strict := realLess.of_not_le at complexNormSquared(z), radius with *169    have beyond := realLess.implies_le at radius, complexNormSquared(z) with *170    have larger := escape with z, zIn, beyond171    have leastStrict := realLe.transitive_less at complexNormSquared(p(a)), complexNormSquared(p(ℂ[0])), complexNormSquared(p(z)) with *172    exact realLess.implies_le with *173174theorem complexPolynomial.minimum_of_disk_minima (c : Set) (cs : List(complexCarrier))175  requires coefficient : c ∈ ℂ176  requires diskMinima : ∀ radius ∈ ℝ, realZero ≤ radius → ComplexDiskMinimum(complexPolynomial(c :: cs), radius)177  shows ∃ a ∈ ℂ, ∀ z ∈ ℂ, complexNormSquared(complexPolynomial(c :: cs)(a)) ≤ complexNormSquared(complexPolynomial(c :: cs)(z))178proof179  have function := complexPolynomial.function at c :: cs with *180  have field := complexes.is_field181  have ring := IsField.comm_ring with field182  have image := FunctionBetween.apply_closed at complexPolynomial(c :: cs), complexCarrier, complexCarrier, complexZero with *183  obtain ⟨radius, radiusIn, nonnegative, escape⟩ := complexPolynomial.grows_at_infinity at c, complexNormSquared(complexPolynomial(c :: cs)(ℂ[0])), cs with *184  have diskMinimum := diskMinima with radius, radiusIn, nonnegative185  exact complexFunction.global_minimum_of_disk_minimum with *186187theorem complexPolynomial.root_of_disk_minima_and_descent (c : Set) (cs : List(complexCarrier))188  requires coefficient : c ∈ ℂ189  requires diskMinima : ∀ radius ∈ ℝ, realZero ≤ radius → ComplexDiskMinimum(complexPolynomial(c :: cs), radius)190  requires descent : ∀ a ∈ ℂ, complexPolynomial(c :: cs)(a) ≠ ℂ[0] → ∃ z ∈ ℂ, complexNormSquared(complexPolynomial(c :: cs)(z)) < complexNormSquared(complexPolynomial(c :: cs)(a))191  shows ∃ a ∈ ℂ, monicValue(ℂ, identity(ℂ), ℂ, a, c :: cs) = ℂ[0]192proof193  have minimum := complexPolynomial.minimum_of_disk_minima with *194  exact complexPolynomial.root_of_minimum_and_descent with *195196end Complexes197