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

Open in Workbench Download source

Imports

PartitionSplit · RiemannSums · ContinuousIntegral · IntegralOrderBound

Declarations

Source

1-- Real analysis: IndefiniteIntegral2-- 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.IndefiniteIntegral8import PartitionSplit9import RiemannSums10import ContinuousIntegral11import IntegralOrderBound1213-- Section: IndefiniteIntegral14theorem FinePartition.split_at_vertex (f p t : Set) (A B C D : Real, M i : Nat)15  requires function : f : ℝ → ℝ16  requires fine : FinePartition(p, A, B, M, D)17  requires tagged : TaggedPartition(p, t, A, B, M)18  requires bounded : i ≤ M19  requires vertex : p[i] = C20  shows ∃ j ∈ ℕ, add(i, j) = M ∧21    FinePartition(p, A, C, i, D) ∧22    FinePartition(shiftedRealSequence(p, i), C, B, j, D) ∧23    TaggedPartition(p, t, A, C, i) ∧24    TaggedPartition(shiftedRealSequence(p, i), shiftedRealSequence(t, i), C, B, j) ∧25    riemannSum(f, p, t, M) =26      (riemannSum(f, p, t, i):R) +27      (riemannSum(f, shiftedRealSequence(p, i), shiftedRealSequence(t, i), j):R)28proof29  obtain ⟨j, naturalJ, sum⟩ := bounded30  have memberJ := nat.omega.forward with naturalJ31  have splitFine : FinePartition(p, A, B, add(i, j), D) by rwa sum32  have splitTagged : TaggedPartition(p, t, A, B, add(i, j)) by rwa sum33  have parts := FinePartition.split_tagged_sum with function, splitFine, splitTagged34  rw [vertex, sum] at parts35  witness j36  refine ⟨memberJ, sum, parts⟩3738-- CommonMesh39theorem positiveMesh.common_two (D E : Real)40  requires positiveD : 0 < D41  requires positiveE : 0 < E42  shows ∃ H ∈ ℝ, 0 < H ∧ H ≤ D ∧ H ≤ E43proof44  have alternatives : D ≤ E ∨ ¬(D ≤ E) by tauto45  cases alternatives with first | second46  . witness D47    have realD : D ∈ ℝ by simp [Real]48    refine ⟨realD, positiveD, realLe.reflexive at D with assumption, first⟩49  . have reverse := realLess.of_not_le with second50    have weak := realLess.implies_le with reverse51    witness E52    have realE : E ∈ ℝ by simp [Real]53    refine ⟨realE, positiveE, weak, realLe.reflexive at E with assumption⟩5455theorem positiveMesh.common_three (D E F : Real)56  requires positiveD : 0 < D57  requires positiveE : 0 < E58  requires positiveF : 0 < F59  shows ∃ H ∈ ℝ, 0 < H ∧ H ≤ D ∧ H ≤ E ∧ H ≤ F60proof61  obtain ⟨G, realG, positiveG, gD, gE⟩ := positiveMesh.common_two with positiveD, positiveE62  obtain ⟨H, realH, positiveH, hG, hF⟩ := positiveMesh.common_two with positiveG, positiveF63  have hD := realLe.transitive with hG, gD64  have hE := realLe.transitive with hG, gE65  witness H66  refine ⟨realH, positiveH, hD, hE, hF⟩6768-- IntegralAdditivity69theorem HasRiemannIntegral.add_interior (f : Set) (A C B IL IR : Real)70  requires left : A < C71  requires right : C < B72  requires continuous : ContinuousOn(f, closedInterval(A, B))73  requires integralL : HasRiemannIntegral(f, A, C, IL)74  requires integralR : HasRiemannIntegral(f, C, B, IR)75  shows HasRiemannIntegral(f, A, B, IL + IR)76proof77  have function : f : ℝ → ℝ78    rcases continuous with ⟨function, subset, points⟩79    exact function80  have ordered := realLess.transitive with left, right81  rcases integralL with ⟨functionL, orderL, controlL⟩82  rcases integralR with ⟨functionR, orderR, controlR⟩83  constructor84  . exact function85  . constructor86    . exact realLess.implies_le with ordered87    . intros E realE positiveE88      have typedE : Real(E) by exact realE89      have halfReal := half.real with typedE90      have halfPositive := half.positive with positiveE91      have quarterReal := half.real with halfReal92      have quarterPositive := half.positive with halfPositive93      obtain ⟨DC, realDC, positiveDC, compare⟩ := ContinuousOn.fine_sums_close with94        ordered, continuous, halfPositive95      obtain ⟨DL, realDL, positiveDL, estimateL⟩ :=96        controlL with half(half(E)), quarterPositive97      obtain ⟨DR, realDR, positiveDR, estimateR⟩ :=98        controlR with half(half(E)), quarterPositive99      obtain ⟨D, realD, positiveD, dC, dL, dR⟩ := positiveMesh.common_three with100        positiveDC, positiveDL, positiveDR101      witness D102      constructor103      . exact realD104      . constructor105        . exact positiveD106        . intros p t N naturalN tagged fine107          have typedN := nat.omega.backward with naturalN108          obtain ⟨q, M, naturalM, u, v, fineQ, taggedQ, shared, preserved, i, naturalI, boundedI, vertex⟩ := FinePartition.insert_or_hit with109            function, fine, left, right110          have typedM := nat.omega.backward with naturalM111          have typedI := nat.omega.backward with naturalI112          have finePCompare := FinePartition.weaken with fine, dC113          have fineQCompare := FinePartition.weaken with fineQ, dC114          have nearPQ := compare with p, t, N, naturalN, q, leftPartitionTags(q), M,115            naturalM, tagged, finePCompare, taggedQ, fineQCompare116          obtain ⟨j, naturalJ, sumIndex, finePrefix, fineSuffix, taggedPrefix, taggedSuffix, splitSum⟩ := FinePartition.split_at_vertex with117            function, fineQ, taggedQ, boundedI, vertex118          have typedJ := nat.omega.backward with naturalJ119          have fineLocalL := FinePartition.weaken with finePrefix, dL120          have fineLocalR := FinePartition.weaken with fineSuffix, dR121          have nearL := estimateL with q, leftPartitionTags(q), i, naturalI,122            taggedPrefix, fineLocalL123          have nearR := estimateR with shiftedRealSequence(q, i),124            shiftedRealSequence(leftPartitionTags(q), i), j, naturalJ,125            taggedSuffix, fineLocalR126          have pointsQ : RealSequence(q)127            rcases taggedQ with ⟨partition, tags, cells⟩128            rcases partition with ⟨points, start, finish, increasing⟩129            exact points130          have tagsQ : RealSequence(leftPartitionTags(q))131            rcases taggedQ with ⟨partition, tags, cells⟩132            exact tags133          have pointsR := shiftedRealSequence.sequence at q, i with pointsQ134          have tagsR := shiftedRealSequence.sequence at leftPartitionTags(q), i with tagsQ135          have sumL := riemannSum.real at f, q, leftPartitionTags(q), i with136            function, pointsQ, tagsQ137          have sumR := riemannSum.real at f, shiftedRealSequence(q, i),138            shiftedRealSequence(leftPartitionTags(q), i), j with function, pointsR, tagsR139          have memberL : riemannSum(f, q, leftPartitionTags(q), i) ∈ ℝ by exact sumL140          have memberR : riemannSum(f, shiftedRealSequence(q, i), shiftedRealSequence(leftPartitionTags(q), i), j) ∈ ℝ141            exact sumR142          have dataL : riemannSum(f, q, leftPartitionTags(q), i) ∈ ℝ ∧ dist(riemannSum(f, q, leftPartitionTags(q), i), IL) < half(half(E))143            refine ⟨memberL, nearL⟩144          have dataR : riemannSum(f, shiftedRealSequence(q, i), shiftedRealSequence(leftPartitionTags(q), i), j) ∈ ℝ ∧ dist(riemannSum(f, shiftedRealSequence(q, i), shiftedRealSequence(leftPartitionTags(q), i), j), IR) < half(half(E))145            refine ⟨memberR, nearR⟩146          have ballL := openBall.membership.backward with dataL147          have ballR := openBall.membership.backward with dataR148          have ballSum := openBall.add at149            riemannSum(f, q, leftPartitionTags(q), i),150            riemannSum(f, shiftedRealSequence(q, i), shiftedRealSequence(leftPartitionTags(q), i), j),151            IL, IR, half(half(E)), half(half(E)) with152              sumL, sumR, *{2}, quarterReal, quarterReal, ballL, ballR153          have quarters := half.add_self with halfReal154          rw [quarters, ← splitSum] at ballSum155          have pointsP : RealSequence(p)156            rcases tagged with ⟨partition, tags, cells⟩157            rcases partition with ⟨points, start, finish, increasing⟩158            exact points159          have tagsP : RealSequence(t)160            rcases tagged with ⟨partition, tags, cells⟩161            exact tags162          have sumP := riemannSum.real at f, p, t, N with function, pointsP, tagsP163          have memberP : riemannSum(f, p, t, N) ∈ ℝ by exact sumP164          have dataPQ : riemannSum(f, p, t, N) ∈ ℝ ∧ dist(riemannSum(f, p, t, N), riemannSum(f, q, leftPartitionTags(q), M)) < half(E)165            refine ⟨memberP, nearPQ⟩166          have ballPQ := openBall.membership.backward with dataPQ167          have together := openBall.triangle with ballPQ, ballSum168          have halves := half.add_self with typedE169          rw halves at together170          obtain ⟨realSum, bound⟩ := openBall.membership.forward with together171          exact bound172173-- LocalContinuity174theorem ContinuousWithinAt.mono (f S T : Set) (A : Real)175  requires continuous : ContinuousWithinAt(f, T, A)176  requires subset : S ⊆ T177  shows ContinuousWithinAt(f, S, A)178proof179  rcases continuous with ⟨function, reals, control⟩180  constructor181  . exact function182  . constructor183      intros X member184      have included : X ∈ T by exact subset with X, member185      exact reals with X, included186    . intros E realE positive187      obtain ⟨D, realD, positiveD, maps⟩ := control with E, realE, positive188      witness D189      constructor190      . exact realD191      . constructor192        . exact positiveD193        . intros X realX member near194          have included : X ∈ T by exact subset with X, member195          exact maps with X, realX, included, near196197theorem ContinuousOn.mono (f S T : Set)198  requires continuous : ContinuousOn(f, T)199  requires subset : S ⊆ T200  shows ContinuousOn(f, S)201proof202  rcases continuous with ⟨function, reals, atPoints⟩203  constructor204  . exact function205  . constructor206      intros X member207      have included : X ∈ T by exact subset with X, member208      exact reals with X, included209    . intros X member210      have included : X ∈ T by exact subset with X, member211      have point := atPoints with X, included212      have typedX : Real(X)213        unfold Real214        exact reals with X, included215      exact ContinuousWithinAt.mono with point, subset216217theorem ContinuousOn.partition_cell (F p : Set) (A B : Real, N i : Nat)218  requires continuous : ContinuousOn(F, closedInterval(A, B))219  requires partition : IntervalPartition(p, A, B, N)220  requires before : i < N221  shows ContinuousOn(F, closedInterval(p[i], p[succ(i)]))222proof223  have subset := IntervalPartition.cell_subset with partition, before224  exact ContinuousOn.mono with continuous, subset225226-- IndefiniteIntegral227theorem ContinuousOn.subinterval (f : Set) (A B X Y : Real)228  requires continuous : ContinuousOn(f, closedInterval(A, B))229  requires left : A ≤ X230  requires right : Y ≤ B231  shows ContinuousOn(f, closedInterval(X, Y))232proof233  have subset := closedInterval.nested with left, right234  exact ContinuousOn.mono with continuous, subset235236defunique integralValue (f : Set, A B X : Real) (I ∈ ℝ) :=237  (X ∈ closedInterval(A, B) → HasRiemannIntegral(f, A, X, I)) ∧238  (¬(X ∈ closedInterval(A, B)) → I = realZero)239requires ordered : A ≤ B240requires continuous : ContinuousOn(f, closedInterval(A, B))241proof242  have alternatives : X ∈ closedInterval(A, B) ∨ ¬(X ∈ closedInterval(A, B)) by tauto243  cases alternatives with inside | outside244  . have bounds := closedInterval.membership.forward at A, B, X with inside245    rcases bounds with ⟨realX, lower, upper⟩246    have restricted := ContinuousOn.subinterval at f, A, B, A, X with247      continuous, realLe.reflexive at A with assumption, upper248    obtain ⟨I, realI, integral⟩ := ContinuousOn.integrable_interval with lower, restricted249    witness I250    constructor251    . exact realI252    . constructor253      . intro again254        exact integral255      . intro impossible256        exfalso257        exact impossible with inside258  . witness realZero259    constructor260    . have realZ := realZero.real261      exact realZ262    . constructor263      . intro impossible264        exfalso265        exact outside with impossible266      . intro ignored267        rfl268269uniqueness270  intros I memberI first J memberJ second271  have alternatives : X ∈ closedInterval(A, B) ∨ ¬(X ∈ closedInterval(A, B)) by tauto272  cases alternatives with inside | outside273  . have firstIntegral : HasRiemannIntegral(f, A, X, I)274      tauto275    have secondIntegral : HasRiemannIntegral(f, A, X, J) by tauto276    obtain ⟨typedX, lower, upper⟩ := closedInterval.membership.forward with inside277    exact HasRiemannIntegral.unique_on_interval with *278  . have firstZero : I = realZero279      tauto280    have secondZero : J = realZero by tauto281    cc282283defgraph integralFrom (f : Set, A B : Real) (X ∈ ℝ) : ℝ := integralValue(f, A, B, X)284requires ordered : A ≤ B285requires continuous : ContinuousOn(f, closedInterval(A, B))286proof287  obtain ⟨realValue, inside, outside⟩ := integralValue.selected at f, A, B, X with ordered, continuous288  exact realValue289290theorem integralFrom.integral (f : Set) (A B X : Real)291  requires ordered : A ≤ B292  requires continuous : ContinuousOn(f, closedInterval(A, B))293  requires inside : X ∈ closedInterval(A, B)294  shows HasRiemannIntegral(f, A, X, integralFrom(f, A, B)(X))295proof296  obtain ⟨realValue, valid, outside⟩ := integralValue.selected at f, A, B, X with ordered, continuous297  have integral := valid with inside298  have value := integralFrom.value at f, A, B, X with ordered, continuous299  rwa value300301theorem integralFrom.increment_right (f : Set) (A B X Y I : Real)302  requires ordered : A ≤ B303  requires continuous : ContinuousOn(f, closedInterval(A, B))304  requires left : A < X305  requires middle : X < Y306  requires right : Y ≤ B307  requires local : HasRiemannIntegral(f, X, Y, I)308  shows integralFrom(f, A, B)(Y) =309    integralFrom(f, A, B)(X) + I310proof311  have weakLeft := realLess.implies_le with left312  have weakMiddle := realLess.implies_le with middle313  have xBound : X ≤ B by exact realLe.transitive at X, Y, B with weakMiddle, right314  have realX : X ∈ ℝ by simp [Real]315  have realY : Y ∈ ℝ by simp [Real]316  have insideX : X ∈ closedInterval(A, B)317    have data : X ∈ ℝ ∧ A ≤ X ∧ X ≤ B by refine ⟨realX, weakLeft, xBound⟩318    exact closedInterval.membership.backward with data319  have insideY : Y ∈ closedInterval(A, B)320    have weakAY := realLe.transitive with weakLeft, weakMiddle321    have data : Y ∈ ℝ ∧ A ≤ Y ∧ Y ≤ B by refine ⟨realY, weakAY, right⟩322    exact closedInterval.membership.backward with data323  have first := integralFrom.integral with ordered, continuous, insideX324  have whole := integralFrom.integral with ordered, continuous, insideY325  have restricted := ContinuousOn.subinterval at f, A, B, A, Y with326    continuous, realLe.reflexive at A with assumption, right327  have combined := HasRiemannIntegral.add_interior with left, middle, restricted, first, local328  have strict := realLess.transitive with left, middle329  exact HasRiemannIntegral.unique_positive with strict, whole, combined330331theorem integralFrom.increment_left (f : Set) (A B X Y I : Real)332  requires ordered : A ≤ B333  requires continuous : ContinuousOn(f, closedInterval(A, B))334  requires left : A < Y335  requires middle : Y < X336  requires right : X ≤ B337  requires local : HasRiemannIntegral(f, Y, X, I)338  shows integralFrom(f, A, B)(X) =339    integralFrom(f, A, B)(Y) + I340proof341  exact integralFrom.increment_right with ordered, continuous, left, middle, right, local342