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

Open in Workbench Download source

Imports

Set.Choice · RiemannSums · CommonRefinementComparison · Squares

Declarations

Source

1-- Real analysis: IntegralOrderBound2-- 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.IntegralOrderBound8import Set.Choice9import RiemannSums10import CommonRefinementComparison11import Squares1213-- Section: IntegralOrderBound14theorem Nat.not_less_zero (i : Nat)15  shows ¬(i < 0)16proof17  intro before18  have weak := Grace.Core.Nat.Order.LessEqual.zero at i19  have typedZero : Nat(0) by typecheck20  have cycle := Less.transitive_LessEqual at i, 0, i with21    assumption, typedZero, assumption, before, weak22  have impossible := Less.irreflexive at i23  exact impossible with cycle2425-- A singleton interval has the empty tagged partition at every mesh size.26theorem FineTaggedPartitionsExist.point (A : Real)27  shows FineTaggedPartitionsExist(A, A)28proof29  intros D realD positive30  have sequence := constantSequence.sequence at A31  have atZero := constantSequence.value at A, 0 with *32  have partition : IntervalPartition(constantSequence(A), A, A, 0)33    constructor34    . exact sequence35    . constructor36      . exact atZero37      . constructor38        . exact atZero39        . intros i naturalI before40          exfalso41          have typedI := nat.omega.backward with naturalI42          have impossible := Nat.not_less_zero with typedI43          exact impossible with before44  have tagged : TaggedPartition(constantSequence(A), constantSequence(A), A, A, 0)45    constructor46    . exact partition47    . constructor48      . exact sequence49      . intros i naturalI before50        exfalso51        have typedI := nat.omega.backward with naturalI52        have impossible := Nat.not_less_zero with typedI53        exact impossible with before54  have fine : FinePartition(constantSequence(A), A, A, 0, D)55    constructor56    . exact partition57    . constructor58      . exact positive59      . intros i naturalI before60        exfalso61        have typedI := nat.omega.backward with naturalI62        have impossible := Nat.not_less_zero with typedI63        exact impossible with before64  witness constantSequence(A)65  witness constantSequence(A)66  witness 067  constructor68  . exact nat.omega.forward at 0 with Naturals.constructor.zero69  . refine ⟨tagged, fine⟩7071-- IntegralUniqueness72theorem HasRiemannIntegral.unique (f : Set) (A B I J : Real)73  requires cofinal : FineTaggedPartitionsExist(A, B)74  requires first : HasRiemannIntegral(f, A, B, I)75  requires second : HasRiemannIntegral(f, A, B, J)76  shows I = J77proof78  by_contra unequal79  have distanceReal := dist.real at I, J with *80  have radiusReal := half.real with distanceReal81  have distancePositive := dist.positive_of_ne with unequal82  have radiusPositive := half.positive with distancePositive83  rcases first with ⟨function, ordered, controlI⟩84  rcases second with ⟨functionJ, orderedJ, controlJ⟩85  obtain ⟨D, realD, positiveD, estimateI⟩ :=86    controlI with half(dist(I, J)), radiusPositive87  obtain ⟨E, realE, positiveE, estimateJ⟩ :=88    controlJ with half(dist(I, J)), radiusPositive89  obtain ⟨p, t, N, naturalN, tagged, fineD, fineE⟩ := FineTaggedPartitionsExist.common with90    cofinal, positiveD, positiveE91  have nearI := estimateI with p, t, N, naturalN, tagged, fineD92  have nearJ := estimateJ with p, t, N, naturalN, tagged, fineE93  have typedN := nat.omega.backward with naturalN94  have points : RealSequence(p)95    rcases tagged with ⟨partition, tags, cells⟩96    rcases partition with ⟨sequence, left, right, increasing⟩97    exact sequence98  have tags : RealSequence(t)99    rcases tagged with ⟨partition, sequence, cells⟩100    exact sequence101  have sumReal := riemannSum.real with function, points, tags102  have sumMember : riemannSum(f, p, t, N) ∈ ℝ by exact sumReal103  have ballI : riemannSum(f, p, t, N) ∈ openBall(I, half(dist(I, J)))104    apply openBall.membership.backward105    refine ⟨sumMember, nearI⟩106  have ballJ : riemannSum(f, p, t, N) ∈ openBall(J, half(dist(I, J)))107    apply openBall.membership.backward108    refine ⟨sumMember, nearJ⟩109  have equal := openBall.half_radius_unique with ballI, ballJ110  exact unequal with equal111112theorem HasRiemannIntegral.unique_point (f : Set) (A I J : Real)113  requires first : HasRiemannIntegral(f, A, A, I)114  requires second : HasRiemannIntegral(f, A, A, J)115  shows I = J116proof117  exact HasRiemannIntegral.unique at f, A, A, I, J with118    FineTaggedPartitionsExist.point at A with assumption, first, second119120-- PointIntegral121theorem HasRiemannIntegral.point (f : Set) (A : Real)122  requires function : f : ℝ → ℝ123  shows HasRiemannIntegral(f, A, A, (0:R))124proof125  constructor126  . exact function127  . constructor128    . exact realLe.reflexive at A129    . intros E realE positiveE130      witness E131      constructor132      . exact realE133      . constructor134        . exact positiveE135        . intros p t N naturalN tagged fine136          have typedN := nat.omega.backward with naturalN137          rcases tagged with ⟨partition, tags, cells⟩138          have empty := IntervalPartition.point_empty with partition139          rw [empty, riemannSum.zero]140          have same := dist.self with realZero.real141          rwa same142143theorem RiemannIntegrable.point (f : Set) (A : Real)144  requires function : f : ℝ → ℝ145  shows RiemannIntegrable(f, A, A)146proof147  witness realZero148  constructor149  . exact realZero.real150  . exact HasRiemannIntegral.point at f, A with function151152-- PositiveIntegralUniqueness153theorem FineTaggedPartitionsExist.ordered_interval (A B : Real)154  requires ordered : A ≤ B155  shows FineTaggedPartitionsExist(A, B)156proof157  have alternatives : A = B ∨ ¬(A = B) by tauto158  cases alternatives with equal | unequal159  . rw ← equal160    exact FineTaggedPartitionsExist.point with assumption161  . have le := realLe.characterization.forward with ordered162    rcases le with ⟨realA, realB, subset⟩163    have proper : A ⊂ B by refine ⟨subset, unequal⟩164    have strict : A < B := realLess.characterization.backward with ⟨realA, realB, proper⟩165    exact FineTaggedPartitionsExist.positive_interval with strict166167theorem HasRiemannIntegral.unique_positive (f : Set) (A B I J : Real)168  requires ordered : A < B169  requires first : HasRiemannIntegral(f, A, B, I)170  requires second : HasRiemannIntegral(f, A, B, J)171  shows I = J172proof173  have cofinal := FineTaggedPartitionsExist.positive_interval with ordered174  exact HasRiemannIntegral.unique with cofinal, first, second175176theorem HasRiemannIntegral.unique_on_interval (f : Set) (A B I J : Real)177  requires ordered : A ≤ B178  requires first : HasRiemannIntegral(f, A, B, I)179  requires second : HasRiemannIntegral(f, A, B, J)180  shows I = J181proof182  have cofinal := FineTaggedPartitionsExist.ordered_interval with ordered183  exact HasRiemannIntegral.unique with cofinal, first, second184185-- IntegralOrderBound186theorem HasRiemannIntegral.upper_bound (f : Set) (A B I U : Real)187  requires cofinal : FineTaggedPartitionsExist(A, B)188  requires integral : HasRiemannIntegral(f, A, B, I)189  requires bounds : ∀ p, ∀ t, ∀ N ∈ ℕ,190    TaggedPartition(p, t, A, B, N) → (riemannSum(f, p, t, N):R) ≤ U191  shows I ≤ U192proof193  by_contra notLe194  have strict := realLess.of_not_le with notLe195  have positiveDifference : 0 < I - U by linarith196  rcases integral with ⟨function, ordered, control⟩197  obtain ⟨D, realD, positiveD, estimate⟩ :=198    control with I - U, positiveDifference199  obtain ⟨p, t, N, naturalN, tagged, fine⟩ := cofinal with D, realD, positiveD200  have typedN := nat.omega.backward with naturalN201  have close := estimate with p, t, N, naturalN, tagged, fine202  have upper := bounds with p, t, N, naturalN, tagged203  have points : RealSequence(p)204    rcases tagged with ⟨partition, tags, cells⟩205    rcases partition with ⟨points, start, finish, increasing⟩206    exact points207  have tags : RealSequence(t)208    rcases tagged with ⟨partition, tags, cells⟩209    exact tags210  have sumReal := riemannSum.real with function, points, tags211  have data : riemannSum(f, p, t, N) ∈ ℝ ∧ dist(riemannSum(f, p, t, N), I) < I - U by refine ⟨sumReal, close⟩212  have ball := openBall.membership.backward at I, I - U, riemannSum(f, p, t, N)213    with data214  obtain ⟨lower, upperBall⟩ := openBall.order_characterization.forward with ball215  have cancel : I - (I - U) = U by ring216  rw cancel at lower217  have impossible : U < riemannSum(f, p, t, N) by exact lower218  have cycle := realLe.transitive_less with upper, impossible219  have contradiction := realLess.characterization.forward with cycle220  exact RealLess.irreflexive with contradiction221222theorem HasRiemannIntegral.lower_bound (f : Set) (A B I L : Real)223  requires cofinal : FineTaggedPartitionsExist(A, B)224  requires integral : HasRiemannIntegral(f, A, B, I)225  requires bounds : ∀ p, ∀ t, ∀ N ∈ ℕ,226    TaggedPartition(p, t, A, B, N) → L ≤ (riemannSum(f, p, t, N):R)227  shows L ≤ I228proof229  by_contra notLe230  have strict := realLess.of_not_le with notLe231  have positiveDifference : 0 < L - I by linarith232  rcases integral with ⟨function, ordered, control⟩233  obtain ⟨D, realD, positiveD, estimate⟩ :=234    control with L - I, positiveDifference235  obtain ⟨p, t, N, naturalN, tagged, fine⟩ := cofinal with D, realD, positiveD236  have typedN := nat.omega.backward with naturalN237  have close := estimate with p, t, N, naturalN, tagged, fine238  have lower := bounds with p, t, N, naturalN, tagged239  have points : RealSequence(p)240    rcases tagged with ⟨partition, tags, cells⟩241    rcases partition with ⟨points, start, finish, increasing⟩242    exact points243  have tags : RealSequence(t)244    rcases tagged with ⟨partition, tags, cells⟩245    exact tags246  have sumReal := riemannSum.real with function, points, tags247  have data : riemannSum(f, p, t, N) ∈ ℝ ∧ dist(riemannSum(f, p, t, N), I) < L - I by refine ⟨sumReal, close⟩248  have ball := openBall.membership.backward at I, L - I, riemannSum(f, p, t, N)249    with data250  obtain ⟨lowerBall, upperBall⟩ := openBall.order_characterization.forward with ball251  have cancel : I + (L - I) = L by ring252  rw cancel at upperBall253  have cycle := realLe.transitive_less with lower, upperBall254  have contradiction := realLess.characterization.forward with cycle255  exact RealLess.irreflexive with contradiction256257theorem HasRiemannIntegral.between_constants (f : Set) (A B I L U : Real)258  requires ordered : A < B259  requires integral : HasRiemannIntegral(f, A, B, I)260  requires lower : ∀ X ∈ closedInterval(A, B), L ≤ (f(X):R)261  requires upper : ∀ X ∈ closedInterval(A, B), (f(X):R) ≤ U262  shows L * (B - A) ≤ I ∧ I ≤ U * (B - A)263proof264  have function : f : ℝ → ℝ265    rcases integral with ⟨function, ordered, estimates⟩266    exact function267  have cofinal := FineTaggedPartitionsExist.positive_interval with ordered268  have lowerSums : ∀ p, ∀ t, ∀ N ∈ ℕ,269      TaggedPartition(p, t, A, B, N) → L * (B - A) ≤ (riemannSum(f, p, t, N):R)270    intros p t N naturalN tagged271    have typedN := nat.omega.backward with naturalN272    have partition : IntervalPartition(p, A, B, N)273      rcases tagged with ⟨partition, tags, cells⟩274      exact partition275    have lowerTags : ∀ i ∈ ℕ, i < N → L ≤ (f(t[i]):R)276      intros i naturalI before277      have typedI := nat.omega.backward with naturalI278      have cell := TaggedPartition.cell with tagged, before279      have subset := IntervalPartition.cell_subset with partition, before280      have global := subset with t[i], cell281      exact lower with t[i], global282    have upperTags : ∀ i ∈ ℕ, i < N → (f(t[i]):R) ≤ U283      intros i naturalI before284      have typedI := nat.omega.backward with naturalI285      have cell := TaggedPartition.cell with tagged, before286      have subset := IntervalPartition.cell_subset with partition, before287      have global := subset with t[i], cell288      exact upper with t[i], global289    obtain ⟨low, high⟩ := riemannSum.between_constants with function, tagged, lowerTags, upperTags290    exact low291  have upperSums : ∀ p, ∀ t, ∀ N ∈ ℕ,292      TaggedPartition(p, t, A, B, N) → (riemannSum(f, p, t, N):R) ≤ U * (B - A)293    intros p t N naturalN tagged294    have typedN := nat.omega.backward with naturalN295    have partition : IntervalPartition(p, A, B, N)296      rcases tagged with ⟨partition, tags, cells⟩297      exact partition298    have lowerTags : ∀ i ∈ ℕ, i < N → L ≤ (f(t[i]):R)299      intros i naturalI before300      have typedI := nat.omega.backward with naturalI301      have cell := TaggedPartition.cell with tagged, before302      have subset := IntervalPartition.cell_subset with partition, before303      have global := subset with t[i], cell304      exact lower with t[i], global305    have upperTags : ∀ i ∈ ℕ, i < N → (f(t[i]):R) ≤ U306      intros i naturalI before307      have typedI := nat.omega.backward with naturalI308      have cell := TaggedPartition.cell with tagged, before309      have subset := IntervalPartition.cell_subset with partition, before310      have global := subset with t[i], cell311      exact upper with t[i], global312    obtain ⟨low, high⟩ := riemannSum.between_constants with function, tagged, lowerTags, upperTags313    exact high314  have low := HasRiemannIntegral.lower_bound with cofinal, integral, lowerSums315  have high := HasRiemannIntegral.upper_bound with cofinal, integral, upperSums316  refine ⟨low, high⟩317318-- Section: LocalIntegralBounds319theorem realLe.divide_positive (A B C : Real)320  requires bound : A ≤ B321  requires positive : 0 < C322  shows A / C ≤ B / C323proof324  have inverseReal := realInvValue.real at C325  have inversePositive := realInvValue.positive with positive326  have nonnegative := realLess.implies_le with realZero.real, inversePositive327  have scaled := realLe.mul_right_of_nonnegative at A, B, realInvValue(C) with328    *{2}, inverseReal, bound, nonnegative329  have leftShape := realDiv.eq_mul_inv at A, C with *330  have rightShape := realDiv.eq_mul_inv at B, C with *331  rwa [← leftShape, ← rightShape] at scaled332333theorem realDiv.neg_both (A B : Real)334  requires nonzero : B ≠ realZero335  shows (-A) / (-B) = A / B336proof337  have negAReal := realNegValue.real at A338  have negBReal := realNegValue.real at B339  have negNonzero : -B ≠ realZero340    intro equal341    have involutive := realNegValue.involutive at B342    rw [equal, realNegValue.zero] at involutive343    apply nonzero344    cc345  have inverseLaw := realInvValue.mul_right with nonzero346  have negLaw : (-B) * (-realInvValue(B)) = 1347    have shape : (-B) * (-realInvValue(B)) = B * realInvValue(B) by ring348    rwa shape349  have negInverse := realInvValue.eq_of_mul_right with negNonzero, negLaw350  have leftShape := realDiv.eq_mul_inv with negAReal, negBReal351  have rightShape := realDiv.eq_mul_inv at A, B with *352  rw [leftShape, rightShape, ← negInverse]353  ring354355-- LocalIntegralBounds356theorem ContinuousOn.local_image_bounds (f : Set) (A B X E : Real)357  requires continuous : ContinuousOn(f, closedInterval(A, B))358  requires inside : X ∈ closedInterval(A, B)359  requires positive : 0 < E360  shows ∃ D ∈ ℝ, 0 < D ∧361    (∀ Z ∈ closedInterval(A, B), dist(X, Z) < D →362      f(X) - E < (f(Z):R) ∧363        (f(Z):R) < f(X) + E)364proof365  rcases continuous with ⟨function, subset, atPoints⟩366  obtain ⟨functionX, subsetX, control⟩ := atPoints with X, inside367  obtain ⟨D, realD, positiveD, maps⟩ := control with E, positive368  witness D369  constructor370  . exact realD371  . constructor372    . exact positiveD373    . intros Z member near374      have realZ : Z ∈ ℝ375        obtain ⟨realZ, lower, upper⟩ := closedInterval.membership.forward with member376        exact realZ377      have realX : X ∈ ℝ378        obtain ⟨realX, lower, upper⟩ := closedInterval.membership.forward with inside379        exact realX380      have symmetry := dist.symmetric at X, Z with *381      rw symmetry at near382      have data : Z ∈ ℝ ∧ dist(Z, X) < D by refine ⟨realZ, near⟩383      have inputBall := openBall.membership.backward with data384      have outputBall := maps with Z, member, inputBall385      exact openBall.order_characterization.forward with outputBall386387theorem ContinuousOn.right_integral_bounds (f : Set) (A B X E D Y I : Real)388  requires continuous : ContinuousOn(f, closedInterval(A, B))389  requires inside : X ∈ closedInterval(A, B)390  requires control : ∀ Z ∈ closedInterval(A, B), dist(X, Z) < D →391    f(X) - E < (f(Z):R) ∧392      (f(Z):R) < f(X) + E393  requires ordered : X < Y394  requires right : Y ≤ B395  requires small : Y - X < D396  requires integral : HasRiemannIntegral(f, X, Y, I)397  shows (f(X) - E) * (Y - X) ≤ I ∧398    I ≤ (f(X) + E) * (Y - X)399proof400  obtain ⟨realX, leftBound, rightBound⟩ := closedInterval.membership.forward with inside401  have function : f : ℝ → ℝ402    rcases continuous with ⟨function, subset, points⟩403    exact function404  have valueX := FunctionBetween.apply_closed with function, realX405  have weak := realLess.implies_le with ordered406  have subset := closedInterval.nested with leftBound, right407  have lowerValues : ∀ Z ∈ closedInterval(X, Y),408      f(X) - E ≤ (f(Z):R)409    intros Z local410    have global := subset with Z, local411    obtain ⟨realZ, xLeZ, zLeY⟩ := closedInterval.membership.forward with local412    have distance := dist.le_interval_width with xLeZ, zLeY413    have near := realLe.transitive_less with distance, small414    obtain ⟨lowValue, highValue⟩ := control with Z, global, near415    have valueZ := FunctionBetween.apply_closed with function, realZ416    exact realLess.implies_le with lowValue417  have upperValues : ∀ W ∈ closedInterval(X, Y),418      (f(W):R) ≤ f(X) + E419    intros W local420    have global := subset with W, local421    obtain ⟨realW, xLeW, wLeY⟩ := closedInterval.membership.forward with local422    have distance := dist.le_interval_width with xLeW, wLeY423    have near := realLe.transitive_less with distance, small424    obtain ⟨lowValue, highValue⟩ := control with W, global, near425    have valueW := FunctionBetween.apply_closed with function, realW426    exact realLess.implies_le with highValue427  exact HasRiemannIntegral.between_constants with ordered, integral, lowerValues, upperValues428429theorem ContinuousOn.right_integral_average (f : Set) (A B X E D Y I : Real)430  requires continuous : ContinuousOn(f, closedInterval(A, B))431  requires inside : X ∈ closedInterval(A, B)432  requires control : ∀ Z ∈ closedInterval(A, B), dist(X, Z) < D →433    f(X) - E < (f(Z):R) ∧434      (f(Z):R) < f(X) + E435  requires ordered : X < Y436  requires right : Y ≤ B437  requires small : Y - X < D438  requires integral : HasRiemannIntegral(f, X, Y, I)439  shows f(X) - E ≤ I / (Y - X) ∧440    I / (Y - X) ≤ f(X) + E441proof442  have bounds := ContinuousOn.right_integral_bounds with443    continuous, inside, control, ordered, right, small, integral444  rcases bounds with ⟨lower, upper⟩445  have positive : 0 < Y - X by linarith446  have width := realSubValue.real at Y, X with *447  have nonzero : Y - X ≠ realZero448    intro equal449    have strict := realLess.characterization.forward with positive450    rw equal at strict451    exact RealLess.irreflexive with strict452  have function : f : ℝ → ℝ453    rcases continuous with ⟨function, subset, points⟩454    exact function455  have realX : X ∈ ℝ by simp [Real]456  have valueX := FunctionBetween.apply_closed with function, realX457  have typedFX : Real(f(X)) by exact valueX458  have lowReal := realSubValue.real at f(X), E with typedFX, assumption459  have highReal := realAddValue.real at f(X), E with typedFX, assumption460  have lowProduct := realMulValue.real with lowReal, width461  have highProduct := realMulValue.real with highReal, width462  have lowDiv := realLe.divide_positive at (f(X) - E) * (Y - X), I,463    Y - X with lowProduct, assumption, width, lower, positive464  have highDiv := realLe.divide_positive at I, (f(X) + E) * (Y - X),465    Y - X with assumption, highProduct, width, upper, positive466  have lowShape := realDiv.mul_numerator_left with lowReal, width, width467  have highShape := realDiv.mul_numerator_left with highReal, width, width468  have cancel := realDiv.self with nonzero469  rw lowShape at lowDiv470  rw highShape at highDiv471  rw cancel at lowDiv472  rw cancel at highDiv473  have oneLow := realMulValue.one_right with lowReal474  have oneHigh := realMulValue.one_right with highReal475  rw oneLow at lowDiv476  rw oneHigh at highDiv477  refine ⟨lowDiv, highDiv⟩478479theorem ContinuousOn.left_integral_bounds (f : Set) (A B X E D Y I : Real)480  requires continuous : ContinuousOn(f, closedInterval(A, B))481  requires inside : X ∈ closedInterval(A, B)482  requires control : ∀ Z ∈ closedInterval(A, B), dist(X, Z) < D →483    f(X) - E < (f(Z):R) ∧484      (f(Z):R) < f(X) + E485  requires ordered : Y < X486  requires left : A ≤ Y487  requires small : X - Y < D488  requires integral : HasRiemannIntegral(f, Y, X, I)489  shows (f(X) - E) * (X - Y) ≤ I ∧490    I ≤ (f(X) + E) * (X - Y)491proof492  obtain ⟨realX, leftBound, rightBound⟩ := closedInterval.membership.forward with inside493  have function : f : ℝ → ℝ494    rcases continuous with ⟨function, subset, points⟩495    exact function496  have valueX := FunctionBetween.apply_closed with function, realX497  have subset := closedInterval.nested with left, rightBound498  have lowerValues : ∀ Z ∈ closedInterval(Y, X),499      f(X) - E ≤ (f(Z):R)500    intros Z local501    have global := subset with Z, local502    obtain ⟨realZ, yLeZ, zLeX⟩ := closedInterval.membership.forward with local503    have distance := dist.le_interval_width at Z, X, X with504      zLeX, realLe.reflexive at X with assumption505    have difference : X - Z ≤ X - Y by linarith506    have distanceBound := realLe.transitive with distance, difference507    have symmetry := dist.symmetric at X, Z with *508    rw ← symmetry at distanceBound509    have near := realLe.transitive_less with distanceBound, small510    obtain ⟨lowValue, highValue⟩ := control with Z, global, near511    have valueZ := FunctionBetween.apply_closed with function, realZ512    exact realLess.implies_le with lowValue513  have upperValues : ∀ W ∈ closedInterval(Y, X),514      (f(W):R) ≤ f(X) + E515    intros W local516    have global := subset with W, local517    obtain ⟨realW, yLeW, wLeX⟩ := closedInterval.membership.forward with local518    have distance := dist.le_interval_width at W, X, X with519      wLeX, realLe.reflexive at X with assumption520    have difference : X - W ≤ X - Y by linarith521    have distanceBound := realLe.transitive with distance, difference522    have symmetry := dist.symmetric at X, W with *523    rw ← symmetry at distanceBound524    have near := realLe.transitive_less with distanceBound, small525    obtain ⟨lowValue, highValue⟩ := control with W, global, near526    have valueW := FunctionBetween.apply_closed with function, realW527    exact realLess.implies_le with highValue528  exact HasRiemannIntegral.between_constants with ordered, integral, lowerValues, upperValues529530theorem ContinuousOn.left_integral_average (f : Set) (A B X E D Y I : Real)531  requires continuous : ContinuousOn(f, closedInterval(A, B))532  requires inside : X ∈ closedInterval(A, B)533  requires control : ∀ Z ∈ closedInterval(A, B), dist(X, Z) < D →534    f(X) - E < (f(Z):R) ∧535      (f(Z):R) < f(X) + E536  requires ordered : Y < X537  requires left : A ≤ Y538  requires small : X - Y < D539  requires integral : HasRiemannIntegral(f, Y, X, I)540  shows f(X) - E ≤ I / (X - Y) ∧541    I / (X - Y) ≤ f(X) + E542proof543  have bounds := ContinuousOn.left_integral_bounds with544    continuous, inside, control, ordered, left, small, integral545  rcases bounds with ⟨lower, upper⟩546  have positive : 0 < X - Y by linarith547  have width := realSubValue.real at X, Y with *548  have nonzero : X - Y ≠ realZero549    intro equal550    have strict := realLess.characterization.forward with positive551    rw equal at strict552    exact RealLess.irreflexive with strict553  have function : f : ℝ → ℝ554    rcases continuous with ⟨function, subset, points⟩555    exact function556  have realX : X ∈ ℝ by simp [Real]557  have valueX := FunctionBetween.apply_closed with function, realX558  have typedFX : Real(f(X)) by exact valueX559  have lowReal := realSubValue.real at f(X), E with typedFX, assumption560  have highReal := realAddValue.real at f(X), E with typedFX, assumption561  have lowProduct := realMulValue.real with lowReal, width562  have highProduct := realMulValue.real with highReal, width563  have lowDiv := realLe.divide_positive at (f(X) - E) * (X - Y), I,564    X - Y with lowProduct, assumption, width, lower, positive565  have highDiv := realLe.divide_positive at I, (f(X) + E) * (X - Y),566    X - Y with assumption, highProduct, width, upper, positive567  have lowShape := realDiv.mul_numerator_left with lowReal, width, width568  have highShape := realDiv.mul_numerator_left with highReal, width, width569  have cancel := realDiv.self with nonzero570  rw lowShape at lowDiv571  rw highShape at highDiv572  rw cancel at lowDiv573  rw cancel at highDiv574  have oneLow := realMulValue.one_right with lowReal575  have oneHigh := realMulValue.one_right with highReal576  rw oneLow at lowDiv577  rw oneHigh at highDiv578  refine ⟨lowDiv, highDiv⟩579580-- Section: CellMeanValueChoice581defgraph functionIncrements (f p : Set) (n ∈ ℕ) : ℝ :=582  realSubValue(f(p[succ(n)]), f(p[n]))583requires function : f : ℝ → ℝ584requires points : RealSequence(p)585proof586  have pointN := RealSequence.value with points587  have pointNext := RealSequence.value at p, succ(n) with points588  unfold Real at pointN589  unfold Real at pointNext590  have valueN := FunctionBetween.apply_closed with function, pointN591  have valueNext := FunctionBetween.apply_closed with function, pointNext592  have realN : Real(f(p[n])) by exact valueN593  have realNext : Real(f(p[succ(n)])) by exact valueNext594  exact realSubValue.real with realNext, realN595596theorem functionIncrements.sequence (f p : Set)597  requires function : f : ℝ → ℝ598  requires points : RealSequence(p)599  shows RealSequence(functionIncrements(f, p))600proof601  unfold RealSequence602  exact functionIncrements.function with function, points603604theorem functionIncrements.telescoping (f p : Set) (N : Nat)605  requires function : f : ℝ → ℝ606  requires points : RealSequence(p)607  shows realPartialSum(functionIncrements(f, p), N) =608    f(p[N]) - f(p[0])609proof610  induction N611  | zero =>612    rw realPartialSum.zero613    have point0 := RealSequence.value at p, 0 with points614    unfold Real at point0615    have value0 := FunctionBetween.apply_closed with function, point0616    ring617  | succ(k) using ih =>618    rw [realPartialSum.succ, ih]619    have value := functionIncrements.value with function, points620    rw value621    have point0 := RealSequence.value with points622    have pointK := RealSequence.value with points623    have pointNext := RealSequence.value with points624    unfold Real at point0625    unfold Real at pointK626    unfold Real at pointNext627    have value0 := FunctionBetween.apply_closed with function, point0628    have valueK := FunctionBetween.apply_closed with function, pointK629    have valueNext := FunctionBetween.apply_closed with function, pointNext630    ring631632theorem IntervalPartition.sum_function_increments (f p : Set) (A B : Real, N : Nat)633  requires function : f : ℝ → ℝ634  requires partition : IntervalPartition(p, A, B, N)635  shows realPartialSum(functionIncrements(f, p), N) =636    f(B) - f(A)637proof638  rcases partition with ⟨points, left, right, increasing⟩639  have sum := functionIncrements.telescoping with function, points640  rwa [left, right] at sum641642-- This is the finite algebraic part of FTC. A mean value theorem will later643-- produce tags satisfying the displayed cell equation.644theorem TaggedPartition.riemann_sum_of_cell_increments (f F p t : Set) (A B : Real, N : Nat)645  requires functionF : F : ℝ → ℝ646  requires functionf : f : ℝ → ℝ647  requires tagged : TaggedPartition(p, t, A, B, N)648  requires cells : ∀ i ∈ ℕ, i < N →649    realMulValue(f(t[i]), realSubValue(p[succ(i)], p[i])) =650      realSubValue(F(p[succ(i)]), F(p[i]))651  shows riemannSum(f, p, t, N) = F(B) - F(A)652proof653  rcases tagged with ⟨partition, tags, tagCells⟩654  have points : RealSequence(p)655    rcases partition with ⟨sequence, left, right, increasing⟩656    exact sequence657  have fTerms : RealSequence(riemannTerms(f, p, t))658    unfold RealSequence659    exact riemannTerms.function with functionf, points, tags660  have increments := functionIncrements.sequence with functionF, points661  have equalTerms : ∀ i ∈ ℕ, i < N →662      riemannTerms(f, p, t)[i] = functionIncrements(F, p)[i]663    intros i naturalI before664    have riemannValue := riemannTerms.value at f, p, t, i with665      functionf, points, tags666    have incrementValue := functionIncrements.value at F, p, i with667      functionF, points668    rw [riemannValue, incrementValue]669    exact cells with i, naturalI, before670  have sameSum := realPartialSum.eq_prefix with fTerms, increments, equalTerms671  have endpoint := IntervalPartition.sum_function_increments with functionF, partition672  simp [riemannSum]673674-- CellMeanValueBridge675predicate CellMeanValueTagsExist (f F : Set) (A B : Real) :=676  ∀ p, ∀ N ∈ ℕ, IntervalPartition(p, A, B, N) →677    ∃ t, TaggedPartition(p, t, A, B, N) ∧678      (∀ i ∈ ℕ, i < N →679        realMulValue(f(t[i]), realSubValue(p[succ(i)], p[i])) =680          realSubValue(F(p[succ(i)]), F(p[i])))681682-- For every epsilon, take a fine partition, then its mean-value683-- tags. Its Riemann sum telescopes exactly, so the proposed integral cannot684-- differ from the endpoint increment.685theorem HasRiemannIntegral.eq_endpoint_of_cell_tags (f F : Set) (A B I : Real)686  requires functionF : F : ℝ → ℝ687  requires integral : HasRiemannIntegral(f, A, B, I)688  requires meanTags : CellMeanValueTagsExist(f, F, A, B)689  shows I = F(B) - F(A)690proof691  by_contra unequal692  have functionf : f : ℝ → ℝ693    rcases integral with ⟨function, ordered, control⟩694    exact function695  have realA : A ∈ ℝ by simp [Real]696  have realB : B ∈ ℝ by simp [Real]697  have valueA := FunctionBetween.apply_closed with functionF, realA698  have valueB := FunctionBetween.apply_closed with functionF, realB699  have distinct : F(B) - F(A) ≠ I700    intro same701    apply unequal702    rw same703    rfl704  have positive := dist.positive_of_ne with distinct705  rcases integral with ⟨functionAgain, ordered, control⟩706  obtain ⟨D, realD, positiveD, estimate⟩ :=707    control with dist(F(B) - F(A), I), positive708  have cofinal := FineTaggedPartitionsExist.ordered_interval with ordered709  obtain ⟨p, preliminaryTags, N, naturalN, preliminary, fine⟩ :=710    cofinal with D, realD, positiveD711  have partition : IntervalPartition(p, A, B, N)712    rcases preliminary with ⟨points, tags, cells⟩713    exact points714  obtain ⟨t, tagged, cells⟩ := meanTags with p, N, naturalN, partition715  have typedN := nat.omega.backward with naturalN716  have sum := TaggedPartition.riemann_sum_of_cell_increments with functionF, functionf, tagged, cells717  have near := estimate with p, t, N, naturalN, tagged, fine718  rw sum at near719  have contradiction := realLess.characterization.forward with near720  exact RealLess.irreflexive with contradiction721722-- CellMeanValueChoice723predicate CellMeanValueWitnesses (f F p : Set) (N : Nat) :=724  ∀ i ∈ ℕ, i < N →725    ∃ X ∈ closedInterval(p[i], p[succ(i)]),726      realMulValue(f(X), realSubValue(p[succ(i)], p[i])) =727        realSubValue(F(p[succ(i)]), F(p[i]))728729-- Outside the finite prefix a tag is the left endpoint, which makes the730-- sequence total without a condition on unused cells.731defchoose cellMeanValueTag (f F p : Set, N i : Nat) (X ∈ ℝ) :=732  (i < N → X ∈ closedInterval(p[i], p[succ(i)]) ∧733    realMulValue(f(X), realSubValue(p[succ(i)], p[i])) =734      realSubValue(F(p[succ(i)]), F(p[i]))) ∧735  (¬(i < N) → X = p[i])736requires points : RealSequence(p)737requires witnesses : CellMeanValueWitnesses(f, F, p, N)738proof739  have alternatives : i < N ∨ ¬(i < N)740    tauto741  cases alternatives with before | beyond742  . unfold CellMeanValueWitnesses at witnesses743    have naturalI := nat.omega.forward at i with assumption744    obtain ⟨X, inCell, equation⟩ := witnesses with i, naturalI, before745    have pointI := RealSequence.value at p, i with points746    have pointNext := RealSequence.value at p, succ(i) with points747    have data := closedInterval.membership.forward at p[i], p[succ(i)], X748      with inCell749    rcases data with ⟨realX, lower, upper⟩750    witness X751    constructor752    . exact realX753    . constructor754      . intro beforeAgain755        refine ⟨inCell, equation⟩756      . intro notBefore757        exfalso758        exact notBefore with before759  . have pointI := RealSequence.value at p, i with points760    witness p[i]761    constructor762    . unfold Real at pointI763      exact pointI764    . constructor765      . intro before766        exfalso767        exact beyond with before768      . intro notBefore769        rfl770771defgraph cellMeanValueTags (f F p : Set, N : Nat) (i ∈ ℕ) : ℝ :=772  cellMeanValueTag(f, F, p, N, i)773requires points : RealSequence(p)774requires witnesses : CellMeanValueWitnesses(f, F, p, N)775proof776  have selected := cellMeanValueTag.selected at f, F, p, N, i with777    assumption, points, witnesses778  rcases selected with ⟨realTag, properties⟩779  exact realTag780781theorem CellMeanValueWitnesses.tags (f F p : Set) (A B : Real, N : Nat)782  requires partition : IntervalPartition(p, A, B, N)783  requires witnesses : CellMeanValueWitnesses(f, F, p, N)784  shows TaggedPartition(p, cellMeanValueTags(f, F, p, N), A, B, N) ∧785    (∀ i ∈ ℕ, i < N →786      realMulValue(f(cellMeanValueTags(f, F, p, N)[i]),787        realSubValue(p[succ(i)], p[i])) =788          realSubValue(F(p[succ(i)]), F(p[i])))789proof790  have points : RealSequence(p)791    rcases partition with ⟨sequence, left, right, increasing⟩792    exact sequence793  have sequence : RealSequence(cellMeanValueTags(f, F, p, N))794    unfold RealSequence795    exact cellMeanValueTags.function with points, witnesses796  have cell : ∀ i ∈ ℕ, i < N → cellMeanValueTags(f, F, p, N)[i] ∈ closedInterval(p[i], p[succ(i)]) ∧ realMulValue(f(cellMeanValueTags(f, F, p, N)[i]), realSubValue(p[succ(i)], p[i])) = realSubValue(F(p[succ(i)]), F(p[i]))797    intros i naturalI before798    have typedI := nat.omega.backward with naturalI799    have value := cellMeanValueTags.value at f, F, p, N, i with800      points, witnesses801    have selected := cellMeanValueTag.selected at f, F, p, N, i with802      points, witnesses803    rcases selected with ⟨realTag, valid, unused⟩804    have selectedCell := valid with before805    rwa value806  constructor807    constructor808    . exact partition809    . constructor810      . exact sequence811      . intros j naturalJ before812        obtain ⟨member, equation⟩ := cell with j, naturalJ, before813        exact member814  . intros j naturalJ before815    obtain ⟨member, equation⟩ := cell with j, naturalJ, before816    exact equation817818theorem CellMeanValueWitnesses.all_tags (f F : Set) (A B : Real)819  requires local : ∀ p, ∀ N ∈ ℕ,820    IntervalPartition(p, A, B, N) → CellMeanValueWitnesses(f, F, p, N)821  shows CellMeanValueTagsExist(f, F, A, B)822proof823  intros p N naturalN partition824  have witnesses := local with p, N, naturalN, partition825  have typedN := nat.omega.backward with naturalN826  obtain ⟨tagged, equations⟩ := CellMeanValueWitnesses.tags with partition, witnesses827  witness cellMeanValueTags(f, F, p, N)828  refine ⟨tagged, equations⟩829830-- This is the interval form of the mean value theorem needed by FTC. The831-- choice construction above turns its individual cell witnesses into a832-- single tagged partition without an additional choice assumption.833predicate CellMeanValueProperty (f F : Set) :=834  ∀ X ∈ ℝ, ∀ Y ∈ ℝ, (X:R) < (Y:R) →835    ∃ T ∈ closedInterval(X, Y),836      realMulValue(f(T), realSubValue(Y, X)) =837        realSubValue(F(Y), F(X))838839theorem CellMeanValueProperty.partition_witnesses (f F p : Set) (A B : Real, N : Nat)840  requires partition : IntervalPartition(p, A, B, N)841  requires meanValue : CellMeanValueProperty(f, F)842  shows CellMeanValueWitnesses(f, F, p, N)843proof844  intros i naturalI before845  have typedI := nat.omega.backward with naturalI846  have points : RealSequence(p)847    rcases partition with ⟨sequence, left, right, increasing⟩848    exact sequence849  have pointI := RealSequence.value at p, i with points850  have pointNext := RealSequence.value at p, succ(i) with points851  have increasing := IntervalPartition.cell with partition, before852  exact meanValue with p[i], pointI, p[succ(i)], pointNext, increasing853854theorem HasRiemannIntegral.eq_endpoint_of_mean_value (f F : Set) (A B I : Real)855  requires functionF : F : ℝ → ℝ856  requires integral : HasRiemannIntegral(f, A, B, I)857  requires meanValue : CellMeanValueProperty(f, F)858  shows I = F(B) - F(A)859proof860  have local : ∀ p, ∀ N ∈ ℕ,861      IntervalPartition(p, A, B, N) → CellMeanValueWitnesses(f, F, p, N)862    intros p N naturalN partition863    have typedN := nat.omega.backward with naturalN864    exact CellMeanValueProperty.partition_witnesses with partition, meanValue865  have tags := CellMeanValueWitnesses.all_tags with local866  exact HasRiemannIntegral.eq_endpoint_of_cell_tags with functionF, integral, tags867