Grace/Cumulus/Real/Analysis/MeanValueIntegration.g17

Open in Workbench Download source

Imports

Differentiation · Intervals · ExtremeValue · Continuity · Integration.CommonRefinementComparison · Integration.IntegralOrderBound

Declarations

Source

1-- Real analysis: MeanValueIntegration2-- 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.MeanValueIntegration8import Differentiation9import Intervals10import ExtremeValue11import Continuity12import Integration.CommonRefinementComparison13import Integration.IntegralOrderBound1415-- Section: MeanValueCorrectionDerivative16def meanValueCorrection (F : Set) (A B : Real) : Set :=17  pointwiseSub(18    pointwiseMul(constantRealFunction(realSubValue(B, A)), F),19    pointwiseMul(constantRealFunction(realSubValue(F(B), F(A))), identity(ℝ)))2021theorem meanValueCorrection.continuous_on (F : Set) (A B : Real)22  requires continuous : ContinuousOn(F, closedInterval(A, B))23  shows ContinuousOn(meanValueCorrection(F, A, B), closedInterval(A, B))24proof25  have function : F : ℝ → ℝ26    rcases continuous with ⟨graph, subset, everywhere⟩27    exact graph28  have realA : A ∈ ℝ by simp [Real]29  have realB : B ∈ ℝ by simp [Real]30  have valueA := FunctionBetween.apply_closed with function, realA31  have valueB := FunctionBetween.apply_closed with function, realB32  have typedFA : Real(F(A)) by exact valueA33  have typedFB : Real(F(B)) by exact valueB34  have widthReal : Real(B - A)35    exact realSubValue.real with *36  have deltaReal : Real(F(B) - F(A)) by exact realSubValue.real at F(B), F(A) with typedFB, typedFA37  have subset := closedInterval.subset_reals at A, B with *38  have constantWidth := Continuous.continuous_on at39    constantRealFunction(B - A), closedInterval(A, B) with40      constantRealFunction.continuous at B - A with widthReal, subset41  have first := ContinuousOn.mul with constantWidth, continuous42  have linear := Continuous.mul at43    constantRealFunction(F(B) - F(A)), identity(ℝ) with44      constantRealFunction.continuous at45        F(B) - F(A) with deltaReal,46      identity.continuous47  have negLinear := Continuous.neg with linear48  have second := Continuous.continuous_on at49    pointwiseNeg(pointwiseMul(50      constantRealFunction(F(B) - F(A)), identity(ℝ))),51    closedInterval(A, B) with negLinear, subset52  unfold meanValueCorrection53  unfold pointwiseSub54  exact ContinuousOn.add at55    pointwiseMul(constantRealFunction(B - A), F),56    pointwiseNeg(pointwiseMul(57      constantRealFunction(F(B) - F(A)), identity(ℝ))),58    closedInterval(A, B) with first, second5960-- MeanValueCorrectionValues61theorem meanValueCorrection.value (F : Set) (A B X : Real)62  requires function : F : ℝ → ℝ63  shows meanValueCorrection(F, A, B)(X) =64    (B - A) * F(X) - (F(B) - F(A)) * X65proof66  have realA : A ∈ ℝ by simp [Real]67  have realB : B ∈ ℝ by simp [Real]68  have realX : X ∈ ℝ by simp [Real]69  have fA := FunctionBetween.apply_closed with function, realA70  have fB := FunctionBetween.apply_closed with function, realB71  have fX := FunctionBetween.apply_closed with function, realX72  have typedFA : Real(F(A)) by exact fA73  have typedFB : Real(F(B)) by exact fB74  have typedFX : Real(F(X)) by exact fX75  have typedWidth := realSubValue.real at B, A with *76  have typedDelta := realSubValue.real with typedFB, typedFA77  have widthFunction := constantRealFunction.function with typedWidth78  have deltaFunction := constantRealFunction.function with typedDelta79  have identityFunction := identity.function at ℝ80  have leftFunction := pointwiseMul.function with widthFunction, function81  have rightFunction := pointwiseMul.function with deltaFunction, identityFunction82  have widthX := FunctionBetween.apply_closed with widthFunction, realX83  have deltaX := FunctionBetween.apply_closed with deltaFunction, realX84  have identityX := FunctionBetween.apply_closed with identityFunction, realX85  have typedWidthX : Real(constantRealFunction(B - A)(X)) by exact widthX86  have typedDeltaX : Real(constantRealFunction(F(B) - F(A))(X)) by exact deltaX87  have typedIdentityX : Real(identity(ℝ)(X)) by exact identityX88  have leftValue := pointwiseMul.value at89    constantRealFunction(B - A), F, X with90      assumption, widthFunction, function, typedWidthX, typedFX91  have rightValue := pointwiseMul.value at92    constantRealFunction(F(B) - F(A)), identity(ℝ), X with93      assumption, deltaFunction, identityFunction, typedDeltaX, typedIdentityX94  have leftReal := FunctionBetween.apply_closed with leftFunction, realX95  have rightReal := FunctionBetween.apply_closed with rightFunction, realX96  have typedLeft : Real(pointwiseMul(constantRealFunction(B - A), F)(X)) by exact leftReal97  have typedRight : Real(pointwiseMul(constantRealFunction(F(B) - F(A)), identity(ℝ))(X)) by exact rightReal98  have subtraction := pointwiseSub.value at99    pointwiseMul(constantRealFunction(B - A), F),100    pointwiseMul(constantRealFunction(F(B) - F(A)), identity(ℝ)),101    X with assumption, leftFunction, rightFunction, typedLeft, typedRight102  have widthValue := constantRealFunction.value at B - A, X with typedWidth, assumption103  have deltaValue := constantRealFunction.value at104    F(B) - F(A), X with typedDelta, assumption105  have identityValue := identity.apply with realX106  have equality : meanValueCorrection(F, A, B)(X) =107      pointwiseMul(constantRealFunction(B - A), F)(X) -108        pointwiseMul(constantRealFunction(F(B) - F(A)), identity(ℝ))(X)109    simp [meanValueCorrection]110  rwa [leftValue, rightValue, widthValue, deltaValue, identityValue] at equality111112theorem meanValueCorrection.endpoints (F : Set) (A B : Real)113  requires function : F : ℝ → ℝ114  shows meanValueCorrection(F, A, B)(A) =115    meanValueCorrection(F, A, B)(B)116proof117  have atA := meanValueCorrection.value at F, A, B, A with function118  have atB := meanValueCorrection.value at F, A, B, B with function119  have realA : A ∈ ℝ by simp [Real]120  have realB : B ∈ ℝ by simp [Real]121  have fA := FunctionBetween.apply_closed with function, realA122  have fB := FunctionBetween.apply_closed with function, realB123  rw [atA, atB]124  ring125126-- MeanValueCorrectionDerivative127theorem meanValueCorrection.derivative (F : Set) (A B C D : Real)128  requires derivative : HasDerivativeAt(F, D, C)129  shows HasDerivativeAt(meanValueCorrection(F, A, B), (B - A) * D - ((F(B):R) - (F(A):R)), C)130proof131  have function := HasDerivativeAt.function with derivative132  have realA : A ∈ ℝ by simp [Real]133  have realB : B ∈ ℝ by simp [Real]134  have valueA := FunctionBetween.apply_closed with function, realA135  have valueB := FunctionBetween.apply_closed with function, realB136  have typedFA : Real(F(A)) by exact valueA137  have typedFB : Real(F(B)) by exact valueB138  have widthReal := realSubValue.real at B, A with *139  have deltaReal := realSubValue.real with typedFB, typedFA140  have constantWidth := constantRealFunction.has_derivative_at at B - A, C with141    widthReal, assumption142  have constantDelta := constantRealFunction.has_derivative_at at143    F(B) - F(A), C with deltaReal, assumption144  have identityDerivative := identity.has_derivative_at at C145  have first := HasDerivativeAt.mul with realZero.real, constantWidth, derivative146  have second := HasDerivativeAt.mul with realZero.real, realOne.real, constantDelta, identityDerivative147  have realC : C ∈ ℝ by simp [Real]148  have fC := FunctionBetween.apply_closed with function, realC149  have typedFC : Real(F(C)) by exact fC150  have widthC := FunctionBetween.apply_closed at151    constantRealFunction(B - A), ℝ, ℝ, C with152      constantRealFunction.function at B - A with widthReal, realC153  have deltaC := FunctionBetween.apply_closed at154    constantRealFunction(F(B) - F(A)), ℝ, ℝ, C with155      constantRealFunction.function at F(B) - F(A) with deltaReal, realC156  have idC := FunctionBetween.apply_closed at identity(ℝ), ℝ, ℝ, C with157    identity.function at ℝ, realC158  have typedWidthC : Real(constantRealFunction(B - A)(C)) by exact widthC159  have typedDeltaC : Real(constantRealFunction(F(B) - F(A))(C)) by exact deltaC160  have typedIdC : Real(identity(ℝ)(C)) by exact idC161  have productZeroF := realMulValue.real with realZero.real, typedFC162  have productWidth := realMulValue.real at constantRealFunction(B - A)(C), D with typedWidthC, assumption163  have productZeroId := realMulValue.real with realZero.real, typedIdC164  have productDelta := realMulValue.real with typedDeltaC, realOne.real165  have raw := HasDerivativeAt.sub with first, second166  have widthValue := constantRealFunction.value at B - A, C with widthReal, assumption167  have deltaValue := constantRealFunction.value at168    F(B) - F(A), C with deltaReal, assumption169  have result : (realZero * F(C) + constantRealFunction(B - A)(C) * D) -170    (realZero * identity(ℝ)(C) +171      constantRealFunction(F(B) - F(A))(C) * realOne) =172      (B - A) * D - (F(B) - F(A))173    rw [widthValue, deltaValue]174    ring175  have view : realSubValue(176      realAddValue(realMulValue(realZero, F(C)),177        realMulValue(constantRealFunction(B - A)(C), D)),178      realAddValue(realMulValue(realZero, identity(ℝ)(C)),179        realMulValue(constantRealFunction(F(B) - F(A))(C), realOne))) =180      (realZero * F(C) + constantRealFunction(B - A)(C) * D) -181      (realZero * identity(ℝ)(C) +182        constantRealFunction(F(B) - F(A))(C) * realOne)183    unfold realSubValue184    unfold realAddValue185    unfold realMulValue186    unfold call2187    rfl188  unfold meanValueCorrection189  rwa [view, result] at raw190191-- Section: InteriorSteps192theorem differenceQuotient.positive_increment (f : Set) (C H : Real)193  requires function : f : ℝ → ℝ194  requires positiveH : 0 < H195  requires positiveQ : 0 < (differenceQuotient(f, C)(H):R)196  shows 0 < f(C + H) - f(C)197proof198  have realCPlusH := realAddValue.real at C, H with *199  have memberCPlusH : C + H ∈ ℝ by exact realCPlusH200  have memberC : C ∈ ℝ by simp [Real]201  have valueCPlusH := FunctionBetween.apply_closed with function, memberCPlusH202  have valueC := FunctionBetween.apply_closed with function, memberC203  have realValueCPlusH : Real(f(C + H)) by exact valueCPlusH204  have realValueC : Real(f(C)) by exact valueC205  have realIncrement := realSubValue.real with realValueCPlusH, realValueC206  have realQ := differenceQuotient.function at f, C with function207  have memberH : H ∈ ℝ by simp [Real]208  have valueQ := FunctionBetween.apply_closed with realQ, memberH209  have nonzero : H ≠ 0210    intro equal211    rw equal at positiveH212    have impossible := realLess.characterization.forward with positiveH213    exact RealLess.irreflexive with impossible214  have quotient := differenceQuotient.value at f, C, H with function215  have cancels := realDiv.mul_right with realIncrement, assumption, nonzero216  rw ← quotient at cancels217  have product := realMulValue.positive with positiveQ, positiveH218  rwa cancels at product219220theorem differenceQuotient.negative_step_positive_increment (f : Set) (C H : Real)221  requires function : f : ℝ → ℝ222  requires negativeH : H < 0223  requires negativeQ : (differenceQuotient(f, C)(H):R) < 0224  shows 0 < f(C + H) - f(C)225proof226  have realCPlusH := realAddValue.real at C, H with *227  have memberCPlusH : C + H ∈ ℝ by exact realCPlusH228  have memberC : C ∈ ℝ by simp [Real]229  have valueCPlusH := FunctionBetween.apply_closed with function, memberCPlusH230  have valueC := FunctionBetween.apply_closed with function, memberC231  have realValueCPlusH : Real(f(C + H)) by exact valueCPlusH232  have realValueC : Real(f(C)) by exact valueC233  have realIncrement := realSubValue.real with realValueCPlusH, realValueC234  have realQ := differenceQuotient.function at f, C with function235  have memberH : H ∈ ℝ by simp [Real]236  have valueQ := FunctionBetween.apply_closed with realQ, memberH237  have typedQ : Real(differenceQuotient(f, C)(H)) by exact valueQ238  have nonzero : H ≠ 0239    intro equal240    rw equal at negativeH241    have impossible := realLess.characterization.forward with negativeH242    exact RealLess.irreflexive with impossible243  have quotient := differenceQuotient.value at f, C, H with function244  have cancels := realDiv.mul_right with realIncrement, assumption, nonzero245  rw ← quotient at cancels246  have negativeQView := realLess.characterization.forward with negativeQ247  have negativeHView := realLess.characterization.forward with negativeH248  have positiveNegQView := RealLess.neg_reverse with negativeQView249  have positiveNegHView := RealLess.neg_reverse with negativeHView250  have positiveNegQ := realLess.characterization.backward with positiveNegQView251  have positiveNegH := realLess.characterization.backward with positiveNegHView252  rw realNegValue.zero at positiveNegQ253  rw realNegValue.zero at positiveNegH254  have positiveProduct := realMulValue.positive at255    -differenceQuotient(f, C)(H), -H with256      realNegValue.real at differenceQuotient(f, C)(H) with typedQ,257      realNegValue.real at H with assumption,258      positiveNegQ, positiveNegH259  have sameProduct : (-differenceQuotient(f, C)(H)) * (-H) =260      differenceQuotient(f, C)(H) * H261    ring262  rwa [sameProduct, cancels] at positiveProduct263264-- InteriorSteps265theorem closedInterval.right_step (A C B H : Real)266  requires left : A < C267  requires positive : 0 < H268  requires small : H < B - C269  shows C + H ∈ closedInterval(A, B)270proof271  have pointReal := realAddValue.real at C, H with *272  have pointMember : C + H ∈ ℝ by exact pointReal273  have aboveC := realLess.add_left at realZero, H, C with274    realZero.real, *{2}, positive275  have zero := realAddValue.zero_right at C276  rw zero at aboveC277  have lowerStrict : A < C + H278    exact realLess.transitive at A, C, C + H with279      *{2}, pointReal, left, aboveC280  have widthReal := realSubValue.real at B, C with *281  have shifted := realLess.add_right at H, B - C, C with282    assumption, widthReal, assumption, small283  have cancel := realSubValue.add_right_cancel at B, C with284    *{2}285  rw cancel at shifted286  have commute := realAddValue.commutative at H, C with *287  rw commute at shifted288  have upperStrict : C + H < B by exact shifted289  have lower := realLess.implies_le with lowerStrict290  have upper := realLess.implies_le with upperStrict291  apply closedInterval.membership.backward292  refine ⟨pointMember, lower, upper⟩293294theorem closedInterval.left_step (A C B H : Real)295  requires right : C < B296  requires positive : 0 < H297  requires small : H < C - A298  shows C - H ∈ closedInterval(A, B)299proof300  have pointReal := realSubValue.real at C, H with *301  have pointMember : C - H ∈ ℝ by exact pointReal302  have widthReal := realSubValue.real at C, A with *303  have shifted := realLess.add_right at H, C - A, A with304    assumption, widthReal, assumption, small305  have cancel := realSubValue.add_right_cancel at C, A with306    *{2}307  rw cancel at shifted308  have shiftBack := realLess.add_right_iff.forward at309    A, C - H, H with310      assumption, pointReal, assumption311  have lowerStrict : A < C - H312    have same : A + H = H + A by ring313    have cancelH : (C - H) + H = C by ring314    rw [← same, ← cancelH] at shifted315    exact shiftBack with shifted316  have negativeView := realLess.characterization.forward with positive317  have reversed := RealLess.neg_reverse with negativeView318  have negative := realLess.characterization.backward with reversed319  rw realNegValue.zero at negative320  have belowC := realLess.add_left at -H, realZero, C with321    realNegValue.real at H with assumption, realZero.real, assumption,322    negative323  have zero := realAddValue.zero_right at C324  rw zero at belowC325  have belowCSub : C - H < C326    unfold realSubValue327    exact belowC328  have upperStrict : C - H < B by exact realLess.transitive with belowCSub, right329  have lower := realLess.implies_le with lowerStrict330  have upper := realLess.implies_le with upperStrict331  apply closedInterval.membership.backward332  refine ⟨pointMember, lower, upper⟩333334-- Section: IntervalInterior335theorem Real.exists_small_positive (E W : Real)336  requires positiveE : 0 < E337  requires positiveW : 0 < W338  shows ∃ H ∈ ℝ, 0 < H ∧ H < E ∧ H < W339proof340  obtain ⟨N, naturalN, near⟩ := ConvergesTo.common_eventually with341    dyadicRadii.converges_zero, dyadicRadii.converges_zero, positiveE, positiveW342  have typedN := nat.omega.backward with naturalN343  have close := near with N, naturalN,344    LessEqual.reflexive with typedN345  rcases close with ⟨nearE, nearW⟩346  have value := dyadicRadii.value with typedN347  rw value at nearE348  rw value at nearW349  have first := openBall.order_characterization.forward with nearE350  have second := openBall.order_characterization.forward with nearW351  rcases first with ⟨lowerE, upperE⟩352  rcases second with ⟨lowerW, upperW⟩353  have zeroE := realAddValue.zero_left at E354  have zeroW := realAddValue.zero_left at W355  rw zeroE at upperE356  rw zeroW at upperW357  have realH := dyadicRadius.real with typedN358  witness dyadicRadius(N)359  constructor360    exact realH361  . refine ⟨dyadicRadius.positive at N with typedN, upperE, upperW⟩362363theorem Real.small_positive_in_ball (H E : Real)364  requires positive : 0 < H365  requires below : H < E366  shows H ∈ openBall(realZero, E)367proof368  have positiveE := realLess.transitive with realZero.real, positive, below369  have negativeE := realLess.characterization.forward with positiveE370  have reversed := RealLess.neg_reverse with negativeE371  have negative := realLess.characterization.backward with reversed372  rw realNegValue.zero at negative373  have lower := realLess.transitive at -E, realZero, H with374    realNegValue.real at E with assumption, realZero.real, assumption,375    negative, positive376  have zeroMinus := realSubValue.zero_left at E377  have zeroPlus := realAddValue.zero_left at E378  rw ← zeroMinus at lower379  rw ← zeroPlus at below380  apply openBall.order_characterization.backward with realZero.real381  refine ⟨lower, below⟩382383theorem Real.small_negative_in_ball (H E : Real)384  requires positive : 0 < H385  requires below : H < E386  shows -H ∈ openBall(realZero, E)387proof388  have negativeHView := realLess.characterization.forward with positive389  have reversedH := RealLess.neg_reverse with negativeHView390  have negativeH := realLess.characterization.backward with reversedH391  rw realNegValue.zero at negativeH392  have positiveE := realLess.transitive with realZero.real, positive, below393  have upper := realLess.transitive at -H, realZero, E with394    realNegValue.real at H with assumption, realZero.real, assumption,395    negativeH, positiveE396  have belowView := realLess.characterization.forward with below397  have reversed := RealLess.neg_reverse with belowView398  have lower := realLess.characterization.backward with reversed399  have zeroMinus := realSubValue.zero_left at E400  have zeroPlus := realAddValue.zero_left at E401  rw ← zeroMinus at lower402  rw ← zeroPlus at upper403  apply openBall.order_characterization.backward at -H, realZero, E with404    realNegValue.real at H with assumption, realZero.real, assumption405  refine ⟨lower, upper⟩406407-- PuncturedSign408theorem TendsToAt.eventually_positive (f : Set) (D A : Real)409  requires limit : TendsToAt(f, D, A)410  requires positive : 0 < D411  shows ∃ E ∈ ℝ, 0 < E ∧412    (∀ H ∈ ℝ, H ≠ A → H ∈ openBall(A, E) → (0:R) < (f(H):R))413proof414  obtain ⟨E, realE, positiveE, near⟩ := TendsToAt.eventually with limit, positive415  witness E416  constructor417  . exact realE418  . constructor419    . exact positiveE420    . intros H realH nonzero close421      have image := near with H, realH, nonzero, close422      have function := TendsToAt.function with limit423      have imageReal := FunctionBetween.apply_closed with function, realH424      obtain ⟨lower, upper⟩ := openBall.order_characterization.forward with image425      have self := realSubValue.self at D426      rwa self at lower427428theorem TendsToAt.eventually_negative (f : Set) (D A : Real)429  requires limit : TendsToAt(f, D, A)430  requires negative : D < 0431  shows ∃ E ∈ ℝ, 0 < E ∧432    (∀ H ∈ ℝ, H ≠ A → H ∈ openBall(A, E) → (f(H):R) < (0:R))433proof434  have negativeView := realLess.characterization.forward with negative435  have reversed := RealLess.neg_reverse with negativeView436  have positiveNeg := realLess.characterization.backward with reversed437  rw realNegValue.zero at positiveNeg438  obtain ⟨E, realE, positiveE, near⟩ := TendsToAt.eventually with limit, positiveNeg439  witness E440  constructor441  . exact realE442  . constructor443    . exact positiveE444    . intros H realH nonzero close445      have image := near with H, realH, nonzero, close446      have function := TendsToAt.function with limit447      have imageReal := FunctionBetween.apply_closed with function, realH448      obtain ⟨lower, upper⟩ := openBall.order_characterization.forward with image449      have cancel := realAddValue.neg_right at D450      rwa cancel at upper451452-- Fermat453theorem HasDerivativeAt.not_positive_at_interval_max (f : Set) (A C B D : Real)454  requires left : A < C455  requires right : C < B456  requires derivative : HasDerivativeAt(f, D, C)457  requires maximal : ∀ X ∈ closedInterval(A, B),458    (f(X):R) ≤ (f(C):R)459  shows ¬(0 < D)460proof461  intro positiveD462  have function := HasDerivativeAt.function with derivative463  have limit := HasDerivativeAt.limit with derivative464  obtain ⟨E, realE, positiveE, sign⟩ := TendsToAt.eventually_positive with limit, positiveD465  have width := realLess.iff_pos_sub.forward with right466  obtain ⟨H, realH, positiveH, belowE, belowWidth⟩ := Real.exists_small_positive with positiveE, width467  have typedH : Real(H) by exact realH468  have near := Real.small_positive_in_ball with positiveH, belowE469  have nonzero : H ≠ realZero470    intro equal471    rw equal at positiveH472    have impossible := realLess.characterization.forward with positiveH473    exact RealLess.irreflexive with impossible474  have positiveQ := sign with H, realH, nonzero, near475  have member := closedInterval.right_step with left, positiveH, belowWidth476  have increment := differenceQuotient.positive_increment with function, positiveH, positiveQ477  have realC : C ∈ ℝ by simp [Real]478  have realNext : C + H ∈ ℝ by exact realAddValue.real at C, H with assumption, typedH479  have valueC := FunctionBetween.apply_closed with function, realC480  have valueNext := FunctionBetween.apply_closed with function, realNext481  have strict := realLess.iff_pos_sub.backward with increment482  have bound := maximal with C + H, member483  have cycle := realLess.transitive_le with strict, bound484  have impossible := realLess.characterization.forward with cycle485  exact RealLess.irreflexive with impossible486487theorem HasDerivativeAt.not_negative_at_interval_max (f : Set) (A C B D : Real)488  requires left : A < C489  requires right : C < B490  requires derivative : HasDerivativeAt(f, D, C)491  requires maximal : ∀ X ∈ closedInterval(A, B),492    (f(X):R) ≤ (f(C):R)493  shows ¬(D < 0)494proof495  intro negativeD496  have function := HasDerivativeAt.function with derivative497  have limit := HasDerivativeAt.limit with derivative498  obtain ⟨E, realE, positiveE, sign⟩ := TendsToAt.eventually_negative with limit, negativeD499  have width := realLess.iff_pos_sub.forward with left500  obtain ⟨H, realH, positiveH, belowE, belowWidth⟩ := Real.exists_small_positive with positiveE, width501  have typedH : Real(H) by exact realH502  have near := Real.small_negative_in_ball with positiveH, belowE503  have negativeHView := realLess.characterization.forward with positiveH504  have reversed := RealLess.neg_reverse with negativeHView505  have negativeH := realLess.characterization.backward with reversed506  rw realNegValue.zero at negativeH507  have nonzero : -H ≠ realZero508    intro equal509    rw equal at negativeH510    have impossible := realLess.characterization.forward with negativeH511    exact RealLess.irreflexive with impossible512  have negativeQ := sign with -H, nonzero, near513  have member := closedInterval.left_step with right, positiveH, belowWidth514  have increment := differenceQuotient.negative_step_positive_increment with function, negativeH, negativeQ515  have shape : C + (-H) = C - H by ring516  rw shape at increment517  have realC : C ∈ ℝ by simp [Real]518  have realPrevious : C - H ∈ ℝ by exact realSubValue.real at C, H with assumption, typedH519  have valueC := FunctionBetween.apply_closed with function, realC520  have valuePrevious := FunctionBetween.apply_closed with function, realPrevious521  have strict := realLess.iff_pos_sub.backward with increment522  have bound := maximal with C - H, member523  have cycle := realLess.transitive_le with strict, bound524  have impossible := realLess.characterization.forward with cycle525  exact RealLess.irreflexive with impossible526527theorem HasDerivativeAt.zero_at_interval_max (f : Set) (A C B D : Real)528  requires left : A < C529  requires right : C < B530  requires derivative : HasDerivativeAt(f, D, C)531  requires maximal : ∀ X ∈ closedInterval(A, B),532    (f(X):R) ≤ (f(C):R)533  shows D = 0534proof535  have notPositive := HasDerivativeAt.not_positive_at_interval_max with left, right, derivative, maximal536  have notNegative := HasDerivativeAt.not_negative_at_interval_max with left, right, derivative, maximal537  have upper : D ≤ realZero538    by_contra notUpper539    have positive := realLess.of_not_le with notUpper540    exact notPositive with positive541  have lower : realZero ≤ D542    by_contra notLower543    have negative := realLess.of_not_le with notLower544    exact notNegative with negative545  have upperView := realLe.characterization.forward with upper546  have lowerView := realLe.characterization.forward with lower547  exact RealLe.antisymmetric with upperView, lowerView548549theorem HasDerivativeAt.zero_at_interval_min (f : Set) (A C B D : Real)550  requires left : A < C551  requires right : C < B552  requires derivative : HasDerivativeAt(f, D, C)553  requires minimal : ∀ X ∈ closedInterval(A, B),554    (f(C):R) ≤ (f(X):R)555  shows D = 0556proof557  have function := HasDerivativeAt.function with derivative558  have negDerivative := HasDerivativeAt.neg with derivative559  have negMax : ∀ X ∈ closedInterval(A, B),560      (pointwiseNeg(f)(X):R) ≤ (pointwiseNeg(f)(C):R)561    intros X member562    have inReals := closedInterval.subset_reals at A, B with563      *{2}564    have realXMember := inReals with X, member565    have typedX : Real(X) by exact realXMember566    have valueX := FunctionBetween.apply_closed with function, realXMember567    have realCMember : C ∈ ℝ by simp [Real]568    have valueC := FunctionBetween.apply_closed with function, realCMember569    have typedValueX : Real(f(X)) by exact valueX570    have typedValueC : Real(f(C)) by exact valueC571    have lower := minimal with X, member572    have reversed := realLe.neg_reverse with lower573    have negX := pointwiseNeg.value with typedX, function, typedValueX574    have negC := pointwiseNeg.value at f, C with575      assumption, function, typedValueC576    rwa [negX, negC]577  have zeroNeg := HasDerivativeAt.zero_at_interval_max at578    pointwiseNeg(f), A, C, B, -D with579      realNegValue.real at D with assumption,580      left, right, negDerivative, negMax581  have involutive := realNegValue.involutive at D582  rw [← involutive, zeroNeg]583  exact realNegValue.zero584585-- IntervalInterior586theorem closedInterval.left_lt_of_ne (A B T : Real)587  requires member : T ∈ closedInterval(A, B)588  requires distinct : T ≠ A589  shows A < T590proof591  obtain ⟨realT, lower, upper⟩ := closedInterval.membership.forward with member592  have notReverse : ¬(T ≤ A)593    intro reverse594    have first := realLe.characterization.forward with lower595    have second := realLe.characterization.forward with reverse596    have equal := RealLe.antisymmetric with first, second597    apply distinct598    rw equal599    rfl600  exact realLess.of_not_le with notReverse601602theorem closedInterval.right_lt_of_ne (A B T : Real)603  requires member : T ∈ closedInterval(A, B)604  requires distinct : T ≠ B605  shows T < B606proof607  obtain ⟨realT, lower, upper⟩ := closedInterval.membership.forward with member608  have notReverse : ¬(B ≤ T)609    intro reverse610    have first := realLe.characterization.forward with upper611    have second := realLe.characterization.forward with reverse612    have equal := RealLe.antisymmetric with first, second613    exact distinct with equal614  exact realLess.of_not_le with notReverse615616theorem closedInterval.endpoint_or_interior (A B T : Real)617  requires member : T ∈ closedInterval(A, B)618  shows T = A ∨ T = B ∨ (A < T ∧ T < B)619proof620  obtain ⟨realT, lower, upper⟩ := closedInterval.membership.forward with member621  have alternativeA : T = A ∨ T ≠ A by tauto622  have alternativeB : T = B ∨ T ≠ B by tauto623  cases alternativeA with atA | awayA624  . tauto625  . cases alternativeB with atB | awayB626    . tauto627    . have strictA := closedInterval.left_lt_of_ne at A, B, T with628        member, awayA629      have strictB := closedInterval.right_lt_of_ne with member, awayB630      tauto631632-- Section: Rolle633theorem Rolle.midpoint_of_endpoint_extrema (f : Set) (A B T D : Real)634  requires ordered : A < B635  requires continuous : ContinuousOn(f, closedInterval(A, B))636  requires endpoints : f(A) = f(B)637  requires maximumA : ∀ X ∈ closedInterval(A, B),638    (f(X):R) ≤ (f(A):R)639  requires minimumT : ∀ X ∈ closedInterval(A, B),640    (f(T):R) ≤ (f(X):R)641  requires endpointT : T = A ∨ T = B642  requires derivative : HasDerivativeAt(f, D, intervalMidpoint(A, B))643  shows D = 0644proof645  obtain ⟨left, right⟩ := intervalMidpoint.between with ordered646  have middleReal := intervalMidpoint.real at A, B with *647  have middleMember : intervalMidpoint(A, B) ∈ closedInterval(A, B)648    have lower := realLess.implies_le with left649    have upper := realLess.implies_le with right650    have inReals : intervalMidpoint(A, B) ∈ ℝ by exact middleReal651    apply closedInterval.membership.backward652    refine ⟨inReals, lower, upper⟩653  have minimumAtMiddle := minimumT with intervalMidpoint(A, B), middleMember654  have minimumA : (f(A):R) ≤ (f(intervalMidpoint(A, B)):R)655    cases endpointT with atA | atB656    . rw atA at minimumAtMiddle657      exact minimumAtMiddle658    . rw [atB, ← endpoints] at minimumAtMiddle659      exact minimumAtMiddle660  have maximumAtMiddle := maximumA with intervalMidpoint(A, B), middleMember661  have function : f : ℝ → ℝ662    rcases continuous with ⟨graph, subset, atPoints⟩663    exact graph664  have realA : A ∈ ℝ by simp [Real]665  have realMiddle : intervalMidpoint(A, B) ∈ ℝ by exact middleReal666  have valueA := FunctionBetween.apply_closed with function, realA667  have valueMiddle := FunctionBetween.apply_closed with function, realMiddle668  have lowerView := realLe.characterization.forward with minimumA669  have upperView := realLe.characterization.forward with maximumAtMiddle670  have equal := RealLe.antisymmetric with lowerView, upperView671  have maximalMiddle : ∀ X ∈ closedInterval(A, B),672      (f(X):R) ≤ (f(intervalMidpoint(A, B)):R)673    intros X member674    have bound := maximumA with X, member675    rwa equal at bound676  exact HasDerivativeAt.zero_at_interval_max with left, right, derivative, maximalMiddle677678theorem Rolle.of_endpoint_maximum (f : Set) (A B : Real)679  requires ordered : A < B680  requires continuous : ContinuousOn(f, closedInterval(A, B))681  requires endpoints : f(A) = f(B)682  requires maximumA : ∀ X ∈ closedInterval(A, B),683    (f(X):R) ≤ (f(A):R)684  requires differentiable : ∀ C ∈ ℝ, A < C → C < B →685    ∃ D ∈ ℝ, HasDerivativeAt(f, D, C)686  shows ∃ C ∈ ℝ, A < C ∧ C < B ∧ HasDerivativeAt(f, realZero, C)687proof688  have orderedWeak := realLess.implies_le with ordered689  obtain ⟨T, member, minimum⟩ := ContinuousOn.closed_interval_minimum with orderedWeak, continuous690  obtain ⟨realT, lowerT, upperT⟩ := closedInterval.membership.forward with member691  have typedT : Real(T) by exact realT692  have status := closedInterval.endpoint_or_interior at A, B, T with693    typedT, member694  cases status with atA | other695  . have midpointReal := intervalMidpoint.real at A, B with *{2}696    obtain ⟨left, right⟩ := intervalMidpoint.between with ordered697    have midpointMember : intervalMidpoint(A, B) ∈ ℝ by exact midpointReal698    obtain ⟨D, realD, derivative⟩ := differentiable with699      intervalMidpoint(A, B), midpointMember, left, right700    have endpointT : T = A ∨ T = B by tauto701    have zero := Rolle.midpoint_of_endpoint_extrema with702      ordered, continuous, endpoints, maximumA, minimum, endpointT, derivative703    witness intervalMidpoint(A, B)704    refine ⟨midpointMember, left, right, _⟩705    rwa ← zero706  . cases other with atB | interior707    . have midpointReal := intervalMidpoint.real at A, B with *{2}708      obtain ⟨left, right⟩ := intervalMidpoint.between with ordered709      have midpointMember : intervalMidpoint(A, B) ∈ ℝ by exact midpointReal710      obtain ⟨E0, realE0, derivativeE0⟩ := differentiable with711        intervalMidpoint(A, B), midpointMember, left, right712      have endpointT : T = A ∨ T = B by tauto713      have zero := Rolle.midpoint_of_endpoint_extrema with714        ordered, continuous, endpoints, maximumA, minimum, endpointT, derivativeE0715      witness intervalMidpoint(A, B)716      refine ⟨midpointMember, left, right, _⟩717      rwa ← zero718    . rcases interior with ⟨left, right⟩719      obtain ⟨E1, realE1, derivativeE1⟩ := differentiable with720        T, realT, left, right721      have zero := HasDerivativeAt.zero_at_interval_min with left, right, derivativeE1, minimum722      witness T723      refine ⟨realT, left, right, _⟩724      rwa ← zero725726theorem Rolle.endpoint_maximum_value (f : Set) (A B T : Real)727  requires endpoints : f(A) = f(B)728  requires maximum : ∀ X ∈ closedInterval(A, B),729    (f(X):R) ≤ (f(T):R)730  requires endpointT : T = A ∨ T = B731  shows ∀ X ∈ closedInterval(A, B),732    (f(X):R) ≤ (f(A):R)733proof734  intros X member735  have bound := maximum with X, member736  cases endpointT with atA | atB737  . rw atA at bound738    exact bound739  . rw [atB, ← endpoints] at bound740    exact bound741742theorem Rolle.endpoint_maximum_left (f : Set) (A B T : Real)743  requires endpoints : f(A) = f(B)744  requires maximum : ∀ X ∈ closedInterval(A, B),745    (f(X):R) ≤ (f(T):R)746  requires atA : T = A747  shows ∀ X ∈ closedInterval(A, B),748    (f(X):R) ≤ (f(A):R)749proof750  intros X member751  have bound := maximum with X, member752  rwa atA at bound753754theorem Rolle.endpoint_maximum_right (f : Set) (A B T : Real)755  requires endpoints : f(A) = f(B)756  requires maximum : ∀ X ∈ closedInterval(A, B),757    (f(X):R) ≤ (f(T):R)758  requires atB : T = B759  shows ∀ X ∈ closedInterval(A, B),760    (f(X):R) ≤ (f(A):R)761proof762  intros X member763  have bound := maximum with X, member764  rwa [atB, ← endpoints] at bound765766-- The textbook hypotheses: continuity on the closed interval, differentiability767-- at every interior point, and equal endpoint values.768theorem Rolle.theorem (f : Set) (A B : Real)769  requires ordered : A < B770  requires continuous : ContinuousOn(f, closedInterval(A, B))771  requires endpoints : f(A) = f(B)772  requires differentiable : ∀ C ∈ ℝ, A < C → C < B →773    ∃ D ∈ ℝ, HasDerivativeAt(f, D, C)774  shows ∃ C ∈ ℝ, A < C ∧ C < B ∧ HasDerivativeAt(f, realZero, C)775proof776  have orderedWeak := realLess.implies_le with ordered777  obtain ⟨T, member, maximum⟩ := ContinuousOn.closed_interval_maximum with orderedWeak, continuous778  obtain ⟨realT, lowerT, upperT⟩ := closedInterval.membership.forward with member779  have typedT : Real(T) by exact realT780  have status := closedInterval.endpoint_or_interior at A, B, T with781    typedT, member782  cases status with atA | other783  . have maxA := Rolle.endpoint_maximum_left at f, A, B, T with784      endpoints, maximum, atA785    exact Rolle.of_endpoint_maximum with ordered, continuous, endpoints, maxA, differentiable786  . cases other with atB | interior787    . have maxA := Rolle.endpoint_maximum_right at f, A, B, T with788        endpoints, maximum, atB789      exact Rolle.of_endpoint_maximum with ordered, continuous, endpoints, maxA, differentiable790    . rcases interior with ⟨left, right⟩791      obtain ⟨D, realD, derivative⟩ := differentiable with792        T, realT, left, right793      have zero := HasDerivativeAt.zero_at_interval_max with left, right, derivative, maximum794      witness T795      refine ⟨realT, left, right, _⟩796      rwa ← zero797798-- Section: MeanValueIntegration799theorem MeanValue.theorem (F : Set) (A B : Real)800  requires ordered : A < B801  requires continuous : ContinuousOn(F, closedInterval(A, B))802  requires differentiable : ∀ C ∈ ℝ, A < C → C < B → ∃ D ∈ ℝ, HasDerivativeAt(F, D, C)803  shows ∃ C ∈ ℝ, A < C ∧ C < B ∧ ∃ D ∈ ℝ, HasDerivativeAt(F, D, C) ∧ D * (B - A) = F(B) - F(A)804proof805  have function : F : ℝ → ℝ806    rcases continuous with ⟨graph, subset, everywhere⟩807    exact graph808  have correctionContinuous := meanValueCorrection.continuous_on with continuous809  have endpoints := meanValueCorrection.endpoints at F, A, B with function810  have correctionDifferentiable : ∀ C ∈ ℝ, A < C → C < B →811      ∃ E ∈ ℝ, HasDerivativeAt(meanValueCorrection(F, A, B), E, C)812    intros C realC left right813    obtain ⟨D, realD, derivative⟩ := differentiable with C, realC, left, right814    have typedD : Real(D) by exact realD815    have atC := meanValueCorrection.derivative at F, A, B, C, D with derivative816    have realA : A ∈ ℝ by simp [Real]817    have realB : B ∈ ℝ by simp [Real]818    have valueA := FunctionBetween.apply_closed with function, realA819    have valueB := FunctionBetween.apply_closed with function, realB820    have typedFA : Real(F(A)) by exact valueA821    have typedFB : Real(F(B)) by exact valueB822    have widthReal := realSubValue.real at B, A with *823    have deltaReal := realSubValue.real with typedFB, typedFA824    have productReal := realMulValue.real with widthReal, typedD825    have slopeReal := realSubValue.real with productReal, deltaReal826    witness (B - A) * D - (F(B) - F(A))827    constructor828      exact slopeReal829    . exact atC830  obtain ⟨T, realT, left, right, zeroDerivative⟩ := Rolle.theorem with831    ordered, correctionContinuous, endpoints, correctionDifferentiable832  obtain ⟨E, realE, derivative⟩ := differentiable with T, realT, left, right833  have slopeDerivative := meanValueCorrection.derivative at F, A, B, T, E with derivative834  have unique := HasDerivativeAt.unique with slopeDerivative, zeroDerivative835  witness T836  have realA : A ∈ ℝ by simp [Real]837  have realB : B ∈ ℝ by simp [Real]838  have fA := FunctionBetween.apply_closed with function, realA839  have fB := FunctionBetween.apply_closed with function, realB840  have typedFA : Real(F(A)) by exact fA841  have typedFB : Real(F(B)) by exact fB842  have deltaReal := realSubValue.real with typedFB, typedFA843  have equation : E * (B - A) = F(B) - F(A)844    have transform : E * (B - A) =845        ((B - A) * E - (F(B) - F(A))) +846          (F(B) - F(A))847      ring848    rw unique at transform849    have zero := realAddValue.zero_left with deltaReal850    rwa zero at transform851  refine ⟨realT, left, right, E, realE, derivative, equation⟩852853-- A differentiable primitive provides every mean-value tag required by the854-- checked tagged-partition endpoint theorem.855856-- MeanValueIntegration857theorem CellMeanValueProperty.of_derivative (f F : Set)858  requires fFunction : f : ℝ → ℝ859  requires continuous : Continuous(F)860  requires derivative : ∀ C ∈ ℝ, HasDerivativeAt(F, f(C), C)861  shows CellMeanValueProperty(f, F)862proof863  have function := Continuous.function with continuous864  intros A realA B realB ordered865  have subset := closedInterval.subset_reals at A, B with *866  have onInterval := Continuous.continuous_on with continuous, subset867  have differentiable : ∀ C ∈ ℝ, A < C → C < B →868      ∃ D ∈ ℝ, HasDerivativeAt(F, D, C)869    intros C realC left right870    have derivativeValue := FunctionBetween.apply_closed with fFunction, realC871    have value := derivative with C, realC872    witness f(C)873    refine ⟨derivativeValue, value⟩874  obtain ⟨T, realT, left, right, D, realD, derivativeD, equation⟩ := MeanValue.theorem with875    ordered, onInterval, differentiable876  have typedT : Real(T)877    unfold Real878    exact realT879  have derivativeValue := FunctionBetween.apply_closed with fFunction, realT880  have derivativeF := derivative with T, realT881  have equal := HasDerivativeAt.unique with derivativeD, derivativeF882  have member : T ∈ closedInterval(A, B)883    have lower := realLess.implies_le with left884    have upper := realLess.implies_le with right885    have data : T ∈ ℝ ∧ A ≤ T ∧ T ≤ B by refine ⟨realT, lower, upper⟩886    exact closedInterval.membership.backward with data887  witness T888  constructor889  . exact member890  . unfold realMulValue891    unfold call2 at equation892    rwa equal at equation893894theorem HasRiemannIntegral.eq_endpoint_of_derivative (f F : Set) (A B I : Real)895  requires fFunction : f : ℝ → ℝ896  requires continuous : Continuous(F)897  requires derivative : ∀ C ∈ ℝ, HasDerivativeAt(F, f(C), C)898  requires integral : HasRiemannIntegral(f, A, B, I)899  shows I = F(B) - F(A)900proof901  have function := Continuous.function with continuous902  have meanValue := CellMeanValueProperty.of_derivative with fFunction, continuous, derivative903  exact HasRiemannIntegral.eq_endpoint_of_mean_value with function, integral, meanValue904