Grace/Cumulus/Real/Analysis/Taylor.g17

Open in Workbench Download source

Imports

TaylorPolynomial

Declarations

• Taylor.theorem theorem derivation
• Taylor.mean_value theorem derivation

Source

1-- Real analysis: Taylor's theorem with the Lagrange remainder2-- 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.Taylor8import TaylorPolynomial910-- Section: Taylor11-- Taylor's theorem with the Lagrange remainder: when f is n + 1 times12-- differentiable on [A, B], some C strictly between A and B has13-- f(B) = ∑_{k ≤ n} f⁽ᵏ⁾(A)(B − A)ᵏ/k! + f⁽ⁿ⁺¹⁾(C)(B − A)ⁿ⁺¹/(n + 1)!.14-- The proof applies the Cauchy mean value theorem to the approximant15-- x ↦ ∑_{k ≤ n} f⁽ᵏ⁾(x)(B − x)ᵏ/k! and to x ↦ (B − x)ⁿ⁺¹.16theorem Taylor.theorem (f : ℝ → ℝ) (A B : Real, n : Nat)17  requires ordered : A < B18  requires smooth : ∀ k ≤ n,19    ∀ X ∈ closedInterval(A, B), DifferentiableAt(f⁽ᵏ⁾, X)20  shows ∃ C ∈ ℝ, A < C ∧ C < B ∧21    f(B) = ∑ k ≤ n, f⁽ᵏ⁾(A) * (B - A) ^ k / k! +22      f⁽ⁿ⁺¹⁾(C) * (B - A) ^ (n + 1) / (n + 1)!23proof24  have orderedWeak := realLess.implies_le with ordered25  have memberA := closedInterval.left_mem with orderedWeak26  have function : f : ℝ → ℝ by assumption27  have approximantFunction := taylorApproximant.function at f, B, n with28    function29  have powerFunction := basePower.function at B, n + 130  have intervalReal := closedInterval.subset_reals at A, B31  have pointwise : ∀ X ∈ closedInterval(A, B), ∀ k, Nat(k) → k ≤ n →32      DifferentiableAt(iteratedDerivative(f, k), X)33    intros X memberX k naturalK below34    have onInterval := smooth with k, naturalK, below35    exact onInterval with X, memberX36  have approximantDifferentiable : ∀ X ∈ closedInterval(A, B),37      DifferentiableAt(taylorApproximant(f, B, n), X)38    intros X memberX39    have realX := intervalReal with X, memberX40    have typedX : Real(X) by exact realX41    have atX := pointwise with X, memberX42    have implication := taylorApproximant.derivative at f, B, X, n with function43    have hasDerivative := implication with atX44    exact HasDerivativeAt.differentiable_at with hasDerivative45  have powerDifferentiable : ∀ X ∈ closedInterval(A, B),46      DifferentiableAt(basePower(B, n + 1), X)47    intros X memberX48    have realX := intervalReal with X, memberX49    have typedX : Real(X) by exact realX50    have hasDerivative := basePower.derivative at B, X, n51    exact HasDerivativeAt.differentiable_at with hasDerivative52  have continuousApproximant := ContinuousOn.of_differentiable with53    approximantFunction, intervalReal, approximantDifferentiable54  have continuousPower := ContinuousOn.of_differentiable with55    powerFunction, intervalReal, powerDifferentiable56  have interior : ∀ C ∈ ℝ, A < C → C < B → C ∈ closedInterval(A, B)57    intros C realC left right58    have lower := realLess.implies_le with left59    have upper := realLess.implies_le with right60    have data : C ∈ ℝ ∧ A ≤ C ∧ C ≤ B by refine ⟨realC, lower, upper⟩61    exact closedInterval.membership.backward with data62  have interiorApproximant : ∀ C ∈ ℝ, A < C → C < B →63      DifferentiableAt(taylorApproximant(f, B, n), C)64    intros C realC left right65    have member := interior with C, realC, left, right66    exact approximantDifferentiable with C, member67  have interiorPower : ∀ C ∈ ℝ, A < C → C < B →68      DifferentiableAt(basePower(B, n + 1), C)69    intros C realC left right70    have member := interior with C, realC, left, right71    exact powerDifferentiable with C, member72  obtain ⟨C, realC, left, right, equation⟩ := CauchyMeanValue.theorem with73    approximantFunction, powerFunction, ordered, continuousApproximant,74    continuousPower, interiorApproximant, interiorPower75  have typedC : Real(C) by exact realC76  have memberC := interior with C, realC, left, right77  have atC := pointwise with C, memberC78  have implication := taylorApproximant.derivative at f, B, C, n with function79  have approximantDerivative := implication with atC80  have approximantValue := derivative.of_has_derivative with81    approximantDerivative82  have powerDerivative := basePower.derivative at B, C, n83  have powerDerivativeValue := derivative.of_has_derivative with powerDerivative84  have powerAtB : basePower(B, n + 1)(B) = (0:R)85    have value := basePower.value at B, B, n + 186    have self := realSubValue.self at B87    have one : n + 1 = succ(n) := add.right_one with *88    rw [value, self, one]89    exact realPow.zero_succ at n90  have powerAtA := basePower.value at B, A, n + 191  have approximantAtB := taylorApproximant.at_endpoint at f, B, n with function92  have approximantAtA := taylorApproximant.value at f, B, A, n with function93  rw [approximantValue, powerDerivativeValue, powerAtB, powerAtA,94    approximantAtB, approximantAtA] at equation95  have realB : B ∈ ℝ by simp [Real]96  have typedFB : Real(f(B))97    exact FunctionBetween.apply_closed with function, realB98  have nextFunction := iteratedDerivative.function at f, n + 1 with function99  have typedNext : Real(iteratedDerivative(f, n + 1)(C))100    exact FunctionBetween.apply_closed with nextFunction, realC101  have typedWidth := realSubValue.real at B, A102  have typedGap := realSubValue.real at B, C103  have gapNonzero : B - C ≠ 0104    intro zero105    linarith106  have powerNonzero := realPow.nonzero at B - C, n with typedGap, gapNonzero107  have typedPowerGap := realPow.real at B - C, n108  have typedPowerWidth := realPow.real at B - A, n + 1109  have typedNat := realNat.real at n110  have successorNonzero := realNat.succ_nonzero at n111  have factorialNat := factorial.closed at n112  have factorialSuccNat := factorial.closed at n + 1113  have typedFactorial := realNat.real at n!114  have typedFactorialSucc := realNat.real at (n + 1)!115  have factorialNonzero := realNat.factorial_nonzero at n116  have factorialSplit := realNat.factorial_succ at n117  have inverseSplit : realInvValue(realNat((n + 1)!)) =118      realInvValue((realNat(n):R) + 1) * realInvValue(realNat(n!))119    rw factorialSplit120    exact realInvValue.mul with successorNonzero, factorialNonzero121  have unitGap := realInvValue.mul_right with powerNonzero122  have unitSuccessor := realInvValue.mul_right with successorNonzero123  have typedGapInverse := realInvValue.real with typedPowerGap124  have typedSuccessorInverse := realInvValue.real at (realNat(n):R) + 1125  have typedFactorialInverse := realInvValue.real with typedFactorial126  have typedFactorialSuccInverse := realInvValue.real with typedFactorialSucc127  have sequence : RealSequence(taylorTerms(f, A, B))128    unfold RealSequence129    exact taylorTerms.function at f, A, B with function130  have typedSum := realPartialSum.real at taylorTerms(f, A, B), n + 1 with131    sequence132  have typedProductGap := realMulValue.real with typedNext, typedPowerGap133  have typedProductWidth := realMulValue.real with typedNext, typedPowerWidth134  have divisionGap := realDiv.eq_mul_inv with typedProductGap, typedFactorial135  have divisionWidth := realDiv.eq_mul_inv with136    typedProductWidth, typedFactorialSucc137  rw divisionGap at equation138  witness C139  refine ⟨realC, left, right, _⟩140  rw divisionWidth141  symm142  linear_combination ((f(B) - (∑ k < n + 1, taylorTerms(f, A, B)(k):R)) *143        ((realNat(n):R) + 1) * realInvValue((realNat(n):R) + 1) -144      iteratedDerivative(f, n + 1)(C) * realInvValue(realNat(n!)) *145        (B - A) ^ (n + 1) * realInvValue((realNat(n):R) + 1)) * unitGap +146    (f(B) - (∑ k < n + 1, taylorTerms(f, A, B)(k):R)) * unitSuccessor +147    (iteratedDerivative(f, n + 1)(C) * (B - A) ^ (n + 1)) * inverseSplit -148    (realInvValue((B - C) ^ n) * realInvValue((realNat(n):R) + 1)) * equation149150-- With n = 0 the sum is the single term f(A) and the remainder is151-- f′(C)(B − A): Taylor's theorem specializes to the mean value theorem.152theorem Taylor.mean_value (f : ℝ → ℝ) (A B : Real)153  requires ordered : A < B154  requires differentiable : ∀ X ∈ closedInterval(A, B), DifferentiableAt(f, X)155  shows ∃ C ∈ ℝ, A < C ∧ C < B ∧ f(B) = f(A) + f′(C) * (B - A)156proof157  have function : f : ℝ → ℝ by assumption158  have smooth : ∀ k ≤ (0:N),159      ∀ X ∈ closedInterval(A, B), DifferentiableAt(f⁽ᵏ⁾, X)160    intros k naturalK below161    have split := natural.zero_or_successor with naturalK162    cases split with zero | successor163    . intros X memberX164      rw [zero, iteratedDerivative.zero]165      exact differentiable with X, memberX166    . obtain ⟨j, naturalJ, equal⟩ := successor167      rw equal at below168      exfalso169      arith170  obtain ⟨C, realC, left, right, expansion⟩ := Taylor.theorem at f, A, B, (0:N) with171    function, ordered, smooth172  have typedC : Real(C) by exact realC173  have one : (0:N) + 1 = succ(0) := add.right_one at (0:N)174  rw one at expansion175  rw [realPartialSum.succ, realPartialSum.zero] at expansion176  have termValue := taylorTerms.value at f, A, B, (0:N) with function177  rw [termValue, iteratedDerivative.zero, realPow.zero] at expansion178  have factorialZero : (0:N)! = 1 by simp [factorial]179  have factorialOne : succ(0)! = 1 by simp [factorial]180  rw [factorialZero, factorialOne, realNat.one] at expansion181  rw [← one, iteratedDerivative.succ, iteratedDerivative.zero, one] at expansion182  have realA : A ∈ ℝ by simp [Real]183  have typedFA : Real(f(A)) by exact FunctionBetween.apply_closed with function, realA184  have typedDerivative := derivative.real at f, C185  have typedWidth := realSubValue.real at B, A186  have powerOne : (B - A) ^ succ(0) = B - A187    rw [realPow.succ, realPow.zero]188    exact realMulValue.one_right with typedWidth189  have unitA := realMulValue.one_right with typedFA190  have typedProduct := realMulValue.real with typedDerivative, typedWidth191  rw [powerOne, unitA, realDiv.one_right, realDiv.one_right] at expansion192  have zeroLeft := realAddValue.zero_left with typedFA193  unfold call2 at zeroLeft194  unfold realAddValue at expansion195  rw zeroLeft at expansion196  witness C197  refine ⟨realC, left, right, _⟩198  exact expansion199