Grace/Cumulus/Real/Analysis/Differentiation.g17

Open in Workbench Download source

Imports

Continuity

Declarations

Source

1-- Real analysis: Differentiation2-- 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.Differentiation8import Continuity910-- Section: Differentiation11def constantRealFunction (L : Set) : Set :=12  constantFunction(ℝ, ℝ, L)1314theorem constantRealFunction.function (L : Real)15  shows constantRealFunction(L) : ℝ → ℝ16proof17  have realL : L ∈ ℝ by simp [Real]18  unfold constantRealFunction19  exact constantFunction.function with realL2021theorem constantRealFunction.value (L X : Real)22  shows constantRealFunction(L)(X) = L23proof24  have realL : L ∈ ℝ by simp [Real]25  have realX : X ∈ ℝ by simp [Real]26  unfold constantRealFunction27  exact constantFunction.apply with realX, realL2829theorem constantRealFunction.continuous_at (L A : Real)30  shows ContinuousAt(constantRealFunction(L), A)31proof32  have function := constantRealFunction.function at L33  constructor34  . exact function35  . intros E realE positive36    witness E37    constructor38    . exact realE39    . constructor40      . exact positive41      . intros X realX near42        have typedX : Real(X) by exact realX43        have valueX := constantRealFunction.value at L, X with44          assumption, typedX45        have valueA := constantRealFunction.value at L, A with46          *{2}47        rw [valueX, valueA]48        exact openBall.center with positive4950theorem constantRealFunction.continuous (L : Real)51  shows Continuous(constantRealFunction(L))52proof53  constructor54  . exact constantRealFunction.function at L55  . intros A realA56    have typedA : Real(A) by exact realA57    exact constantRealFunction.continuous_at with assumption, typedA5859-- Translation is represented by the graph x ↦ A + x.60def translateBy (A : Real) : Set :=61  pointwiseAdd(constantRealFunction(A), identity(ℝ))6263theorem translateBy.function (A : Real)64  shows translateBy(A) : ℝ → ℝ65proof66  unfold translateBy67  exact pointwiseAdd.function at constantRealFunction(A), identity(ℝ) with68    constantRealFunction.function at A with assumption,69    identity.function at ℝ7071theorem translateBy.value (A X : Real)72  shows translateBy(A)(X) = A + X73proof74  have constantFunction := constantRealFunction.function at A75  have identityFunction := identity.function at ℝ76  have constantValue := constantRealFunction.value at A, X with77    *{2}78  have realX : X ∈ ℝ by simp [Real]79  have mappedX := identity.relates with realX80  have identityValue := FunctionBetween.apply_value with identityFunction, mappedX81  have sumValue := pointwiseAdd.value at82    constantRealFunction(A), identity(ℝ), X with83      assumption, constantFunction, identityFunction, *{2}84  unfold translateBy85  rw [constantValue, identityValue] at sumValue86  exact sumValue8788theorem translateBy.continuous (A : Real)89  shows Continuous(translateBy(A))90proof91  unfold translateBy92  exact Continuous.add at constantRealFunction(A), identity(ℝ) with93    constantRealFunction.continuous at A with assumption,94    identity.continuous9596-- The increment h ↦ f(A+h)-f(A) is useful both in the definition of the97-- difference quotient and in the proof that differentiability is continuous.98def incrementAt (f : Set) (A : Real) : Set :=99  pointwiseSub(100    compose(f, translateBy(A), ℝ, ℝ, ℝ),101    constantRealFunction(f(A)))102103theorem incrementAt.function (f : Set) (A : Real)104  requires function : f : ℝ → ℝ105  shows incrementAt(f, A) : ℝ → ℝ106proof107  have realA : A ∈ ℝ by simp [Real]108  have fAInReals := FunctionBetween.apply_closed with function, realA109  have typedFA : Real(f(A)) by exact fAInReals110  have translation := translateBy.function at A111  have shifted := compose.function with translation, function112  have constant := constantRealFunction.function with typedFA113  unfold incrementAt114  exact pointwiseSub.function with shifted, constant115116theorem incrementAt.value (f : Set) (A H : Real)117  requires function : f : ℝ → ℝ118  shows incrementAt(f, A)(H) =119    f(A + H) - f(A)120proof121  have realH : H ∈ ℝ by simp [Real]122  have realA : A ∈ ℝ by simp [Real]123  have sumReal := realAddValue.real at A, H with *124  have sumInReals : A + H ∈ ℝ by exact sumReal125  have fShiftInReals := FunctionBetween.apply_closed with function, sumInReals126  have fAInReals := FunctionBetween.apply_closed with function, realA127  have typedFShift : Real(f(A + H)) by exact fShiftInReals128  have typedFA : Real(f(A)) by exact fAInReals129  have translation := translateBy.function at A130  have translationValue := translateBy.value at A, H with131    *{2}132  have shifted := compose.function with translation, function133  have shiftedValue := compose.apply with translation, function, realH134  rw translationValue at shiftedValue135  have constant := constantRealFunction.function with typedFA136  have constantValue := constantRealFunction.value at f(A), H with137    typedFA, assumption138  have shiftedAtHReal : Real(compose(f, translateBy(A), ℝ, ℝ, ℝ)(H)) by rwa shiftedValue139  have constantAtHReal : Real(constantRealFunction(f(A))(H)) by rwa constantValue140  have value := pointwiseSub.value at141    compose(f, translateBy(A), ℝ, ℝ, ℝ),142    constantRealFunction(f(A)), H with143      assumption, shifted, constant, shiftedAtHReal, constantAtHReal144  rw [shiftedValue, constantValue] at value145  simp [incrementAt]146147-- The total graph h ↦ (f(A+h)-f(A))/h. Its value at zero is harmless because148-- differentiation uses the punctured limit.149def differenceQuotient (f : Set) (A : Real) : Set :=150  pointwiseDiv(incrementAt(f, A), identity(ℝ))151152theorem differenceQuotient.function (f : Set) (A : Real)153  requires function : f : ℝ → ℝ154  shows differenceQuotient(f, A) : ℝ → ℝ155proof156  have numerator := incrementAt.function with function157  unfold differenceQuotient158  exact pointwiseDiv.function at incrementAt(f, A), identity(ℝ) with159    numerator, identity.function at ℝ160161theorem differenceQuotient.value (f : Set) (A H : Real)162  requires function : f : ℝ → ℝ163  shows differenceQuotient(f, A)(H) =164    (f(A + H) - f(A)) / H165proof166  have realH : H ∈ ℝ by simp [Real]167  have numerator := incrementAt.function at f, A with function168  have numeratorValue := incrementAt.value at f, A, H with169    *{2}, function170  have identityMapsH := identity.relates with realH171  have identityValue := FunctionBetween.apply_value at172    identity(ℝ), ℝ, ℝ, H, H with173      identity.function at ℝ, realH, identityMapsH174  have numeratorAtHReal := FunctionBetween.apply_closed with numerator, realH175  have typedNumeratorAtH : Real(incrementAt(f, A)(H))176    exact numeratorAtHReal177  have identityAtHReal : Real(identity(ℝ)(H)) by rwa identityValue178  have quotientValue := pointwiseDiv.value at179    incrementAt(f, A), identity(ℝ), H with180      assumption, numerator, identity.function at ℝ,181      typedNumeratorAtH, identityAtHReal182  unfold differenceQuotient183  rw [numeratorValue, identityValue] at quotientValue184  exact quotientValue185186predicate HasDerivativeAt (f : Set) (D A : Real) :=187  FunctionBetween(f, ℝ, ℝ) ∧188  TendsToAt(differenceQuotient(f, A), D, realZero)189190predicate DifferentiableAt (f : Set) (A : Real) :=191  ∃ D ∈ ℝ, HasDerivativeAt(f, D, A)192193theorem HasDerivativeAt.function (f : Set) (D A : Real)194  requires derivative : HasDerivativeAt(f, D, A)195  shows f : ℝ → ℝ196proof197  simp [HasDerivativeAt]198199theorem HasDerivativeAt.limit (f : Set) (D A : Real)200  requires derivative : HasDerivativeAt(f, D, A)201  shows TendsToAt(differenceQuotient(f, A), D, realZero)202proof203  simp [HasDerivativeAt]204205theorem HasDerivativeAt.differentiable_at (f : Set) (D A : Real)206  requires derivative : HasDerivativeAt(f, D, A)207  shows DifferentiableAt(f, A)208proof209  have realD : D ∈ ℝ by simp [Real]210  unfold DifferentiableAt211  refine ⟨D, realD, derivative⟩212213-- In increment coordinates, differentiability says exactly that214-- f(A+h) tends to f(A) as h tends to zero.215theorem HasDerivativeAt.shifted_limit (f : Set) (D A : Real)216  requires derivative : HasDerivativeAt(f, D, A)217  shows TendsToAt(218    compose(f, translateBy(A), ℝ, ℝ, ℝ), f(A), realZero)219proof220  have function := HasDerivativeAt.function with derivative221  have derivativeLimit := HasDerivativeAt.limit with derivative222  have quotientFunction := differenceQuotient.function at f, A with function223  have identityLimit := identity.tends_to_at with realZero.real224  have productLimit := TendsToAt.mul with identityLimit, derivativeLimit225  have zeroProduct := realMulValue.zero_left at D with assumption226  rw zeroProduct at productLimit227  have incrementFunction := incrementAt.function at f, A with function228  have equalIncrement : ∀ H ∈ ℝ, (H ≠ realZero →229      incrementAt(f, A)(H) =230        pointwiseMul(identity(ℝ), differenceQuotient(f, A))(H))231    intros H realH nonzero232    have typedH : Real(H)233      exact realH234    have incrementValue := incrementAt.value at f, A, H with235      assumption, typedH, function236    have quotientValue := differenceQuotient.value at f, A, H with237      assumption, typedH, function238    have numeratorReal := realSubValue.real at239      f(A + H), f(A) with *{2}240    have quotientReal := FunctionBetween.apply_closed with quotientFunction, realH241    have typedQuotient : Real(differenceQuotient(f, A)(H))242      exact quotientReal243    have identityMaps := identity.relates with realH244    have identityValue := FunctionBetween.apply_value at245      identity(ℝ), ℝ, ℝ, H, H with246        identity.function at ℝ, realH, identityMaps247    have typedIdentity : Real(identity(ℝ)(H)) by rwa identityValue248    have productValue := pointwiseMul.value at249      identity(ℝ), differenceQuotient(f, A), H with250        typedH, identity.function at ℝ, quotientFunction,251        typedIdentity, typedQuotient252    have cancellation := realDiv.mul_left with numeratorReal, typedH, nonzero253    calc254      incrementAt(f, A)(H) =255          f(A + H) - f(A) := incrementValue256      _ = H * ((f(A + H) - f(A)) / H) := by cc257      _ = H * differenceQuotient(f, A)(H) :=258        by simp [quotientValue]259      _ = pointwiseMul(identity(ℝ),260          differenceQuotient(f, A))(H) := by cc261  have incrementLimit := TendsToAt.congr with productLimit, incrementFunction, equalIncrement262  have realA : A ∈ ℝ by simp [Real]263  have fAInReals := FunctionBetween.apply_closed with function, realA264  have typedFA : Real(f(A))265    exact fAInReals266  have constantContinuous := constantRealFunction.continuous_at with typedFA, realZero.real267  have constantLimit := ContinuousAt.tends_to with constantContinuous268  have constantValue := constantRealFunction.value with typedFA, realZero.real269  rw constantValue at constantLimit270  have sumLimit := TendsToAt.add with constantLimit, incrementLimit271  have zeroSum := realAddValue.zero_right with typedFA272  rw zeroSum at sumLimit273  have translation := translateBy.function at A with assumption274  have shiftedFunction := compose.function with translation, function275  have equalShift : ∀ H ∈ ℝ, (H ≠ realZero →276      compose(f, translateBy(A), ℝ, ℝ, ℝ)(H) =277        pointwiseAdd(constantRealFunction(f(A)),278          incrementAt(f, A))(H))279    intros H realH nonzero280    have typedH : Real(H)281      exact realH282    have sumReal := realAddValue.real at A, H with assumption, typedH283    have shiftedValue := compose.apply with translation, function, realH284    have translationValue := translateBy.value at A, H with285      assumption, typedH286    rw translationValue at shiftedValue287    have incrementValue := incrementAt.value at f, A, H with288      assumption, typedH, function289    have constantFunction := constantRealFunction.function with typedFA290    have constantAtH := constantRealFunction.value with typedFA, typedH291    have sumInReals : A + H ∈ ℝ292      exact sumReal293    have shiftedInReals := FunctionBetween.apply_closed with function, sumInReals294    have typedShifted : Real(f(A + H))295      exact shiftedInReals296    have incrementAtHReal := FunctionBetween.apply_closed with incrementFunction, realH297    have typedIncrement : Real(incrementAt(f, A)(H))298      exact incrementAtHReal299    have typedConstant : Real(constantRealFunction(f(A))(H)) by rwa constantAtH300    have sumValue := pointwiseAdd.value with301      typedH, constantFunction, incrementFunction, typedConstant, typedIncrement302    have cancel := realSubValue.add_right_cancel with typedShifted, typedFA303    have differenceReal := realSubValue.real with typedShifted, typedFA304    have commute := realAddValue.commutative with typedFA, differenceReal305    have reconstructed : f(A) +306        (f(A + H) - f(A)) = f(A + H)307      calc308        f(A) + (f(A + H) - f(A)) =309            (f(A + H) - f(A)) + f(A) := commute310        _ = f(A + H) := cancel311    rw ← reconstructed at shiftedValue312    rw [constantAtH, incrementValue] at sumValue313    rwa ← sumValue at shiftedValue314  exact TendsToAt.congr with sumLimit, shiftedFunction, equalShift315316-- Every differentiable real function is continuous at the point of317-- differentiation.  Translation carries the increment-coordinate result318-- back from zero to A.319theorem HasDerivativeAt.continuous_at (f : Set) (D A : Real)320  requires derivative : HasDerivativeAt(f, D, A)321  shows ContinuousAt(f, A)322proof323  have function := HasDerivativeAt.function with derivative324  have shiftedLimit := HasDerivativeAt.shifted_limit with derivative325  have translation := translateBy.function at A326  have shiftedFunction := compose.function with translation, function327  have realA : A ∈ ℝ by simp [Real]328  have fAInReals := FunctionBetween.apply_closed with function329  have zeroInReals : realZero ∈ ℝ by exact realZero.real330  have shiftedAtZero := compose.apply with translation, function, zeroInReals331  have translationAtZero := translateBy.value at A, realZero with332    assumption, realZero.real333  have addZero := realAddValue.zero_right at A334  rw [translationAtZero, addZero] at shiftedAtZero335  have shiftedContinuous := TendsToAt.continuous_at with shiftedLimit, shiftedAtZero336  have negAReal := realNegValue.real at A337  have backContinuousEverywhere := translateBy.continuous with negAReal338  have backContinuous := Continuous.at at translateBy(-A), A with339    backContinuousEverywhere340  have backFunction := translateBy.function with negAReal341  have backAtA := translateBy.value at -A, A with negAReal, assumption342  have cancelA := realAddValue.neg_left at A343  rw cancelA at backAtA344  have shiftedAtBack : ContinuousAt(345      compose(f, translateBy(A), ℝ, ℝ, ℝ), translateBy(-A)(A))346    rwa backAtA347  have composedContinuous := ContinuousAt.comp with backContinuous, shiftedAtBack348  have equal : ∀ X ∈ ℝ,349      compose(350        compose(f, translateBy(A), ℝ, ℝ, ℝ),351        translateBy(-A), ℝ, ℝ, ℝ)(X) = f(X)352    intros X realX353    have typedX : Real(X) by exact realX354    have backValue := translateBy.value with negAReal, typedX355    have backXInReals := FunctionBetween.apply_closed with backFunction, realX356    have typedBackX : Real(translateBy(-A)(X)) by exact backXInReals357    have outerValue := compose.apply with backFunction, shiftedFunction, realX358    have innerValue := compose.apply with translation, function, backXInReals359    have forwardValue := translateBy.value at360      A, translateBy(-A)(X) with assumption, typedBackX361    rw [forwardValue, backValue] at innerValue362    rw backValue at outerValue363    have associate := realAddValue.associative at A, -A, X with364      assumption, negAReal, typedX365    have cancel := realAddValue.neg_right at A366    have zeroX := realAddValue.zero_left with typedX367    have restored : A + ((-A) + X) = X by rwa [← associate, cancel]368    rw restored at innerValue369    calc370      compose(371        compose(f, translateBy(A), ℝ, ℝ, ℝ),372        translateBy(-A), ℝ, ℝ, ℝ)(X) =373          compose(f, translateBy(A), ℝ, ℝ, ℝ)((-A) + X) := outerValue374      _ = f(X) := innerValue375  exact ContinuousAt.congr with composedContinuous, function, equal376377-- Difference quotients commute with negation.378theorem differenceQuotient.neg (f : Set) (A H : Real)379  requires function : f : ℝ → ℝ380  shows differenceQuotient(pointwiseNeg(f), A)(H) =381    -differenceQuotient(f, A)(H)382proof383  have negFunction := pointwiseNeg.function with function384  have sumReal := realAddValue.real at A, H with *385  have realA : A ∈ ℝ by simp [Real]386  have sumInReals : A + H ∈ ℝ by exact sumReal387  have fShiftInReals := FunctionBetween.apply_closed with function, sumInReals388  have fAInReals := FunctionBetween.apply_closed with function, realA389  have typedFShift : Real(f(A + H)) by exact fShiftInReals390  have typedFA : Real(f(A)) by exact fAInReals391  have shiftedNeg := pointwiseNeg.value with sumReal, function, typedFShift392  have centerNeg := pointwiseNeg.value at f, A with393    assumption, function, typedFA394  have negQuotient := differenceQuotient.value at395    pointwiseNeg(f), A, H with *{2}, negFunction396  have quotient := differenceQuotient.value at f, A, H with397    *{2}, function398  have negNumerator := realSubValue.neg_neg with typedFShift, typedFA399  have numeratorReal := realSubValue.real with typedFShift, typedFA400  have negDivision := realDiv.neg_left at401    f(A + H) - f(A), H with402      numeratorReal, assumption403  calc404    differenceQuotient(pointwiseNeg(f), A)(H) =405        (pointwiseNeg(f)(A + H) -406          pointwiseNeg(f)(A)) / H := negQuotient407    _ = ((-f(A + H)) - (-f(A))) / H :=408      by simp [shiftedNeg, centerNeg]409    _ = (-(f(A + H) - f(A))) / H :=410      by simp [negNumerator]411    _ = -((f(A + H) - f(A)) / H) := negDivision412    _ = -differenceQuotient(f, A)(H) := by simp [quotient]413414-- The quotient of a pointwise sum is the sum of the quotients.415theorem differenceQuotient.add (f g : Set) (A H : Real)416  requires fFunction : f : ℝ → ℝ417  requires gFunction : g : ℝ → ℝ418  shows differenceQuotient(pointwiseAdd(f, g), A)(H) =419    pointwiseAdd(differenceQuotient(f, A),420      differenceQuotient(g, A))(H)421proof422  have sumFunction := pointwiseAdd.function with fFunction, gFunction423  have quotientF := differenceQuotient.function at f, A with fFunction424  have quotientG := differenceQuotient.function at g, A with gFunction425  have sumReal := realAddValue.real at A, H with *426  have realA : A ∈ ℝ by simp [Real]427  have realH : H ∈ ℝ by simp [Real]428  have sumInReals : A + H ∈ ℝ by exact sumReal429  have fShiftInReals := FunctionBetween.apply_closed with fFunction, sumInReals430  have gShiftInReals := FunctionBetween.apply_closed with gFunction, sumInReals431  have fAInReals := FunctionBetween.apply_closed with fFunction, realA432  have gAInReals := FunctionBetween.apply_closed with gFunction, realA433  have typedFShift : Real(f(A + H)) by exact fShiftInReals434  have typedGShift : Real(g(A + H)) by exact gShiftInReals435  have typedFA : Real(f(A)) by exact fAInReals436  have typedGA : Real(g(A)) by exact gAInReals437  have shiftedSum := pointwiseAdd.value with sumReal, fFunction, gFunction, typedFShift, typedGShift438  have centerSum := pointwiseAdd.value at f, g, A with439    assumption, fFunction, gFunction, typedFA, typedGA440  have sumQuotient := differenceQuotient.value at441    pointwiseAdd(f, g), A, H with *{2}, sumFunction442  have fQuotient := differenceQuotient.value at f, A, H with443    *{2}, fFunction444  have gQuotient := differenceQuotient.value at g, A, H with445    *{2}, gFunction446  have fQuotientInReals := FunctionBetween.apply_closed with quotientF, realH447  have gQuotientInReals := FunctionBetween.apply_closed with quotientG, realH448  have typedFQuotient : Real(differenceQuotient(f, A)(H)) by exact fQuotientInReals449  have typedGQuotient : Real(differenceQuotient(g, A)(H)) by exact gQuotientInReals450  have pointwiseValue := pointwiseAdd.value at451    differenceQuotient(f, A), differenceQuotient(g, A), H with452      assumption, quotientF, quotientG, typedFQuotient, typedGQuotient453  have rearranged := realSubValue.add_add with typedFShift, typedGShift, typedFA, typedGA454  have fDifferenceReal := realSubValue.real with typedFShift, typedFA455  have gDifferenceReal := realSubValue.real with typedGShift, typedGA456  have dividedSum := realDiv.add_left at457    f(A + H) - f(A),458    g(A + H) - g(A), H with459      fDifferenceReal, gDifferenceReal, assumption460  calc461    differenceQuotient(pointwiseAdd(f, g), A)(H) =462        (pointwiseAdd(f, g)(A + H) -463          pointwiseAdd(f, g)(A)) / H := sumQuotient464    _ = ((f(A + H) + g(A + H)) -465        (f(A) + g(A))) / H :=466      by simp [shiftedSum, centerSum]467    _ = ((f(A + H) - f(A)) +468        (g(A + H) - g(A))) / H := by simp [rearranged]469    _ = (f(A + H) - f(A)) / H +470        (g(A + H) - g(A)) / H := dividedSum471    _ = differenceQuotient(f, A)(H) +472        differenceQuotient(g, A)(H) :=473      by simp [fQuotient, gQuotient]474    _ = pointwiseAdd(differenceQuotient(f, A),475        differenceQuotient(g, A))(H) := by simp [pointwiseValue]476477-- The product quotient is the sum of the two textbook terms.  The first478-- factor is evaluated at A+h, which is what makes the identity hold479-- before taking a limit.480theorem HasDerivativeAt.neg (f : Set) (D A : Real)481  requires derivative : HasDerivativeAt(f, D, A)482  shows HasDerivativeAt(pointwiseNeg(f), -D, A)483proof484  have function := HasDerivativeAt.function with derivative485  have limit := HasDerivativeAt.limit with derivative486  have negFunction := pointwiseNeg.function with function487  have quotientFunction := differenceQuotient.function at488    pointwiseNeg(f), A with negFunction489  have negLimit := TendsToAt.neg with limit490  have equalAway : ∀ H ∈ ℝ, (H ≠ realZero →491      differenceQuotient(pointwiseNeg(f), A)(H) =492        pointwiseNeg(differenceQuotient(f, A))(H))493    intros H realH nonzero494    have typedH : Real(H) by exact realH495    have quotientF := differenceQuotient.function at f, A with function496    have valueReal := FunctionBetween.apply_closed with quotientF, realH497    have typedValue : Real(differenceQuotient(f, A)(H)) by exact valueReal498    have negValue := pointwiseNeg.value with quotientF499    have quotientNeg := differenceQuotient.neg at f, A, H with500      assumption, typedH, function501    calc502      differenceQuotient(pointwiseNeg(f), A)(H) =503          -differenceQuotient(f, A)(H) := quotientNeg504      _ = pointwiseNeg(differenceQuotient(f, A))(H) :=505        by simp [negValue]506  have quotientLimit := TendsToAt.congr with negLimit, quotientFunction, equalAway507  unfold HasDerivativeAt508  refine ⟨negFunction, quotientLimit⟩509510theorem HasDerivativeAt.add (f g : Set) (D E A : Real)511  requires derivativeF : HasDerivativeAt(f, D, A)512  requires derivativeG : HasDerivativeAt(g, E, A)513  shows HasDerivativeAt(pointwiseAdd(f, g), D + E, A)514proof515  have fFunction := HasDerivativeAt.function with derivativeF516  have gFunction := HasDerivativeAt.function with derivativeG517  have limitF := HasDerivativeAt.limit with derivativeF518  have limitG := HasDerivativeAt.limit with derivativeG519  have sumFunction := pointwiseAdd.function with fFunction, gFunction520  have quotientFunction := differenceQuotient.function at521    pointwiseAdd(f, g), A with sumFunction522  have sumLimit := TendsToAt.add with limitF, limitG523  have equalAway : ∀ H ∈ ℝ, (H ≠ realZero →524      differenceQuotient(pointwiseAdd(f, g), A)(H) =525        pointwiseAdd(differenceQuotient(f, A),526          differenceQuotient(g, A))(H))527    intros H realH nonzero528    exact differenceQuotient.add with fFunction, gFunction529  have quotientLimit := TendsToAt.congr with sumLimit, quotientFunction, equalAway530  unfold HasDerivativeAt531  refine ⟨sumFunction, quotientLimit⟩532533-- The product rule in its familiar handwritten form.534theorem HasDerivativeAt.sub (f g : Set) (D E A : Real)535  requires derivativeF : HasDerivativeAt(f, D, A)536  requires derivativeG : HasDerivativeAt(g, E, A)537  shows HasDerivativeAt(pointwiseSub(f, g), D - E, A)538proof539  have negDerivative := HasDerivativeAt.neg with derivativeG540  have sumDerivative := HasDerivativeAt.add with derivativeF, negDerivative541  unfold pointwiseSub542  unfold realSubValue543  exact sumDerivative544545theorem DifferentiableAt.neg (f : Set) (A : Real)546  requires differentiable : DifferentiableAt(f, A)547  shows DifferentiableAt(pointwiseNeg(f), A)548proof549  obtain ⟨D, realD, derivative⟩ := differentiable550  have typedD : Real(D) by exact realD551  have negDReal := realNegValue.real with typedD552  have negDerivative := HasDerivativeAt.neg with derivative553  witness -D554  constructor555    exact negDReal556  . exact negDerivative557558theorem DifferentiableAt.add (f g : Set) (A : Real)559  requires differentiableF : DifferentiableAt(f, A)560  requires differentiableG : DifferentiableAt(g, A)561  shows DifferentiableAt(pointwiseAdd(f, g), A)562proof563  obtain ⟨D, realD, derivativeF⟩ := differentiableF564  obtain ⟨E, realE, derivativeG⟩ := differentiableG565  have typedD : Real(D) by exact realD566  have typedE : Real(E) by exact realE567  have sumReal := realAddValue.real with typedD, typedE568  have sumDerivative := HasDerivativeAt.add with derivativeF, derivativeG569  witness D + E570  constructor571    exact sumReal572  . exact sumDerivative573574theorem DifferentiableAt.sub (f g : Set) (A : Real)575  requires differentiableF : DifferentiableAt(f, A)576  requires differentiableG : DifferentiableAt(g, A)577  shows DifferentiableAt(pointwiseSub(f, g), A)578proof579  have negG := DifferentiableAt.neg with differentiableG580  have sum := DifferentiableAt.add with differentiableF, negG581  unfold pointwiseSub582  exact sum583584theorem constantRealFunction.has_derivative_at (C A : Real)585  shows HasDerivativeAt(constantRealFunction(C), realZero, A)586proof587  have function := constantRealFunction.function at C588  have quotientFunction := differenceQuotient.function at589    constantRealFunction(C), A with function590  have zeroContinuous := constantRealFunction.continuous_at with realZero.real, realZero.real591  have zeroLimit := ContinuousAt.tends_to with zeroContinuous592  have zeroValue := constantRealFunction.value with realZero.real, realZero.real593  rw zeroValue at zeroLimit594  have equalAway : ∀ H ∈ ℝ, (H ≠ realZero →595      differenceQuotient(constantRealFunction(C), A)(H) =596        constantRealFunction(realZero)(H))597    intros H realH nonzero598    have typedH : Real(H) by exact realH599    have sumReal := realAddValue.real at A, H with assumption, typedH600    have quotientValue := differenceQuotient.value at601      constantRealFunction(C), A, H with602        assumption, typedH, function603    have shiftedValue := constantRealFunction.value at C, A + H with604      assumption, sumReal605    have centerValue := constantRealFunction.value at C, A with606      *{2}607    have numeratorZero := realSubValue.self at C608    have quotientZero := realDiv.zero_left with typedH609    have constantZero := constantRealFunction.value with realZero.real, typedH610    calc611      differenceQuotient(constantRealFunction(C), A)(H) =612          (constantRealFunction(C)(A + H) -613            constantRealFunction(C)(A)) / H := quotientValue614      _ = (C - constantRealFunction(C)(A)) / H := by simp [shiftedValue]615      _ = (C - C) / H := by simp [centerValue]616      _ = 0 / H := by simp [numeratorZero]617      _ = 0 := quotientZero618      _ = constantRealFunction(realZero)(H) := by simp [constantZero]619  have quotientLimit := TendsToAt.congr with zeroLimit, quotientFunction, equalAway620  unfold HasDerivativeAt621  refine ⟨function, quotientLimit⟩622623theorem identity.has_derivative_at (A : Real)624  shows HasDerivativeAt(identity(ℝ), realOne, A)625proof626  have function := identity.function at ℝ627  have quotientFunction := differenceQuotient.function with function628  have oneContinuous := constantRealFunction.continuous_at with realOne.real, realZero.real629  have oneLimit := ContinuousAt.tends_to with oneContinuous630  have oneValue := constantRealFunction.value with realOne.real, realZero.real631  rw oneValue at oneLimit632  have equalAway : ∀ H ∈ ℝ, (H ≠ realZero →633      differenceQuotient(identity(ℝ), A)(H) =634        constantRealFunction(realOne)(H))635    intros H realH nonzero636    have typedH : Real(H) by exact realH637    have sumReal := realAddValue.real at A, H with assumption, typedH638    have sumInReals : A + H ∈ ℝ by exact sumReal639    have quotientValue := differenceQuotient.value at640      identity(ℝ), A, H with assumption, typedH, function641    have shiftedMaps := identity.relates with sumInReals642    have shiftedValue := FunctionBetween.apply_value with function, shiftedMaps643    have realA : A ∈ ℝ by simp [Real]644    have centerMaps := identity.relates with realA645    have centerValue := FunctionBetween.apply_value with function, centerMaps646    have numerator := realSubValue.add_cancel_left at A, H with647      assumption, typedH648    have quotientOne := realDiv.self with nonzero649    have constantOne := constantRealFunction.value with realOne.real, typedH650    calc651      differenceQuotient(identity(ℝ), A)(H) =652          (identity(ℝ)(A + H) - identity(ℝ)(A)) / H :=653            quotientValue654      _ = ((A + H) - identity(ℝ)(A)) / H := by simp [shiftedValue]655      _ = ((A + H) - A) / H := by simp [centerValue]656      _ = H / H := by simp [numerator]657      _ = 1 := quotientOne658      _ = constantRealFunction(realOne)(H) := by simp [constantOne]659  have quotientLimit := TendsToAt.congr with oneLimit, quotientFunction, equalAway660  unfold HasDerivativeAt661  refine ⟨function, quotientLimit⟩662663theorem HasDerivativeAt.unique (f : Set) (D E A : Real)664  requires first : HasDerivativeAt(f, D, A)665  requires second : HasDerivativeAt(f, E, A)666  shows D = E667proof668  have firstLimit := HasDerivativeAt.limit with first669  have secondLimit := HasDerivativeAt.limit with second670  exact TendsToAt.unique with firstLimit, secondLimit671672-- Section: ProductRule673theorem differenceQuotient.mul (f g : Set) (A H : Real)674  requires fFunction : f : ℝ → ℝ675  requires gFunction : g : ℝ → ℝ676  shows differenceQuotient(pointwiseMul(f, g), A)(H) =677    pointwiseAdd(678      pointwiseMul(differenceQuotient(f, A),679        constantRealFunction(g(A))),680      pointwiseMul(compose(f, translateBy(A), ℝ, ℝ, ℝ),681        differenceQuotient(g, A)))(H)682proof683  have productFunction := pointwiseMul.function with fFunction, gFunction684  have quotientF := differenceQuotient.function at f, A with fFunction685  have quotientG := differenceQuotient.function at g, A with gFunction686  have realA : A ∈ ℝ by simp [Real]687  have realH : H ∈ ℝ by simp [Real]688  have sumReal := realAddValue.real at A, H with *689  have sumInReals : A + H ∈ ℝ by exact sumReal690  have fShiftInReals := FunctionBetween.apply_closed with fFunction, sumInReals691  have gShiftInReals := FunctionBetween.apply_closed with gFunction, sumInReals692  have fAInReals := FunctionBetween.apply_closed with fFunction, realA693  have gAInReals := FunctionBetween.apply_closed with gFunction, realA694  have typedFShift : Real(f(A + H)) by exact fShiftInReals695  have typedGShift : Real(g(A + H)) by exact gShiftInReals696  have typedFA : Real(f(A)) by exact fAInReals697  have typedGA : Real(g(A)) by exact gAInReals698  have shiftedProduct := pointwiseMul.value with sumReal, fFunction, gFunction, typedFShift, typedGShift699  have centerProduct := pointwiseMul.value at f, g, A with700    assumption, fFunction, gFunction, typedFA, typedGA701  have productQuotient := differenceQuotient.value at702    pointwiseMul(f, g), A, H with *{2}, productFunction703  have fQuotient := differenceQuotient.value at f, A, H with704    *{2}, fFunction705  have gQuotient := differenceQuotient.value at g, A, H with706    *{2}, gFunction707  have fDifferenceReal := realSubValue.real with typedFShift, typedFA708  have gDifferenceReal := realSubValue.real with typedGShift, typedGA709  have firstProductReal := realMulValue.real with typedFShift, gDifferenceReal710  have secondProductReal := realMulValue.real with typedGA, fDifferenceReal711  have rearranged := realSubValue.mul_mul with typedFShift, typedGShift, typedFA, typedGA712  have dividedSum := realDiv.add_left at713    f(A + H) * (g(A + H) - g(A)),714    g(A) * (f(A + H) - f(A)), H with715      firstProductReal, secondProductReal, assumption716  have factorFirst := realDiv.mul_numerator_left at717    f(A + H), g(A + H) - g(A), H with718      typedFShift, gDifferenceReal, assumption719  have factorSecond := realDiv.mul_numerator_left at720    g(A), f(A + H) - f(A), H with721      typedGA, fDifferenceReal, assumption722  have fQuotientInReals := FunctionBetween.apply_closed with quotientF, realH723  have gQuotientInReals := FunctionBetween.apply_closed with quotientG, realH724  have typedFQuotient : Real(differenceQuotient(f, A)(H)) by exact fQuotientInReals725  have typedGQuotient : Real(differenceQuotient(g, A)(H)) by exact gQuotientInReals726  have constantGA := constantRealFunction.function with typedGA727  have constantValue := constantRealFunction.value at g(A), H with728    typedGA, assumption729  have typedConstant : Real(constantRealFunction(g(A))(H)) by rwa constantValue730  have translation := translateBy.function at A731  have shiftedF := compose.function with translation, fFunction732  have translationValue := translateBy.value at A, H with733    *{2}734  have shiftedValue := compose.apply with translation, fFunction, realH735  rw translationValue at shiftedValue736  have typedShifted : Real(compose(f, translateBy(A), ℝ, ℝ, ℝ)(H)) by rwa shiftedValue737  have firstTermFunction := pointwiseMul.function with quotientF, constantGA738  have secondTermFunction := pointwiseMul.function with shiftedF, quotientG739  have firstTermValue := pointwiseMul.value at740    differenceQuotient(f, A), constantRealFunction(g(A)), H with741      assumption, quotientF, constantGA, typedFQuotient, typedConstant742  have secondTermValue := pointwiseMul.value at743    compose(f, translateBy(A), ℝ, ℝ, ℝ), differenceQuotient(g, A), H with744      assumption, shiftedF, quotientG, typedShifted, typedGQuotient745  have typedFirstTerm := realMulValue.real with typedFQuotient, typedConstant746  have typedSecondTerm := realMulValue.real with typedShifted, typedGQuotient747  have typedFirstTermValue : Real(pointwiseMul(differenceQuotient(f, A),748        constantRealFunction(g(A)))(H))749    rwa firstTermValue750  have typedSecondTermValue : Real(pointwiseMul(compose(f, translateBy(A), ℝ, ℝ, ℝ),751        differenceQuotient(g, A))(H))752    rwa secondTermValue753  have sumValue := pointwiseAdd.value at754    pointwiseMul(differenceQuotient(f, A),755      constantRealFunction(g(A))),756    pointwiseMul(compose(f, translateBy(A), ℝ, ℝ, ℝ),757      differenceQuotient(g, A)), H with758        assumption, firstTermFunction, secondTermFunction,759        typedFirstTermValue, typedSecondTermValue760  have commuteFirst := realMulValue.commutative with typedGA, typedFQuotient761  have firstRawReal := realMulValue.real with typedFShift, typedGQuotient762  have secondRawReal := realMulValue.real with typedGA, typedFQuotient763  have commuteSum := realAddValue.commutative with firstRawReal, secondRawReal764  calc765    differenceQuotient(pointwiseMul(f, g), A)(H) =766        (pointwiseMul(f, g)(A + H) -767          pointwiseMul(f, g)(A)) / H := productQuotient768    _ = (f(A + H) * g(A + H) -769        f(A) * g(A)) / H :=770      by simp [shiftedProduct, centerProduct]771    _ = (f(A + H) * (g(A + H) - g(A)) +772        g(A) * (f(A + H) - f(A))) / H :=773      by simp [rearranged]774    _ = (f(A + H) * (g(A + H) - g(A))) / H +775        (g(A) * (f(A + H) - f(A))) / H := dividedSum776    _ = f(A + H) *777          ((g(A + H) - g(A)) / H) +778        g(A) * ((f(A + H) - f(A)) / H) :=779      by simp [factorFirst, factorSecond]780    _ = f(A + H) * differenceQuotient(g, A)(H) +781        g(A) * differenceQuotient(f, A)(H) :=782      by simp [fQuotient, gQuotient]783    _ = differenceQuotient(f, A)(H) * g(A) +784        f(A + H) * differenceQuotient(g, A)(H) := by cc785    _ = pointwiseMul(differenceQuotient(f, A),786          constantRealFunction(g(A)))(H) +787        pointwiseMul(compose(f, translateBy(A), ℝ, ℝ, ℝ),788          differenceQuotient(g, A))(H) :=789      by simp [firstTermValue, secondTermValue, constantValue, shiftedValue]790    _ = pointwiseAdd(791        pointwiseMul(differenceQuotient(f, A),792          constantRealFunction(g(A))),793        pointwiseMul(compose(f, translateBy(A), ℝ, ℝ, ℝ),794          differenceQuotient(g, A)))(H) := by cc795796theorem HasDerivativeAt.mul (f g : Set) (D E A : Real)797  requires derivativeF : HasDerivativeAt(f, D, A)798  requires derivativeG : HasDerivativeAt(g, E, A)799  shows HasDerivativeAt(pointwiseMul(f, g),800    realAddValue(801      realMulValue(D, g(A)),802      realMulValue(f(A), E)), A)803proof804  have fFunction := HasDerivativeAt.function with derivativeF805  have gFunction := HasDerivativeAt.function with derivativeG806  have limitF := HasDerivativeAt.limit with derivativeF807  have limitG := HasDerivativeAt.limit with derivativeG808  have productFunction := pointwiseMul.function with fFunction, gFunction809  have quotientFunction := differenceQuotient.function at810    pointwiseMul(f, g), A with productFunction811  have realA : A ∈ ℝ by simp [Real]812  have fAInReals := FunctionBetween.apply_closed with fFunction, realA813  have gAInReals := FunctionBetween.apply_closed with gFunction, realA814  have typedFA : Real(f(A)) by exact fAInReals815  have typedGA : Real(g(A)) by exact gAInReals816  have firstDerivativeReal := realMulValue.real at817    D, g(A) with assumption, typedGA818  have secondDerivativeReal := realMulValue.real at819    f(A), E with typedFA, assumption820  have productDerivativeReal := realAddValue.real with firstDerivativeReal, secondDerivativeReal821  have constantContinuous := constantRealFunction.continuous_at with typedGA, realZero.real822  have constantLimit := ContinuousAt.tends_to with constantContinuous823  have constantValue := constantRealFunction.value with typedGA, realZero.real824  rw constantValue at constantLimit825  have firstLimit := TendsToAt.mul with limitF, constantLimit826  have shiftedLimit := HasDerivativeAt.shifted_limit with derivativeF827  have secondLimit := TendsToAt.mul with shiftedLimit, limitG828  have sumLimit := TendsToAt.add with firstLimit, secondLimit829  have equalAway : ∀ H ∈ ℝ, (H ≠ realZero →830      differenceQuotient(pointwiseMul(f, g), A)(H) =831        pointwiseAdd(832          pointwiseMul(differenceQuotient(f, A),833            constantRealFunction(g(A))),834          pointwiseMul(compose(f, translateBy(A), ℝ, ℝ, ℝ),835            differenceQuotient(g, A)))(H))836    intros H realH nonzero837    exact differenceQuotient.mul with fFunction, gFunction838  have quotientLimit := TendsToAt.congr at839    pointwiseAdd(840      pointwiseMul(differenceQuotient(f, A),841        constantRealFunction(g(A))),842      pointwiseMul(compose(f, translateBy(A), ℝ, ℝ, ℝ),843        differenceQuotient(g, A))),844    differenceQuotient(pointwiseMul(f, g), A),845    D * g(A) + f(A) * E, realZero with846      sumLimit, quotientFunction, equalAway847  unfold realAddValue848  unfold realMulValue849  unfold call2 at productDerivativeReal850  unfold call2 at quotientLimit851  unfold HasDerivativeAt852  refine ⟨productFunction, quotientLimit⟩853854theorem DifferentiableAt.mul (f g : Set) (A : Real)855  requires differentiableF : DifferentiableAt(f, A)856  requires differentiableG : DifferentiableAt(g, A)857  shows DifferentiableAt(pointwiseMul(f, g), A)858proof859  obtain ⟨D, realD, derivativeF⟩ := differentiableF860  obtain ⟨E, realE, derivativeG⟩ := differentiableG861  have typedD : Real(D) by exact realD862  have typedE : Real(E) by exact realE863  have fFunction := HasDerivativeAt.function with derivativeF864  have gFunction := HasDerivativeAt.function with derivativeG865  have realA : A ∈ ℝ by simp [Real]866  have fAInReals := FunctionBetween.apply_closed with fFunction, realA867  have gAInReals := FunctionBetween.apply_closed with gFunction, realA868  have typedFA : Real(f(A)) by exact fAInReals869  have typedGA : Real(g(A)) by exact gAInReals870  have firstReal := realMulValue.real with typedD, typedGA871  have secondReal := realMulValue.real with typedFA, typedE872  have derivativeReal := realAddValue.real with firstReal, secondReal873  have productDerivative := HasDerivativeAt.mul with derivativeF, derivativeG874  unfold realAddValue at productDerivative875  unfold realMulValue at productDerivative876  witness D * g(A) + f(A) * E877  constructor878    exact derivativeReal879  . unfold call2880    exact productDerivative881