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

Open in Workbench Download source

Imports

SequentialCompactness · FiniteSum · Intervals · ExtremeValue

Declarations

Source

1-- Real analysis: RiemannSums2-- 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.RiemannSums8import SequentialCompactness9import FiniteSum10import Intervals11import ExtremeValue1213-- Section: RiemannSums14predicate CauchySequence (u : Set) :=15  RealSequence(u) ∧16  (∀ E ∈ ℝ, 0 < E →17    ∃ N ∈ ℕ, ∀ m ∈ ℕ, N ≤ m →18      ∀ n ∈ ℕ, N ≤ n → uₘ ∈ openBall(uₙ, E))1920theorem nat.common_upper (N M : Nat)21  shows ∃ K ∈ ℕ, N ≤ K ∧ M ≤ K22proof23  have cases := Less.trichotomy at N, M with *24  cases cases with less | rest25  . witness M26    have naturalM := nat.omega.forward at M with assumption27    have le := Less.implies_LessEqual with less28    have refl := LessEqual.reflexive at M with assumption29    refine ⟨naturalM, le, refl⟩30  . cases rest with equal | greater31    . witness N32      have naturalN := nat.omega.forward at N with assumption33      have refl := LessEqual.reflexive at N with assumption34      have back : M ≤ N35        rw ← equal36        exact refl37      refine ⟨naturalN, refl, back⟩38    . witness N39      have naturalN := nat.omega.forward at N with assumption40      have refl := LessEqual.reflexive at N with assumption41      have le := Less.implies_LessEqual with greater42      refine ⟨naturalN, refl, le⟩4344theorem CauchySequence.converges_of_subsequence (u k : Set) (L : Real)45  requires cauchy : CauchySequence(u)46  requires increasing : StrictlyIncreasingNat(k)47  requires selected : ConvergesTo(subsequence(u, k), L)48  shows ConvergesTo(u, L)49proof50  rcases cauchy with ⟨sequence, control⟩51  constructor52  . exact sequence53  . intros E realE positive54    have typedE : Real(E) by exact realE55    have halfReal := half.real with typedE56    have halfPositive := half.positive with positive57    obtain ⟨N, naturalN, close⟩ :=58      control with half(E), halfPositive59    obtain ⟨M, naturalM, near⟩ := ConvergesTo.eventually with selected, halfPositive60    have typedN := nat.omega.backward with naturalN61    have typedM := nat.omega.backward with naturalM62    obtain ⟨K, naturalK, nLeK, mLeK⟩ :=63      nat.common_upper at N, M with *{2}64    have typedK := nat.omega.backward with naturalK65    have selectedNatural := FunctionBetween.apply_closed at66      k, ℕ, ℕ, K with StrictlyIncreasingNat.function at k with increasing,67        naturalK68    have typedSelected := nat.omega.backward with selectedNatural69    have indexLe := StrictlyIncreasingNat.index_le_value at k, K with increasing70    have selectedAfterN := LessEqual.transitive with typedN, typedK, typedSelected, nLeK, indexLe71    have closeToL := near with K, naturalK, mLeK72    have selectedValue := subsequence.value at u, k, K with73      sequence, increasing74    rw selectedValue at closeToL75    witness N76    constructor77    . exact naturalN78    . intros n naturalLittleN nAfterN79      have typedLittleN := nat.omega.backward with naturalLittleN80      have nearSelected := close with n, naturalLittleN, nAfterN,81        k[K], selectedNatural, selectedAfterN82      have realLittleN := RealSequence.value at u, n with sequence83      have realSelected := RealSequence.value at u, k[K] with sequence84      have joined := openBall.triangle at85        u[n], u[k[K]], L, half(E), half(E) with86          realLittleN, realSelected, assumption, halfReal, halfReal,87          nearSelected, closeToL88      have halves := half.add_self with typedE89      rwa halves at joined9091theorem CauchySequence.converges_in_interval (u : Set) (A B : Real)92  requires cauchy : CauchySequence(u)93  requires terms : TermsIn(u, closedInterval(A, B))94  shows ∃ L ∈ closedInterval(A, B), ConvergesTo(u, L)95proof96  have compact := closedInterval.sequentially_compact at A, B with97    *{2}98  rcases compact with ⟨reals, subsequences⟩99  have sequence : RealSequence(u)100    rcases cauchy with ⟨sequence, control⟩101    exact sequence102  obtain ⟨k, increasing, L, realL, member, selected⟩ :=103    subsequences with u, sequence, terms104  witness L105  constructor106  . exact member107  . exact CauchySequence.converges_of_subsequence at u, k, L with108      cauchy, increasing, selected109110-- RiemannSums111predicate IntervalPartition (p : Set) (A B : Real, N : Nat) :=112  RealSequence(p) ∧ p[0] = A ∧ p[N] = B ∧113  (∀ i ∈ ℕ, i < N → (p[i]:R) < (p[succ(i)]:R))114115predicate TaggedPartition (p t : Set) (A B : Real, N : Nat) :=116  IntervalPartition(p, A, B, N) ∧ RealSequence(t) ∧117  (∀ i ∈ ℕ, i < N → t[i] ∈ closedInterval(p[i], p[succ(i)]))118119-- A δ-fine partition uses a strict bound on every cell width. An explicit120-- bound is more useful in epsilon proofs than prematurely taking a maximum.121predicate FinePartition (p : Set) (A B : Real, N : Nat, D : Real) :=122  IntervalPartition(p, A, B, N) ∧ (0:R) < D ∧123  (∀ i ∈ ℕ, i < N → (p[succ(i)]:R) - (p[i]:R) < D)124125-- The successive widths form a real sequence even without monotonicity.126defgraph cellWidths (p : Set) (n ∈ ℕ) : ℝ :=127  realSubValue(p[succ(n)], p[n])128requires points : RealSequence(p)129proof130  have pointN := RealSequence.value at p, n with points131  have pointNext := RealSequence.value at p, succ(n) with points132  have width := realSubValue.real at p[succ(n)], p[n] with pointNext, pointN133  unfold Real at width134  exact width135136theorem IntervalPartition.cell (p : Set) (A B : Real, N i : Nat)137  requires partition : IntervalPartition(p, A, B, N)138  requires beforeEnd : i < N139  shows (p[i]:R) < (p[succ(i)]:R)140proof141  rcases partition with ⟨points, left, right, increasing⟩142  exact increasing with i, beforeEnd143144theorem FinePartition.cell_width (p : Set) (A B : Real, N i : Nat, D : Real)145  requires fine : FinePartition(p, A, B, N, D)146  requires beforeEnd : i < N147  shows (p[succ(i)]:R) - (p[i]:R) < D148proof149  rcases fine with ⟨partition, positive, widths⟩150  exact widths with i, beforeEnd151152theorem IntervalPartition.positive_width (p : Set) (A B : Real, N i : Nat)153  requires partition : IntervalPartition(p, A, B, N)154  requires beforeEnd : i < N155  shows (0:R) < (p[succ(i)]:R) - (p[i]:R)156proof157  have cell := IntervalPartition.cell with partition, beforeEnd158  rcases partition with ⟨sequence, left, right, increasing⟩159  have realI := RealSequence.value at p, i with sequence160  have realNext := RealSequence.value at p, succ(i) with sequence161  exact realLess.iff_pos_sub.forward with realI, realNext, cell162163theorem TaggedPartition.cell (p t : Set) (A B : Real, N i : Nat)164  requires tagged : TaggedPartition(p, t, A, B, N)165  requires beforeEnd : i < N166  shows t[i] ∈ closedInterval(p[i], p[succ(i)])167proof168  rcases tagged with ⟨partition, tags, cells⟩169  exact cells with i, beforeEnd170171theorem TaggedPartition.tag_bounds (p t : Set) (A B : Real, N i : Nat)172  requires tagged : TaggedPartition(p, t, A, B, N)173  requires beforeEnd : i < N174  shows (p[i]:R) ≤ (t[i]:R) ∧ (t[i]:R) ≤ (p[succ(i)]:R)175proof176  rcases tagged with ⟨partition, tags, cells⟩177  rcases partition with ⟨points, left, right, increasing⟩178  have pointI := RealSequence.value at p, i with points179  have pointNext := RealSequence.value at p, succ(i) with points180  have cell := cells with i, beforeEnd181  obtain ⟨tagReal, lower, upper⟩ := closedInterval.membership.forward with cell182  refine ⟨lower, upper⟩183184-- Every cell contribution is real; Replacement constructs the sequence graph.185defgraph riemannTerms (f p t : Set) (n ∈ ℕ) : ℝ :=186  realMulValue(f(t[n]), realSubValue(p[succ(n)], p[n]))187requires function : f : ℝ → ℝ188requires points : RealSequence(p)189requires tags : RealSequence(t)190proof191  have pointN := RealSequence.value with points192  have pointNext := RealSequence.value at p, succ(n) with points193  have tagReal := RealSequence.value with tags194  have tagMember : t[n] ∈ ℝ195    exact tagReal196  have valueMember := FunctionBetween.apply_closed with function, tagMember197  have valueReal : Real(f(t[n]))198    exact valueMember199  have difference := realSubValue.real with pointNext, pointN200  have product := realMulValue.real with valueReal, difference201  unfold call2 at product202  unfold realMulValue203  exact product204205-- Σ_{i<N} f(tᵢ) · (pᵢ₊₁ − pᵢ).206def riemannSum (f p t : Set, N : Nat) : Set :=207  realPartialSum(riemannTerms(f, p, t), N)208209theorem riemannSum.real (f p t : Set, N : Nat)210  requires function : f : ℝ → ℝ211  requires points : RealSequence(p)212  requires tags : RealSequence(t)213  shows Real(riemannSum(f, p, t, N))214proof215  have terms : RealSequence(riemannTerms(f, p, t))216    unfold RealSequence217    exact riemannTerms.function with function, points, tags218  unfold riemannSum219  exact realPartialSum.real with terms220221theorem riemannSum.zero (f p t : Set)222  shows riemannSum(f, p, t, 0) = (0:R)223proof224  unfold riemannSum225  exact realPartialSum.zero226227theorem riemannSum.succ (f p t : Set, N : Nat)228  requires function : f : ℝ → ℝ229  requires points : RealSequence(p)230  requires tags : RealSequence(t)231  shows riemannSum(f, p, t, succ(N)) =232    realAddValue(riemannSum(f, p, t, N),233      realMulValue(f(t[N]), realSubValue(p[succ(N)], p[N])))234proof235  unfold riemannSum236  have step := realPartialSum.succ at riemannTerms(f, p, t), N237  have value := riemannTerms.value with function, points, tags238  rwa value at step239240-- Section: DyadicRiemannSums241def affinePoint (A H : Real, n : Nat) → Set242  | A, H, zero => A243  | A, H, succ(k) => realAddValue(affinePoint(A, H, k), H)244245theorem affinePoint.real (A H : Real, n : Nat)246  shows Real(affinePoint(A, H, n))247proof248  induction n249  | zero =>250    rwa affinePoint251  | succ(k) using ih =>252    rw affinePoint253    have added := realAddValue.real at affinePoint(A, H, k), H with ih254    unfold call2 at added255    unfold realAddValue256    exact added257258theorem affinePoint.succ (A H : Real, n : Nat)259  shows affinePoint(A, H, succ(n)) = (affinePoint(A, H, n):R) + H260proof261  rw affinePoint262  unfold realAddValue263  unfold call2264  rfl265266defgraph affinePoints (A H : Real) (n ∈ ℕ) : ℝ := affinePoint(A, H, n)267proof268  have point := affinePoint.real at A, H, n with269    *{3}270  exact point271272theorem affinePoints.sequence (A H : Real)273  shows RealSequence(affinePoints(A, H))274proof275  unfold RealSequence276  exact affinePoints.function at A, H with *277278theorem affinePoints.zero (A H : Real)279  shows affinePoints(A, H)[0] = A280proof281  have value := affinePoints.value at A, H, 0 with282    *{2}, Naturals.constructor.zero283  rwa affinePoint at value284285theorem affinePoints.succ (A H : Real, n : Nat)286  shows affinePoints(A, H)[succ(n)] = (affinePoints(A, H)[n]:R) + H287proof288  have next := Naturals.constructor.succ at n289  have valueNext := affinePoints.value at A, H, succ(n) with290    *{2}, next291  have valueN := affinePoints.value at A, H, n with292    *{3}293  rw [affinePoint, ← valueN] at valueNext294  unfold realAddValue at valueNext295  simp [call2]296297theorem affinePoints.width (A H : Real, n : Nat)298  shows (affinePoints(A, H)[succ(n)]:R) - (affinePoints(A, H)[n]:R) = H299proof300  have value := affinePoints.value at A, H, n with301    *{3}302  have next := affinePoints.succ at A, H, n with303    *{3}304  rw next305  ring306307theorem affinePoints.partition (A B H : Real, N : Nat)308  requires positive : (0:R) < H309  requires endpoint : affinePoint(A, H, N) = B310  shows IntervalPartition(affinePoints(A, H), A, B, N)311proof312  constructor313  . exact affinePoints.sequence with *{2}314  . constructor315    . exact affinePoints.zero with *{2}316    . constructor317      . have value := affinePoints.value at A, H, N with318          *{3}319        rwa value320      . intros i naturalI before321        have typedI := nat.omega.backward with naturalI322        have width := affinePoints.width at A, H, i with323          *{2}, typedI324        have sequence := affinePoints.sequence at A, H with325          *{2}326        have first := RealSequence.value at affinePoints(A, H), i with sequence327        have next := RealSequence.value at affinePoints(A, H), succ(i) with sequence328        rw ← width at positive329        exact realLess.iff_pos_sub.backward with first, next, positive330331theorem affinePoints.fine (A B H D : Real, N : Nat)332  requires positive : (0:R) < H333  requires endpoint : affinePoint(A, H, N) = B334  requires small : H < D335  shows FinePartition(affinePoints(A, H), A, B, N, D)336proof337  constructor338  . exact affinePoints.partition with positive, endpoint339  . constructor340    . exact realLess.transitive at realZero, H, D with341        realZero.real, *{2}, positive, small342    . intros i naturalI before343      have typedI := nat.omega.backward with naturalI344      have width := affinePoints.width at A, H, i with345        *{2}, typedI346      rwa width347348-- Doubling the cell count while halving the step preserves the endpoint.349-- Express doubling by a Nat recursion so the induction does not depend on350-- arithmetic normalization of a symbolic index.351def doubleCellCount (n : Nat) → Nat352  | zero => zero353  | succ(k) => succ(succ(doubleCellCount(k)))354355def dyadicCellCount (n : Nat) → Nat356  | zero => succ(0)357  | succ(k) => doubleCellCount(dyadicCellCount(k))358359theorem doubleCellCount.nat (n : Nat)360  shows Nat(doubleCellCount(n))361proof362  induction n363  | zero =>364    rw doubleCellCount365    exact Naturals.constructor.zero366  | succ(k) using ih =>367    rw doubleCellCount368    have first := Naturals.constructor.succ with ih369    exact Naturals.constructor.succ with first370371theorem affinePoint.double_half (A H : Real, n : Nat)372  shows affinePoint(A, half(H), doubleCellCount(n)) = affinePoint(A, H, n)373proof374  induction n375  | zero =>376    rw [doubleCellCount, affinePoint, affinePoint]377    rfl378  | succ(k) using ih =>379    have doubleNat := doubleCellCount.nat at k380    have doubled := half.add_self at H381    rw [doubleCellCount, affinePoint.succ, affinePoint.succ, affinePoint.succ, ih]382    calc383      ((affinePoint(A, H, k):R) + half(H)) + half(H) =384        affinePoint(A, H, k) + (half(H) + half(H)) := by ring385      _ = affinePoint(A, H, k) + H := by simp [doubled]386387theorem half.mul_left (W R : Real)388  shows half(W * R) = W * half(R)389proof390  unfold half391  unfold fieldHalf392  ring393394theorem dyadicCellCount.nat (n : Nat)395  shows Nat(dyadicCellCount(n))396proof397  induction n398  | zero =>399    rw dyadicCellCount400    exact Naturals.constructor.succ with Naturals.constructor.zero401  | succ(k) using ih =>402    rw dyadicCellCount403    exact doubleCellCount.nat with ih404405theorem affinePoint.dyadic_endpoint (A B : Real, n : Nat)406  shows affinePoint(A, (B - A) * dyadicRadius(n), dyadicCellCount(n)) = B407proof408  induction n409  | zero =>410    rw [dyadicCellCount, dyadicRadius]411    have widthReal := realSubValue.real at B, A with *412    have unit := realMulValue.one_right with widthReal413    rw [unit, affinePoint.succ, affinePoint]414    ring415  | succ(k) using ih =>416    have widthReal := realSubValue.real at B, A with *417    have radiusReal := dyadicRadius.real at k418    have commuteHalf := half.mul_left with widthReal, radiusReal419    rwa [dyadicCellCount, dyadicRadius, ← commuteHalf, affinePoint.double_half]420421-- The (n+1)-st dyadic grid has mesh strictly below the n-th scale.422theorem affinePoints.dyadic_fine (A B : Real, n : Nat)423  requires ordered : A < B424  shows FinePartition(425    affinePoints(A, (B - A) * dyadicRadius(succ(n))), A, B,426    dyadicCellCount(succ(n)), (B - A) * dyadicRadius(n))427proof428  have widthReal := realSubValue.real at B, A with *429  have widthPositive := realLess.iff_pos_sub.forward with ordered430  have radiusReal := dyadicRadius.real at n431  have next := Naturals.constructor.succ at n432  have nextRadiusReal := dyadicRadius.real with next433  have nextPositive := dyadicRadius.positive with next434  have stepPositive := realMulValue.positive with widthPositive, nextPositive435  have smaller := dyadicRadius.strictly_decreasing at n436  have stepSmall := realLess.mul_left_of_positive with437    nextRadiusReal, radiusReal, widthReal, smaller, widthPositive438  have exactEndpoint := affinePoint.dyadic_endpoint at A, B, succ(n) with *439  exact affinePoints.fine with stepPositive, exactEndpoint, stepSmall440441-- PartitionExistence442predicate FineTaggedPartitionsExist (A B : Real) :=443  ∀ D ∈ ℝ, (0:R) < D →444    ∃ p, ∃ t, ∃ N ∈ ℕ,445      TaggedPartition(p, t, A, B, N) ∧ FinePartition(p, A, B, N, D)446447predicate FinePartitionsExist (A B : Real) :=448  ∀ D ∈ ℝ, (0:R) < D →449    ∃ p, ∃ N ∈ ℕ, FinePartition(p, A, B, N, D)450451-- Tags are obtained uniformly from any partition by choosing its left452-- endpoints, so the mesh construction does not depend on tag bookkeeping.453defgraph leftPartitionTags (p : Set) (n ∈ ℕ) : ℝ := p[n]454requires points : RealSequence(p)455proof456  have point := RealSequence.value at p, n with points457  unfold Real at point458  exact point459460theorem IntervalPartition.left_tagged (p : Set) (A B : Real, N : Nat)461  requires partition : IntervalPartition(p, A, B, N)462  shows TaggedPartition(p, leftPartitionTags(p), A, B, N)463proof464  rcases partition with ⟨points, left, right, increasing⟩465  constructor466  . refine ⟨points, left, right, increasing⟩467  . constructor468    . unfold RealSequence469      exact leftPartitionTags.function with points470    . intros i naturalI before471      have typedI := nat.omega.backward with naturalI472      have value := leftPartitionTags.value at p, i with points473      rw value474      have ordered := increasing with i, naturalI, before475      have pointI := RealSequence.value at p, i with points476      have pointNext := RealSequence.value at p, succ(i) with points477      have weak := realLess.implies_le with ordered478      exact closedInterval.left_mem with weak479480theorem FinePartitionsExist.tagged (A B : Real)481  requires fineExists : FinePartitionsExist(A, B)482  shows FineTaggedPartitionsExist(A, B)483proof484  intros D realD positiveD485  obtain ⟨p, N, naturalN, fine⟩ := fineExists with D, realD, positiveD486  rcases fine with ⟨partition, positive, widths⟩487  have tagged := IntervalPartition.left_tagged with partition488  witness p489  witness leftPartitionTags(p)490  witness N491  refine ⟨naturalN, tagged, _⟩492  refine ⟨partition, positive, widths⟩493494theorem FineTaggedPartitionsExist.untagged (A B : Real)495  requires taggedExists : FineTaggedPartitionsExist(A, B)496  shows FinePartitionsExist(A, B)497proof498  intros D realD positiveD499  obtain ⟨p, t, N, naturalN, tagged, fine⟩ :=500    taggedExists with D, realD, positiveD501  witness p502  witness N503  refine ⟨naturalN, fine⟩504505theorem FinePartition.weaken (p : Set) (A B : Real, N : Nat, D E : Real)506  requires fine : FinePartition(p, A, B, N, D)507  requires le : D ≤ E508  shows FinePartition(p, A, B, N, E)509proof510  rcases fine with ⟨partition, positive, widths⟩511  constructor512  . exact partition513  . constructor514    . exact realLess.transitive_le at realZero, D, E with515        realZero.real, *{2}, positive, le516    . intros i naturalI before517      have typedI := nat.omega.backward with naturalI518      have width := widths with i, naturalI, before519      have points : RealSequence(p)520        rcases partition with ⟨sequence, left, right, increasing⟩521        exact sequence522      have pointI := RealSequence.value at p, i with points523      have pointNext := RealSequence.value at p, succ(i) with points524      exact realLess.transitive_le with width, le525526-- One sufficiently fine partition satisfies two mesh requirements at once.527theorem FineTaggedPartitionsExist.common (A B D E : Real)528  requires cofinal : FineTaggedPartitionsExist(A, B)529  requires positiveD : (0:R) < D530  requires positiveE : (0:R) < E531  shows ∃ p, ∃ t, ∃ N ∈ ℕ,532    TaggedPartition(p, t, A, B, N) ∧533      FinePartition(p, A, B, N, D) ∧ FinePartition(p, A, B, N, E)534proof535  have comparable : D ≤ E ∨ ¬(D ≤ E) by tauto536  cases comparable with leDE | notLe537  . obtain ⟨p, t, N, naturalN, tagged, fineD⟩ :=538      cofinal with D, positiveD539    have fineE := FinePartition.weaken with fineD, leDE540    witness p541    witness t542    witness N543    refine ⟨naturalN, tagged, fineD, fineE⟩544  . have ltED := realLess.of_not_le with notLe545    have leED := realLess.implies_le with ltED546    obtain ⟨q, s, M, naturalM, taggedM, fineE⟩ :=547      cofinal with E, positiveE548    have fineD := FinePartition.weaken with fineE, leED549    witness q550    witness s551    witness M552    refine ⟨naturalM, taggedM, fineD, fineE⟩553554-- DyadicRiemannSums555defgraph dyadicRiemannSums (f : Set, A B : Real) (n ∈ ℕ) : ℝ :=556  riemannSum(f,557    affinePoints(A, (B - A) * dyadicRadius(succ(n))),558    leftPartitionTags(affinePoints(A, (B - A) * dyadicRadius(succ(n)))),559    dyadicCellCount(succ(n)))560requires function : f : ℝ → ℝ561proof562  have width := realSubValue.real at B, A with *563  have next := Naturals.constructor.succ at n564  have radius := dyadicRadius.real with next565  have step := realMulValue.real with width, radius566  have points := affinePoints.sequence at A, (B - A) * dyadicRadius(succ(n))567    with assumption, step568  have tags : RealSequence(leftPartitionTags(569      affinePoints(A, (B - A) * dyadicRadius(succ(n)))))570    unfold RealSequence571    exact leftPartitionTags.function with points572  have count := dyadicCellCount.nat with next573  have sum := riemannSum.real at f,574    affinePoints(A, (B - A) * dyadicRadius(succ(n))),575    leftPartitionTags(affinePoints(A, (B - A) * dyadicRadius(succ(n)))),576    dyadicCellCount(succ(n)) with function, points, tags577  exact sum578579theorem dyadicRiemannSums.sequence (f : Set) (A B : Real)580  requires function : f : ℝ → ℝ581  shows RealSequence(dyadicRiemannSums(f, A, B))582proof583  unfold RealSequence584  exact dyadicRiemannSums.function with function585586theorem dyadicRiemannSums.fine_grid (A B : Real, n : Nat)587  requires ordered : A < B588  shows TaggedPartition(589    affinePoints(A, (B - A) * dyadicRadius(succ(n))),590    leftPartitionTags(affinePoints(A, (B - A) * dyadicRadius(succ(n)))),591    A, B, dyadicCellCount(succ(n))) ∧592    FinePartition(593      affinePoints(A, (B - A) * dyadicRadius(succ(n))),594      A, B, dyadicCellCount(succ(n)), (B - A) * dyadicRadius(n))595proof596  have fine := affinePoints.dyadic_fine with ordered597  have partition : IntervalPartition(598      affinePoints(A, (B - A) * dyadicRadius(succ(n))),599      A, B, dyadicCellCount(succ(n)))600    rcases fine with ⟨partition, positive, widths⟩601    exact partition602  have tagged := IntervalPartition.left_tagged with partition603  refine ⟨tagged, fine⟩604605-- Section: Bounds606theorem cellWidths.telescoping (p : Set) (N : Nat)607  requires points : RealSequence(p)608  shows realPartialSum(cellWidths(p), N) = (p[N]:R) - (p[0]:R)609proof610  induction N611  | zero =>612    rw realPartialSum.zero613    have point0 := RealSequence.value at p, 0 with points614    ring615  | succ(k) using ih =>616    rw [realPartialSum.succ, ih]617    have width := cellWidths.value with points618    rw width619    have point0 := RealSequence.value with points620    have pointK := RealSequence.value with points621    have pointNext := RealSequence.value with points622    ring623624theorem IntervalPartition.sum_cell_widths (p : Set) (A B : Real, N : Nat)625  requires partition : IntervalPartition(p, A, B, N)626  shows realPartialSum(cellWidths(p), N) = B - A627proof628  rcases partition with ⟨points, left, right, increasing⟩629  have widths := cellWidths.telescoping with points630  rwa [left, right] at widths631632-- ConstantSums633theorem riemannSum.constant (p t : Set) (L : Real, N : Nat)634  requires points : RealSequence(p)635  requires tags : RealSequence(t)636  shows riemannSum(constantFunction(ℝ, ℝ, L), p, t, N) =637    L * ((p[N]:R) - (p[0]:R))638proof639  induction N640  | zero =>641    rw riemannSum.zero642    have point0 := RealSequence.value at p, 0 with points643    ring644  | succ(k) using ih =>645    have realL : L ∈ ℝ by simp [Real]646    have constant := constantFunction.function at ℝ, ℝ, L with realL647    have step := riemannSum.succ with constant, points, tags648    rw [step, ih]649    have tagReal := RealSequence.value with tags650    have tagMember : t[k] ∈ ℝ by exact tagReal651    have value := constantFunction.apply with tagMember, realL652    rw value653    have point0 := RealSequence.value with points654    have pointK := RealSequence.value with points655    have pointNext := RealSequence.value with points656    ring657658theorem IntervalPartition.constant_sum (p t : Set) (A B L : Real, N : Nat)659  requires partition : IntervalPartition(p, A, B, N)660  requires tags : RealSequence(t)661  shows riemannSum(constantFunction(ℝ, ℝ, L), p, t, N) = L * (B - A)662proof663  rcases partition with ⟨points, left, right, increasing⟩664  have total := riemannSum.constant at p, t, L, N with points, tags665  rwa [left, right] at total666667-- Integral668predicate HasRiemannIntegral (f : Set) (A B I : Real) :=669  FunctionBetween(f, ℝ, ℝ) ∧ A ≤ B ∧670  (∀ E ∈ ℝ, (0:R) < E →671    ∃ D ∈ ℝ, (0:R) < D ∧672      ∀ p, ∀ t, ∀ N ∈ ℕ,673        (TaggedPartition(p, t, A, B, N) →674          FinePartition(p, A, B, N, D) →675            dist(riemannSum(f, p, t, N), I) < E))676677predicate RiemannIntegrable (f : Set) (A B : Real) :=678  ∃ I ∈ ℝ, HasRiemannIntegral(f, A, B, I)679680-- The exact constant-sum identity gives the epsilon-delta theorem with any681-- positive mesh bound. No positivity of L is needed.682theorem HasRiemannIntegral.constant (A B L : Real)683  requires ordered : A ≤ B684  shows HasRiemannIntegral(constantFunction(ℝ, ℝ, L), A, B, L * (B - A))685proof686  unfold HasRiemannIntegral687  have realL : L ∈ ℝ by simp [Real]688  constructor689  . exact constantFunction.function with realL690  . constructor691    . exact ordered692    . intros E realE positiveE693      witness E694      constructor695      . exact realE696      . constructor697        . exact positiveE698        . intros p t N naturalN tagged fine699          rcases tagged with ⟨partition, tags, cells⟩700          have sum := IntervalPartition.constant_sum at p, t, A, B, L, N with701            partition, tags702          rw sum703          have difference := realSubValue.real at B, A with *704          have product := realMulValue.real at L, B - A with assumption, difference705          have same := dist.self with product706          rwa same707708theorem RiemannIntegrable.constant (A B L : Real)709  requires ordered : A ≤ B710  shows RiemannIntegrable(constantFunction(ℝ, ℝ, L), A, B)711proof712  unfold RiemannIntegrable713  have difference := realSubValue.real at B, A with *714  have product := realMulValue.real at L, B - A with assumption, difference715  witness L * (B - A)716  constructor717    exact product718  . exact HasRiemannIntegral.constant with ordered719720-- Extensionality721theorem riemannSum.ext (f g p t : Set, N : Nat)722  requires functionF : f : ℝ → ℝ723  requires functionG : g : ℝ → ℝ724  requires points : RealSequence(p)725  requires tags : RealSequence(t)726  requires values : ∀ X ∈ ℝ, f(X) = g(X)727  shows riemannSum(f, p, t, N) = riemannSum(g, p, t, N)728proof729  induction N730  | zero =>731    rw [riemannSum.zero, riemannSum.zero]732    rfl733  | succ(k) using ih =>734    have left := riemannSum.succ with functionF, points, tags735    have right := riemannSum.succ with functionG, points, tags736    rw [left, right, ih]737    have tagReal := RealSequence.value with tags738    have tagMember : t[k] ∈ ℝ by exact tagReal739    have value := values with t[k]740    rw value741    rfl742743-- An integral is unchanged when the functions agree everywhere on the reals.744theorem HasRiemannIntegral.congr (f g : Set) (A B I : Real)745  requires integral : HasRiemannIntegral(f, A, B, I)746  requires functionG : g : ℝ → ℝ747  requires values : ∀ X ∈ ℝ, f(X) = g(X)748  shows HasRiemannIntegral(g, A, B, I)749proof750  rcases integral with ⟨functionF, ordered, control⟩751  constructor752  . exact functionG753  . constructor754    . exact ordered755    . intros E realE positiveE756      obtain ⟨D, realD, positiveD, estimate⟩ :=757        control with E, realE, positiveE758      witness D759      constructor760      . exact realD761      . constructor762        . exact positiveD763        . intros p t N naturalN tagged fine764          have typedN : Nat(N) by exact nat.omega.backward at N with naturalN765          have bound := estimate with p, t, N, naturalN, tagged, fine766          rcases tagged with ⟨partition, tags, cells⟩767          rcases partition with ⟨points, left, right, increasing⟩768          have same := riemannSum.ext with functionF, functionG, points, tags, values769          rwa same at bound770771theorem RiemannIntegrable.congr (f g : Set) (A B : Real)772  requires integrable : RiemannIntegrable(f, A, B)773  requires functionG : g : ℝ → ℝ774  requires values : ∀ X ∈ ℝ, f(X) = g(X)775  shows RiemannIntegrable(g, A, B)776proof777  obtain ⟨I, realI, integral⟩ := integrable778  witness I779  constructor780  . exact realI781  . exact HasRiemannIntegral.congr at f, g, A, B, I with782      integral, functionG, values783784-- Bounds785theorem riemannSum.monotone_on_tags (f g p t : Set) (A B : Real, N : Nat)786  requires functionF : f : ℝ → ℝ787  requires functionG : g : ℝ → ℝ788  requires tagged : TaggedPartition(p, t, A, B, N)789  requires values : ∀ i ∈ ℕ, i < N →790    (f(t[i]):R) ≤ (g(t[i]):R)791  shows (riemannSum(f, p, t, N):R) ≤ (riemannSum(g, p, t, N):R)792proof793  have partitionCopy : IntervalPartition(p, A, B, N)794    rcases tagged with ⟨partition, tags, cells⟩795    exact partition796  rcases tagged with ⟨partition, tags, cells⟩797  rcases partition with ⟨points, left, right, increasing⟩798  have sequenceF : RealSequence(riemannTerms(f, p, t))799    unfold RealSequence800    exact riemannTerms.function with functionF, points, tags801  have sequenceG : RealSequence(riemannTerms(g, p, t))802    unfold RealSequence803    exact riemannTerms.function with functionG, points, tags804  have bounds : ∀ i ∈ ℕ, i < N →805    (riemannTerms(f, p, t)[i]:R) ≤ (riemannTerms(g, p, t)[i]:R)806    intros i naturalI before807    have typedI := nat.omega.backward with naturalI808    have tagReal := RealSequence.value at t, i with tags809    have tagMember : t[i] ∈ ℝ by exact tagReal810    have realF := FunctionBetween.apply_closed with functionF, tagMember811    have realG := FunctionBetween.apply_closed with functionG, tagMember812    have typedF : Real(f(t[i])) by exact realF813    have typedG : Real(g(t[i])) by exact realG814    have pointI := RealSequence.value at p, i with points815    have pointNext := RealSequence.value at p, succ(i) with points816    have widthReal := realSubValue.real with pointNext, pointI817    have widthPositive := IntervalPartition.positive_width with partitionCopy, before818    have widthNonnegative := realLess.implies_le with realZero.real, widthPositive819    have comparison := values with i, naturalI, before820    have scaled := realLe.mul_right_of_nonnegative with821      typedF, typedG, widthReal, comparison, widthNonnegative822    have leftTerm := riemannTerms.value at f, p, t, i with functionF, points, tags823    have rightTerm := riemannTerms.value at g, p, t, i with functionG, points, tags824    rw [leftTerm, rightTerm]825    unfold realMulValue826    unfold call2 at scaled827    exact scaled828  unfold riemannSum829  exact realPartialSum.monotone_prefix with sequenceF, sequenceG, bounds830831-- A tagged sum lies between the integrals of its constant lower and upper832-- bounds. Only the finitely many tag values need to satisfy the bounds.833theorem riemannSum.between_constants (f p t : Set) (A B L U : Real, N : Nat)834  requires function : f : ℝ → ℝ835  requires tagged : TaggedPartition(p, t, A, B, N)836  requires lower : ∀ i ∈ ℕ, i < N → L ≤ (f(t[i]):R)837  requires upper : ∀ i ∈ ℕ, i < N → (f(t[i]):R) ≤ U838  shows L * (B - A) ≤ (riemannSum(f, p, t, N):R) ∧839    (riemannSum(f, p, t, N):R) ≤ U * (B - A)840proof841  have partition : IntervalPartition(p, A, B, N)842    rcases tagged with ⟨cells, tags, bounds⟩843    exact cells844  have tags : RealSequence(t)845    rcases tagged with ⟨cells, sequence, bounds⟩846    exact sequence847  have realL : L ∈ ℝ by simp [Real]848  have realU : U ∈ ℝ by simp [Real]849  have constantL := constantFunction.function at ℝ, ℝ, L with realL850  have constantU := constantFunction.function at ℝ, ℝ, U with realU851  have lowerValues : ∀ i ∈ ℕ, i < N →852    (constantFunction(ℝ, ℝ, L)(t[i]):R) ≤ (f(t[i]):R)853    intros i naturalI before854    have typedI := nat.omega.backward with naturalI855    have tagReal := RealSequence.value at t, i with tags856    have tagMember : t[i] ∈ ℝ by exact tagReal857    have value := constantFunction.apply with tagMember, realL858    rw value859    exact lower with i, naturalI, before860  have upperValues : ∀ i ∈ ℕ, i < N →861    (f(t[i]):R) ≤ (constantFunction(ℝ, ℝ, U)(t[i]):R)862    intros i naturalI before863    have typedI := nat.omega.backward with naturalI864    have tagReal := RealSequence.value at t, i with tags865    have tagMember : t[i] ∈ ℝ by exact tagReal866    have value := constantFunction.apply with tagMember, realU867    rw value868    exact upper with i, naturalI, before869  have below := riemannSum.monotone_on_tags with constantL, function, tagged, lowerValues870  have above := riemannSum.monotone_on_tags with function, constantU, tagged, upperValues871  have sumL := IntervalPartition.constant_sum at p, t, A, B, L, N with872    partition, tags873  have sumU := IntervalPartition.constant_sum at p, t, A, B, U, N with874    partition, tags875  rw sumL at below876  rw sumU at above877  refine ⟨below, above⟩878879-- Section: DyadicSumConvergence880theorem IntervalPartition.strict_prefix (p : Set, n : Nat)881  requires sequence : RealSequence(p)882  shows (∀ i ∈ ℕ, i < succ(n) → (p[i]:R) < (p[succ(i)]:R)) →883    (p[0]:R) < (p[succ(n)]:R)884proof885  induction n886  | zero =>887    intro steps888    have zeroNatural := nat.omega.forward with Naturals.constructor.zero889    have before : 0 < succ(0)890      unfold Less891      exact LessEqual.reflexive at succ(0) with892        Naturals.constructor.succ at 0 with Naturals.constructor.zero893    exact steps with 0, zeroNatural, before894  | succ(k) using ih =>895    intro steps896    have naturalK := nat.omega.forward at k897    have prefix : ∀ i ∈ ℕ, i < succ(k) →898      (p[i]:R) < (p[succ(i)]:R)899      intros i naturalI before900      have typedI := nat.omega.backward with naturalI901      have below := Less.transitive_LessEqual at i, succ(k), succ(succ(k)) with902        typedI, Naturals.constructor.succ at k with assumption,903        Naturals.constructor.succ at succ(k) with904          Naturals.constructor.succ at k with assumption,905        before, LessEqual.successor at succ(k) with906          Naturals.constructor.succ at k with assumption907      exact steps with i, naturalI, below908    have first := ih with prefix909    have before : Less(succ(k), succ(succ(k)))910      unfold Less911      exact LessEqual.reflexive at succ(succ(k)) with912        Naturals.constructor.succ at succ(k) with913          Naturals.constructor.succ at k with assumption914    have last := steps with succ(k),915      nat.omega.forward at succ(k) with916        Naturals.constructor.succ at k with assumption, before917    have realZeroPoint := RealSequence.value at p, 0 with sequence918    have realMiddle := RealSequence.value at p, succ(k) with sequence919    have realLast := RealSequence.value at p, succ(succ(k)) with sequence920    exact realLess.transitive with realZeroPoint, realMiddle, realLast, first, last921922theorem IntervalPartition.positive_length (p : Set) (A B : Real, N : Nat)923  requires partition : IntervalPartition(p, A, B, N)924  requires nonzero : N ≠ 0925  shows A < B926proof927  have shape := natural.zero_or_successor at N928  cases shape with zero | successor929  . exfalso930    exact nonzero with zero931  . obtain ⟨k, naturalK, NShape⟩ := successor932    rcases partition with ⟨sequence, left, right, increasing⟩933    have steps : ∀ i ∈ ℕ, i < succ(k) →934      (p[i]:R) < (p[succ(i)]:R)935      intros i naturalI before936      rw ← NShape at before937      exact increasing with i, naturalI, before938    have strict := IntervalPartition.strict_prefix with sequence, steps939    rw NShape at right940    rwa [left, right] at strict941942theorem IntervalPartition.point_empty (p : Set) (A : Real, N : Nat)943  requires partition : IntervalPartition(p, A, A, N)944  shows N = 0945proof946  by_contra nonzero947  have strict := IntervalPartition.positive_length with partition, nonzero948  have contradiction := realLess.characterization.forward with strict949  exact RealLess.irreflexive with contradiction950951-- PartitionBounds952theorem nat.le_succ_cases (i k : Nat)953  requires bound : i ≤ succ(k)954  shows i ≤ k ∨ i = succ(k)955proof956  have alternatives : i ≤ k ∨ ¬(i ≤ k) by tauto957  cases alternatives with earlier | later958  . left959    exact earlier960  . have reverse := Less.of_not_LessEqual with later961    unfold Less at reverse962    have equal := LessEqual.antisymmetric with bound, reverse963    right964    exact equal965966-- Induct before introducing the sequence, so the same induction hypothesis967-- applies to all its shorter prefixes.968theorem IntervalPartition.prefix_mono_aux (n : Nat)969  shows ∀ p, RealSequence(p) →970    (∀ j ∈ ℕ, j < n → (p[j]:R) < (p[succ(j)]:R)) →971      (∀ i ∈ ℕ, i ≤ n → (p[i]:R) ≤ (p[n]:R))972proof973  induction n974  | zero =>975    intros p sequence steps i naturalI bound976    have typedI := nat.omega.backward with naturalI977    have zeroLe := Grace.Core.Nat.Order.LessEqual.zero with typedI978    have equal := LessEqual.antisymmetric with bound, zeroLe979    rw equal980    have pointZero := RealSequence.value at p, 0 with sequence981    exact realLe.reflexive with pointZero982  | succ(k) using ih =>983    intros p sequence steps i naturalI bound984    have typedI := nat.omega.backward with naturalI985    have naturalK := nat.omega.forward at k with assumption986    have prefix : ∀ j ∈ ℕ, j < k → (p[j]:R) < (p[succ(j)]:R)987      intros j naturalJ smaller988      have typedJ := nat.omega.backward with naturalJ989      have below := Less.transitive_LessEqual at j, k, succ(k) with990        typedJ, assumption, Naturals.constructor.succ at k with assumption,991        smaller, LessEqual.successor at k with assumption992      exact steps with j, naturalJ, below993    have before : k < succ(k)994      unfold Less995      exact LessEqual.reflexive at succ(k) with996        Naturals.constructor.succ at k with assumption997    have step := steps with k, naturalK, before998    have alternatives := nat.le_succ_cases with bound999    cases alternatives with earlier | last1000    . have prefixBound := ih with p, sequence, prefix, i, naturalI, earlier1001      have pointI := RealSequence.value at p, i with sequence1002      have pointK := RealSequence.value at p, k with sequence1003      have pointNext := RealSequence.value at p, succ(k) with sequence1004      have weakStep := realLess.implies_le with step1005      exact realLe.transitive with pointI, pointK, pointNext, prefixBound, weakStep1006    . rw last1007      have pointNext := RealSequence.value at p, succ(k) with sequence1008      exact realLe.reflexive with pointNext10091010theorem IntervalPartition.prefix_mono (p : Set, n : Nat)1011  requires sequence : RealSequence(p)1012  requires steps : ∀ j ∈ ℕ, j < n → (p[j]:R) < (p[succ(j)]:R)1013  shows ∀ i ∈ ℕ, i ≤ n → (p[i]:R) ≤ (p[n]:R)1014proof1015  exact IntervalPartition.prefix_mono_aux at n with p, sequence, steps10161017-- All used partition points remain between its declared endpoints.1018theorem IntervalPartition.point_bounds (p : Set) (A B : Real, N i : Nat)1019  requires partition : IntervalPartition(p, A, B, N)1020  requires bounded : i ≤ N1021  shows A ≤ (p[i]:R) ∧ (p[i]:R) ≤ B1022proof1023  rcases partition with ⟨sequence, start, finish, steps⟩1024  have zeroLe := Grace.Core.Nat.Order.LessEqual.zero at i1025  have prefix : ∀ j ∈ ℕ, j < i → (p[j]:R) < (p[succ(j)]:R)1026    intros j naturalJ before1027    have typedJ := nat.omega.backward with naturalJ1028    have below := Less.transitive_LessEqual with typedJ, before, bounded1029    exact steps with j, naturalJ, below1030  have lowerPrefix := IntervalPartition.prefix_mono with sequence, prefix1031  have upperPrefix := IntervalPartition.prefix_mono with sequence, steps1032  have lower := lowerPrefix with 0,1033    nat.omega.forward at 0 with Naturals.constructor.zero, zeroLe1034  have upper := upperPrefix with i, bounded1035  rw start at lower1036  rw finish at upper1037  refine ⟨lower, upper⟩10381039-- A whole cell, including any tag in it, belongs to the parent interval.1040theorem IntervalPartition.cell_subset (p : Set) (A B : Real, N i : Nat)1041  requires partition : IntervalPartition(p, A, B, N)1042  requires before : i < N1043  shows closedInterval(p[i], p[succ(i)]) ⊆ closedInterval(A, B)1044proof1045  have indexLe := Less.implies_LessEqual with before1046  have successorLe : succ(i) ≤ N by exact before1047  have leftBounds := IntervalPartition.point_bounds with partition, indexLe1048  have rightBounds := IntervalPartition.point_bounds with partition, successorLe1049  rcases leftBounds with ⟨left, upperLeft⟩1050  rcases rightBounds with ⟨lowerRight, right⟩1051  have points : RealSequence(p)1052    rcases partition with ⟨points, start, finish, steps⟩1053    exact points1054  have pointI := RealSequence.value at p, i with points1055  have pointNext := RealSequence.value at p, succ(i) with points1056  exact closedInterval.nested with pointI, pointNext, left, right10571058-- ContinuousSumBounds1059theorem ContinuousOn.closed_interval_value_bounds (f : Set) (A B : Real)1060  requires ordered : A ≤ B1061  requires continuous : ContinuousOn(f, closedInterval(A, B))1062  shows ∃ L ∈ ℝ, ∃ U ∈ ℝ,1063    ∀ X ∈ closedInterval(A, B), L ≤ (f(X):R) ∧1064      (f(X):R) ≤ U1065proof1066  obtain ⟨S, inMinimum, minimum⟩ := ContinuousOn.closed_interval_minimum with ordered, continuous1067  obtain ⟨T, inMaximum, maximum⟩ := ContinuousOn.closed_interval_maximum with ordered, continuous1068  have function : f : ℝ → ℝ1069    rcases continuous with ⟨function, subset, points⟩1070    exact function1071  have realS : S ∈ ℝ1072    obtain ⟨realS, lower, upper⟩ := closedInterval.membership.forward with inMinimum1073    exact realS1074  have realT : T ∈ ℝ1075    obtain ⟨realT, lower, upper⟩ := closedInterval.membership.forward with inMaximum1076    exact realT1077  have valueS := FunctionBetween.apply_closed with function, realS1078  have valueT := FunctionBetween.apply_closed with function, realT1079  witness f(S)1080  constructor1081  . exact valueS1082  . witness f(T)1083    constructor1084    . exact valueT1085    . intros X inInterval1086      have low := minimum with X, inInterval1087      have high := maximum with X, inInterval1088      refine ⟨low, high⟩10891090theorem riemannSum.continuous_bounds (f p t : Set) (A B : Real, N : Nat)1091  requires ordered : A ≤ B1092  requires continuous : ContinuousOn(f, closedInterval(A, B))1093  requires tagged : TaggedPartition(p, t, A, B, N)1094  shows ∃ L ∈ ℝ, ∃ U ∈ ℝ,1095    L * (B - A) ≤ (riemannSum(f, p, t, N):R) ∧1096      (riemannSum(f, p, t, N):R) ≤ U * (B - A)1097proof1098  obtain ⟨L, realL, U, realU, values⟩ := ContinuousOn.closed_interval_value_bounds with ordered, continuous1099  have function : f : ℝ → ℝ1100    rcases continuous with ⟨function, subset, points⟩1101    exact function1102  have partition : IntervalPartition(p, A, B, N)1103    rcases tagged with ⟨partition, tags, cells⟩1104    exact partition1105  have lower : ∀ i ∈ ℕ, i < N → L ≤ (f(t[i]):R)1106    intros i naturalI before1107    have typedI := nat.omega.backward with naturalI1108    have cell := TaggedPartition.cell with tagged, before1109    have subset := IntervalPartition.cell_subset with partition, before1110    have global := subset with t[i], cell1111    obtain ⟨lower, upper⟩ := values with t[i], global1112    exact lower1113  have upper : ∀ i ∈ ℕ, i < N → (f(t[i]):R) ≤ U1114    intros i naturalI before1115    have typedI := nat.omega.backward with naturalI1116    have cell := TaggedPartition.cell with tagged, before1117    have subset := IntervalPartition.cell_subset with partition, before1118    have global := subset with t[i], cell1119    have bounds := values with t[i], global1120    rcases bounds with ⟨lower, upper⟩1121    exact upper1122  witness L1123  constructor1124  . exact realL1125  . witness U1126    constructor1127    . exact realU1128    . exact riemannSum.between_constants at f, p, t, A, B, L, U, N with1129        function, tagged, lower, upper11301131-- DyadicSumBounds1132theorem dyadicRiemannSums.bounded (f : Set) (A B : Real)1133  requires ordered : A < B1134  requires continuous : ContinuousOn(f, closedInterval(A, B))1135  shows ∃ L ∈ ℝ, ∃ U ∈ ℝ,1136    TermsIn(dyadicRiemannSums(f, A, B), closedInterval(L, U))1137proof1138  have weak := realLess.implies_le with ordered1139  obtain ⟨lo, realLo, hi, realHi, values⟩ := ContinuousOn.closed_interval_value_bounds with weak, continuous1140  have function : f : ℝ → ℝ1141    rcases continuous with ⟨function, subset, points⟩1142    exact function1143  have typedLo : Real(lo) by exact realLo1144  have typedHi : Real(hi) by exact realHi1145  have width := realSubValue.real at B, A with *1146  have lowerReal := realMulValue.real with typedLo, width1147  have upperReal := realMulValue.real with typedHi, width1148  witness lo * (B - A)1149  constructor1150    exact lowerReal1151  . witness hi * (B - A)1152    constructor1153      exact upperReal1154      intros n naturalN1155      have typedN := nat.omega.backward with naturalN1156      obtain ⟨tagged, fine⟩ := dyadicRiemannSums.fine_grid with ordered1157      have partition : IntervalPartition(1158          affinePoints(A, (B - A) * dyadicRadius(succ(n))),1159          A, B, dyadicCellCount(succ(n)))1160        rcases tagged with ⟨partition, tags, cells⟩1161        exact partition1162      have points : RealSequence(1163          affinePoints(A, (B - A) * dyadicRadius(succ(n))))1164        rcases partition with ⟨points, start, finish, steps⟩1165        exact points1166      have lower : ∀ i ∈ ℕ, i < dyadicCellCount(succ(n)) →1167          lo ≤ (f(leftPartitionTags(1168            affinePoints(A, (B - A) * dyadicRadius(succ(n))))[i]):R)1169        intros i naturalI before1170        have typedI := nat.omega.backward with naturalI1171        have cell := TaggedPartition.cell with tagged, before1172        have subset := IntervalPartition.cell_subset with partition, before1173        have global := subset with1174          leftPartitionTags(affinePoints(A, (B - A) * dyadicRadius(succ(n))))[i], cell1175        have bounds := values with1176          leftPartitionTags(affinePoints(A, (B - A) * dyadicRadius(succ(n))))[i], global1177        rcases bounds with ⟨below, above⟩1178        exact below1179      have upper : ∀ j ∈ ℕ, j < dyadicCellCount(succ(n)) →1180          (f(leftPartitionTags(1181            affinePoints(A, (B - A) * dyadicRadius(succ(n))))[j]):R) ≤ hi1182        intros j naturalJ before1183        have typedI := nat.omega.backward with naturalJ1184        have cell := TaggedPartition.cell with tagged, before1185        have subset := IntervalPartition.cell_subset with partition, before1186        have global := subset with1187          leftPartitionTags(affinePoints(A, (B - A) * dyadicRadius(succ(n))))[j], cell1188        have bounds := values with1189          leftPartitionTags(affinePoints(A, (B - A) * dyadicRadius(succ(n))))[j], global1190        rcases bounds with ⟨below, above⟩1191        exact above1192      have bounded := riemannSum.between_constants with function, tagged, lower, upper1193      have value := dyadicRiemannSums.value at f, A, B, n with1194        function1195      rw ← value at bounded1196      have sequence := dyadicRiemannSums.sequence at f, A, B with1197        *{2}, function1198      have sumReal := RealSequence.value with sequence1199      have sumMember : dyadicRiemannSums(f, A, B)[n] ∈ ℝ by exact sumReal1200      have data : dyadicRiemannSums(f, A, B)[n] ∈ ℝ ∧ lo * (B - A) ≤ dyadicRiemannSums(f, A, B)[n] ∧ dyadicRiemannSums(f, A, B)[n] ≤ hi * (B - A)1201        rcases bounded with ⟨below, above⟩1202        refine ⟨sumMember, below, above⟩1203      exact closedInterval.membership.backward with data12041205-- DyadicSumConvergence1206theorem dyadicRiemannSums.converges_of_cauchy (f : Set) (A B : Real)1207  requires ordered : A < B1208  requires continuous : ContinuousOn(f, closedInterval(A, B))1209  requires cauchy : CauchySequence(dyadicRiemannSums(f, A, B))1210  shows ∃ I ∈ ℝ, ConvergesTo(dyadicRiemannSums(f, A, B), I)1211proof1212  obtain ⟨L, realL, U, realU, terms⟩ := dyadicRiemannSums.bounded with ordered, continuous1213  obtain ⟨I, inInterval, converges⟩ := CauchySequence.converges_in_interval with cauchy, terms1214  obtain ⟨realI, lower, upper⟩ := closedInterval.membership.forward with inInterval1215  witness I1216  refine ⟨realI, converges⟩1217