Grace/Cumulus/Complex/PolynomialStationarity.g17

Open in Workbench Download source

Imports

SequenceAlgebra

Declarations

• complexPolynomial.minimum_leading_term theorem derivation

Source

1-- The first nonconstant term at a global minimum has nonnegative real pairing.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.PolynomialStationarity8import SequenceAlgebra910section Complexes11notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)12notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)1314theorem complexPolynomial.minimum_leading_term (c a s : Set) (cs : List(ℂ))15  requires coefficient : c ∈ ℂ16  requires center : a ∈ ℂ17  requires steps : ConvergesTo(s, realZero)18  requires positive : ∀ j ∈ ℕ, realZero < s(j)19  requires minimum : ∀ z ∈ ℂ, complexNormSquared(complexPolynomial(c :: cs)(a)) ≤ complexNormSquared(complexPolynomial(c :: cs)(z))20  shows ∃ n ∈ ℕ, ∃ ds, List(ℂ, ds) ∧ complexPolynomial(ds)(ℂ[0]) ≠ ℂ[0] ∧21    length{ℂ}(cs) = Grace.Core.Nat.Rec.add(n, length{ℂ}(ds)) ∧22    (∀ u ∈ ℂ, realZero ≤ Euclidean.dot(complexPolynomial(c :: cs)(a), ℂ[u ^ succ(n) * complexPolynomial(ds)(ℂ[0])]))23proof24  obtain ⟨n, nIn, ds, dsList, nonzero, degree, continuous, expansion⟩ := complexPolynomial.ray_normal_form at c, a, cs with *25  have nNat := nat.omega.backward at n with *26  have pFunction := complexPolynomial.function at c :: cs with *27  have base := FunctionBetween.apply_closed at complexPolynomial(c :: cs), ℂ, ℂ, a with *28  have qFunction := complexPolynomial.function at ds with *29  have zeroIn := complexZero.member30  have qZero := FunctionBetween.apply_closed at complexPolynomial(ds), ℂ, ℂ, ℂ[0] with *31  have stepSequence := ConvergesTo.sequence at s, realZero with *32  have powerSteps := ConvergesTo.pow at s, realZero, succ(n) with *33  rw realPow.zero_succ at powerSteps34  have powerSequence := powSequence.sequence at s, succ(n) with *35  have powerPositive : ∀ j ∈ ℕ, realZero < powSequence(s, succ(n))(j)36    intros j jIn37    have jNat := nat.omega.backward at j with *38    have value := RealSequence.value at s, j with *39    have stepPositive := positive with j, jIn40    rw powSequence.value41    exact realPow.positive at s(j), succ(n) with *42  refine ⟨n, nIn, ds, dsList, nonzero, degree, ?_⟩43  intros u uIn44  have ring := complexes.comm_ring45  have ordinary := IsCommRing.ring with ring46  have monoid := IsRing.multiplicative with ordinary47  have power := monoidPow.closed at ℂ, complexMul, complexOne, u, succ(n) with *48  have ray := complexRaySequence.converges_zero at s, u with *49  have raySequence := complexRaySequence.sequence at s, u with *50  have qLimit := complexPolynomial.converges at complexRaySequence(s, u), ℂ[0], ds with *51  have qSequence := complexMappedSequence.sequence at complexPolynomial(ds), complexRaySequence(s, u) with *52  have multiplier := complexLeftMul.function at u ^ succ(n) with *53  have multiplierContinuous := complexLeftMul.continuous_at at u ^ succ(n), complexPolynomial(ds)(ℂ[0]) with *54  have directionLimit := ComplexContinuousAt.converges at complexLeftMul(u ^ succ(n)), complexMappedSequence(complexPolynomial(ds), complexRaySequence(s, u)), complexPolynomial(ds)(ℂ[0]) with *55  rw complexLeftMul.value at directionLimit56  have along := expansion with u, uIn57  have least : ∀ j ∈ ℕ, complexNormSquared(complexPolynomial(c :: cs)(a)) ≤ complexNormSquared(ℂ[complexPolynomial(c :: cs)(a) + complexScale(powSequence(s, succ(n))(j), complexMappedSequence(complexLeftMul(u ^ succ(n)), complexMappedSequence(complexPolynomial(ds), complexRaySequence(s, u)))(j))])58    intros j jIn59    have jNat := nat.omega.backward at j with *60    have sjReal := RealSequence.value at s, j with *61    have sjIn : s(j) ∈ ℝ by typecheck62    have scaled := complexScale.closed at s(j), u with *63    have sum := IsRing.add_closed with ordinary, center, scaled64    have bound := minimum with ℂ[a + complexScale(s(j), u)], sum65    have equation := along with s(j)66    rw equation at bound67    have rayFunction : complexRaySequence(s, u) : ℕ → ℂ by exact raySequence68    have rayMember := FunctionBetween.apply_closed at complexRaySequence(s, u), ℕ, ℂ, j with *69    have qMember := FunctionBetween.apply_closed at complexPolynomial(ds), ℂ, ℂ, complexRaySequence(s, u)(j) with *70    rwa [powSequence.value, complexMappedSequence.value, complexMappedSequence.value, complexLeftMul.value, complexRaySequence.value]71  exact complexNormSquared.minimum_direction at complexPolynomial(c :: cs)(a), powSequence(s, succ(n)), complexMappedSequence(complexLeftMul(u ^ succ(n)), complexMappedSequence(complexPolynomial(ds), complexRaySequence(s, u))), ℂ[u ^ succ(n) * complexPolynomial(ds)(ℂ[0])] with *7273end Complexes74