Grace/Cumulus/Real/Polynomial.g17

Open in Workbench Download source

Imports

FiniteSum · Power

Declarations

Source

1-- Finite real polynomials2-- 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.Real.Polynomial8import FiniteSum9import Power1011-- A polynomial is represented by a real coefficient sequence and a finite12-- cutoff. Only the first n coefficients affect the value.13def polynomialEval (coeff : Set, n : Nat, X : Real) → Set14  | coeff, zero, X => realZero15  | coeff, succ(k), X =>16      realAddValue(polynomialEval(coeff, k, X), realMulValue(coeff[k], realPow(X, k)))1718-- A polynomial's weighted terms form a real sequence, permitting general19-- finite-sum laws to be applied to polynomial evaluations.20defgraph polynomialTerms (coeff : Set, X : Real) (k ∈ ℕ) : ℝ :=21  realMulValue(coeff[k], realPow(X, k))22requires coefficients : RealSequence(coeff)23proof24  have typedK := nat.omega.backward at k with member25  have coefficient := RealSequence.value at coeff, k with coefficients26  have power := realPow.real at X, k with assumption, typedK27  have product := realMulValue.real at coeff[k], realPow(X, k) with28    coefficient, power29  unfold Real at product30  unfold realMulValue31  unfold call2 at product32  exact product3334theorem polynomialTerms.sequence (coeff : Set, X : Real)35  requires coefficients : RealSequence(coeff)36  shows RealSequence(polynomialTerms(coeff, X))37proof38  unfold RealSequence39  exact polynomialTerms.function with coefficients4041theorem polynomialEval.zero (coeff : Set) (X : Real)42  shows polynomialEval(coeff, 0, X) = (0:R)43proof44  rw polynomialEval45  rfl4647theorem polynomialEval.succ (coeff : Set) (k : Nat, X : Real)48  shows polynomialEval(coeff, succ(k), X) =49    realAddValue(polynomialEval(coeff, k, X),50      realMulValue(coeff[k], realPow(X, k)))51proof52  rw polynomialEval53  rfl5455theorem polynomialEval.real (coeff : Set, n : Nat, X : Real)56  requires coefficients : RealSequence(coeff)57  shows Real(polynomialEval(coeff, n, X))58proof59  induction n60  | zero =>61    rw polynomialEval.zero62    exact realZero.real63  | succ(k) using ih =>64    rw polynomialEval.succ65    have coefficient := RealSequence.value with coefficients66    have power := realPow.real at X, k with *67    have term := realMulValue.real with coefficient, power68    have typedTerm : Real(realMulValue(coeff[k], realPow(X, k)))69      unfold realMulValue70      unfold call2 at term71      exact term72    have sum := realAddValue.real at73      polynomialEval(coeff, k, X), realMulValue(coeff[k], realPow(X, k)) with ih, typedTerm74    unfold realAddValue75    unfold call2 at sum76    exact sum7778theorem polynomialEval.as_sum (coeff : Set, n : Nat, X : Real)79  requires coefficients : RealSequence(coeff)80  shows polynomialEval(coeff, n, X) = realPartialSum(polynomialTerms(coeff, X), n)81proof82  induction n83  | zero =>84    rw [polynomialEval.zero, realPartialSum.zero]85    rfl86  | succ(k) using ih =>87    have value := polynomialTerms.value with coefficients88    rw [polynomialEval.succ, realPartialSum.succ, ih, value]89    rfl9091-- Increasing a cutoff adds precisely the weighted terms in its new suffix.92theorem polynomialEval.split_at (coeff : Set, n m : Nat, X : Real)93  requires coefficients : RealSequence(coeff)94  shows polynomialEval(coeff, add(n, m), X) =95    (polynomialEval(coeff, n, X):R) +96      realPartialSum(shiftedRealSequence(polynomialTerms(coeff, X), n), m)97proof98  have terms := polynomialTerms.sequence with coefficients99  rw [polynomialEval.as_sum, polynomialEval.as_sum]100  exact realPartialSum.split_at with terms101102-- Constant coefficients form a scalar multiple of the geometric polynomial.103theorem polynomialEval.geometric_coefficients (C X : Real, n : Nat)104  shows polynomialEval(constantSequence(C), n, X) =105    C * (realPartialSum(geometricTerms(X), n):R)106proof107  induction n108  | zero =>109    rw [polynomialEval.zero, realPartialSum.zero]110    ring111  | succ(k) using ih =>112    have constants := constantSequence.sequence at C113    have coefficient := constantSequence.value at C, k with *114    have geometric := geometricTerms.value at X, k with *115    rw [polynomialEval.succ, realPartialSum.succ, coefficient, geometric, ih]116    ring117118theorem polynomialEval.geometric_identity (X : Real, n : Nat)119  shows ((1:R) - X) * (polynomialEval(constantSequence(realOne), n, X):R) =120    (1:R) - X ^ n121proof122  have eval := polynomialEval.geometric_coefficients at realOne, X, n123  have sum := realPartialSum.geometric with *124  have sequence := geometricTerms.sequence at X125  have sumReal := realPartialSum.real with sequence126  have one := realMulValue.one_left with sumReal127  rwa [eval, one]128129theorem polynomialEval.add (u v : Set, n : Nat, X : Real)130  requires sequenceU : RealSequence(u)131  requires sequenceV : RealSequence(v)132  shows polynomialEval(addSequence(u, v), n, X) =133    (polynomialEval(u, n, X):R) + (polynomialEval(v, n, X):R)134proof135  induction n136  | zero =>137    rw [polynomialEval.zero, polynomialEval.zero, polynomialEval.zero]138    ring139  | succ(k) using ih =>140    have valueU := RealSequence.value with sequenceU141    have valueV := RealSequence.value with sequenceV142    have combined := addSequence.sequence with sequenceU, sequenceV143    have value := addSequence.value with sequenceU, sequenceV, valueU, valueV144    rw [polynomialEval.succ, polynomialEval.succ, polynomialEval.succ, ih, value]145    ring146147-- Evaluation depends only on coefficients below the cutoff.148theorem polynomialEval.eq_prefix_aux (X : Real, n : Nat)149  shows ∀ u, ∀ v, RealSequence(u) → RealSequence(v) →150    (∀ k ∈ ℕ, k < n → u[k] = v[k]) →151      polynomialEval(u, n, X) = polynomialEval(v, n, X)152proof153  induction n154  | zero =>155    intros u v sequenceU sequenceV equal156    rw [polynomialEval.zero, polynomialEval.zero]157    rfl158  | succ(k) using ih =>159    intros u v sequenceU sequenceV equal160    have naturalK := nat.omega.forward at k with assumption161    have before : k < succ(k)162      unfold Less163      exact LessEqual.reflexive at succ(k) with164        Naturals.constructor.succ at k with assumption165    have termEqual := equal with k, naturalK, before166    have prefix : ∀ j ∈ ℕ, j < k → u[j] = v[j]167      intros j naturalJ smaller168      have typedJ := nat.omega.backward with naturalJ169      have below := Less.transitive_LessEqual at j, k, succ(k) with170        typedJ, assumption, Naturals.constructor.succ at k with assumption,171        smaller, LessEqual.successor at k with assumption172      exact equal with j, naturalJ, below173    have sumEqual := ih with u, v, sequenceU, sequenceV, prefix174    rw [polynomialEval.succ, polynomialEval.succ, sumEqual, termEqual]175    rfl176177theorem polynomialEval.eq_prefix (u v : Set, n : Nat, X : Real)178  requires sequenceU : RealSequence(u)179  requires sequenceV : RealSequence(v)180  requires equal : ∀ k ∈ ℕ, k < n → u[k] = v[k]181  shows polynomialEval(u, n, X) = polynomialEval(v, n, X)182proof183  exact polynomialEval.eq_prefix_aux at X, n with184    u, v, sequenceU, sequenceV, equal185186-- Multiplying every coefficient by a real scalar multiplies the value.187theorem polynomialEval.scale (coeff : Set, n : Nat, X C : Real)188  requires coefficients : RealSequence(coeff)189  shows polynomialEval(mulSequence(constantSequence(C), coeff), n, X) =190    C * (polynomialEval(coeff, n, X):R)191proof192  induction n193  | zero =>194    rw [polynomialEval.zero, polynomialEval.zero]195    ring196  | succ(k) using ih =>197    have constants := constantSequence.sequence at C198    have scaled := mulSequence.sequence with constants, coefficients199    have constantValue := RealSequence.value with constants200    have coeffValue := RealSequence.value with coefficients201    have value := mulSequence.value with constants, coefficients, constantValue, coeffValue202    have constant := constantSequence.value at C, k with *203    rw [polynomialEval.succ, polynomialEval.succ, ih, value, constant]204    ring205206theorem polynomialEval.neg (coeff : Set, n : Nat, X : Real)207  requires coefficients : RealSequence(coeff)208  shows polynomialEval(negSequence(coeff), n, X) =209    -(polynomialEval(coeff, n, X):R)210proof211  induction n212  | zero =>213    rw [polynomialEval.zero, polynomialEval.zero]214    ring215  | succ(k) using ih =>216    have coefficient := RealSequence.value with coefficients217    have negated := negSequence.sequence with coefficients218    have value := negSequence.value with coefficients, coefficient219    rw [polynomialEval.succ, polynomialEval.succ, ih, value]220    ring221222theorem polynomialEval.sub (u v : Set, n : Nat, X : Real)223  requires sequenceU : RealSequence(u)224  requires sequenceV : RealSequence(v)225  shows polynomialEval(subSequence(u, v), n, X) =226    (polynomialEval(u, n, X):R) - (polynomialEval(v, n, X):R)227proof228  have negated := negSequence.sequence with sequenceV229  unfold subSequence230  rw [polynomialEval.add, polynomialEval.neg]231  unfold realSubValue232  rfl233234-- At one, evaluation is exactly the finite sum of the coefficients.235theorem polynomialEval.at_one (coeff : Set, n : Nat)236  requires coefficients : RealSequence(coeff)237  shows polynomialEval(coeff, n, realOne) = realPartialSum(coeff, n)238proof239  induction n240  | zero =>241    rw [polynomialEval.zero, realPartialSum.zero]242    rfl243  | succ(k) using ih =>244    rw [polynomialEval.succ, realPartialSum.succ, ih, realPow.one]245    have coefficient := RealSequence.value with coefficients246    have product : realMulValue(coeff[k], realOne) = coeff[k]247      have value := realMulValue.one_right with coefficient248      unfold realMulValue249      unfold call2 at value250      exact value251    rw product252    rfl253254theorem polynomialEval.constant (coeff : Set) (X : Real)255  requires coefficients : RealSequence(coeff)256  shows polynomialEval(coeff, succ(0), X) = coeff[0]257proof258  rw [polynomialEval.succ, polynomialEval.zero, realPow.zero]259  have coefficient := RealSequence.value at coeff, 0 with coefficients260  have product : realMulValue(coeff[0], realOne) = coeff[0]261    have value := realMulValue.one_right with coefficient262    unfold realMulValue263    unfold call2 at value264    exact value265  rw product266  have zero : realAddValue(realZero, coeff[0]) = coeff[0]267    have value := realAddValue.zero_left with coefficient268    unfold realAddValue269    unfold call2 at value270    exact value271  exact zero272273-- A nonempty coefficient prefix evaluated at zero is its constant term.274theorem polynomialEval.at_zero_succ (coeff : Set, n : Nat)275  requires coefficients : RealSequence(coeff)276  shows polynomialEval(coeff, succ(n), realZero) = coeff[0]277proof278  induction n279  | zero =>280    exact polynomialEval.constant at coeff, realZero with coefficients281  | succ(k) using ih =>282    rw [polynomialEval.succ, ih, realPow.zero_succ]283    have coefficient := RealSequence.value at coeff, succ(k) with coefficients284    have constant := RealSequence.value at coeff, 0 with coefficients285    have product : realMulValue(coeff[succ(k)], realZero) = realZero286      have value := realMulValue.zero_right with coefficient287      unfold realMulValue288      unfold call2 at value289      exact value290    rw product291    have sum : realAddValue(coeff[0], realZero) = coeff[0]292      have value := realAddValue.zero_right with constant293      unfold realAddValue294      unfold call2 at value295      exact value296    exact sum297298theorem polynomialEval.linear (coeff : Set) (X : Real)299  requires coefficients : RealSequence(coeff)300  shows polynomialEval(coeff, succ(succ(0)), X) =301    (coeff[0]:R) + (coeff[succ(0)]:R) * X302proof303  rw [polynomialEval.succ, polynomialEval.constant]304  have first := RealSequence.value at coeff, 0 with coefficients305  have second := RealSequence.value at coeff, succ(0) with coefficients306  have powerOne : X ^ succ(0) = X307    rw [realPow.succ, realPow.zero]308    exact realMulValue.one_right with assumption309  rw powerOne310  unfold realAddValue311  unfold realMulValue312  unfold call2313  rfl314315theorem polynomialEval.quadratic (coeff : Set) (X : Real)316  requires coefficients : RealSequence(coeff)317  shows polynomialEval(coeff, succ(succ(succ(0))), X) =318    ((coeff[0]:R) + (coeff[succ(0)]:R) * X) +319      (coeff[succ(succ(0))]:R) * (X * X)320proof321  rw [polynomialEval.succ, polynomialEval.linear, realPow.two]322  have first := RealSequence.value at coeff, 0 with coefficients323  have second := RealSequence.value at coeff, succ(0) with coefficients324  have third := RealSequence.value at coeff, succ(succ(0)) with coefficients325  ring326