Grace/Cumulus/Real/Analysis/TaylorPolynomial.g17

Open in Workbench Download source

Imports

CauchyMeanValue · FiniteSum

Declarations

Source

1-- Real analysis: Taylor 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.Analysis.TaylorPolynomial8import CauchyMeanValue9import FiniteSum1011-- Section: Preparations12theorem realInvValue.one13  shows realInvValue((1:R)) = (1:R)14proof15  have nonzero : (1:R) ≠ 016    intro zero17    linarith18  have unit := realInvValue.mul_right with nonzero19  have typedInverse := realInvValue.real at (1:R) with realOne.real20  have identity := realMulValue.one_left with typedInverse21  rw ← identity22  exact unit2324theorem realDiv.one_right (A : Real)25  shows A / (1:R) = A26proof27  have division := realDiv.eq_mul_inv at A, (1:R) with assumption, realOne.real28  rw [division, realInvValue.one]29  exact realMulValue.one_right with assumption3031theorem realPow.nonzero (A : Real, n : Nat)32  requires nonzero : A ≠ 033  shows A ^ n ≠ 034proof35  induction n36  | zero =>37    rw realPow.zero38    intro zero39    linarith40  | succ(j) using ih =>41    rw realPow.succ42    intro vanishes43    have unit := realInvValue.mul_left with nonzero44    have typedInverse := realInvValue.real at A45    have typedPower := realPow.real at A, j46    have zero : A ^ j = 047      linear_combination realInvValue(A) * vanishes - A ^ j * unit48    exact ih with zero4950theorem realNat.succ_value (n : Nat)51  shows realNat(succ(n)) = (realNat(n):R) + 152proof53  rw realNat.succ54  unfold realAddValue55  unfold call256  rfl5758theorem realNat.ge_zero (n : Nat)59  shows (0:R) ≤ realNat(n)60proof61  induction n62  | zero =>63    rw realNat.zero64    linarith65  | succ(k) using ih =>66    have typedNat := realNat.real at k67    rw realNat.succ_value68    linarith6970theorem realNat.succ_nonzero (n : Nat)71  shows (realNat(n):R) + 1 ≠ 072proof73  have nonnegative := realNat.ge_zero at n74  have typedNat := realNat.real at n75  intro zero76  linarith7778theorem realNat.factorial_succ (n : Nat)79  shows realNat((n + 1)!) = ((realNat(n):R) + 1) * realNat(n!)80proof81  have step := factorial.succ at n82  rw [step, realNat.mul, realNat.add, realNat.one]83  rfl8485theorem realNat.factorial_positive (n : Nat)86  shows (0:R) < realNat(n!)87proof88  induction n89  | zero =>90    have factorialZero : (0:N)! = 1 by simp [factorial]91    rw [factorialZero, realNat.one]92    linarith93  | succ(k) using ih =>94    have one : k + 1 = succ(k) := add.right_one with *95    rw ← one96    rw realNat.factorial_succ97    have nonnegative := realNat.ge_zero at k98    have typedNat := realNat.real at k99    have factorialNat := factorial.closed at k100    have typedFactorial := realNat.real at k!101    have positive : (0:R) < (realNat(k):R) + 1 by linarith102    exact realMulValue.positive with positive, ih103104theorem realNat.factorial_nonzero (n : Nat)105  shows realNat(n!) ≠ (0:R)106proof107  have positive := realNat.factorial_positive at n108  have factorialNat := factorial.closed at n109  have typedFactorial := realNat.real at n!110  intro zero111  linarith112113-- Section: BasePowers114-- The function x ↦ (B − x)^k, built from the pointwise constructors so that115-- the derivative rules apply to it directly.116def basePower (B : Real, k : Nat) → Set117  | B, zero => constantRealFunction(realOne)118  | B, succ(j) =>119    pointwiseMul(pointwiseSub(constantRealFunction(B), identity(ℝ)),120      basePower(B, j))121122def linearFactor (B : Real) : Set :=123  pointwiseSub(constantRealFunction(B), identity(ℝ))124125theorem linearFactor.function (B : Real)126  shows linearFactor(B) : ℝ → ℝ127proof128  have constant := constantRealFunction.function at B129  have identityFunction := identity.function at ℝ130  unfold linearFactor131  exact pointwiseSub.function with constant, identityFunction132133theorem linearFactor.value (B X : Real)134  shows linearFactor(B)(X) = B - X135proof136  have realX : X ∈ ℝ by simp [Real]137  have constant := constantRealFunction.function at B138  have identityFunction := identity.function at ℝ139  have constantValue := constantRealFunction.value at B, X140  have identityValue := identity.apply with realX141  have typedConstant : Real(constantRealFunction(B)(X)) by rwa constantValue142  have typedIdentity : Real(identity(ℝ)(X)) by rwa identityValue143  have value := pointwiseSub.value at144    constantRealFunction(B), identity(ℝ), X with145    assumption, constant, identityFunction, typedConstant, typedIdentity146  rw [constantValue, identityValue] at value147  unfold linearFactor148  cc149150theorem linearFactor.derivative (B X : Real)151  shows HasDerivativeAt(linearFactor(B), -(1:R), X)152proof153  have constant := constantRealFunction.has_derivative_at at B, X154  have identityDerivative := identity.has_derivative_at at X155  have raw := HasDerivativeAt.sub with constant, identityDerivative156  have value : realZero - realOne = -(1:R) by ring157  unfold linearFactor158  exact HasDerivativeAt.congr_value with raw, value159160theorem basePower.succ (B : Real, k : Nat)161  shows basePower(B, k + 1) = pointwiseMul(linearFactor(B), basePower(B, k))162proof163  have one : k + 1 = succ(k) := add.right_one with *164  rw one165  rw basePower166  unfold linearFactor167  rfl168169theorem basePower.function (B : Real, k : Nat)170  shows basePower(B, k) : ℝ → ℝ171proof172  induction k173  | zero =>174    rw basePower175    exact constantRealFunction.function with realOne.real176  | succ(j) using ih =>177    have one : j + 1 = succ(j) := add.right_one with *178    rw ← one179    rw basePower.succ180    have linear := linearFactor.function at B181    exact pointwiseMul.function with linear, ih182183theorem basePower.value (B X : Real, k : Nat)184  shows basePower(B, k)(X) = (B - X) ^ k185proof186  induction k187  | zero =>188    rw [basePower, realPow.zero]189    exact constantRealFunction.value with realOne.real, assumption190  | succ(j) using ih =>191    have one : j + 1 = succ(j) := add.right_one with *192    rw ← one193    rw [basePower.succ, one, realPow.succ]194    have realX : X ∈ ℝ by simp [Real]195    have linear := linearFactor.function at B196    have power := basePower.function at B, j197    have linearValue := linearFactor.value at B, X198    have typedDifference := realSubValue.real at B, X199    have typedLinear : Real(linearFactor(B)(X)) by rwa linearValue200    have typedPower : Real(basePower(B, j)(X))201      exact FunctionBetween.apply_closed with power, realX202    have value := pointwiseMul.value at linearFactor(B), basePower(B, j), X with203      assumption, linear, power, typedLinear, typedPower204    rwa [linearValue, ih] at value205206-- Section: TaylorTerms207-- The Taylor terms f⁽ᵏ⁾(X) (B − X)ᵏ / k! as a real sequence in k; written208-- by name here so that the generated laws can substitute the index.209defgraph taylorTerms (f : Set, X B : Real) (k ∈ ℕ) : ℝ :=210  iteratedDerivative(f, k)(X) * (B - X) ^ k / k!211requires function : f : ℝ → ℝ212proof213  have naturalK := nat.omega.backward with member214  have realX : X ∈ ℝ by simp [Real]215  have kFunction := iteratedDerivative.function at f, k with function216  have typedValue : Real(iteratedDerivative(f, k)(X))217    exact FunctionBetween.apply_closed with kFunction, realX218  have factorialNat := factorial.closed at k219  have typedFactorial := realNat.real at k!220  have typedPower := realPow.real at B - X, k221  have typedProduct := realMulValue.real with typedValue, typedPower222  exact realDiv.real with typedProduct, typedFactorial223224-- A sum of Taylor terms is written out, ∑ k ≤ n, f⁽ᵏ⁾(A) * (B - A) ^ k / k!,225-- and prints that way.226notation sequence taylorTerms227228-- Section: TaylorApproximant229-- The function x ↦ ∑_{k ≤ n} f⁽ᵏ⁾(x) (B − x)ᵏ / k!, built from the pointwise230-- constructors; its value at B is f(B) and its derivative telescopes.231def taylorApproximant (f : Set, B : Real, n : Nat) → Set232  | f, B, zero => f233  | f, B, succ(j) =>234    pointwiseAdd(taylorApproximant(f, B, j),235      pointwiseMul(236        constantRealFunction(realInvValue(realNat(factorial(succ(j))))),237        pointwiseMul(iteratedDerivative(f, succ(j)), basePower(B, succ(j)))))238239def taylorStep (f : Set, B : Real, k : Nat) : Set :=240  pointwiseMul(constantRealFunction(realInvValue(realNat(k!))),241    pointwiseMul(iteratedDerivative(f, k), basePower(B, k)))242243theorem taylorApproximant.succ (f : Set) (B : Real, n : Nat)244  shows taylorApproximant(f, B, n + 1) =245    pointwiseAdd(taylorApproximant(f, B, n), taylorStep(f, B, n + 1))246proof247  have one : n + 1 = succ(n) := add.right_one with *248  rw one249  rw taylorApproximant250  unfold taylorStep251  rfl252253theorem taylorStep.function (f : Set) (B : Real, k : Nat)254  requires function : f : ℝ → ℝ255  shows taylorStep(f, B, k) : ℝ → ℝ256proof257  have factorialNat := factorial.closed at k258  have typedFactorial := realNat.real at k!259  have typedInverse := realInvValue.real with typedFactorial260  have constant := constantRealFunction.function with typedInverse261  have kFunction := iteratedDerivative.function at f, k with function262  have power := basePower.function at B, k263  have product := pointwiseMul.function with kFunction, power264  unfold taylorStep265  exact pointwiseMul.function with constant, product266267theorem taylorStep.value (f : Set) (B X : Real, k : Nat)268  requires function : f : ℝ → ℝ269  shows taylorStep(f, B, k)(X) = f⁽ᵏ⁾(X) * (B - X) ^ k / k!270proof271  have realX : X ∈ ℝ by simp [Real]272  have factorialNat := factorial.closed at k273  have typedFactorial := realNat.real at k!274  have typedInverse := realInvValue.real with typedFactorial275  have constant := constantRealFunction.function with typedInverse276  have kFunction := iteratedDerivative.function at f, k with function277  have power := basePower.function at B, k278  have product := pointwiseMul.function with kFunction, power279  have constantValue := constantRealFunction.value at280    realInvValue(realNat(k!)), X with281    typedInverse, assumption282  have typedConstant : Real(constantRealFunction(realInvValue(realNat(k!)))(X))283    rwa constantValue284  have typedK : Real(iteratedDerivative(f, k)(X))285    exact FunctionBetween.apply_closed with kFunction, realX286  have powerValue := basePower.value at B, X, k287  have typedPowerValue := realPow.real at B - X, k288  have typedPower : Real(basePower(B, k)(X)) by rwa powerValue289  have innerValue := pointwiseMul.value at290    iteratedDerivative(f, k), basePower(B, k), X with291      assumption, kFunction, power, typedK, typedPower292  have typedInner : Real(pointwiseMul(iteratedDerivative(f, k), basePower(B, k))(X))293    exact FunctionBetween.apply_closed with product, realX294  have outerValue := pointwiseMul.value at295    constantRealFunction(realInvValue(realNat(k!))),296    pointwiseMul(iteratedDerivative(f, k), basePower(B, k)), X with297      assumption, constant, product, typedConstant, typedInner298  have typedProduct := realMulValue.real with typedK, typedPowerValue299  have division := realDiv.eq_mul_inv with typedProduct, typedFactorial300  simp [taylorStep]301  ring302303theorem taylorApproximant.function (f : Set) (B : Real, n : Nat)304  requires function : f : ℝ → ℝ305  shows taylorApproximant(f, B, n) : ℝ → ℝ306proof307  induction n308  | zero =>309    rw taylorApproximant310    exact function311  | succ(j) using ih =>312    have one : j + 1 = succ(j) := add.right_one with *313    rw ← one314    rw taylorApproximant.succ315    have step := taylorStep.function at f, B, j + 1 with function316    exact pointwiseAdd.function with ih, step317318theorem taylorApproximant.step (f : Set) (B X : Real, n : Nat)319  requires function : f : ℝ → ℝ320  shows taylorApproximant(f, B, n + 1)(X) =321    taylorApproximant(f, B, n)(X) + f⁽ⁿ⁺¹⁾(X) * (B - X) ^ (n + 1) / (n + 1)!322proof323  have realX : X ∈ ℝ by simp [Real]324  have previous := taylorApproximant.function at f, B, n with function325  have step := taylorStep.function at f, B, n + 1 with function326  have typedPrevious : Real(taylorApproximant(f, B, n)(X))327    exact FunctionBetween.apply_closed with previous, realX328  have typedStep : Real(taylorStep(f, B, n + 1)(X))329    exact FunctionBetween.apply_closed with step, realX330  have sum := pointwiseAdd.value at331    taylorApproximant(f, B, n), taylorStep(f, B, n + 1), X with332      assumption, previous, step, typedPrevious, typedStep333  have stepValue := taylorStep.value at f, B, X, n + 1 with function334  rw taylorApproximant.succ335  rwa stepValue at sum336337-- Section: TaylorApproximantValues338theorem taylorApproximant.value (f : Set) (B X : Real, n : Nat)339  requires function : f : ℝ → ℝ340  shows taylorApproximant(f, B, n)(X) = ∑ k ≤ n, f⁽ᵏ⁾(X) * (B - X) ^ k / k!341proof342  induction n343  | zero =>344    have one : (0:N) + 1 = succ(0) := add.right_one at (0:N)345    rw one346    rw [realPartialSum.succ, realPartialSum.zero, taylorApproximant]347    have termValue := taylorTerms.value at f, X, B, (0:N) with function348    rw [termValue, iteratedDerivative.zero, realPow.zero]349    have factorialZero : (0:N)! = 1 by simp [factorial]350    rw [factorialZero, realNat.one]351    have realX : X ∈ ℝ by simp [Real]352    have typedFX : Real(f(X))353      exact FunctionBetween.apply_closed with function, realX354    have unit := realMulValue.one_right with typedFX355    rw [unit, realDiv.one_right]356    have zero := realAddValue.zero_left with typedFX357    unfold call2 at zero358    unfold realAddValue359    cc360  | succ(j) using ih =>361    have one : j + 1 = succ(j) := add.right_one with *362    rw ← one363    have step := taylorApproximant.step at f, B, X, j with function364    have two : j + 1 + 1 = succ(j + 1) := add.right_one at j + 1365    rw [step, two, realPartialSum.succ, ← ih]366    have termValue := taylorTerms.value at f, X, B, j + 1 with function367    rw termValue368    unfold realAddValue369    unfold call2370    rfl371372theorem taylorApproximant.at_endpoint (f : Set) (B : Real, n : Nat)373  requires function : f : ℝ → ℝ374  shows taylorApproximant(f, B, n)(B) = f(B)375proof376  induction n377  | zero =>378    rw taylorApproximant379    rfl380  | succ(j) using ih =>381    have one : j + 1 = succ(j) := add.right_one with *382    rw ← one383    have step := taylorApproximant.step at f, B, B, j with function384    rw [step, ih]385    have self := realSubValue.self at B386    rw [self, one, realPow.zero_succ]387    have realB : B ∈ ℝ by simp [Real]388    have kFunction := iteratedDerivative.function at f, succ(j) with function389    have typedK : Real(iteratedDerivative(f, succ(j))(B))390      exact FunctionBetween.apply_closed with kFunction, realB391    have factorialNat := factorial.closed at succ(j)392    have typedFactorial := realNat.real at succ(j)!393    have zeroProduct := realMulValue.zero_right with typedK394    have zeroQuotient := realDiv.zero_left with typedFactorial395    rw [zeroProduct, zeroQuotient]396    have typedFB : Real(f(B))397      exact FunctionBetween.apply_closed with function, realB398    ring399400-- Section: TaylorDerivatives401theorem basePower.derivative (B X : Real, k : Nat)402  shows HasDerivativeAt(basePower(B, k + 1),403    -((realNat(k) + 1) * (B - X) ^ k), X)404proof405  induction k406  | zero =>407    rw basePower.succ408    rw basePower409    have linear := linearFactor.derivative at B, X410    have constantDerivative := constantRealFunction.has_derivative_at at411      realOne, X412    have linearValue := linearFactor.value at B, X413    have constantValue := constantRealFunction.value at realOne, X with414      realOne.real, assumption415    have typedDifference := realSubValue.real at B, X416    have typedOne := realOne.real417    have typedLinear : Real(linearFactor(B)(X)) by rwa linearValue418    have typedConstant : Real(constantRealFunction(realOne)(X))419      rwa constantValue420    have product := HasDerivativeAt.mul_value with421      linear, constantDerivative, typedLinear, typedConstant422    have algebra : -(1:R) * constantRealFunction(realOne)(X) +423        linearFactor(B)(X) * realZero =424        -(((realNat(0):R) + 1) * (B - X) ^ 0)425      rw [constantValue, linearValue, realPow.zero, realNat.zero]426      ring427    exact HasDerivativeAt.congr_value with product, algebra428  | succ(j) using ih =>429    rw basePower.succ430    have one : j + 1 = succ(j) := add.right_one with *431    rw ← one432    have linear := linearFactor.derivative at B, X433    have linearValue := linearFactor.value at B, X434    have powerValue := basePower.value at B, X, j + 1435    have typedDifference := realSubValue.real at B, X436    have typedLinear : Real(linearFactor(B)(X)) by rwa linearValue437    have typedPowerValue := realPow.real at B - X, j + 1438    have typedPower : Real(basePower(B, j + 1)(X)) by rwa powerValue439    have product := HasDerivativeAt.mul_value with440      linear, ih, typedLinear, typedPower441    have typedBase := realPow.real at B - X, j442    have typedNat := realNat.real at j443    have algebra : -(1:R) * basePower(B, j + 1)(X) +444        linearFactor(B)(X) * (-(((realNat(j):R) + 1) * (B - X) ^ j)) =445        -(((realNat(j + 1):R) + 1) * (B - X) ^ (j + 1))446      rw [powerValue, linearValue, one, realPow.succ, realNat.succ_value]447      ring448    exact HasDerivativeAt.congr_value with product, algebra449450theorem taylorStep.derivative (f : Set) (B X : Real, k : Nat)451  requires function : f : ℝ → ℝ452  requires differentiable : DifferentiableAt(f⁽ᵏ⁺¹⁾, X)453  shows HasDerivativeAt(taylorStep(f, B, k + 1),454    f⁽ᵏ⁺¹⁺¹⁾(X) * (B - X) ^ (k + 1) / (k + 1)! -455      f⁽ᵏ⁺¹⁾(X) * (B - X) ^ k / k!, X)456proof457  have realX : X ∈ ℝ by simp [Real]458  have kFunction := iteratedDerivative.function at f, k + 1 with function459  have nextFunction := iteratedDerivative.function at f, k + 1 + 1 with function460  have derivativeK := derivative.has_derivative_at with differentiable461  have shift := iteratedDerivative.succ at f, k + 1462  rw ← shift at derivativeK463  have powerDerivative := basePower.derivative at B, X, k464  have powerValue := basePower.value at B, X, k + 1465  have typedDifference := realSubValue.real at B, X466  have typedPowerValue := realPow.real at B - X, k + 1467  have typedBase := realPow.real at B - X, k468  have typedPower : Real(basePower(B, k + 1)(X)) by rwa powerValue469  have typedK : Real(iteratedDerivative(f, k + 1)(X))470    exact FunctionBetween.apply_closed with kFunction, realX471  have typedNext : Real(iteratedDerivative(f, k + 1 + 1)(X))472    exact FunctionBetween.apply_closed with nextFunction, realX473  have product := HasDerivativeAt.mul_value with474    derivativeK, powerDerivative, typedK, typedPower475  have factorialNat := factorial.closed at k476  have factorialSuccNat := factorial.closed at k + 1477  have typedFactorial := realNat.real at k!478  have typedFactorialSucc := realNat.real at (k + 1)!479  have typedInverse := realInvValue.real with typedFactorialSucc480  have typedNat := realNat.real at k481  have scaled := HasDerivativeAt.scale at482    pointwiseMul(iteratedDerivative(f, k + 1), basePower(B, k + 1)),483    realInvValue(realNat((k + 1)!)),484    iteratedDerivative(f, k + 1 + 1)(X) * basePower(B, k + 1)(X) +485      iteratedDerivative(f, k + 1)(X) * (-(((realNat(k):R) + 1) * (B - X) ^ k)),486    X with typedInverse, product487  have successorNonzero := realNat.succ_nonzero at k488  have factorialNonzero := realNat.factorial_nonzero at k489  have factorialSplit := realNat.factorial_succ at k490  have inverseSplit : realInvValue(realNat((k + 1)!)) =491      realInvValue((realNat(k):R) + 1) * realInvValue(realNat(k!))492    rw factorialSplit493    exact realInvValue.mul with successorNonzero, factorialNonzero494  have unit := realInvValue.mul_right with successorNonzero495  have typedProductNext := realMulValue.real with typedNext, typedPowerValue496  have typedProductK := realMulValue.real with typedK, typedBase497  have divisionNext := realDiv.eq_mul_inv with498    typedProductNext, typedFactorialSucc499  have divisionK := realDiv.eq_mul_inv with typedProductK, typedFactorial500  have typedSuccessorInverse := realInvValue.real at (realNat(k):R) + 1501  have typedFactorialInverse := realInvValue.real with typedFactorial502  have algebra : realInvValue(realNat((k + 1)!)) *503      (iteratedDerivative(f, k + 1 + 1)(X) * basePower(B, k + 1)(X) +504        iteratedDerivative(f, k + 1)(X) *505          (-(((realNat(k):R) + 1) * (B - X) ^ k))) =506      iteratedDerivative(f, k + 1 + 1)(X) * (B - X) ^ (k + 1) /507          realNat((k + 1)!) -508        iteratedDerivative(f, k + 1)(X) * (B - X) ^ k / realNat(k!)509    rw [powerValue, divisionNext, divisionK]510    symm511    linear_combination (iteratedDerivative(f, k + 1)(X) * (B - X) ^ k *512        realInvValue(realNat(k!))) * unit +513      (iteratedDerivative(f, k + 1)(X) * (B - X) ^ k * ((realNat(k):R) + 1)) *514        inverseSplit515  unfold taylorStep516  exact HasDerivativeAt.congr_value with scaled, algebra517518-- The derivative of x ↦ ∑_{k ≤ n} f⁽ᵏ⁾(x)(B − x)ᵏ/k! telescopes to its last519-- term's derivative, f⁽ⁿ⁺¹⁾(x)(B − x)ⁿ/n!.520theorem taylorApproximant.derivative (f : Set) (B X : Real, n : Nat)521  requires function : f : ℝ → ℝ522  shows (∀ k ≤ n, DifferentiableAt(f⁽ᵏ⁾, X)) →523    HasDerivativeAt(taylorApproximant(f, B, n),524      f⁽ⁿ⁺¹⁾(X) * (B - X) ^ n / n!, X)525proof526  induction n527  | zero =>528    intro smooth529    rw taylorApproximant530    have naturalZero : Nat((0:N)) by typecheck531    have reflexive : (0:N) ≤ (0:N) by arith532    have differentiable := smooth with (0:N), naturalZero, reflexive533    rw iteratedDerivative.zero at differentiable534    have hasDerivative := derivative.has_derivative_at with differentiable535    have typedValue := derivative.real at f, X536    have factorialZero : (0:N)! = 1 by simp [factorial]537    have algebra : derivative(f)(X) =538        iteratedDerivative(f, (0:N) + 1)(X) * (B - X) ^ (0:N) / realNat((0:N)!)539      rw [iteratedDerivative.succ, iteratedDerivative.zero, realPow.zero,540        factorialZero, realNat.one]541      have unit := realMulValue.one_right with typedValue542      rw [unit, realDiv.one_right]543      rfl544    exact HasDerivativeAt.congr_value with hasDerivative, algebra545  | succ(j) using ih =>546    intro smooth547    have one : j + 1 = succ(j) := add.right_one with *548    rw ← one549    have previous : ∀ k, Nat(k) → k ≤ j →550        DifferentiableAt(iteratedDerivative(f, k), X)551      intros k naturalK below552      have belowSucc : k ≤ succ(j) by arith553      exact smooth with k, naturalK, belowSucc554    have previousDerivative := ih with previous555    have naturalSucc : Nat(j + 1) by typecheck556    have reflexive : j + 1 ≤ succ(j) by arith557    have differentiable := smooth with j + 1, naturalSucc, reflexive558    have stepDerivative := taylorStep.derivative at f, B, X, j with559      function, differentiable560    rw taylorApproximant.succ561    have sum := HasDerivativeAt.add with previousDerivative, stepDerivative562    have realX : X ∈ ℝ by simp [Real]563    have kFunction := iteratedDerivative.function at f, j + 1 with function564    have nextFunction := iteratedDerivative.function at f, j + 1 + 1 with565      function566    have typedK : Real(iteratedDerivative(f, j + 1)(X))567      exact FunctionBetween.apply_closed with kFunction, realX568    have typedNext : Real(iteratedDerivative(f, j + 1 + 1)(X))569      exact FunctionBetween.apply_closed with nextFunction, realX570    have typedDifference := realSubValue.real at B, X571    have typedBase := realPow.real at B - X, j572    have typedPowerValue := realPow.real at B - X, j + 1573    have factorialNat := factorial.closed at j574    have factorialSuccNat := factorial.closed at j + 1575    have typedFactorial := realNat.real at j!576    have typedFactorialSucc := realNat.real at (j + 1)!577    have typedProductK := realMulValue.real with typedK, typedBase578    have typedProductNext := realMulValue.real with typedNext, typedPowerValue579    have typedQuotientK := realDiv.real with typedProductK, typedFactorial580    have typedQuotientNext := realDiv.real with581      typedProductNext, typedFactorialSucc582    have algebra : iteratedDerivative(f, j + 1)(X) * (B - X) ^ j / realNat(j!) +583        (iteratedDerivative(f, j + 1 + 1)(X) * (B - X) ^ (j + 1) /584            realNat((j + 1)!) -585          iteratedDerivative(f, j + 1)(X) * (B - X) ^ j / realNat(j!)) =586        iteratedDerivative(f, j + 1 + 1)(X) * (B - X) ^ (j + 1) /587          realNat((j + 1)!)588      ring589    exact HasDerivativeAt.congr_value with sum, algebra590