Grace/Cumulus/Real/Analysis/Derivative.g17

Open in Workbench Download source

Imports

Set.Choice · Differentiation

Declarations

Source

1-- Real analysis: the derivative as a function2-- 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.Derivative8import Set.Choice9import Differentiation1011-- Section: Derivative12-- The derivative of f at X is the number D with HasDerivativeAt(f, D, X)13-- when f is differentiable there, and zero otherwise.14defchoose derivativeValue (f : Set, X : Real) (D ∈ ℝ) :=15  HasDerivativeAt(f, D, X) ∨ (¬DifferentiableAt(f, X) ∧ D = (0:R))16proof17  have split : DifferentiableAt(f, X) ∨ ¬DifferentiableAt(f, X) by tauto18  cases split with differentiable | nowhere19  . obtain ⟨D, realD, hasDerivative⟩ := differentiable20    witness D21    refine ⟨realD, _⟩22    left23    exact hasDerivative24  . have realZeroMember : (0:R) ∈ ℝ by exact realZero.real25    witness (0:R)26    refine ⟨realZeroMember, _⟩27    right28    refine ⟨nowhere, _⟩29    rfl3031defgraph derivative (f : Set) (X ∈ ℝ) : ℝ := derivativeValue(f, X)32proof33  obtain ⟨realD, property⟩ := derivativeValue.selected at f, X34  exact realD3536-- The derivative is written with a prime, f′, and its value f′(X); a37-- doubled prime is the second derivative, f″.38notation postfix 95 "′" => derivative3940theorem derivative.of_has_derivative (f : Set) (D X : Real)41  requires hasDerivative : HasDerivativeAt(f, D, X)42  shows f′(X) = D43proof44  have value := derivative.value at f, X45  obtain ⟨realD, property⟩ := derivativeValue.selected at f, X46  rw value47  cases property with chosen | nowhere48  . exact HasDerivativeAt.unique with chosen, hasDerivative49  . obtain ⟨notDifferentiable, zero⟩ := nowhere50    exfalso51    apply notDifferentiable52    exact HasDerivativeAt.differentiable_at with hasDerivative5354theorem derivative.has_derivative_at (f : Set) (X : Real)55  requires differentiable : DifferentiableAt(f, X)56  shows HasDerivativeAt(f, f′(X), X)57proof58  have value := derivative.value at f, X59  obtain ⟨realD, property⟩ := derivativeValue.selected at f, X60  rw value61  cases property with chosen | nowhere62  . exact chosen63  . obtain ⟨notDifferentiable, zero⟩ := nowhere64    exfalso65    exact notDifferentiable with differentiable6667theorem derivative.real (f : Set) (X : Real)68  shows Real(f′(X))69proof70  have realX : X ∈ ℝ by simp [Real]71  have function := derivative.function at f72  exact FunctionBetween.apply_closed with function, realX7374-- Section: IteratedDerivative75def iteratedDerivative (f : Set, k : Nat) → Set76  | f, zero => f77  | f, succ(k) => derivative(iteratedDerivative(f, k))7879-- The k-th derivative is written f⁽ᵏ⁾, with the index in superscript, so80-- f⁽ⁿ⁺¹⁾(C) is iteratedDerivative(f, n + 1)(C).81notation postfix 95 "⁽_⁾" => iteratedDerivative8283theorem iteratedDerivative.zero (f : Set)84  shows f⁽⁰⁾ = f85proof86  simp [iteratedDerivative]8788theorem iteratedDerivative.succ (f : Set, k : Nat)89  shows f⁽ᵏ⁺¹⁾ = f⁽ᵏ⁾′90proof91  have one : k + 1 = succ(k) := add.right_one with *92  rw one93  simp [iteratedDerivative]9495theorem iteratedDerivative.shift (f : Set, k : Nat)96  shows f⁽ᵏ⁺¹⁾ = (f′)⁽ᵏ⁾97proof98  induction k99  | zero =>100    rw [iteratedDerivative.succ, iteratedDerivative.zero,101      iteratedDerivative.zero]102    rfl103  | succ(j) using ih =>104    have one : j + 1 = succ(j) := add.right_one with *105    rw ← one106    rw [iteratedDerivative.succ, ih, iteratedDerivative.succ]107    rfl108109theorem iteratedDerivative.function (f : Set, k : Nat)110  requires function : f : ℝ → ℝ111  shows f⁽ᵏ⁾ : ℝ → ℝ112proof113  induction k114  | zero =>115    rw iteratedDerivative.zero116    exact function117  | succ(j) using ih =>118    have one : j + 1 = succ(j) := add.right_one with *119    rw ← one120    rw iteratedDerivative.succ121    exact derivative.function at iteratedDerivative(f, j)122123-- Section: DerivativeLaws124-- Multiplying by a constant scales the derivative.125theorem HasDerivativeAt.scale (g : Set) (K E C : Real)126  requires derivativeG : HasDerivativeAt(g, E, C)127  shows HasDerivativeAt(pointwiseMul(constantRealFunction(K), g), K * E, C)128proof129  have gFunction := HasDerivativeAt.function with derivativeG130  have constantDerivative := constantRealFunction.has_derivative_at at K, C131  have raw := HasDerivativeAt.mul with132    realZero.real, constantDerivative, derivativeG133  have realC : C ∈ ℝ by simp [Real]134  have gC := FunctionBetween.apply_closed with gFunction, realC135  have typedGC : Real(g(C)) by exact gC136  have constantValue := constantRealFunction.value at K, C137  have result : realZero * g(C) + constantRealFunction(K)(C) * E = K * E138    rw constantValue139    ring140  have view : realAddValue(realMulValue(realZero, g(C)),141      realMulValue(constantRealFunction(K)(C), E)) =142      realZero * g(C) + constantRealFunction(K)(C) * E143    unfold realAddValue144    unfold realMulValue145    unfold call2146    rfl147  rwa [view, result] at raw148149theorem derivative.scale (g : Set) (K C : Real)150  requires differentiable : DifferentiableAt(g, C)151  shows pointwiseMul(constantRealFunction(K), g)′(C) = K * g′(C)152proof153  have derivativeG := derivative.has_derivative_at with differentiable154  have typedValue := derivative.real at g, C155  have scaled := HasDerivativeAt.scale at g, K, derivative(g)(C), C with156    typedValue, derivativeG157  exact derivative.of_has_derivative with scaled158159theorem HasDerivativeAt.congr_value (f : Set) (D E A : Real)160  requires hasDerivative : HasDerivativeAt(f, D, A)161  requires equal : D = E162  shows HasDerivativeAt(f, E, A)163proof164  rwa equal at hasDerivative165166-- The product rule with its value written in the usual notation.167theorem HasDerivativeAt.mul_value (f g : Set) (D E A : Real)168  requires derivativeF : HasDerivativeAt(f, D, A)169  requires derivativeG : HasDerivativeAt(g, E, A)170  requires typedFA : Real(f(A))171  requires typedGA : Real(g(A))172  shows HasDerivativeAt(pointwiseMul(f, g), D * g(A) + f(A) * E, A)173proof174  have raw := HasDerivativeAt.mul with derivativeF, derivativeG175  have view : realAddValue(realMulValue(D, g(A)), realMulValue(f(A), E)) =176      D * g(A) + f(A) * E177    unfold realAddValue178    unfold realMulValue179    unfold call2180    rfl181  rwa view at raw182