Grace/Cumulus/Complex/LocalPolynomial.g17

Open in Workbench Download source

Imports

SequentialContinuity · Algebra.Field.Powers · Algebra.Polynomial.HornerVanishing

Declarations

Source

1-- A checked local normal form for every nonconstant monic complex polynomial.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.LocalPolynomial8import SequentialContinuity9import Algebra.Field.Powers10import Algebra.Polynomial.HornerVanishing1112section Complexes13notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)1415theorem complexPolynomial.horner_value (x : Set) (cs : List(ℂ))16  requires member : x ∈ ℂ17  shows complexPolynomial(cs)(x) = hornerAt{ℂ}(complexAdd, complexMul, complexOne, x, cs)18proof19  rw complexPolynomial.value20  unfold hornerAt21  rfl2223-- No nonroot hypothesis is needed: the normal form also describes roots.24-- n+1 is the first nonconstant exponent; the degree equation bounds it.25theorem complexPolynomial.local_normal_form (c a : Set) (cs : List(ℂ))26  requires coefficient : c ∈ ℂ27  requires center : a ∈ ℂ28  shows ∃ n ∈ ℕ, ∃ ds, List(ℂ, ds) ∧ complexPolynomial(ds)(ℂ[0]) ≠ ℂ[0] ∧29    length{ℂ}(cs) = Grace.Core.Nat.Rec.add(n, length{ℂ}(ds)) ∧30    ComplexContinuous(complexPolynomial(ds)) ∧31    (∀ h ∈ ℂ, complexPolynomial(c :: cs)(ℂ[a + h]) = ℂ[complexPolynomial(c :: cs)(a) + h ^ succ(n) * complexPolynomial(ds)(h)])32proof33  have field := complexes.is_field34  have ring := IsField.comm_ring with field35  have ordinary := IsCommRing.ring with ring36  have monoid := IsRing.multiplicative with ordinary37  have zeroIn : ℂ[0] ∈ ℂ by typecheck38  have unitNonzero : ℂ[1] ≠ ℂ[0]39    have distinct := Nontrivial.distinct with complexes.nontrivial40    intro same41    apply distinct42    symm43    exact same44  have list : List(ℂ, c :: cs) by typecheck45  have data := hornerTranslate.data at ℂ, complexAdd, complexZero, complexNeg, complexMul, complexOne, complexOne, a, c :: cs with *46  have shape := List.cases at ℂ, hornerTranslate{ℂ}(complexAdd, complexMul, complexOne, complexOne, a, c :: cs) with *47  cases shape with empty | nonempty48  . have degree := data.right49    rw [empty, length.nil, length.cons] at degree50    have impossible := Naturals.disjoint.zero.succ at length{ℂ}(cs)51    exfalso52    exact impossible with degree53  . obtain ⟨d, dIn, tail, tailList, translatedShape⟩ := nonempty54    have degree := data.right55    rw [translatedShape, length.cons, length.cons] at degree56    have tailDegree := Naturals.injective.succ with degree57    obtain ⟨n, nIn, ds, dsList, headNonzero, factorDegree, factor⟩ := hornerAt.first_nonzero at ℂ, complexAdd, complexZero, complexNeg, complexMul, complexOne, complexOne, tail with *58    have nNat := nat.omega.backward at n with *59    have constant := hornerTranslate.constant at ℂ, complexAdd, complexZero, complexNeg, complexMul, complexOne, complexOne, a, c :: cs with *60    rw [translatedShape, listHeadOr] at constant61    have headValue := hornerAt.at_zero at ℂ, complexAdd, complexZero, complexNeg, complexMul, complexOne, complexOne, a, ds with *62    have qNonzero : complexPolynomial(ds)(ℂ[0]) ≠ ℂ[0] by rwa [complexPolynomial.horner_value, headValue]63    have degreeBound : length{ℂ}(cs) = Grace.Core.Nat.Rec.add(n, length{ℂ}(ds)) by rwa ← tailDegree64    have continuous := complexPolynomial.continuous at ds with *65    refine ⟨n, nIn, ds, dsList, qNonzero, degreeBound, continuous, ?_⟩66    intros h hIn67    have sum := IsRing.add_closed with ordinary, center, hIn68    have power := monoidPow.closed at ℂ, complexMul, complexOne, h, n with *69    have qValue := hornerAt.closed at ℂ, complexAdd, complexZero, complexNeg, complexMul, complexOne, complexOne, h, ds with *70    have translated := hornerTranslate.value at ℂ, complexAdd, complexZero, complexNeg, complexMul, complexOne, complexOne, a, h, c :: cs with *71    rw [translatedShape, hornerAt.cons] at translated72    have tailFactor := factor with h, hIn73    rw tailFactor at translated74    rw [complexPolynomial.horner_value, ← translated, complexPolynomial.horner_value, complexPolynomial.horner_value, ← constant, monoidPow.succ]75    ring7677-- A continuous nonzero value stays nonzero in a sufficiently small disk.78theorem ComplexContinuousAt.eventually_nonzero (f a : Set)79  requires continuous : ComplexContinuousAt(f, a)80  requires nonzero : f(a) ≠ ℂ[0]81  shows ∃ d ∈ ℝ, realZero < d ∧82    (∀ x ∈ ℂ, complexNormSquared(ℂ[x - a]) < d → f(x) ≠ ℂ[0])83proof84  unfold ComplexContinuousAt at continuous85  have image := FunctionBetween.apply_closed at f, ℂ, ℂ, a with *86  have positive := complexNormSquared.positive with *87  obtain ⟨d, dReal, dPositive, control⟩ := continuous.right.right with complexNormSquared(f(a)), positive88  refine ⟨d, dReal, dPositive, ?_⟩89  intros x xIn near vanishes90  have small := control with x, xIn, near91  rw vanishes at small92  have ring := complexes.comm_ring93  have ordinary := IsCommRing.ring with ring94  have difference : ℂ[0 - f(a)] = ℂ[-f(a)] by ring95  rw [difference, complexNormSquared.neg] at small96  have irrefl := realLess.irreflexive_on97  exact irrefl with complexNormSquared(f(a)), small9899-- Every root of a nonconstant monic polynomial is isolated.100theorem complexPolynomial.isolated_root (c a : Set) (cs : List(ℂ))101  requires coefficient : c ∈ ℂ102  requires center : a ∈ ℂ103  requires root : complexPolynomial(c :: cs)(a) = ℂ[0]104  shows ∃ d ∈ ℝ, realZero < d ∧105    (∀ h ∈ ℂ, h ≠ ℂ[0] → complexNormSquared(h) < d → complexPolynomial(c :: cs)(ℂ[a + h]) ≠ ℂ[0])106proof107  obtain ⟨n, nIn, ds, dsList, nonzero, degree, continuous, expansion⟩ := complexPolynomial.local_normal_form at c, a, cs with *108  have zeroIn := complexZero.member109  have atZero := continuous.right with ℂ[0], zeroIn110  obtain ⟨d, dReal, dPositive, nonvanishing⟩ := ComplexContinuousAt.eventually_nonzero at complexPolynomial(ds), ℂ[0] with *111  refine ⟨d, dReal, dPositive, ?_⟩112  intros h hIn hNonzero near113  have field := complexes.is_field114  have ring := IsField.comm_ring with field115  have ordinary := IsCommRing.ring with ring116  have monoid := IsRing.multiplicative with ordinary117  have difference : ℂ[h - 0] = h by ring118  have nearZero : complexNormSquared(ℂ[h - 0]) < d by rwa difference119  have qNonzero := nonvanishing with h, hIn, nearZero120  have nNat := nat.omega.backward at n with *121  have powerNonzero := IsField.power_nonzero at ℂ, complexAdd, complexZero, complexNeg, complexMul, complexOne, h, succ(n) with *122  have power := monoidPow.closed at ℂ, complexMul, complexOne, h, succ(n) with *123  have function := continuous.left124  have qValue := FunctionBetween.apply_closed at complexPolynomial(ds), ℂ, ℂ, h with *125  have value := expansion with h, hIn126  rw root at value127  have simplify : ℂ[0 + h ^ succ(n) * complexPolynomial(ds)(h)] = ℂ[h ^ succ(n) * complexPolynomial(ds)(h)] by ring128  rw simplify at value129  rw value130  intro vanishes131  have noZero := IsField.no_zero_divisors with field132  have alternatives := noZero with h ^ succ(n), complexPolynomial(ds)(h), qValue, vanishes133  cases alternatives with first | second134  . exact powerNonzero with first135  . exact qNonzero with second136137end Complexes138