Grace/Cumulus/Complex/PolynomialMinimum.g17

Open in Workbench Download source

Imports

Norm · Algebra.Polynomial.HornerTranslation

Declarations

Source

1-- The minimum-modulus reduction for concrete complex polynomials (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.PolynomialMinimum8import Norm9import Algebra.Polynomial.HornerTranslation1011defgraph complexPolynomial (cs : Set) (z ∈ complexCarrier) : complexCarrier := monicValue{complexCarrier}(identity(complexCarrier), complexAdd, complexMul, complexOne, z, cs)12requires coefficients : List(complexCarrier, cs)13proof14  have field := complexes.is_field15  have ring := IsField.comm_ring with field16  have hom := IsRingHom.identity with ring17  exact monicValue.closed with *1819-- The analytic premises are hypotheses of the theorem; nothing here defines20-- algebraic closure.21theorem complexFunction.root_of_minimum_and_descent (p : Set)22  requires function : p : complexCarrier → complexCarrier23  requires minimum : ∃ a ∈ complexCarrier, ∀ z ∈ complexCarrier, complexNormSquared(p(a)) ≤ complexNormSquared(p(z))24  requires descent : ∀ a ∈ complexCarrier, p(a) ≠ complexZero → ∃ z ∈ complexCarrier, complexNormSquared(p(z)) < complexNormSquared(p(a))25  shows ∃ a ∈ complexCarrier, p(a) = complexZero26proof27  obtain ⟨a, member, least⟩ := minimum28  have image := FunctionBetween.apply_closed with *29  have root : p(a) = complexZero30    by_contra nonzero31    obtain ⟨z, zIn, smaller⟩ := descent with a, member, nonzero32    have otherImage := FunctionBetween.apply_closed at p, complexCarrier, complexCarrier, z with *33    have bound := least with z, zIn34    have impossible := realLe.transitive_less with *35    have irreflexive := realLess.irreflexive_on36    exact irreflexive with complexNormSquared(p(a)), impossible37  refine ⟨a, member, root⟩3839section Polynomials40notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)4142theorem complexPolynomial.root_of_minimum_and_descent (cs : List(complexCarrier))43  requires minimum : ∃ a ∈ ℂ, ∀ z ∈ ℂ, complexNormSquared(complexPolynomial(cs)(a)) ≤ complexNormSquared(complexPolynomial(cs)(z))44  requires descent : ∀ a ∈ ℂ, complexPolynomial(cs)(a) ≠ ℂ[0] → ∃ z ∈ ℂ, complexNormSquared(complexPolynomial(cs)(z)) < complexNormSquared(complexPolynomial(cs)(a))45  shows ∃ a ∈ ℂ, monicValue(ℂ, identity(ℂ), ℂ, a, cs) = ℂ[0]46proof47  have function := complexPolynomial.function at cs with *48  obtain ⟨a, member, root⟩ := complexFunction.root_of_minimum_and_descent at complexPolynomial(cs) with *49  have value := complexPolynomial.value at cs, a with *50  refine ⟨a, member, ?_⟩51  rwa value at root5253end Polynomials54