Grace/Cumulus/Real/Analysis/CauchyMeanValue.g17

Open in Workbench Download source

Imports

Derivative · MeanValueIntegration

Declarations

Source

1-- Real analysis: the Cauchy mean value theorem2-- 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.CauchyMeanValue8import Derivative9import MeanValueIntegration1011-- Section: Preparations12theorem ContinuousOn.of_differentiable (f S : Set)13  requires function : f : ℝ → ℝ14  requires subset : S ⊆ ℝ15  requires differentiable : ∀ X ∈ S, DifferentiableAt(f, X)16  shows ContinuousOn(f, S)17proof18  constructor19  . exact function20  . constructor21    . exact subset22    . intros X memberX23      have realX := subset with X, memberX24      have typedX : Real(X) by exact realX25      have differentiableAt := differentiable with X, memberX26      have hasDerivative := derivative.has_derivative_at with differentiableAt27      have continuousAt := HasDerivativeAt.continuous_at with hasDerivative28      exact ContinuousAt.continuous_within_at with continuousAt, subset2930theorem DifferentiableAt.function (f : Set) (X : Real)31  requires differentiable : DifferentiableAt(f, X)32  shows f : ℝ → ℝ33proof34  obtain ⟨D, realD, hasDerivative⟩ := differentiable35  exact HasDerivativeAt.function with hasDerivative3637-- Section: CauchyCombination38-- The function (g(B) - g(A)) f + (f(A) - f(B)) g takes the same value at A39-- and at B; Rolle's theorem applied to it is the Cauchy mean value theorem.40def cauchyCombination (f g : Set) (A B : Real) : Set :=41  pointwiseAdd(42    pointwiseMul(constantRealFunction(realSubValue(g(B), g(A))), f),43    pointwiseMul(constantRealFunction(realSubValue(f(A), f(B))), g))4445theorem cauchyCombination.value (f g : Set) (A B X : Real)46  requires fFunction : f : ℝ → ℝ47  requires gFunction : g : ℝ → ℝ48  shows cauchyCombination(f, g, A, B)(X) =49    (g(B) - g(A)) * f(X) + (f(A) - f(B)) * g(X)50proof51  have realA : A ∈ ℝ by simp [Real]52  have realB : B ∈ ℝ by simp [Real]53  have realX : X ∈ ℝ by simp [Real]54  have typedFA : Real(f(A))55    exact FunctionBetween.apply_closed with fFunction, realA56  have typedFB : Real(f(B))57    exact FunctionBetween.apply_closed with fFunction, realB58  have typedFX : Real(f(X))59    exact FunctionBetween.apply_closed with fFunction, realX60  have typedGA : Real(g(A))61    exact FunctionBetween.apply_closed with gFunction, realA62  have typedGB : Real(g(B))63    exact FunctionBetween.apply_closed with gFunction, realB64  have typedGX : Real(g(X))65    exact FunctionBetween.apply_closed with gFunction, realX66  have typedWidthG := realSubValue.real with typedGB, typedGA67  have typedWidthF := realSubValue.real with typedFA, typedFB68  have widthGFunction := constantRealFunction.function with typedWidthG69  have widthFFunction := constantRealFunction.function with typedWidthF70  have leftFunction := pointwiseMul.function with widthGFunction, fFunction71  have rightFunction := pointwiseMul.function with widthFFunction, gFunction72  have typedWidthGX : Real(constantRealFunction(g(B) - g(A))(X))73    exact FunctionBetween.apply_closed with widthGFunction, realX74  have typedWidthFX : Real(constantRealFunction(f(A) - f(B))(X))75    exact FunctionBetween.apply_closed with widthFFunction, realX76  have leftValue := pointwiseMul.value at77    constantRealFunction(g(B) - g(A)), f, X with78      assumption, widthGFunction, fFunction, typedWidthGX, typedFX79  have rightValue := pointwiseMul.value at80    constantRealFunction(f(A) - f(B)), g, X with81      assumption, widthFFunction, gFunction, typedWidthFX, typedGX82  have typedLeft : Real(pointwiseMul(constantRealFunction(g(B) - g(A)), f)(X))83    exact FunctionBetween.apply_closed with leftFunction, realX84  have typedRight : Real(pointwiseMul(constantRealFunction(f(A) - f(B)), g)(X))85    exact FunctionBetween.apply_closed with rightFunction, realX86  have sum := pointwiseAdd.value at87    pointwiseMul(constantRealFunction(g(B) - g(A)), f),88    pointwiseMul(constantRealFunction(f(A) - f(B)), g),89    X with assumption, leftFunction, rightFunction, typedLeft, typedRight90  have widthGValue := constantRealFunction.value at g(B) - g(A), X with91    typedWidthG, assumption92  have widthFValue := constantRealFunction.value at f(A) - f(B), X with93    typedWidthF, assumption94  have equality : cauchyCombination(f, g, A, B)(X) =95      pointwiseMul(constantRealFunction(g(B) - g(A)), f)(X) +96        pointwiseMul(constantRealFunction(f(A) - f(B)), g)(X)97    simp [cauchyCombination]98  rwa [leftValue, rightValue, widthGValue, widthFValue] at equality99100theorem cauchyCombination.endpoints (f g : Set) (A B : Real)101  requires fFunction : f : ℝ → ℝ102  requires gFunction : g : ℝ → ℝ103  shows cauchyCombination(f, g, A, B)(A) = cauchyCombination(f, g, A, B)(B)104proof105  have atA := cauchyCombination.value at f, g, A, B, A with fFunction, gFunction106  have atB := cauchyCombination.value at f, g, A, B, B with fFunction, gFunction107  have realA : A ∈ ℝ by simp [Real]108  have realB : B ∈ ℝ by simp [Real]109  have fA := FunctionBetween.apply_closed with fFunction, realA110  have fB := FunctionBetween.apply_closed with fFunction, realB111  have gA := FunctionBetween.apply_closed with gFunction, realA112  have gB := FunctionBetween.apply_closed with gFunction, realB113  rw [atA, atB]114  ring115116theorem cauchyCombination.continuous_on (f g : Set) (A B : Real)117  requires continuousF : ContinuousOn(f, closedInterval(A, B))118  requires continuousG : ContinuousOn(g, closedInterval(A, B))119  shows ContinuousOn(cauchyCombination(f, g, A, B), closedInterval(A, B))120proof121  have fFunction : f : ℝ → ℝ122    rcases continuousF with ⟨graph, subset, everywhere⟩123    exact graph124  have gFunction : g : ℝ → ℝ125    rcases continuousG with ⟨graph, subset, everywhere⟩126    exact graph127  have realA : A ∈ ℝ by simp [Real]128  have realB : B ∈ ℝ by simp [Real]129  have typedFA : Real(f(A))130    exact FunctionBetween.apply_closed with fFunction, realA131  have typedFB : Real(f(B))132    exact FunctionBetween.apply_closed with fFunction, realB133  have typedGA : Real(g(A))134    exact FunctionBetween.apply_closed with gFunction, realA135  have typedGB : Real(g(B))136    exact FunctionBetween.apply_closed with gFunction, realB137  have typedWidthG := realSubValue.real with typedGB, typedGA138  have typedWidthF := realSubValue.real with typedFA, typedFB139  have subset := closedInterval.subset_reals at A, B with *140  have widthGContinuous := Continuous.continuous_on at141    constantRealFunction(g(B) - g(A)), closedInterval(A, B) with142      constantRealFunction.continuous at g(B) - g(A) with typedWidthG, subset143  have widthFContinuous := Continuous.continuous_on at144    constantRealFunction(f(A) - f(B)), closedInterval(A, B) with145      constantRealFunction.continuous at f(A) - f(B) with typedWidthF, subset146  have first := ContinuousOn.mul with widthGContinuous, continuousF147  have second := ContinuousOn.mul with widthFContinuous, continuousG148  unfold cauchyCombination149  exact ContinuousOn.add with first, second150151theorem cauchyCombination.derivative (f g : Set) (A B C D E : Real)152  requires derivativeF : HasDerivativeAt(f, D, C)153  requires derivativeG : HasDerivativeAt(g, E, C)154  shows HasDerivativeAt(cauchyCombination(f, g, A, B),155    ((g(B):R) - (g(A):R)) * D + ((f(A):R) - (f(B):R)) * E, C)156proof157  have fFunction := HasDerivativeAt.function with derivativeF158  have gFunction := HasDerivativeAt.function with derivativeG159  have realA : A ∈ ℝ by simp [Real]160  have realB : B ∈ ℝ by simp [Real]161  have typedFA : Real(f(A))162    exact FunctionBetween.apply_closed with fFunction, realA163  have typedFB : Real(f(B))164    exact FunctionBetween.apply_closed with fFunction, realB165  have typedGA : Real(g(A))166    exact FunctionBetween.apply_closed with gFunction, realA167  have typedGB : Real(g(B))168    exact FunctionBetween.apply_closed with gFunction, realB169  have typedWidthG := realSubValue.real with typedGB, typedGA170  have typedWidthF := realSubValue.real with typedFA, typedFB171  have first := HasDerivativeAt.scale at f, g(B) - g(A), D, C with172    typedWidthG, derivativeF173  have second := HasDerivativeAt.scale at g, f(A) - f(B), E, C with174    typedWidthF, derivativeG175  unfold cauchyCombination176  exact HasDerivativeAt.add with first, second177178-- Section: CauchyMeanValue179-- The Cauchy mean value theorem: for f and g continuous on [A, B] and180-- differentiable inside, some C between A and B has181-- f′(C) (g(B) − g(A)) = g′(C) (f(B) − f(A)).182theorem CauchyMeanValue.theorem (f g : ℝ → ℝ) (A B : Real)183  requires ordered : A < B184  requires continuousF : ContinuousOn(f, closedInterval(A, B))185  requires continuousG : ContinuousOn(g, closedInterval(A, B))186  requires differentiableF : ∀ C ∈ ℝ, A < C → C < B → DifferentiableAt(f, C)187  requires differentiableG : ∀ C ∈ ℝ, A < C → C < B → DifferentiableAt(g, C)188  shows ∃ C ∈ ℝ, A < C ∧ C < B ∧189    f′(C) * (g(B) - g(A)) = g′(C) * (f(B) - f(A))190proof191  have fFunction : f : ℝ → ℝ by assumption192  have gFunction : g : ℝ → ℝ by assumption193  have realA : A ∈ ℝ by simp [Real]194  have realB : B ∈ ℝ by simp [Real]195  have typedFA : Real(f(A))196    exact FunctionBetween.apply_closed with fFunction, realA197  have typedFB : Real(f(B))198    exact FunctionBetween.apply_closed with fFunction, realB199  have typedGA : Real(g(A))200    exact FunctionBetween.apply_closed with gFunction, realA201  have typedGB : Real(g(B))202    exact FunctionBetween.apply_closed with gFunction, realB203  have continuous := cauchyCombination.continuous_on with204    continuousF, continuousG205  have endpoints := cauchyCombination.endpoints at f, g, A, B with206    fFunction, gFunction207  have differentiable : ∀ C ∈ ℝ, A < C → C < B →208      ∃ D ∈ ℝ, HasDerivativeAt(cauchyCombination(f, g, A, B), D, C)209    intros C realC left right210    have typedC : Real(C) by exact realC211    have differentiableAtF := differentiableF with C, realC, left, right212    have differentiableAtG := differentiableG with C, realC, left, right213    have derivativeF := derivative.has_derivative_at with differentiableAtF214    have derivativeG := derivative.has_derivative_at with differentiableAtG215    have typedF := derivative.real at f, C216    have typedG := derivative.real at g, C217    have combined := cauchyCombination.derivative at218      f, g, A, B, C, derivative(f)(C), derivative(g)(C) with219        typedF, typedG, derivativeF, derivativeG220    have typedValue : Real((g(B) - g(A)) * derivative(f)(C) +221        (f(A) - f(B)) * derivative(g)(C))222      typecheck223    witness (g(B) - g(A)) * derivative(f)(C) + (f(A) - f(B)) * derivative(g)(C)224    refine ⟨typedValue, combined⟩225  obtain ⟨T, realT, left, right, zeroDerivative⟩ := Rolle.theorem with226    ordered, continuous, endpoints, differentiable227  have typedT : Real(T) by exact realT228  have differentiableAtF := differentiableF with T, realT, left, right229  have differentiableAtG := differentiableG with T, realT, left, right230  have derivativeF := derivative.has_derivative_at with differentiableAtF231  have derivativeG := derivative.has_derivative_at with differentiableAtG232  have typedF := derivative.real at f, T233  have typedG := derivative.real at g, T234  have combined := cauchyCombination.derivative at235    f, g, A, B, T, derivative(f)(T), derivative(g)(T) with236      typedF, typedG, derivativeF, derivativeG237  have vanishes := HasDerivativeAt.unique with combined, zeroDerivative238  witness T239  refine ⟨realT, left, right, _⟩240  linear_combination vanishes241242-- The mean value theorem and Rolle's theorem in terms of the derivative.243theorem MeanValue.derivative (f : ℝ → ℝ) (A B : Real)244  requires ordered : A < B245  requires continuous : ContinuousOn(f, closedInterval(A, B))246  requires differentiable : ∀ C ∈ ℝ, A < C → C < B → DifferentiableAt(f, C)247  shows ∃ C ∈ ℝ, A < C ∧ C < B ∧ f′(C) * (B - A) = f(B) - f(A)248proof249  have unfolded : ∀ C ∈ ℝ, A < C → C < B → ∃ D ∈ ℝ, HasDerivativeAt(f, D, C)250    intros C realC left right251    have differentiableAt := differentiable with C, realC, left, right252    unfold DifferentiableAt at differentiableAt253    exact differentiableAt254  obtain ⟨T, realT, left, right, D, realD, hasDerivative, equation⟩ :=255    MeanValue.theorem with ordered, continuous, unfolded256  have value := derivative.of_has_derivative with hasDerivative257  witness T258  refine ⟨realT, left, right, _⟩259  rwa value260