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

Open in Workbench Download source

Imports

CommonRefinementComparison · PartitionSplit · RiemannSums · IntegralOrderBound

Declarations

Source

1-- Real analysis: ContinuousIntegral2-- 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.ContinuousIntegral8import CommonRefinementComparison9import PartitionSplit10import RiemannSums11import IntegralOrderBound1213-- Section: ContinuousIntegral14theorem riemannSum.upper_step (f p t s : Set) (E : Real, k : Nat)15  requires function : f : ℝ → ℝ16  requires points : RealSequence(p)17  requires tagsT : RealSequence(t)18  requires tagsS : RealSequence(s)19  requires prefix : (riemannSum(f, p, t, k):R) ≤20    (riemannSum(f, p, s, k):R) + E * ((p[k]:R) - (p[0]:R))21  requires term : (f(t[k]):R) * ((p[succ(k)]:R) - (p[k]:R)) ≤22    (f(s[k]):R) * ((p[succ(k)]:R) - (p[k]:R)) +23      E * ((p[succ(k)]:R) - (p[k]:R))24  shows (riemannSum(f, p, t, succ(k)):R) ≤25    (riemannSum(f, p, s, succ(k)):R) +26      E * ((p[succ(k)]:R) - (p[0]:R))27proof28  have pointK := RealSequence.value at p, k with points29  have pointNext := RealSequence.value at p, succ(k) with points30  have pointZero := RealSequence.value at p, 0 with points31  have tagT := RealSequence.value at t, k with tagsT32  have tagS := RealSequence.value at s, k with tagsS33  have sumT := riemannSum.real at f, p, t, k with function, points, tagsT34  have sumS := riemannSum.real at f, p, s, k with function, points, tagsS35  have widthReal := realSubValue.real at p[succ(k)], p[k] with pointNext, pointK36  have prefixWidth := realSubValue.real at p[k], p[0] with pointK, pointZero37  have memberT : t[k] ∈ ℝ38    exact tagT39  have memberS : s[k] ∈ ℝ40    exact tagS41  have valueT := FunctionBetween.apply_closed at f, ℝ, ℝ, t[k] with42    function, memberT43  have valueS := FunctionBetween.apply_closed at f, ℝ, ℝ, s[k] with44    function, memberS45  have typedValueT : Real(f(t[k]))46    exact valueT47  have typedValueS : Real(f(s[k]))48    exact valueS49  have prefixProduct := realMulValue.real at E, p[k] - p[0] with50    assumption, prefixWidth51  have cellProduct := realMulValue.real at E, p[succ(k)] - p[k] with52    assumption, widthReal53  have termTReal := realMulValue.real at54    f(t[k]), p[succ(k)] - p[k] with typedValueT, widthReal55  have termSReal := realMulValue.real at56    f(s[k]), p[succ(k)] - p[k] with typedValueS, widthReal57  have prefixRhsReal := realAddValue.real at58    riemannSum(f, p, s, k), E * (p[k] - p[0]) with sumS, prefixProduct59  have termRhsReal := realAddValue.real at60    f(s[k]) * (p[succ(k)] - p[k]),61    E * (p[succ(k)] - p[k]) with termSReal, cellProduct62  have added := realLe.add at63    riemannSum(f, p, t, k),64    riemannSum(f, p, s, k) + E * (p[k] - p[0]),65    f(t[k]) * (p[succ(k)] - p[k]),66    f(s[k]) * (p[succ(k)] - p[k]) + E * (p[succ(k)] - p[k]) with67      sumT, prefixRhsReal, termTReal, termRhsReal, prefix, term68  have split : E * (p[succ(k)] - p[0]) =69      E * (p[k] - p[0]) + E * (p[succ(k)] - p[k])70    ring71  have rearrange : (riemannSum(f, p, s, k) + E * (p[k] - p[0])) +72        (f(s[k]) * (p[succ(k)] - p[k]) + E * (p[succ(k)] - p[k])) =73      (riemannSum(f, p, s, k) + f(s[k]) * (p[succ(k)] - p[k])) +74        E * (p[succ(k)] - p[0])75    rw split76    ring77  rw rearrange at added78  have stepT := riemannSum.succ at f, p, t, k with function, points, tagsT79  have stepS := riemannSum.succ at f, p, s, k with function, points, tagsS80  unfold call2 at added81  unfold realAddValue at stepT82  unfold realAddValue at stepS83  unfold realMulValue at stepT84  unfold realMulValue at stepS85  rw ← stepT at added86  rw ← stepS at added87  unfold call288  exact added8990-- Prefix induction keeps the comparison independent of the unused tail of91-- the partition. At N, p[0]=A and p[N]=B normalize the slack to E(B-A).92theorem riemannSum.upper_prefix (f p t s : Set) (A B D E : Real, N n : Nat)93  requires function : f : ℝ → ℝ94  requires oscillation : FineCellOscillation(f, A, B, D, E)95  requires fine : FinePartition(p, A, B, N, D)96  requires taggedT : TaggedPartition(p, t, A, B, N)97  requires taggedS : TaggedPartition(p, s, A, B, N)98  shows n ≤ N → (riemannSum(f, p, t, n):R) ≤99    (riemannSum(f, p, s, n):R) + E * ((p[n]:R) - (p[0]:R))100proof101  induction n102  | zero =>103    intro bounded104    have partition : IntervalPartition(p, A, B, N)105      rcases fine with ⟨partition, positive, widths⟩106      exact partition107    have points : RealSequence(p)108      rcases partition with ⟨points, start, finish, steps⟩109      exact points110    rw [riemannSum.zero, riemannSum.zero]111    have pointZero := RealSequence.value at p, 0 with points112    have self := realSubValue.self with pointZero113    rw self114    have zeroProduct : E * (0:R) = (0:R) by ring115    rw zeroProduct116    have zeroSum : (0:R) + (0:R) = (0:R) by ring117    rw zeroSum118    exact realLe.reflexive with realZero.real119  | succ(k) using ih =>120    intro bounded121    have partition : IntervalPartition(p, A, B, N)122      rcases fine with ⟨partition, positive, widths⟩123      exact partition124    have points : RealSequence(p)125      rcases partition with ⟨points, start, finish, steps⟩126      exact points127    have tagsT : RealSequence(t)128      rcases taggedT with ⟨partitionT, tags, cells⟩129      exact tags130    have tagsS : RealSequence(s)131      rcases taggedS with ⟨partitionS, tags, cells⟩132      exact tags133    have naturalK := nat.omega.forward at k134    have nextK := Naturals.constructor.succ at k135    have before : k < N by exact bounded136    have kLeNext := LessEqual.successor at k137    have kLeN := LessEqual.transitive at k, succ(k), N with138      assumption, nextK, assumption, kLeNext, bounded139    have prefix := ih with kLeN140    have strict := FineCellOscillation.weighted_tags with141      function, oscillation, fine, taggedT, taggedS, before142    have term := realLess.implies_le with strict143    exact riemannSum.upper_step with function, points, tagsT, tagsS, prefix, term144145-- Both tag choices share the same partition, so the cell widths telescope to146-- B-A. This comparison is uniform in the number and placement of the cells.147theorem FineCellOscillation.tagged_sum_bounds (f p t s : Set) (A B D E : Real, N : Nat)148  requires function : f : ℝ → ℝ149  requires oscillation : FineCellOscillation(f, A, B, D, E)150  requires fine : FinePartition(p, A, B, N, D)151  requires taggedT : TaggedPartition(p, t, A, B, N)152  requires taggedS : TaggedPartition(p, s, A, B, N)153  shows (riemannSum(f, p, t, N):R) ≤154      (riemannSum(f, p, s, N):R) + E * (B - A) ∧155    (riemannSum(f, p, s, N):R) ≤156      (riemannSum(f, p, t, N):R) + E * (B - A)157proof158  have bound := LessEqual.reflexive at N159  have first := riemannSum.upper_prefix with function, oscillation, fine, taggedT, taggedS, bound160  have second := riemannSum.upper_prefix with function, oscillation, fine, taggedS, taggedT, bound161  have partition : IntervalPartition(p, A, B, N)162    rcases fine with ⟨partition, positive, widths⟩163    exact partition164  rcases partition with ⟨points, start, finish, steps⟩165  rw [start, finish] at first166  rw [start, finish] at second167  refine ⟨first, second⟩168169-- ScaledMeshError170theorem scaledRadius.interval_error (A B E : Real)171  requires ordered : A ≤ B172  requires positive : 0 < E173  shows scaledRadius(E, limitScale(B - A)) * (B - A) < E174proof175  have widthReal := realSubValue.real at B, A with *176  have nonnegative : 0 ≤ B - A by linarith177  have absolute := abs.of_nonnegative with nonnegative178  have scaleReal := limitScale.real with widthReal179  have scalePositive := limitScale.positive with widthReal180  have radiusReal := scaledRadius.real at E, limitScale(B - A) with181    assumption, scaleReal182  have radiusPositive := scaledRadius.positive at E, limitScale(B - A) with183    assumption, scaleReal, positive, scalePositive184  have widthLess := abs.lt_limitScale with widthReal185  rw absolute at widthLess186  have productLess := realLess.mul_left_of_positive with187    widthReal, scaleReal, radiusReal, widthLess, radiusPositive188  have cancel := scaledRadius.cancel at E, limitScale(B - A) with189    assumption, scaleReal, scalePositive190  have commute := realMulValue.commutative with radiusReal, scaleReal191  rw [commute, cancel] at productLess192  have halfLess := half.lt_self with positive193  exact realLess.transitive with productLess, halfLess194195-- Convert two one-sided tagged-sum comparisons into the metric condition196-- used by HasRiemannIntegral.197theorem dist.lt_of_two_sided_error (S I H E : Real)198  requires upper : S ≤ I + H199  requires lower : I ≤ S + H200  requires small : H < E201  shows dist(S, I) < E202proof203  have upperShift := realLess.add_left at H, E, I with small204  have lowerShift := realLess.add_left at H, E, S with small205  have sumIH := realAddValue.real at I, H with *206  have sumIE := realAddValue.real at I, E with *207  have sumSH := realAddValue.real at S, H with *208  have sumSE := realAddValue.real at S, E with *209  have upperBall := realLe.transitive_less at S, I + H, I + E with210    assumption, sumIH, sumIE, upper, upperShift211  have shiftedLower := realLe.transitive_less at I, S + H, S + E with212    assumption, sumSH, sumSE, lower, lowerShift213  have lowerBall : I - E < S214    have cancelled := realSubValue.add_right_cancel at I, E with215      *{2}216    have shifted : (I - E) + E < S + E by rwa cancelled217    exact realLess.add_right_iff.forward with shifted218  have bounds : I - E < S ∧ S < I + E by refine ⟨lowerBall, upperBall⟩219  have near := openBall.order_characterization.backward with bounds220  obtain ⟨realS, bound⟩ := openBall.membership.forward with near221  exact bound222223-- FineSumDistance224theorem ContinuousOn.fine_sums_close (f : Set) (A B E : Real)225  requires ordered : A < B226  requires continuous : ContinuousOn(f, closedInterval(A, B))227  requires positive : 0 < E228  shows ∃ D ∈ ℝ, 0 < D ∧229    (∀ p, ∀ t, ∀ N ∈ ℕ, ∀ q, ∀ s, ∀ M ∈ ℕ,230      TaggedPartition(p, t, A, B, N) → FinePartition(p, A, B, N, D) →231        TaggedPartition(q, s, A, B, M) → FinePartition(q, A, B, M, D) →232          dist(riemannSum(f, p, t, N), riemannSum(f, q, s, M)) < E)233proof234  have function : f : ℝ → ℝ235    rcases continuous with ⟨function, subset, points⟩236    exact function237  have widthReal := realSubValue.real at B, A with *238  have scaleReal := limitScale.real with widthReal239  have scalePositive := limitScale.positive with widthReal240  have etaReal := scaledRadius.real at E, limitScale(B - A) with assumption, scaleReal241  have etaPositive := scaledRadius.positive at E, limitScale(B - A) with242    assumption, scaleReal, positive, scalePositive243  have halfPositive := half.positive with etaPositive244  obtain ⟨D, realD, positiveD, oscillation⟩ := ContinuousOn.fine_cell_oscillation with245    continuous, halfPositive246  witness D247  constructor248  . exact realD249  . constructor250    . exact positiveD251    . intros p t N naturalN q s M naturalM taggedP fineP taggedQ fineQ252      have typedN := nat.omega.backward with naturalN253      have typedM := nat.omega.backward with naturalM254      have bounds := FineCellOscillation.compare_fine_partitions at255        f, p, t, q, s, A, B, D, half(scaledRadius(E, limitScale(B - A))), N, M256        with function, oscillation, fineP, fineQ, taggedP, taggedQ257      have double := half.add_self with etaReal258      rw double at bounds259      rcases bounds with ⟨upper, lower⟩260      have weak := realLess.implies_le with ordered261      have small := scaledRadius.interval_error with weak, positive262      have partitionP : IntervalPartition(p, A, B, N)263        rcases taggedP with ⟨partition, tags, cells⟩264        exact partition265      have partitionQ : IntervalPartition(q, A, B, M)266        rcases taggedQ with ⟨partition, tags, cells⟩267        exact partition268      have pointsP : RealSequence(p)269        rcases partitionP with ⟨points, start, finish, cells⟩270        exact points271      have pointsQ : RealSequence(q)272        rcases partitionQ with ⟨points, start, finish, cells⟩273        exact points274      have tagsP : RealSequence(t)275        rcases taggedP with ⟨partition, tags, cells⟩276        exact tags277      have tagsQ : RealSequence(s)278        rcases taggedQ with ⟨partition, tags, cells⟩279        exact tags280      have sumP := riemannSum.real at f, p, t, N with function, pointsP, tagsP281      have sumQ := riemannSum.real at f, q, s, M with function, pointsQ, tagsQ282      have slack := realMulValue.real at scaledRadius(E, limitScale(B - A)), B - A283        with etaReal, widthReal284      exact dist.lt_of_two_sided_error285        with sumP, sumQ, slack, assumption, upper, lower, small286287-- ContinuousDyadicCauchy288theorem ContinuousOn.dyadic_sums_cauchy (f : Set) (A B : Real)289  requires ordered : A < B290  requires continuous : ContinuousOn(f, closedInterval(A, B))291  shows CauchySequence(dyadicRiemannSums(f, A, B))292proof293  have function : f : ℝ → ℝ294    rcases continuous with ⟨function, subset, points⟩295    exact function296  constructor297  . exact dyadicRiemannSums.sequence with function298  . intros E realE positiveE299    obtain ⟨D, realD, positiveD, close⟩ := ContinuousOn.fine_sums_close with ordered, continuous, positiveE300    have positiveWidth : 0 < B - A by linarith301    obtain ⟨K, naturalK, eventually⟩ :=302      dyadicRadius.eventually_scaled_below at B - A, D with positiveD303    witness K304    constructor305    . exact naturalK306    . intros m naturalM afterM n naturalN afterN307      have typedM := nat.omega.backward with naturalM308      have typedN := nat.omega.backward with naturalN309      have gridM := dyadicRiemannSums.fine_grid at A, B, m with ordered310      have gridN := dyadicRiemannSums.fine_grid at A, B, n with ordered311      rcases gridM with ⟨taggedM, fineM⟩312      rcases gridN with ⟨taggedN, fineN⟩313      have smallM := eventually with m, naturalM, afterM314      have smallN := eventually with n, naturalN, afterN315      have weakM := realLess.implies_le with smallM316      have weakN := realLess.implies_le with smallN317      have relaxedM := FinePartition.weaken with fineM, weakM318      have relaxedN := FinePartition.weaken with fineN, weakN319      have countM := dyadicCellCount.nat at succ(m) with320        Naturals.constructor.succ at m with assumption321      have countN := dyadicCellCount.nat at succ(n) with322        Naturals.constructor.succ at n with assumption323      have near := close with324        affinePoints(A, (B - A) * dyadicRadius(succ(m))),325        leftPartitionTags(affinePoints(A, (B - A) * dyadicRadius(succ(m)))),326        dyadicCellCount(succ(m)), nat.omega.forward at dyadicCellCount(succ(m)) with countM,327        affinePoints(A, (B - A) * dyadicRadius(succ(n))),328        leftPartitionTags(affinePoints(A, (B - A) * dyadicRadius(succ(n)))),329        dyadicCellCount(succ(n)), nat.omega.forward at dyadicCellCount(succ(n)) with countN,330        taggedM, relaxedM, taggedN, relaxedN331      have valueM := dyadicRiemannSums.value at f, A, B, m with function332      have valueN := dyadicRiemannSums.value at f, A, B, n with function333      have sequence := dyadicRiemannSums.sequence at f, A, B with function334      have realM := RealSequence.value at dyadicRiemannSums(f, A, B), m with sequence335      rw valueM at realM336      rw [valueM, valueN]337      have ballData : riemannSum(f, affinePoints(A, (B - A) * dyadicRadius(succ(m))), leftPartitionTags(affinePoints(A, (B - A) * dyadicRadius(succ(m)))), dyadicCellCount(succ(m))) ∈ ℝ ∧ dist(riemannSum(f, affinePoints(A, (B - A) * dyadicRadius(succ(m))), leftPartitionTags(affinePoints(A, (B - A) * dyadicRadius(succ(m)))), dyadicCellCount(succ(m))), riemannSum(f, affinePoints(A, (B - A) * dyadicRadius(succ(n))), leftPartitionTags(affinePoints(A, (B - A) * dyadicRadius(succ(n)))), dyadicCellCount(succ(n)))) < E338        refine ⟨realM, near⟩339      exact openBall.membership.backward with ballData340341theorem ContinuousOn.dyadic_sums_converge (f : Set) (A B : Real)342  requires ordered : A < B343  requires continuous : ContinuousOn(f, closedInterval(A, B))344  shows ∃ I ∈ ℝ, ConvergesTo(dyadicRiemannSums(f, A, B), I)345proof346  have cauchy := ContinuousOn.dyadic_sums_cauchy with ordered, continuous347  exact dyadicRiemannSums.converges_of_cauchy with ordered, continuous, cauchy348349-- ContinuousIntegral350theorem ContinuousOn.dyadic_limit_integral (f : Set) (A B I : Real)351  requires ordered : A < B352  requires continuous : ContinuousOn(f, closedInterval(A, B))353  requires limit : ConvergesTo(dyadicRiemannSums(f, A, B), I)354  shows HasRiemannIntegral(f, A, B, I)355proof356  have function : f : ℝ → ℝ357    rcases continuous with ⟨function, subset, points⟩358    exact function359  constructor360  . exact function361  . constructor362    . exact realLess.implies_le with ordered363    . intros E realE positiveE364      have typedE : Real(E) by exact realE365      have halfReal := half.real with typedE366      have halfPositive := half.positive with positiveE367      obtain ⟨D, realD, positiveD, close⟩ := ContinuousOn.fine_sums_close with368        ordered, continuous, halfPositive369      witness D370      constructor371      . exact realD372      . constructor373        . exact positiveD374        . intros p t N naturalN tagged fine375          have typedN := nat.omega.backward with naturalN376          obtain ⟨K, naturalK, fineEventually⟩ :=377            dyadicRadius.eventually_scaled_below at B - A, D with positiveD378          obtain ⟨H, naturalH, nearEventually⟩ := ConvergesTo.eventually with limit, halfPositive379          have typedK := nat.omega.backward with naturalK380          have typedH := nat.omega.backward with naturalH381          obtain ⟨J, naturalJ, afterK, afterH⟩ := nat.common_upper at K, H with382            *{2}383          have typedJ := nat.omega.backward with naturalJ384          obtain ⟨taggedJ, fineJ⟩ := dyadicRiemannSums.fine_grid at A, B, J with ordered385          have small := fineEventually with J, naturalJ, afterK386          have weak := realLess.implies_le with small387          have relaxed := FinePartition.weaken with fineJ, weak388          have count := dyadicCellCount.nat at succ(J) with389            Naturals.constructor.succ at J with assumption390          have near := close with p, t, N, naturalN,391            affinePoints(A, (B - A) * dyadicRadius(succ(J))),392            leftPartitionTags(affinePoints(A, (B - A) * dyadicRadius(succ(J)))),393            dyadicCellCount(succ(J)), nat.omega.forward at dyadicCellCount(succ(J)) with count,394            tagged, fine, taggedJ, relaxed395          have value := dyadicRiemannSums.value at f, A, B, J with function396          rw ← value at near397          have tail := nearEventually with J, naturalJ, afterH398          have partition : IntervalPartition(p, A, B, N)399            rcases tagged with ⟨partition, tags, cells⟩400            exact partition401          have points : RealSequence(p)402            rcases partition with ⟨points, start, finish, cells⟩403            exact points404          have tags : RealSequence(t)405            rcases tagged with ⟨partition, tags, cells⟩406            exact tags407          have sumReal := riemannSum.real at f, p, t, N with function, points, tags408          have sequence := dyadicRiemannSums.sequence at f, A, B with function409          have gridReal := RealSequence.value at dyadicRiemannSums(f, A, B), J with sequence410          have nearData : riemannSum(f, p, t, N) ∈ ℝ ∧ dist(riemannSum(f, p, t, N), dyadicRiemannSums(f, A, B)[J]) < half(E)411            refine ⟨sumReal, near⟩412          have ball := openBall.membership.backward with nearData413          have joined := openBall.triangle at riemannSum(f, p, t, N),414            dyadicRiemannSums(f, A, B)[J], I, half(E), half(E) with415              sumReal, gridReal, assumption, halfReal, halfReal, ball, tail416          have double := half.add_self with typedE417          rw double at joined418          obtain ⟨realSum, bound⟩ := openBall.membership.forward with joined419          exact bound420421theorem ContinuousOn.integrable_positive (f : Set) (A B : Real)422  requires ordered : A < B423  requires continuous : ContinuousOn(f, closedInterval(A, B))424  shows RiemannIntegrable(f, A, B)425proof426  obtain ⟨I, realI, limit⟩ := ContinuousOn.dyadic_sums_converge with ordered, continuous427  witness I428  constructor429  . exact realI430  . exact ContinuousOn.dyadic_limit_integral at f, A, B, I with431      ordered, continuous, limit432433theorem ContinuousOn.integrable_interval (f : Set) (A B : Real)434  requires ordered : A ≤ B435  requires continuous : ContinuousOn(f, closedInterval(A, B))436  shows RiemannIntegrable(f, A, B)437proof438  have alternatives : A = B ∨ ¬(A = B) by tauto439  cases alternatives with equal | different440  . have function : FunctionBetween(f, ℝ, ℝ)441      rcases continuous with ⟨function, subset, points⟩442      exact function443  rw ← equal444  exact RiemannIntegrable.point with function445  . have le := realLe.characterization.forward with ordered446    rcases le with ⟨realA, realB, subset⟩447    have proper : A ⊂ B by refine ⟨subset, different⟩448    have strict : A < B := realLess.characterization.backward with ⟨realA, realB, proper⟩449    exact ContinuousOn.integrable_positive with strict, continuous450451-- Section: IntegralValue452defunique riemannIntegral (f : Set, A B : Real) (I ∈ ℝ) :=453  (RiemannIntegrable(f, A, B) → HasRiemannIntegral(f, A, B, I)) ∧454  (¬RiemannIntegrable(f, A, B) → I = realZero)455proof456  have alternatives : RiemannIntegrable(f, A, B) ∨ ¬RiemannIntegrable(f, A, B) by tauto457  cases alternatives with integrable | absent458  . have exists := integrable459    obtain ⟨I, realI, integral⟩ := exists460    witness I461    constructor462    . exact realI463    . constructor464      . intro again465        exact integral466      . intro impossible467        exfalso468        exact impossible with integrable469  . witness realZero470    constructor471    . exact realZero.real472    . constructor473      . intro impossible474        exfalso475        exact absent with impossible476      . intro ignored477        rfl478479uniqueness480  intros I memberI first J memberJ second481  have alternatives : RiemannIntegrable(f, A, B) ∨ ¬RiemannIntegrable(f, A, B) by tauto482  cases alternatives with integrable | absent483  . have firstIntegral : HasRiemannIntegral(f, A, B, I)484      tauto485    have secondIntegral : HasRiemannIntegral(f, A, B, J) by tauto486    have ordered : A ≤ B487      rcases firstIntegral with ⟨function, order, control⟩488      exact order489    exact HasRiemannIntegral.unique_on_interval with *490  . have firstZero : I = realZero491      tauto492    have secondZero : J = realZero by tauto493    cc494495theorem riemannIntegral.integral (f : Set) (A B : Real)496  requires integrable : RiemannIntegrable(f, A, B)497  shows HasRiemannIntegral(f, A, B, riemannIntegral(f, A, B))498proof499  have selected := riemannIntegral.selected at f, A, B with *500  rcases selected with ⟨realValue, valid, outside⟩501  exact valid with integrable502503theorem riemannIntegral.eq_of_integral (f : Set) (A B I : Real)504  requires integral : HasRiemannIntegral(f, A, B, I)505  shows riemannIntegral(f, A, B) = I506proof507  have ordered : A ≤ B508    rcases integral with ⟨function, order, control⟩509    exact order510  have selected := riemannIntegral.selected at f, A, B with *511  rcases selected with ⟨realValue, valid, outside⟩512  have integrable : RiemannIntegrable(f, A, B)513    witness I514    constructor515    . settle with Real516    . exact integral517  have chosen := valid with integrable518  exact HasRiemannIntegral.unique_on_interval with ordered, chosen, integral519520theorem riemannIntegral.continuous (f : Set) (A B : Real)521  requires ordered : A ≤ B522  requires continuous : ContinuousOn(f, closedInterval(A, B))523  shows HasRiemannIntegral(f, A, B, riemannIntegral(f, A, B))524proof525  have integrable := ContinuousOn.integrable_interval with ordered, continuous526  exact riemannIntegral.integral with integrable527