Grace/Cumulus/Real/Analysis/Integration/FTCFirst.g17

Open in Workbench Download source

Imports

IntegralOrderBound · IndefiniteIntegral · Differentiation · RiemannSums · CommonRefinementComparison · MeanValueIntegration · ContinuousIntegral

Declarations

Source

1-- Real analysis: FTCFirst2-- 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.Integration.FTCFirst8import IntegralOrderBound9import IndefiniteIntegral10import Differentiation11import RiemannSums12import CommonRefinementComparison13import MeanValueIntegration14import ContinuousIntegral1516-- Section: FTCFirst17theorem integralFrom.secant_right (f : Set) (A B X Y H I : Real)18  requires ordered : A ≤ B19  requires continuous : ContinuousOn(f, closedInterval(A, B))20  requires left : A < X21  requires middle : X < Y22  requires right : Y ≤ B23  requires position : Y = X + H24  requires local : HasRiemannIntegral(f, X, Y, I)25  shows differenceQuotient(integralFrom(f, A, B), X)(H) = I / (Y - X)26proof27  have function := integralFrom.function with ordered, continuous28  have value := differenceQuotient.value at integralFrom(f, A, B), X, H with function29  have realX : X ∈ ℝ by simp [Real]30  have realY : Y ∈ ℝ by simp [Real]31  have fx := FunctionBetween.apply_closed with function, realX32  have fy := FunctionBetween.apply_closed with function, realY33  have increment := integralFrom.increment_right with ordered, continuous, left, middle, right, local34  have numerator : integralFrom(f, A, B)(Y) -35      integralFrom(f, A, B)(X) = I36    rw increment37    ring38  have width : Y - X = H39    rw position40    ring41  rw [← position, numerator] at value42  rwa width4344theorem integralFrom.secant_left (f : Set) (A B X Y H I : Real)45  requires ordered : A ≤ B46  requires continuous : ContinuousOn(f, closedInterval(A, B))47  requires left : A < Y48  requires middle : Y < X49  requires right : X ≤ B50  requires position : Y = X + H51  requires local : HasRiemannIntegral(f, Y, X, I)52  shows differenceQuotient(integralFrom(f, A, B), X)(H) = I / (X - Y)53proof54  have function := integralFrom.function with ordered, continuous55  have value := differenceQuotient.value at integralFrom(f, A, B), X, H with function56  have realX : X ∈ ℝ by simp [Real]57  have realY : Y ∈ ℝ by simp [Real]58  have fx := FunctionBetween.apply_closed with function, realX59  have fy := FunctionBetween.apply_closed with function, realY60  have increment := integralFrom.increment_left with ordered, continuous, left, middle, right, local61  have numerator : integralFrom(f, A, B)(Y) -62      integralFrom(f, A, B)(X) = -I63    rw increment64    ring65  have width : H = -(X - Y)66    rw position67    ring68  have positive := realLess.implies_le with middle69  have widthPositive : 0 < X - Y by linarith70  have widthNonzero : X - Y ≠ realZero71    intro equal72    have strict := realLess.characterization.forward with widthPositive73    rw equal at strict74    exact RealLess.irreflexive with strict75  have negBoth := realDiv.neg_both at I, X - Y with widthNonzero76  rw [← position, numerator, width, negBoth] at value77  rwa width7879-- A negative step H with X + H still inside [A, B] and -H below the local80-- control radius: the secant of the integral function over [X + H, X] is an81-- average of f within E of f(X).82theorem integralFrom.secant_bounds_left (f : Set) (A B X E D H : Real)83  requires continuous : ContinuousOn(f, closedInterval(A, B))84  requires inside : X ∈ closedInterval(A, B)85  requires ordered : A ≤ B86  requires right : X ≤ B87  requires control : ∀ Z ∈ closedInterval(A, B), dist(X, Z) < D →88    f(X) - E < (f(Z):R) ∧ (f(Z):R) < f(X) + E89  requires negative : H < 090  requires above : A < X + H91  requires small : -H < D92  shows f(X) - E ≤ differenceQuotient(integralFrom(f, A, B), X)(H) ∧93    differenceQuotient(integralFrom(f, A, B), X)(H) ≤ f(X) + E94proof95  have below : X + H < X by linarith96  have aLeY := realLess.implies_le with above97  have width : X - (X + H) < D by linarith98  have restricted := ContinuousOn.subinterval with continuous, aLeY, right99  obtain ⟨J, realJ, integral⟩ := ContinuousOn.integrable_positive with below, restricted100  have average := ContinuousOn.left_integral_average with101    continuous, inside, control, below, aLeY, width, integral102  have position : X + H = X + H by rfl103  have secant := integralFrom.secant_left with ordered, continuous, above, below, right, position, integral104  rwa ← secant at average105106-- The mirror image for a positive step.107theorem integralFrom.secant_bounds_right (f : Set) (A B X E D H : Real)108  requires continuous : ContinuousOn(f, closedInterval(A, B))109  requires inside : X ∈ closedInterval(A, B)110  requires ordered : A ≤ B111  requires left : A < X112  requires control : ∀ Z ∈ closedInterval(A, B), dist(X, Z) < D →113    f(X) - E < (f(Z):R) ∧ (f(Z):R) < f(X) + E114  requires positive : 0 < H115  requires below : X + H < B116  requires small : H < D117  shows f(X) - E ≤ differenceQuotient(integralFrom(f, A, B), X)(H) ∧118    differenceQuotient(integralFrom(f, A, B), X)(H) ≤ f(X) + E119proof120  have weakLeft := realLess.implies_le with left121  have above : X < X + H by linarith122  have yLeB := realLess.implies_le with below123  have width : (X + H) - X < D by linarith124  have restricted := ContinuousOn.subinterval with continuous, weakLeft, yLeB125  obtain ⟨K, realK, integral⟩ := ContinuousOn.integrable_positive with above, restricted126  have average := ContinuousOn.right_integral_average with127    continuous, inside, control, above, yLeB, width, integral128  have position : X + H = X + H by rfl129  have secant := integralFrom.secant_right with ordered, continuous, left, above, yLeB, position, integral130  rwa ← secant at average131132-- FTCFirst: the integral function of a continuous integrand has derivative133-- f(X) at every interior point. Given E, continuity controls f within E/2 on134-- a radius D around X; for steps H shorter than D and the distances to the135-- endpoints, the secant is an average of f on that stretch, so it lies within136-- E/2 of f(X).137theorem FTC.derivative_of_integral (f : Set) (A B X : Real)138  requires continuous : ContinuousOn(f, closedInterval(A, B))139  requires left : A < X140  requires right : X < B141  shows HasDerivativeAt(integralFrom(f, A, B), f(X), X)142proof143  have ordered := realLess.transitive with left, right144  have weakOrdered := realLess.implies_le with ordered145  have weakLeft := realLess.implies_le with left146  have weakRight := realLess.implies_le with right147  have realX : X ∈ ℝ by typecheck148  have inside : X ∈ closedInterval(A, B)149    have data : X ∈ ℝ ∧ A ≤ X ∧ X ≤ B by refine ⟨realX, weakLeft, weakRight⟩150    exact closedInterval.membership.backward with data151  have function := integralFrom.function with weakOrdered, continuous152  have functionF : f : ℝ → ℝ153    rcases continuous with ⟨function, subset, points⟩154    exact function155  have valueFX := FunctionBetween.apply_closed with functionF156  constructor157  . exact function158    constructor159    . exact differenceQuotient.function with function160    . intros E realE positiveE161      have halfPositive := half.positive with positiveE162      obtain ⟨D, realD, positiveD, control⟩ := ContinuousOn.local_image_bounds with163        continuous, inside, halfPositive164      have positiveLeft : 0 < X - A by linarith165      have positiveRight : 0 < B - X by linarith166      obtain ⟨R, realR, positiveR, rD, rLeft, rRight⟩ := positiveMesh.common_three with167        positiveD, positiveLeft, positiveRight168      witness R169      constructor170      . exact realR171      . constructor172        . exact positiveR173        . intros H realH nonzero near174          have typedH : Real(H)175            unfold Real176            exact realH177          obtain ⟨lowerH, upperH⟩ := openBall.order_characterization.forward with near178          have bounds : f(X) - half(E) ≤ differenceQuotient(integralFrom(f, A, B), X)(H) ∧179              differenceQuotient(integralFrom(f, A, B), X)(H) ≤ f(X) + half(E)180            have sign := realLess.trichotomy at H, realZero with *181            rcases sign with negative | zero | positive182            . have above : A < X + H183                linarith184              have small : -H < D by linarith185              exact integralFrom.secant_bounds_left with186                continuous, inside, weakOrdered, weakRight, control, negative, above, small187            . exfalso188              exact nonzero with zero189            . have below : X + H < B190                linarith191              have small : H < D by linarith192              exact integralFrom.secant_bounds_right with193                continuous, inside, weakOrdered, left, control, positive, below, small194          rcases bounds with ⟨low, high⟩195          exact openBall.of_half_bounds with positiveE, low, high196197-- Section: FTCContinuousDerivative198theorem CellMeanValueWitnesses.of_local_derivative (f F p : Set) (A B : Real, N : Nat)199  requires functionf : f : ℝ → ℝ200  requires continuousF : ContinuousOn(F, closedInterval(A, B))201  requires derivative : ∀ X ∈ ℝ, A < X → X < B →202    HasDerivativeAt(F, f(X), X)203  requires partition : IntervalPartition(p, A, B, N)204  shows CellMeanValueWitnesses(f, F, p, N)205proof206  intros i naturalI before207  have typedI := nat.omega.backward with naturalI208  have points : RealSequence(p)209    rcases partition with ⟨points, start, finish, steps⟩210    exact points211  have pointI := RealSequence.value at p, i with points212  have pointNext := RealSequence.value at p, succ(i) with points213  have increasing := IntervalPartition.cell with partition, before214  have onCell := ContinuousOn.partition_cell with continuousF, partition, before215  have indexLe := Less.implies_LessEqual with before216  have successorLe : succ(i) ≤ N by exact before217  have globalBounds := IntervalPartition.point_bounds with partition, indexLe218  have nextBounds := IntervalPartition.point_bounds with partition, successorLe219  have differentiable : ∀ C ∈ ℝ, (p[i]:R) < C → C < (p[succ(i)]:R) →220      ∃ D ∈ ℝ, HasDerivativeAt(F, D, C)221    intros C realC left right222    rcases globalBounds with ⟨low, high⟩223    rcases nextBounds with ⟨lowNext, highNext⟩224    have fromA : A < C by linarith225    have toB : C < B by linarith226    have derivativeAt := derivative with C, realC, fromA, toB227    have value := FunctionBetween.apply_closed with functionf, realC228    witness f(C)229    refine ⟨value, derivativeAt⟩230  obtain ⟨T, realT, left, right, D, realD, derivativeD, equation⟩ := MeanValue.theorem with231    increasing, onCell, differentiable232  have derivativeT : HasDerivativeAt(F, f(T), T)233    have boundsI := IntervalPartition.point_bounds with partition, indexLe234    have boundsNext := IntervalPartition.point_bounds with partition, successorLe235    rcases boundsI with ⟨low, high⟩236    rcases boundsNext with ⟨lowNext, highNext⟩237    have fromA : A < T by linarith238    have toB : T < B by linarith239    exact derivative with T, realT, fromA, toB240  have equal := HasDerivativeAt.unique with derivativeD, derivativeT241  have inCell : T ∈ closedInterval(p[i], p[succ(i)])242    have low := realLess.implies_le with left243    have high := realLess.implies_le with right244    have data : T ∈ ℝ ∧ p[i] ≤ T ∧ T ≤ p[succ(i)] by refine ⟨realT, low, high⟩245    exact closedInterval.membership.backward with data246  witness T247  constructor248  . exact inCell249  . unfold realMulValue250    unfold call2 at equation251    rwa equal at equation252253-- FTCContinuousDerivative254theorem FTC.continuous_derivative (f : ℝ → ℝ) (F : Set) (A B : Real)255  requires ordered : A ≤ B256  requires continuousF : ContinuousOn(F, closedInterval(A, B))257  requires derivative : ∀ X ∈ ℝ, A < X → X < B →258    HasDerivativeAt(F, f(X), X)259  requires continuousf : ContinuousOn(f, closedInterval(A, B))260  shows HasRiemannIntegral(f, A, B, F(B) - F(A))261proof262  have functionf : f : ℝ → ℝ by assumption263  have functionF : F : ℝ → ℝ264    rcases continuousF with ⟨function, subset, points⟩265    exact function266  have realA : A ∈ ℝ by simp [Real]267  have realB : B ∈ ℝ by simp [Real]268  have valueA := FunctionBetween.apply_closed with functionF, realA269  have valueB := FunctionBetween.apply_closed with functionF, realB270  constructor271  . exact functionf272  . constructor273    . exact ordered274    . intros E realE positiveE275      have widthReal := realSubValue.real at B, A with *276      have scalePositive := limitScale.positive with widthReal277      have etaPositive := scaledRadius.positive with positiveE, scalePositive278      obtain ⟨D, realD, positiveD, oscillation⟩ := ContinuousOn.fine_cell_oscillation with279        continuousf, etaPositive280      witness D281      constructor282      . exact realD283      . constructor284        . exact positiveD285        . intros p t N naturalN tagged fine286          have typedN := nat.omega.backward with naturalN287          have partition : IntervalPartition(p, A, B, N)288            rcases tagged with ⟨partition, tags, cells⟩289            exact partition290          have witnesses := CellMeanValueWitnesses.of_local_derivative with291            functionf, continuousF, derivative, partition292          obtain ⟨special, equations⟩ := CellMeanValueWitnesses.tags with partition, witnesses293          have exactSum := TaggedPartition.riemann_sum_of_cell_increments with294            functionF, functionf, special, equations295          have bounds := FineCellOscillation.tagged_sum_bounds with296            functionf, oscillation, fine, tagged, special297          rw exactSum at bounds298          rcases bounds with ⟨upper, lower⟩299          have small := scaledRadius.interval_error with ordered, positiveE300          have tags : RealSequence(t)301            rcases tagged with ⟨partitionAgain, tags, cells⟩302            exact tags303          have points : RealSequence(p)304            rcases partition with ⟨points, start, finish, steps⟩305            exact points306          exact dist.lt_of_two_sided_error with upper, lower, small307308-- FTCIntegrableDerivative309theorem RiemannIntegrable.continuous_derivative (f F : Set) (A B : Real)310  requires ordered : A ≤ B311  requires functionf : f : ℝ → ℝ312  requires continuousF : ContinuousOn(F, closedInterval(A, B))313  requires derivative : ∀ X ∈ ℝ, A < X → X < B →314    HasDerivativeAt(F, f(X), X)315  requires continuousf : ContinuousOn(f, closedInterval(A, B))316  shows RiemannIntegrable(f, A, B)317proof318  have functionF : F : ℝ → ℝ319    rcases continuousF with ⟨function, subset, points⟩320    exact function321  have realA : A ∈ ℝ by simp [Real]322  have realB : B ∈ ℝ by simp [Real]323  have valueA := FunctionBetween.apply_closed with functionF, realA324  have valueB := FunctionBetween.apply_closed with functionF, realB325  have typedFA : Real(F(A)) by exact valueA326  have typedFB : Real(F(B)) by exact valueB327  have endpointReal := realSubValue.real with typedFB, typedFA328  witness F(B) - F(A)329  constructor330    exact endpointReal331  . exact FTC.continuous_derivative at f, F, A, B with332      ordered, continuousF, derivative, continuousf333334-- LocalDerivativeEndpoint335theorem HasRiemannIntegral.eq_endpoint_of_local_derivative (f F : Set) (A B I : Real)336  requires continuousF : ContinuousOn(F, closedInterval(A, B))337  requires derivative : ∀ X ∈ ℝ, A < X → X < B →338    HasDerivativeAt(F, f(X), X)339  requires integral : HasRiemannIntegral(f, A, B, I)340  shows I = F(B) - F(A)341proof342  have functionf : f : ℝ → ℝ343    rcases integral with ⟨function, ordered, estimates⟩344    exact function345  have functionF : F : ℝ → ℝ346    rcases continuousF with ⟨function, subset, points⟩347    exact function348  have local : ∀ p, ∀ N ∈ ℕ,349      IntervalPartition(p, A, B, N) → CellMeanValueWitnesses(f, F, p, N)350    intros p N naturalN partition351    have typedN := nat.omega.backward with naturalN352    exact CellMeanValueWitnesses.of_local_derivative with functionf, continuousF, derivative, partition353  have tags := CellMeanValueWitnesses.all_tags with local354  exact HasRiemannIntegral.eq_endpoint_of_cell_tags with functionF, integral, tags355356-- Section: FundamentalTheorem357theorem FTC.identity_case (A B : Real)358  requires ordered : A ≤ B359  shows (∀ X ∈ ℝ, HasDerivativeAt(identity(ℝ), realOne, X)) ∧360    HasRiemannIntegral(constantRealFunction(realOne), A, B,361      identity(ℝ)(B) - identity(ℝ)(A))362proof363  constructor364  . intros X realX365    have typedX : Real(X) by exact realX366    exact identity.has_derivative_at with typedX367  . have integral := HasRiemannIntegral.constant at A, B, realOne with ordered368    have realA : A ∈ ℝ by simp [Real]369    have realB : B ∈ ℝ by simp [Real]370    have atA := identity.apply with realA371    have atB := identity.apply with realB372    have value : realOne * (B - A) =373        identity(ℝ)(B) - identity(ℝ)(A)374      rw [atA, atB]375      ring376    rw value at integral377    simpa [constantRealFunction] using integral378379-- The constant function's derivative is zero, and the integral of zero is380-- its endpoint change.381theorem FTC.constant_case (A B C : Real)382  requires ordered : A ≤ B383  shows (∀ X ∈ ℝ, HasDerivativeAt(constantRealFunction(C), realZero, X)) ∧384    HasRiemannIntegral(constantRealFunction(realZero), A, B,385      constantRealFunction(C)(B) - constantRealFunction(C)(A))386proof387  constructor388  . intros X realX389    have typedX : Real(X) by exact realX390    exact constantRealFunction.has_derivative_at with assumption, typedX391  . have integral := HasRiemannIntegral.constant at A, B, realZero with ordered392    have valueA := constantRealFunction.value at C, A with *393    have valueB := constantRealFunction.value at C, B with *394    have value : realZero * (B - A) =395        constantRealFunction(C)(B) - constantRealFunction(C)(A)396      rw [valueA, valueB]397      ring398    rw value at integral399    simpa [constantRealFunction] using integral400401-- Translating x by C leaves its derivative and endpoint change unchanged.402theorem FTC.translation_case (A B C : Real)403  requires ordered : A ≤ B404  shows (∀ X ∈ ℝ, HasDerivativeAt(translateBy(C), realOne, X)) ∧405    HasRiemannIntegral(constantRealFunction(realOne), A, B,406      translateBy(C)(B) - translateBy(C)(A))407proof408  constructor409  . intros X realX410    have typedX : Real(X) by exact realX411    have constant := constantRealFunction.has_derivative_at at C, X with412      assumption, typedX413    have identityDerivative := identity.has_derivative_at with typedX414    have sum := HasDerivativeAt.add with realZero.real, realOne.real, constant, identityDerivative415    have normalized : realZero + realOne = realOne by ring416    rw normalized at sum417    simpa [translateBy] using sum418  . have integral := HasRiemannIntegral.constant at A, B, realOne with ordered419    have atA := translateBy.value at C, A with *420    have atB := translateBy.value at C, B with *421    have value : realOne * (B - A) =422        translateBy(C)(B) - translateBy(C)(A)423      rw [atA, atB]424      ring425    rw value at integral426    simpa [constantRealFunction] using integral427428-- Section: FTCExamples429theorem FTC.identity_integrand (A B X : Real)430  requires left : A < X431  requires right : X < B432  shows HasDerivativeAt(integralFrom(identity(ℝ), A, B), X, X)433proof434  have continuous := closedInterval.identity_continuous at A, B with435    *{2}436  have derivative := FTC.derivative_of_integral with continuous, left, right437  have realX : X ∈ ℝ by simp [Real]438  have value := identity.apply with realX439  rwa value at derivative440441-- FTC-2: the integral of one is the endpoint change of the identity.442-- The result is an equality of real values; the earlier statements are443-- relations.444theorem FTC.integral_one (A B : Real)445  requires ordered : A ≤ B446  shows riemannIntegral(constantRealFunction(realOne), A, B) = B - A447proof448  have identityContinuous := closedInterval.identity_continuous at A, B with449    *{2}450  have constantContinuous := constantRealFunction.continuous with realOne.real451  have subset := closedInterval.subset_reals at A, B with *452  have onInterval := Continuous.continuous_on with constantContinuous, subset453  have function := Continuous.function with constantContinuous454  have derivative : ∀ X ∈ ℝ, A < X → X < B →455      HasDerivativeAt(identity(ℝ), constantRealFunction(realOne)(X), X)456    intros X realX left right457    have typedX : Real(X) by exact realX458    have atX := identity.has_derivative_at with typedX459    have value := constantRealFunction.value with realOne.real, typedX460    rwa ← value at atX461  have integral := FTC.continuous_derivative with462    ordered, identityContinuous, derivative, onInterval463  have realA : A ∈ ℝ by simp [Real]464  have realB : B ∈ ℝ by simp [Real]465  have valueA := identity.apply with realA466  have valueB := identity.apply with realB467  rw [valueA, valueB] at integral468  exact riemannIntegral.eq_of_integral with integral469470-- The value form of FTC-2 is the interface most applications need.471theorem riemannIntegral.of_continuous_derivative (f F : Set) (A B : Real)472  requires ordered : A ≤ B473  requires functionf : f : ℝ → ℝ474  requires continuousF : ContinuousOn(F, closedInterval(A, B))475  requires derivative : ∀ X ∈ ℝ, A < X → X < B →476    HasDerivativeAt(F, f(X), X)477  requires continuousf : ContinuousOn(f, closedInterval(A, B))478  shows riemannIntegral(f, A, B) = F(B) - F(A)479proof480  have integral := FTC.continuous_derivative with481    ordered, continuousF, derivative, continuousf482  have functionF : F : ℝ → ℝ483    rcases continuousF with ⟨function, subset, points⟩484    exact function485  have realA : A ∈ ℝ by simp [Real]486  have realB : B ∈ ℝ by simp [Real]487  have valueA := FunctionBetween.apply_closed with functionF, realA488  have valueB := FunctionBetween.apply_closed with functionF, realB489  exact riemannIntegral.eq_of_integral with integral490491-- The constant case can be used without opening the Riemann-sum layer.492theorem riemannIntegral.constant (A B L : Real)493  requires ordered : A ≤ B494  shows riemannIntegral(constantRealFunction(L), A, B) = L * (B - A)495proof496  have integral := HasRiemannIntegral.constant at A, B, L with ordered497  have normalized : HasRiemannIntegral(constantRealFunction(L), A, B, L * (B - A))498    simpa [constantRealFunction] using integral499  exact riemannIntegral.eq_of_integral with normalized500