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

Open in Workbench Download source

Imports

Nat.Least · CommonRefinementComparison · RiemannSums · Nat.Order

Declarations

Source

1-- Real analysis: PartitionSplit2-- 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.PartitionSplit8import Nat.Least9import CommonRefinementComparison10import RiemannSums11import Nat.Order1213-- Section: PartitionSplit14theorem riemannSum.two_cell_left (f : Set) (A C B : Real)15  requires function : f : ℝ → ℝ16  shows riemannSum(f, twoCellPoints(A, C, B), twoCellPoints(A, C, B),17      succ(succ(0))) =18    f(A) * (C - A) + f(C) * (B - C)19proof20  have points := twoCellPoints.sequence at A, C, B with *21  have first := riemannSum.succ at f, twoCellPoints(A, C, B),22    twoCellPoints(A, C, B), 0 with function, points, points23  have second := riemannSum.succ at f, twoCellPoints(A, C, B),24    twoCellPoints(A, C, B), succ(0) with function, points, points25  rw riemannSum.zero at first26  rw twoCellPoints.zero at first27  rw twoCellPoints.one at first28  rw twoCellPoints.one at second29  rw twoCellPoints.two at second30  rw first at second31  rw second32  ring3334-- SumCongruence35theorem riemannSum.congr_cells (f p t q s : Set, N : Nat)36  requires function : f : ℝ → ℝ37  requires pointsP : RealSequence(p)38  requires pointsQ : RealSequence(q)39  requires tagsT : RealSequence(t)40  requires tagsS : RealSequence(s)41  requires cells : ∀ i ∈ ℕ, i < N →42    p[i] = q[i] ∧ p[succ(i)] = q[succ(i)] ∧ t[i] = s[i]43  shows riemannSum(f, p, t, N) = riemannSum(f, q, s, N)44proof45  have termsP : RealSequence(riemannTerms(f, p, t))46    unfold RealSequence47    exact riemannTerms.function with function, pointsP, tagsT48  have termsQ : RealSequence(riemannTerms(f, q, s))49    unfold RealSequence50    exact riemannTerms.function with function, pointsQ, tagsS51  have equalTerms : ∀ i ∈ ℕ, i < N →52      riemannTerms(f, p, t)[i] = riemannTerms(f, q, s)[i]53    intros i naturalI before54    have typedI := nat.omega.backward with naturalI55    obtain ⟨atI, atNext, atTag⟩ := cells with i, naturalI, before56    have termP := riemannTerms.value at f, p, t, i with function, pointsP, tagsT57    have termQ := riemannTerms.value at f, q, s, i with function, pointsQ, tagsS58    rw [termP, termQ, atI, atNext, atTag]59    rfl60  unfold riemannSum61  exact realPartialSum.eq_prefix with termsP, termsQ, equalTerms6263-- ShiftedRiemannSums64theorem riemannTerms.shifted (f p t : Set, n i : Nat)65  requires function : f : ℝ → ℝ66  requires points : RealSequence(p)67  requires tags : RealSequence(t)68  shows riemannTerms(f, shiftedRealSequence(p, n), shiftedRealSequence(t, n))[i] =69    shiftedRealSequence(riemannTerms(f, p, t), n)[i]70proof71  have shiftedP := shiftedRealSequence.sequence at p, n with points72  have shiftedT := shiftedRealSequence.sequence at t, n with tags73  have terms : RealSequence(riemannTerms(f, p, t))74    unfold RealSequence75    exact riemannTerms.function with function, points, tags76  have shiftedTerm := riemannTerms.value at77    f, shiftedRealSequence(p, n), shiftedRealSequence(t, n), i with78      function, shiftedP, shiftedT79  have originalTerm := riemannTerms.value at f, p, t, add(n, i) with80    function, points, tags81  have rhs := shiftedRealSequence.value at riemannTerms(f, p, t), n, i with terms82  have tag := shiftedRealSequence.value at t, n, i with tags83  have left := shiftedRealSequence.value at p, n, i with points84  have right := shiftedRealSequence.value at p, n, succ(i) with points85  rw [shiftedTerm, rhs, originalTerm, tag, left, right, add.succ_right]86  rfl8788theorem riemannSum.split_at (f p t : Set, n m : Nat)89  requires function : f : ℝ → ℝ90  requires points : RealSequence(p)91  requires tags : RealSequence(t)92  shows riemannSum(f, p, t, add(n, m)) =93    riemannSum(f, p, t, n) +94      riemannSum(f, shiftedRealSequence(p, n), shiftedRealSequence(t, n), m)95proof96  have shiftedP := shiftedRealSequence.sequence at p, n with points97  have shiftedT := shiftedRealSequence.sequence at t, n with tags98  have terms : RealSequence(riemannTerms(f, p, t))99    unfold RealSequence100    exact riemannTerms.function with function, points, tags101  have shiftedTerms : RealSequence(shiftedRealSequence(riemannTerms(f, p, t), n))102    exact shiftedRealSequence.sequence with terms103  have suffixTerms : RealSequence(riemannTerms(f, shiftedRealSequence(p, n), shiftedRealSequence(t, n)))104    unfold RealSequence105    exact riemannTerms.function with function, shiftedP, shiftedT106  have equal : ∀ i ∈ ℕ, i < m →107      shiftedRealSequence(riemannTerms(f, p, t), n)[i] =108        riemannTerms(f, shiftedRealSequence(p, n), shiftedRealSequence(t, n))[i]109    intros i naturalI before110    have typedI := nat.omega.backward with naturalI111    have value := riemannTerms.shifted at f, p, t, n, i with112      function, points, tags113    rw value114    rfl115  have equalSums := realPartialSum.eq_prefix with shiftedTerms, suffixTerms, equal116  have split := realPartialSum.split_at at riemannTerms(f, p, t), n, m with terms117  rw equalSums at split118  simp [riemannSum]119120-- ShiftedPartitions121theorem IntervalPartition.suffix (p : Set) (A B : Real, n m : Nat)122  requires partition : IntervalPartition(p, A, B, add(n, m))123  shows IntervalPartition(shiftedRealSequence(p, n), p[n], B, m)124proof125  rcases partition with ⟨points, start, finish, increasing⟩126  have shifted := shiftedRealSequence.sequence at p, n with points127  have atZero := shiftedRealSequence.value at p, n, 0 with points128  have atEnd := shiftedRealSequence.value at p, n, m with points129  have plusZero := add.right_unit at n130  rw plusZero at atZero131  constructor132  . exact shifted133  . constructor134    . exact atZero135    . constructor136      . rw atEnd137        exact finish138      . intros j naturalJ before139        have typedJ := nat.omega.backward with naturalJ140        have index := add.closed at j, n with typedJ141        have reflexive := LessEqual.reflexive at n with assumption142        have shiftedBefore := LessEqual.add_Less with reflexive, before143        have step := increasing with add(n, j), nat.omega.forward at add(n, j) with index, shiftedBefore144        have left := shiftedRealSequence.value at p, n, j with points145        have right := shiftedRealSequence.value at p, n, succ(j) with points146        rwa [left, right, add.succ_right]147148theorem TaggedPartition.suffix (p t : Set) (A B : Real, n m : Nat)149  requires tagged : TaggedPartition(p, t, A, B, add(n, m))150  shows TaggedPartition(shiftedRealSequence(p, n), shiftedRealSequence(t, n), p[n], B, m)151proof152  rcases tagged with ⟨partition, tags, cells⟩153  have points : RealSequence(p)154    rcases partition with ⟨points, start, finish, increasing⟩155    exact points156  have suffix := IntervalPartition.suffix with partition157  have shiftedTags := shiftedRealSequence.sequence at t, n with tags158  constructor159  . exact suffix160  . constructor161    . exact shiftedTags162    . intros j naturalJ before163      have typedJ := nat.omega.backward with naturalJ164      have index := add.closed at j, n with typedJ165      have reflexive := LessEqual.reflexive at n with assumption166      have shiftedBefore := LessEqual.add_Less with reflexive, before167      have cell := cells with add(n, j), nat.omega.forward at add(n, j) with index, shiftedBefore168      have tag := shiftedRealSequence.value at t, n, j with tags169      have left := shiftedRealSequence.value at p, n, j with points170      have right := shiftedRealSequence.value at p, n, succ(j) with points171      rwa [tag, left, right, add.succ_right]172173theorem FinePartition.suffix (p : Set) (A B D : Real, n m : Nat)174  requires fine : FinePartition(p, A, B, add(n, m), D)175  shows FinePartition(shiftedRealSequence(p, n), p[n], B, m, D)176proof177  rcases fine with ⟨partition, positive, widths⟩178  have points : RealSequence(p)179    rcases partition with ⟨points, start, finish, increasing⟩180    exact points181  have suffix := IntervalPartition.suffix with partition182  constructor183  . exact suffix184  . constructor185    . exact positive186    . intros j naturalJ before187      have typedJ := nat.omega.backward with naturalJ188      have index := add.closed at j, n with typedJ189      have reflexive := LessEqual.reflexive at n with assumption190      have shiftedBefore := LessEqual.add_Less with reflexive, before191      have bound := widths with add(n, j), nat.omega.forward at add(n, j) with index, shiftedBefore192      have left := shiftedRealSequence.value at p, n, j with points193      have right := shiftedRealSequence.value at p, n, succ(j) with points194      rwa [left, right, add.succ_right]195196theorem IntervalPartition.prefix (p : Set) (A B : Real, n m : Nat)197  requires partition : IntervalPartition(p, A, B, add(n, m))198  shows IntervalPartition(p, A, p[n], n)199proof200  rcases partition with ⟨points, start, finish, increasing⟩201  constructor202  . exact points203  . constructor204    . exact start205    . constructor206      . rfl207      . intros j naturalJ before208        have typedJ := nat.omega.backward with naturalJ209        have nLe := LessEqual.add_right at n, m with *210        have originalBefore := Less.transitive_LessEqual with before, nLe211        exact increasing with j, naturalJ, originalBefore212213theorem TaggedPartition.prefix (p t : Set) (A B : Real, n m : Nat)214  requires tagged : TaggedPartition(p, t, A, B, add(n, m))215  shows TaggedPartition(p, t, A, p[n], n)216proof217  rcases tagged with ⟨partition, tags, cells⟩218  have points : RealSequence(p)219    rcases partition with ⟨points, start, finish, increasing⟩220    exact points221  have pointN := RealSequence.value at p, n with points222  have prefix := IntervalPartition.prefix with partition223  constructor224  . exact prefix225  . constructor226    . exact tags227    . intros j naturalJ before228      have typedJ := nat.omega.backward with naturalJ229      have nLe := LessEqual.add_right at n, m with *230      have originalBefore := Less.transitive_LessEqual with before, nLe231      exact cells with j, naturalJ, originalBefore232233theorem FinePartition.prefix (p : Set) (A B D : Real, n m : Nat)234  requires fine : FinePartition(p, A, B, add(n, m), D)235  shows FinePartition(p, A, p[n], n, D)236proof237  rcases fine with ⟨partition, positive, widths⟩238  have points : RealSequence(p)239    rcases partition with ⟨points, start, finish, increasing⟩240    exact points241  have pointN := RealSequence.value at p, n with points242  have prefix := IntervalPartition.prefix with partition243  constructor244  . exact prefix245  . constructor246    . exact positive247    . intros j naturalJ before248      have typedJ := nat.omega.backward with naturalJ249      have nLe := LessEqual.add_right at n, m with *250      have originalBefore := Less.transitive_LessEqual with before, nLe251      exact widths with j, naturalJ, originalBefore252253-- PartitionSplit254theorem FinePartition.split_tagged_sum (f p t : Set) (A B D : Real, n m : Nat)255  requires function : f : ℝ → ℝ256  requires fine : FinePartition(p, A, B, add(n, m), D)257  requires tagged : TaggedPartition(p, t, A, B, add(n, m))258  shows FinePartition(p, A, p[n], n, D) ∧259    FinePartition(shiftedRealSequence(p, n), p[n], B, m, D) ∧260    TaggedPartition(p, t, A, p[n], n) ∧261    TaggedPartition(shiftedRealSequence(p, n), shiftedRealSequence(t, n), p[n], B, m) ∧262    riemannSum(f, p, t, add(n, m)) =263      (riemannSum(f, p, t, n):R) +264        (riemannSum(f, shiftedRealSequence(p, n), shiftedRealSequence(t, n), m):R)265proof266  have partition : IntervalPartition(p, A, B, add(n, m))267    rcases fine with ⟨partition, positive, widths⟩268    exact partition269  have points : RealSequence(p)270    rcases partition with ⟨points, start, finish, increasing⟩271    exact points272  have pointN := RealSequence.value at p, n with points273  have tags : RealSequence(t)274    rcases tagged with ⟨partitionT, tags, cells⟩275    exact tags276  have finePrefix := FinePartition.prefix with fine277  have fineSuffix := FinePartition.suffix with fine278  have taggedPrefix := TaggedPartition.prefix with tagged279  have taggedSuffix := TaggedPartition.suffix with tagged280  have sum := riemannSum.split_at at f, p, t, n, m with function, points, tags281  refine ⟨finePrefix, fineSuffix, taggedPrefix, taggedSuffix, sum⟩282283-- Section: IndexedInsertionSplit284def firstCellTailPoint (p : Set, C : Real, n : Nat) → Set285  | p, C, zero => C286  | p, C, succ(k) => p[succ(k)]287288def firstCellInsertedPoint (p : Set, C : Real, n : Nat) → Set289  | p, C, zero => p[0]290  | p, C, succ(k) => firstCellTailPoint(p, C, k)291292theorem firstCellTailPoint.real (p : Set) (C : Real, n : Nat)293  requires points : RealSequence(p)294  shows Real(firstCellTailPoint(p, C, n))295proof296  induction n297  | zero =>298    rwa firstCellTailPoint299  | succ(k) using ih =>300    rw firstCellTailPoint301    exact RealSequence.value with points302303theorem firstCellInsertedPoint.real (p : Set) (C : Real, n : Nat)304  requires points : RealSequence(p)305  shows Real(firstCellInsertedPoint(p, C, n))306proof307  induction n308  | zero =>309    rw firstCellInsertedPoint310    exact RealSequence.value with points311  | succ(k) using ih =>312    rw firstCellInsertedPoint313    exact firstCellTailPoint.real with points314315defgraph firstCellInsertedPoints (p : Set, C : Real) (n ∈ ℕ) : ℝ :=316  firstCellInsertedPoint(p, C, n)317requires points : RealSequence(p)318proof319  have typedN := nat.omega.backward with member320  exact firstCellInsertedPoint.real with points321322theorem firstCellInsertedPoints.sequence (p : Set, C : Real)323  requires points : RealSequence(p)324  shows RealSequence(firstCellInsertedPoints(p, C))325proof326  unfold RealSequence327  exact firstCellInsertedPoints.function with points328329theorem firstCellInsertedPoints.zero (p : Set, C : Real)330  requires points : RealSequence(p)331  shows firstCellInsertedPoints(p, C)[0] = p[0]332proof333  have value := firstCellInsertedPoints.value at p, C, 0 with points334  rwa firstCellInsertedPoint at value335336theorem firstCellInsertedPoints.one (p : Set, C : Real)337  requires points : RealSequence(p)338  shows firstCellInsertedPoints(p, C)[succ(0)] = C339proof340  have value := firstCellInsertedPoints.value at p, C, succ(0) with points341  rwa [firstCellInsertedPoint, firstCellTailPoint] at value342343theorem firstCellInsertedPoints.later (p : Set, C : Real, k : Nat)344  requires points : RealSequence(p)345  shows firstCellInsertedPoints(p, C)[succ(succ(k))] = p[succ(k)]346proof347  have value := firstCellInsertedPoints.value at p, C, succ(succ(k)) with points348  rwa [firstCellInsertedPoint, firstCellTailPoint] at value349350theorem IntervalPartition.insert_first_cell (p : Set) (A B C : Real, K : Nat)351  requires partition : IntervalPartition(p, A, B, succ(K))352  requires left : A < C353  requires right : C < (p[succ(0)]:R)354  shows IntervalPartition(firstCellInsertedPoints(p, C), A, B, succ(succ(K)))355proof356  rcases partition with ⟨points, start, finish, increasing⟩357  have inserted := firstCellInsertedPoints.sequence at p, C with points358  constructor359  . exact inserted360  . constructor361    . have atZero := firstCellInsertedPoints.zero at p, C with points362      rwa atZero363    . constructor364      . have atEnd := firstCellInsertedPoints.later at p, C, K with points365        rwa atEnd366      . intros i naturalI before367        have typedI := nat.omega.backward with naturalI368        have shape := natural.zero_or_successor with typedI369        cases shape with zero | successor370        . rw [zero, firstCellInsertedPoints.zero, firstCellInsertedPoints.one, start]371          exact left372        . obtain ⟨j, naturalJ, isNext⟩ := successor373          rw isNext374          have jShape := natural.zero_or_successor with naturalJ375          cases jShape with zero | successorJ376          . rw [zero, firstCellInsertedPoints.one, firstCellInsertedPoints.later]377            exact right378          . obtain ⟨k, naturalK, jNext⟩ := successorJ379            rw jNext380            rw [isNext, jNext] at before381            have succK := Naturals.constructor.succ at K with assumption382            have shiftedBefore : Less(add(succ(k), 1), add(succ(K), 1)) by rwa [add.right_one, add.right_one]383            have oldBefore : Less(succ(k), succ(K)) by exact Less.add_right_cancel with shiftedBefore384            have old := increasing with succ(k),385              nat.omega.forward at succ(k) with Naturals.constructor.succ at k with naturalK,386              oldBefore387            rwa [firstCellInsertedPoints.later, firstCellInsertedPoints.later]388389-- FirstCellFine390theorem FinePartition.insert_first_cell (p : Set) (A B C D : Real, K : Nat)391  requires fine : FinePartition(p, A, B, succ(K), D)392  requires left : A < C393  requires right : C < (p[succ(0)]:R)394  shows FinePartition(firstCellInsertedPoints(p, C), A, B, succ(succ(K)), D)395proof396  rcases fine with ⟨partition, positive, widths⟩397  have points : RealSequence(p)398    rcases partition with ⟨points, start, finish, increasing⟩399    exact points400  have pointZero := RealSequence.value with points401  have pointOne := RealSequence.value at p, succ(0) with points402  have start : p[0] = A403    rcases partition with ⟨points, start, finish, increasing⟩404    exact start405  have beforeZero : Less(0, succ(K))406    unfold Less407    have zeroLe := Grace.Core.Nat.Order.LessEqual.zero at K with assumption408    have shifted := LessEqual.add_monotone_right at 0, K, 1 with zeroLe409    simp [add.right_one, add] at shifted410    exact shifted411  have originalWidth := widths with 0,412    nat.omega.forward at 0 with Naturals.constructor.zero, beforeZero413  rw start at originalWidth414  have firstCompare := realSubValue.lt_left at C, p[succ(0)], A with right415  have firstWidth : C - A < D by exact realLess.transitive with firstCompare, originalWidth416  have weakLeft := realLess.implies_le with left417  have self := realLe.reflexive with pointOne418  have secondCompare := realSubValue.le with self, weakLeft419  have secondWidth : (p[succ(0)]:R) - C < D by exact realLe.transitive_less with secondCompare, originalWidth420  have inserted := IntervalPartition.insert_first_cell with partition, left, right421  constructor422  . exact inserted423  . constructor424    . exact positive425    . intros i naturalI before426      have typedI := nat.omega.backward with naturalI427      have shape := natural.zero_or_successor with typedI428      cases shape with zero | successor429      . rw [zero, firstCellInsertedPoints.zero, firstCellInsertedPoints.one, start]430        exact firstWidth431      . obtain ⟨j, naturalJ, isNext⟩ := successor432        rw isNext433        have jShape := natural.zero_or_successor with naturalJ434        cases jShape with zero | successorJ435        . rw [zero, firstCellInsertedPoints.one, firstCellInsertedPoints.later]436          exact secondWidth437        . obtain ⟨k, naturalK, jNext⟩ := successorJ438          rw jNext439          rw [isNext, jNext] at before440          have succK := Naturals.constructor.succ at K with assumption441          have succk := Naturals.constructor.succ with naturalK442          have shiftedBefore : Less(add(succ(k), 1), add(succ(K), 1)) by rwa [add.right_one, add.right_one]443          have oldBefore := Less.add_right_cancel with shiftedBefore444          have old := widths with succ(k),445            nat.omega.forward at succ(k) with succk, oldBefore446          rwa [firstCellInsertedPoints.later, firstCellInsertedPoints.later]447448theorem FinePartition.insert_first_cell_tagged (p : Set) (A B C D : Real, K : Nat)449  requires fine : FinePartition(p, A, B, succ(K), D)450  requires left : A < C451  requires right : C < (p[succ(0)]:R)452  shows TaggedPartition(firstCellInsertedPoints(p, C),453      leftPartitionTags(firstCellInsertedPoints(p, C)), A, B, succ(succ(K))) ∧454    FinePartition(firstCellInsertedPoints(p, C), A, B, succ(succ(K)), D)455proof456  have inserted := FinePartition.insert_first_cell with fine, left, right457  have partition : IntervalPartition(firstCellInsertedPoints(p, C), A, B, succ(succ(K)))458    rcases inserted with ⟨partition, positive, widths⟩459    exact partition460  have tagged := IntervalPartition.left_tagged with partition461  refine ⟨tagged, inserted⟩462463-- IndexedInsertion464def prependRealPoint (A : Real, u : Set, n : Nat) → Set465  | A, u, zero => A466  | A, u, succ(j) => u[j]467468theorem prependRealPoint.real (A : Real, u : Set, n : Nat)469  requires sequence : RealSequence(u)470  shows Real(prependRealPoint(A, u, n))471proof472  induction n473  | zero =>474    rwa prependRealPoint475  | succ(j) using ih =>476    rw prependRealPoint477    exact RealSequence.value with sequence478479defgraph prependRealSequence (A : Real, u : Set) (n ∈ ℕ) : ℝ :=480  prependRealPoint(A, u, n)481requires sequence : RealSequence(u)482proof483  exact prependRealPoint.real with sequence484485theorem prependRealSequence.sequence (A : Real, u : Set)486  requires sequence : RealSequence(u)487  shows RealSequence(prependRealSequence(A, u))488proof489  unfold RealSequence490  exact prependRealSequence.function with sequence491492theorem prependRealSequence.zero (A : Real, u : Set)493  requires sequence : RealSequence(u)494  shows prependRealSequence(A, u)[0] = A495proof496  have value := prependRealSequence.value at A, u, 0 with sequence497  rwa prependRealPoint at value498499theorem prependRealSequence.succ (A : Real, u : Set, j : Nat)500  requires sequence : RealSequence(u)501  shows prependRealSequence(A, u)[succ(j)] = u[j]502proof503  have value := prependRealSequence.value at A, u, succ(j) with sequence504  rwa prependRealPoint at value505506-- Primitive recursion on the cell index. The unchanged first point is507-- prepended to an insertion in the shifted tail.508def indexedInsertedPoints (p : Set, C : Real, k : Nat) → Set509  | p, C, zero => firstCellInsertedPoints(p, C)510  | p, C, succ(j) =>511      prependRealSequence(p[0],512        indexedInsertedPoints(shiftedRealSequence(p, succ(0)), C, j))513514theorem indexedInsertedPoints.sequence_aux (k : Nat)515  shows ∀ p, ∀ C ∈ ℝ,516    RealSequence(p) → RealSequence(indexedInsertedPoints(p, C, k))517proof518  induction k519  | zero =>520    intros p C realC points521    rw indexedInsertedPoints522    exact firstCellInsertedPoints.sequence with points523  | succ(j) using ih =>524    intros p C realC points525    rw indexedInsertedPoints526    have pointZero := RealSequence.value with points527    have shifted := shiftedRealSequence.sequence at p, succ(0) with points528    have recursive := ih with shiftedRealSequence(p, succ(0)), C, realC, shifted529    exact prependRealSequence.sequence with recursive530531theorem indexedInsertedPoints.sequence (p : Set) (C : Real, k : Nat)532  requires points : RealSequence(p)533  shows RealSequence(indexedInsertedPoints(p, C, k))534proof535  have realC : C ∈ ℝ536    have typedC : Real(C) by assumption537    exact typedC538  exact indexedInsertedPoints.sequence_aux at k with p, C, realC, points539540theorem indexedInsertedPoints.zero (p : Set) (C : Real, k : Nat)541  requires points : RealSequence(p)542  shows indexedInsertedPoints(p, C, k)[0] = p[0]543proof544  induction k545  | zero =>546    rw indexedInsertedPoints547    exact firstCellInsertedPoints.zero with points548  | succ(j) using ih =>549    rw indexedInsertedPoints550    have pointZero := RealSequence.value with points551    have shifted := shiftedRealSequence.sequence at p, succ(0) with points552    have recursive := indexedInsertedPoints.sequence at553      shiftedRealSequence(p, succ(0)), C, j with shifted554    exact prependRealSequence.zero with recursive555556theorem indexedInsertedPoints.successor (p : Set) (C : Real, k j : Nat)557  requires points : RealSequence(p)558  shows indexedInsertedPoints(p, C, succ(k))[succ(j)] =559    indexedInsertedPoints(shiftedRealSequence(p, succ(0)), C, k)[j]560proof561  rw indexedInsertedPoints562  have pointZero := RealSequence.value at p, 0 with points563  have shifted := shiftedRealSequence.sequence at p, succ(0) with points564  have recursive := indexedInsertedPoints.sequence at565    shiftedRealSequence(p, succ(0)), C, k with shifted566  exact prependRealSequence.succ with recursive567568theorem indexedInsertedPoints.inserted (p : Set) (C : Real, k : Nat)569  requires points : RealSequence(p)570  shows indexedInsertedPoints(p, C, k)[succ(k)] = C571proof572  induction k generalizing p573  | zero =>574    intros p points575    rw indexedInsertedPoints576    exact firstCellInsertedPoints.one at p, C with points577  | succ(j) using ih =>578    intros p points579    have shifted := shiftedRealSequence.sequence at p, succ(0) with points580    have step := indexedInsertedPoints.successor at p, C, j, succ(j) with points581    have result := ih with shiftedRealSequence(p, succ(0)), shifted582    rwa result at step583584theorem indexedInsertedPoints.after_inserted (p : Set) (C : Real, k : Nat)585  requires points : RealSequence(p)586  shows indexedInsertedPoints(p, C, k)[succ(succ(k))] = p[succ(k)]587proof588  induction k generalizing p589  | zero =>590    intros p points591    rw indexedInsertedPoints592    exact firstCellInsertedPoints.later with points593  | succ(j) using ih =>594    intros p points595    have shifted := shiftedRealSequence.sequence at p, succ(0) with points596    have step := indexedInsertedPoints.successor at p, C, j, succ(succ(j)) with points597    have result := ih with shiftedRealSequence(p, succ(0)), shifted598    rw result at step599    have value := shiftedRealSequence.value at p, succ(0), succ(j) with points600    rw value at step601    simp [add] at step602    exact step603604-- PrependPartitions605theorem IntervalPartition.prepend (q : Set) (A X B : Real, N : Nat)606  requires tail : IntervalPartition(q, X, B, N)607  requires left : A < X608  shows IntervalPartition(prependRealSequence(A, q), A, B, succ(N))609proof610  rcases tail with ⟨points, start, finish, increasing⟩611  have prepended := prependRealSequence.sequence at A, q with points612  constructor613  . exact prepended614  . constructor615    . exact prependRealSequence.zero at A, q with points616    . constructor617      . have endPoint := prependRealSequence.succ at A, q, N with points618        rwa endPoint619      . intros i naturalI before620        have typedI := nat.omega.backward with naturalI621        have shape := natural.zero_or_successor with typedI622        cases shape with zero | successor623        . rw [zero, prependRealSequence.zero, prependRealSequence.succ, start]624          exact left625        . obtain ⟨j, naturalJ, isNext⟩ := successor626          rw isNext at before627          have beforeTail : Less(j, N)628            have shifted : Less(add(j, 1), add(N, 1)) by rwa [add.right_one, add.right_one]629            exact Less.add_right_cancel with shifted630          have old := increasing with j, nat.omega.forward at j with naturalJ, beforeTail631          rwa [isNext, prependRealSequence.succ, prependRealSequence.succ]632633theorem FinePartition.prepend (q : Set) (A X B D : Real, N : Nat)634  requires tail : FinePartition(q, X, B, N, D)635  requires left : A < X636  requires width : X - A < D637  shows FinePartition(prependRealSequence(A, q), A, B, succ(N), D)638proof639  rcases tail with ⟨partition, positive, widths⟩640  have points : RealSequence(q)641    rcases partition with ⟨points, start, finish, increasing⟩642    exact points643  have start : q[0] = X644    rcases partition with ⟨points, start, finish, increasing⟩645    exact start646  have prepended := IntervalPartition.prepend with partition, left647  constructor648  . exact prepended649  . constructor650    . exact positive651    . intros i naturalI before652      have typedI := nat.omega.backward with naturalI653      have shape := natural.zero_or_successor with typedI654      cases shape with zero | successor655      . rw [zero, prependRealSequence.zero, prependRealSequence.succ, start]656        exact width657      . obtain ⟨j, naturalJ, isNext⟩ := successor658        rw isNext at before659        have beforeTail : Less(j, N)660          have shifted : Less(add(j, 1), add(N, 1)) by rwa [add.right_one, add.right_one]661          exact Less.add_right_cancel with shifted662        have old := widths with j, nat.omega.forward at j with naturalJ, beforeTail663        rwa [isNext, prependRealSequence.succ, prependRealSequence.succ]664665-- IndexedPartition666theorem natural.zero_before_successor (K : Nat)667  shows Less(0, succ(K))668proof669  unfold Less670  have zeroLe := Grace.Core.Nat.Order.LessEqual.zero at K with assumption671  have shifted := LessEqual.add_monotone_right at 0, K, 1 with zeroLe672  simp [add.right_one, add] at shifted673  exact shifted674675theorem FinePartition.insert_indexed (p : Set) (A B C D : Real, k L : Nat)676  requires fine : FinePartition(p, A, B, succ(add(k, L)), D)677  requires left : (p[k]:R) < C678  requires right : C < (p[succ(k)]:R)679  shows FinePartition(indexedInsertedPoints(p, C, k), A, B,680    succ(succ(add(k, L))), D)681proof682  induction k generalizing p A683  | zero =>684    intros p A realA fine left right685    have start : p[0] = A686      rcases fine with ⟨partition, positive, widths⟩687      rcases partition with ⟨points, start, finish, increasing⟩688      exact start689    rw start at left690    rw indexedInsertedPoints691    rw add.left_unit at fine692    rw add.left_unit693    exact FinePartition.insert_first_cell at p, A, B, C, D, L with fine, left, right694  | succ(j) using ih =>695    intros p A realA fine left right696    have points : RealSequence(p)697      rcases fine with ⟨partition, positive, widths⟩698      rcases partition with ⟨points, start, finish, increasing⟩699      exact points700    have start : p[0] = A701      rcases fine with ⟨partition, positive, widths⟩702      rcases partition with ⟨points, start, finish, increasing⟩703      exact start704    have before : Less(0, succ(add(succ(j), L)))705      apply natural.zero_before_successor706    have first : (p[0]:R) < (p[succ(0)]:R)707      rcases fine with ⟨partition, positive, widths⟩708      rcases partition with ⟨points, start, finish, increasing⟩709      exact increasing with 0, nat.omega.forward at 0 with Naturals.constructor.zero, before710    have original : FinePartition(p, A, B, add(succ(0), succ(add(j, L))), D)711      rw [add, add]712      rwa add at fine713    have suffix := FinePartition.suffix with original714    have leftValue := shiftedRealSequence.value at p, succ(0), j with points715    have rightValue := shiftedRealSequence.value at p, succ(0), succ(j) with points716    simp [add] at leftValue717    simp [add] at rightValue718    rw <- leftValue at left719    rw <- rightValue at right720    have pointOne := RealSequence.value at p, succ(0) with points721    have inserted := ih with shiftedRealSequence(p, succ(0)), p[succ(0)], pointOne, suffix, left, right722    have firstWidth : (p[succ(0)]:R) - A < D723      rcases fine with ⟨partition, positive, widths⟩724      have width := widths with 0, nat.omega.forward at 0 with Naturals.constructor.zero, before725      rwa start at width726    rw start at first727    have prepended := FinePartition.prepend with inserted, first, firstWidth728    rwa [indexedInsertedPoints, start, add]729730theorem FinePartition.insert_indexed_tagged (p : Set) (A B C D : Real, k L : Nat)731  requires fine : FinePartition(p, A, B, succ(add(k, L)), D)732  requires left : (p[k]:R) < C733  requires right : C < (p[succ(k)]:R)734  shows TaggedPartition(indexedInsertedPoints(p, C, k),735      leftPartitionTags(indexedInsertedPoints(p, C, k)), A, B,736      succ(succ(add(k, L)))) ∧737    FinePartition(indexedInsertedPoints(p, C, k), A, B,738      succ(succ(add(k, L))), D)739proof740  have inserted := FinePartition.insert_indexed with fine, left, right741  have partition : IntervalPartition(indexedInsertedPoints(p, C, k), A, B,742      succ(succ(add(k, L))))743    rcases inserted with ⟨partition, positive, widths⟩744    exact partition745  have tagged := IntervalPartition.left_tagged with partition746  refine ⟨tagged, inserted⟩747748-- User-facing form: an index below the number of cells, with no749-- decomposition of the remaining cell count in the statement.750theorem FinePartition.insert_at (p : Set) (A B C D : Real, N k : Nat)751  requires fine : FinePartition(p, A, B, N, D)752  requires index : Less(k, N)753  requires left : (p[k]:R) < C754  requires right : C < (p[succ(k)]:R)755  shows FinePartition(indexedInsertedPoints(p, C, k), A, B, succ(N), D)756proof757  obtain ⟨L, naturalL, length⟩ := index758  rw [<- length, add] at fine759  have inserted := FinePartition.insert_indexed with fine, left, right760  rwa [<- length, add]761762theorem FinePartition.insert_at_tagged (p : Set) (A B C D : Real, N k : Nat)763  requires fine : FinePartition(p, A, B, N, D)764  requires index : Less(k, N)765  requires left : (p[k]:R) < C766  requires right : C < (p[succ(k)]:R)767  shows TaggedPartition(indexedInsertedPoints(p, C, k),768      leftPartitionTags(indexedInsertedPoints(p, C, k)), A, B, succ(N)) ∧769    FinePartition(indexedInsertedPoints(p, C, k), A, B, succ(N), D)770proof771  have inserted := FinePartition.insert_at with fine, index, left, right772  have partition : IntervalPartition(indexedInsertedPoints(p, C, k), A, B, succ(N))773    rcases inserted with ⟨partition, positive, widths⟩774    exact partition775  have tagged := IntervalPartition.left_tagged with partition776  refine ⟨tagged, inserted⟩777778-- IndexedInsertionSplit779theorem FinePartition.insert_indexed_split (f p : Set) (A B C D : Real, k L : Nat)780  requires function : f : ℝ → ℝ781  requires fine : FinePartition(p, A, B, succ(add(k, L)), D)782  requires left : (p[k]:R) < C783  requires right : C < (p[succ(k)]:R)784  shows FinePartition(indexedInsertedPoints(p, C, k), A, C, succ(k), D) ∧785    FinePartition(shiftedRealSequence(indexedInsertedPoints(p, C, k), succ(k)),786      C, B, succ(L), D) ∧787    TaggedPartition(indexedInsertedPoints(p, C, k),788      leftPartitionTags(indexedInsertedPoints(p, C, k)), A, C, succ(k)) ∧789    TaggedPartition(shiftedRealSequence(indexedInsertedPoints(p, C, k), succ(k)),790      shiftedRealSequence(leftPartitionTags(indexedInsertedPoints(p, C, k)), succ(k)),791      C, B, succ(L)) ∧792    riemannSum(f, indexedInsertedPoints(p, C, k),793      leftPartitionTags(indexedInsertedPoints(p, C, k)), succ(succ(add(k, L)))) =794      (riemannSum(f, indexedInsertedPoints(p, C, k),795        leftPartitionTags(indexedInsertedPoints(p, C, k)), succ(k)):R) +796      (riemannSum(f,797        shiftedRealSequence(indexedInsertedPoints(p, C, k), succ(k)),798        shiftedRealSequence(leftPartitionTags(indexedInsertedPoints(p, C, k)), succ(k)),799        succ(L)):R)800proof801  obtain ⟨tagged, finer⟩ := FinePartition.insert_indexed_tagged with fine, left, right802  have points : RealSequence(p)803    rcases fine with ⟨partition, positive, widths⟩804    rcases partition with ⟨sequence, start, finish, increasing⟩805    exact sequence806  have point := indexedInsertedPoints.inserted at p, C, k with points807  have splitFine : FinePartition(indexedInsertedPoints(p, C, k), A, B,808      add(succ(k), succ(L)), D)809    rwa [add, add.succ_right]810  have splitTagged : TaggedPartition(indexedInsertedPoints(p, C, k),811      leftPartitionTags(indexedInsertedPoints(p, C, k)), A, B,812      add(succ(k), succ(L)))813    rwa [add, add.succ_right]814  have split := FinePartition.split_tagged_sum with function, splitFine, splitTagged815  rwa [point, add, add.succ_right] at split816817-- Section: IndexedSharedTotal818theorem riemannSum.insert_first_cell_prefix (f p : Set) (C : Real)819  requires function : f : ℝ → ℝ820  requires points : RealSequence(p)821  shows riemannSum(f, firstCellInsertedPoints(p, C),822      leftPartitionTags(firstCellInsertedPoints(p, C)), succ(succ(0))) =823    f(p[0]) * (C - (p[0]:R)) +824      f(C) * ((p[succ(0)]:R) - C)825proof826  have A := RealSequence.value at p, 0 with points827  have B := RealSequence.value at p, succ(0) with points828  have inserted := firstCellInsertedPoints.sequence at p, C with points829  have leftTags : RealSequence(leftPartitionTags(firstCellInsertedPoints(p, C)))830    unfold RealSequence831    exact leftPartitionTags.function with inserted832  have two := twoCellPoints.sequence at p[0], C, p[succ(0)] with A, assumption, B833  have cells : ∀ i ∈ ℕ, i < succ(succ(0)) → firstCellInsertedPoints(p, C)[i] = twoCellPoints(p[0], C, p[succ(0)])[i] ∧ firstCellInsertedPoints(p, C)[succ(i)] = twoCellPoints(p[0], C, p[succ(0)])[succ(i)] ∧ leftPartitionTags(firstCellInsertedPoints(p, C))[i] = twoCellPoints(p[0], C, p[succ(0)])[i]834    intros i naturalI before835    have typedI := nat.omega.backward with naturalI836    have cases := Nat.lt_two_cases with typedI, before837    cases cases with first | second838    . rw [first, firstCellInsertedPoints.zero, firstCellInsertedPoints.one, twoCellPoints.zero, twoCellPoints.one, leftPartitionTags.value, firstCellInsertedPoints.zero]839      refine ⟨rfl, rfl, rfl⟩840    . rw [second, firstCellInsertedPoints.one, firstCellInsertedPoints.later, twoCellPoints.one, twoCellPoints.two, leftPartitionTags.value, firstCellInsertedPoints.one]841      refine ⟨rfl, rfl, rfl⟩842  have same := riemannSum.congr_cells with function, inserted, two, leftTags, two, cells843  have value := riemannSum.two_cell_left at f, p[0], C, p[succ(0)] with function844  rwa value at same845846theorem riemannSum.insert_first_cell_tail (f p : Set) (C : Real, K : Nat)847  requires function : f : ℝ → ℝ848  requires points : RealSequence(p)849  shows riemannSum(f,850      shiftedRealSequence(firstCellInsertedPoints(p, C), succ(succ(0))),851      shiftedRealSequence(leftPartitionTags(firstCellInsertedPoints(p, C)), succ(succ(0))), K) =852    riemannSum(f, shiftedRealSequence(p, succ(0)),853      shiftedRealSequence(leftPartitionTags(p), succ(0)), K)854proof855  have inserted := firstCellInsertedPoints.sequence with points856  have insertedTags : RealSequence(leftPartitionTags(firstCellInsertedPoints(p, C)))857    unfold RealSequence858    exact leftPartitionTags.function with inserted859  have originalTags : RealSequence(leftPartitionTags(p))860    unfold RealSequence861    exact leftPartitionTags.function with points862  have newPoints := shiftedRealSequence.sequence at863    firstCellInsertedPoints(p, C), succ(succ(0)) with inserted864  have oldPoints := shiftedRealSequence.sequence at p, succ(0) with points865  have newTags := shiftedRealSequence.sequence at866    leftPartitionTags(firstCellInsertedPoints(p, C)), succ(succ(0)) with insertedTags867  have oldTags := shiftedRealSequence.sequence at leftPartitionTags(p), succ(0) with originalTags868  have atIndex : ∀ j ∈ ℕ,869      shiftedRealSequence(firstCellInsertedPoints(p, C), succ(succ(0)))[j] =870        shiftedRealSequence(p, succ(0))[j]871    intros j naturalJ872    have typedJ := nat.omega.backward with naturalJ873    have newValue := shiftedRealSequence.value at874      firstCellInsertedPoints(p, C), succ(succ(0)), j with inserted875    have oldValue := shiftedRealSequence.value at p, succ(0), j with points876    simp [add] at newValue877    simp [add] at oldValue878    have later := firstCellInsertedPoints.later at p, C, j with points879    rw later at newValue880    rw [newValue, oldValue]881    rfl882  have atTag : ∀ m ∈ ℕ,883      shiftedRealSequence(leftPartitionTags(firstCellInsertedPoints(p, C)), succ(succ(0)))[m] =884        shiftedRealSequence(leftPartitionTags(p), succ(0))[m]885    intros m naturalJ886    have newValue := shiftedRealSequence.value at887      leftPartitionTags(firstCellInsertedPoints(p, C)), succ(succ(0)), m with insertedTags888    have oldValue := shiftedRealSequence.value at leftPartitionTags(p), succ(0), m with originalTags889    simp [add] at newValue890    simp [add] at oldValue891    rw leftPartitionTags.value at newValue892    rw leftPartitionTags.value at oldValue893    have later := firstCellInsertedPoints.later at p, C, m with points894    rw later at newValue895    rw [newValue, oldValue]896    rfl897  have cells : ∀ i ∈ ℕ, i < K → shiftedRealSequence(firstCellInsertedPoints(p, C), succ(succ(0)))[i] = shiftedRealSequence(p, succ(0))[i] ∧ shiftedRealSequence(firstCellInsertedPoints(p, C), succ(succ(0)))[succ(i)] = shiftedRealSequence(p, succ(0))[succ(i)] ∧ shiftedRealSequence(leftPartitionTags(firstCellInsertedPoints(p, C)), succ(succ(0)))[i] = shiftedRealSequence(leftPartitionTags(p), succ(0))[i]898    intros i naturalI before899    have typedI := nat.omega.backward with naturalI900    have next := Naturals.constructor.succ with typedI901    have naturalNext := nat.omega.forward with next902    have first := atIndex with i, naturalI903    have second := atIndex with succ(i), naturalNext904    have third := atTag with i, naturalI905    refine ⟨first, second, third⟩906  exact riemannSum.congr_cells with function, newPoints, oldPoints, newTags, oldTags, cells907908theorem riemannSum.insert_first_cell_total (f p : Set) (C : Real, K : Nat)909  requires function : f : ℝ → ℝ910  requires points : RealSequence(p)911  shows riemannSum(f, firstCellInsertedPoints(p, C),912      leftPartitionTags(firstCellInsertedPoints(p, C)), succ(succ(K))) =913    (f(p[0]) * (C - (p[0]:R)) +914      f(C) * ((p[succ(0)]:R) - C)) +915    riemannSum(f, shiftedRealSequence(p, succ(0)),916      shiftedRealSequence(leftPartitionTags(p), succ(0)), K)917proof918  have inserted := firstCellInsertedPoints.sequence with points919  have tags : RealSequence(leftPartitionTags(firstCellInsertedPoints(p, C)))920    unfold RealSequence921    exact leftPartitionTags.function with inserted922  have split := riemannSum.split_at at f, firstCellInsertedPoints(p, C),923    leftPartitionTags(firstCellInsertedPoints(p, C)), succ(succ(0)), K with924      function, inserted, tags925  simp [add] at split926  have prefix := riemannSum.insert_first_cell_prefix with function, points927  have tail := riemannSum.insert_first_cell_tail with function, points928  rwa [prefix, tail] at split929930-- PrependSum931theorem realPartialSum.prepend (A : Real, u : Set, N : Nat)932  requires sequence : RealSequence(u)933  shows realPartialSum(prependRealSequence(A, u), succ(N)) =934    A + realPartialSum(u, N)935proof936  induction N937  | zero =>938    rw [realPartialSum.succ, realPartialSum.zero, realPartialSum.zero, prependRealSequence.zero]939    ring940  | succ(k) using ih =>941    rw [realPartialSum.succ, prependRealSequence.succ, ih, realPartialSum.succ]942    have term := RealSequence.value with sequence943    ring944945theorem realPartialSum.first_cell_inserted (f p : Set) (C : Real, K : Nat)946  requires function : f : ℝ → ℝ947  requires points : RealSequence(p)948  shows realPartialSum(949      prependRealSequence(950        riemannSum(f, twoCellPoints(p[0], C, p[succ(0)]),951          twoCellPoints(p[0], C, p[succ(0)]), succ(succ(0))),952        shiftedRealSequence(riemannTerms(f, p, leftPartitionTags(p)), succ(0))),953      succ(K)) =954    riemannSum(f, firstCellInsertedPoints(p, C),955      leftPartitionTags(firstCellInsertedPoints(p, C)), succ(succ(K)))956proof957  have A := RealSequence.value at p, 0 with points958  have B := RealSequence.value at p, succ(0) with points959  have tags : RealSequence(leftPartitionTags(p))960    unfold RealSequence961    exact leftPartitionTags.function with points962  have terms : RealSequence(riemannTerms(f, p, leftPartitionTags(p)))963    unfold RealSequence964    exact riemannTerms.function with function, points, tags965  have suffixTerms := shiftedRealSequence.sequence at966    riemannTerms(f, p, leftPartitionTags(p)), succ(0) with terms967  have twoPoints := twoCellPoints.sequence at p[0], C, p[succ(0)] with A, assumption, B968  have prepended := realPartialSum.prepend at969    riemannSum(f, twoCellPoints(p[0], C, p[succ(0)]),970      twoCellPoints(p[0], C, p[succ(0)]), succ(succ(0))),971    shiftedRealSequence(riemannTerms(f, p, leftPartitionTags(p)), succ(0)), K with suffixTerms972  have shiftedP := shiftedRealSequence.sequence at p, succ(0) with points973  have shiftedT := shiftedRealSequence.sequence at leftPartitionTags(p), succ(0) with tags974  have shiftedRiemannTerms : RealSequence(riemannTerms(f,975      shiftedRealSequence(p, succ(0)), shiftedRealSequence(leftPartitionTags(p), succ(0))))976    unfold RealSequence977    exact riemannTerms.function with function, shiftedP, shiftedT978  have equal : ∀ j ∈ ℕ, j < K → shiftedRealSequence(riemannTerms(f, p, leftPartitionTags(p)), succ(0))[j] = riemannTerms(f, shiftedRealSequence(p, succ(0)), shiftedRealSequence(leftPartitionTags(p), succ(0)))[j]979    intros j naturalJ before980    have typedJ := nat.omega.backward with naturalJ981    have shifted := riemannTerms.shifted at f, p, leftPartitionTags(p), succ(0), j with982      function, points, tags983    rw shifted984    rfl985  have suffix := realPartialSum.eq_prefix with suffixTerms, shiftedRiemannTerms, equal986  rw suffix at prepended987  have suffixRiemann : realPartialSum(riemannTerms(f,988      shiftedRealSequence(p, succ(0)), shiftedRealSequence(leftPartitionTags(p), succ(0))), K) =989    riemannSum(f, shiftedRealSequence(p, succ(0)),990      shiftedRealSequence(leftPartitionTags(p), succ(0)), K)991    unfold riemannSum992    rfl993  rw suffixRiemann at prepended994  have global := riemannSum.insert_first_cell_total at f, p, C, K with function, points995  have local := riemannSum.two_cell_left at f, p[0], C, p[succ(0)] with function996  rw [local, <- global] at prepended997  rwa local998999-- FirstCellSharedTotal1000def firstCellSubdivisionTerms (f p : Set, C : Real) : Set :=1001  prependRealSequence(1002    riemannSum(f, twoCellPoints(p[0], C, p[succ(0)]),1003      twoCellPoints(p[0], C, p[succ(0)]), succ(succ(0))),1004    shiftedRealSequence(riemannTerms(f, p, leftPartitionTags(p)), succ(0)))10051006theorem CellwiseSubdivisionSums.first_cell_inserted (f p : Set) (A B C : Real, K : Nat)1007  requires function : f : ℝ → ℝ1008  requires partition : IntervalPartition(p, A, B, succ(K))1009  requires left : (p[0]:R) < C1010  requires right : C < (p[succ(0)]:R)1011  shows CellwiseSubdivisionSums(f, p, firstCellSubdivisionTerms(f, p, C), succ(K))1012proof1013  rcases partition with ⟨points, start, finish, increasing⟩1014  have pointA := RealSequence.value at p, 0 with points1015  have pointB := RealSequence.value at p, succ(0) with points1016  have original : IntervalPartition(p, A, B, succ(K)) by refine ⟨points, start, finish, increasing⟩1017  have tags : RealSequence(leftPartitionTags(p))1018    unfold RealSequence1019    exact leftPartitionTags.function with points1020  have terms : RealSequence(riemannTerms(f, p, leftPartitionTags(p)))1021    unfold RealSequence1022    exact riemannTerms.function with function, points, tags1023  have tail := shiftedRealSequence.sequence at riemannTerms(f, p, leftPartitionTags(p)), succ(0) with terms1024  have twoPoints := twoCellPoints.sequence at p[0], C, p[succ(0)] with pointA, assumption, pointB1025  have uSequence : RealSequence(firstCellSubdivisionTerms(f, p, C))1026    rw firstCellSubdivisionTerms1027    exact prependRealSequence.sequence with tail1028  constructor1029  . exact uSequence1030  . intros i naturalI before1031    have typedI := nat.omega.backward with naturalI1032    have shape := natural.zero_or_successor with typedI1033    cases shape with zero | successor1034    . witness twoCellPoints(p[0], C, p[succ(0)])1035      witness twoCellPoints(p[0], C, p[succ(0)])1036      witness succ(succ(0))1037      rw zero1038      constructor1039      . exact nat.omega.forward at succ(succ(0)) with1040          Naturals.constructor.succ at succ(0) with1041            Naturals.constructor.succ at 0 with Naturals.constructor.zero1042      . constructor1043        . exact twoCellPoints.tagged at p[0], C, p[succ(0)] with1044            left, right1045        . rw [firstCellSubdivisionTerms, prependRealSequence.zero]1046          rfl1047    . obtain ⟨j, naturalJ, isNext⟩ := successor1048      have oldBefore : Less(succ(j), succ(K)) by rwa isNext at before1049      have oldCell := IntervalPartition.cell with original, oldBefore1050      have valueI := RealSequence.value at p, succ(j) with points1051      have valueNext := RealSequence.value at p, succ(succ(j)) with points1052      have le := realLess.implies_le with oldCell1053      have tag := closedInterval.left_mem with valueI, valueNext, le1054      witness oneCellPoints(p[succ(j)], p[succ(succ(j))])1055      witness constantSequence(p[succ(j)])1056      witness succ(0)1057      constructor1058      . exact nat.omega.forward at succ(0) with1059          Naturals.constructor.succ at 0 with Naturals.constructor.zero1060      . constructor1061        . rw isNext1062          exact oneCellPoints.tagged_at with oldCell, tag1063        . rw [isNext, firstCellSubdivisionTerms, prependRealSequence.succ]1064          have shifted := shiftedRealSequence.value at1065            riemannTerms(f, p, leftPartitionTags(p)), succ(0), j with terms1066          simp [add] at shifted1067          rw shifted1068          have term := riemannTerms.value at f, p, leftPartitionTags(p), succ(j) with1069            function, points, tags1070          rw [term, leftPartitionTags.value]1071          have single := riemannSum.one_cell_tag at f,1072            p[succ(j)], p[succ(succ(j))], p[succ(j)] with function1073          rw single1074          unfold realMulValue1075          unfold call21076          rfl10771078theorem SharedSubdivisionTotal.first_cell_inserted (f p : Set) (A B C : Real, K : Nat)1079  requires function : f : ℝ → ℝ1080  requires partition : IntervalPartition(p, A, B, succ(K))1081  requires left : (p[0]:R) < C1082  requires right : C < (p[succ(0)]:R)1083  shows SharedSubdivisionTotal(f, p, firstCellInsertedPoints(p, C),1084    firstCellSubdivisionTerms(f, p, C),1085    riemannTerms(f, firstCellInsertedPoints(p, C),1086      leftPartitionTags(firstCellInsertedPoints(p, C))),1087    succ(K), succ(succ(K)))1088proof1089  have points : RealSequence(p)1090    rcases partition with ⟨points, start, finish, increasing⟩1091    exact points1092  have start : p[0] = A1093    rcases partition with ⟨points, start, finish, increasing⟩1094    exact start1095  have leftA : A < C by rwa start at left1096  have inserted := IntervalPartition.insert_first_cell with partition, leftA, right1097  have tagged := IntervalPartition.left_tagged with inserted1098  have coarse := CellwiseSubdivisionSums.first_cell_inserted with function, partition, left, right1099  have fine := TaggedPartition.trivial_subdivision with function, tagged1100  have total := realPartialSum.first_cell_inserted at f, p, C, K with function, points1101  constructor1102  . exact coarse1103  . constructor1104    . exact fine1105    . unfold firstCellSubdivisionTerms1106      rw total1107      unfold riemannSum1108      rfl11091110-- SubdivisionTransport1111theorem CellwiseSubdivisionSums.congr_points (f p q u : Set) (N : Nat)1112  requires subdivided : CellwiseSubdivisionSums(f, p, u, N)1113  requires cells : ∀ i ∈ ℕ, i < N → p[i] = q[i] ∧ p[succ(i)] = q[succ(i)]1114  shows CellwiseSubdivisionSums(f, q, u, N)1115proof1116  rcases subdivided with ⟨sequenceU, data⟩1117  constructor1118  . exact sequenceU1119  . intros i naturalI before1120    obtain ⟨left, right⟩ := cells with i, naturalI, before1121    obtain ⟨r, s, M, naturalM, tagged, value⟩ := data with i, naturalI, before1122    witness r1123    witness s1124    witness M1125    constructor1126    . exact naturalM1127    . constructor1128      . rw [<- left, <- right]1129        exact tagged1130      . exact value11311132theorem SharedSubdivisionTotal.congr_right (f p q r u v : Set) (N M : Nat)1133  requires shared : SharedSubdivisionTotal(f, p, q, u, v, N, M)1134  requires cells : ∀ i ∈ ℕ, i < M → q[i] = r[i] ∧ q[succ(i)] = r[succ(i)]1135  shows SharedSubdivisionTotal(f, p, r, u, v, N, M)1136proof1137  rcases shared with ⟨coarse, fine, total⟩1138  have moved := CellwiseSubdivisionSums.congr_points with fine, cells1139  refine ⟨coarse, moved, total⟩11401141-- PrependSubdivision1142def initialCellSum (f p : Set) : Set :=1143  riemannSum(f, oneCellPoints(p[0], p[succ(0)]),1144    constantSequence(p[0]), succ(0))11451146theorem CellwiseSubdivisionSums.prepend_initial (f p u : Set) (N : Nat)1147  requires function : f : ℝ → ℝ1148  requires points : RealSequence(p)1149  requires first : (p[0]:R) < (p[succ(0)]:R)1150  requires tail : CellwiseSubdivisionSums(f, shiftedRealSequence(p, succ(0)), u, N)1151  shows CellwiseSubdivisionSums(f, p,1152    prependRealSequence(initialCellSum(f, p), u), succ(N))1153proof1154  rcases tail with ⟨sequenceU, data⟩1155  have A := RealSequence.value at p, 0 with points1156  have B := RealSequence.value at p, succ(0) with points1157  have le := realLess.implies_le with first1158  have tag := closedInterval.left_mem with A, B, le1159  have single := oneCellPoints.tagged_at with first, tag1160  have value : Real(initialCellSum(f, p))1161    unfold initialCellSum1162    have onePoints := oneCellPoints.sequence with A, B1163    have oneTags := constantSequence.sequence with A1164    exact riemannSum.real with function, onePoints, oneTags1165  have prepended := prependRealSequence.sequence at initialCellSum(f, p), u with sequenceU1166  constructor1167  . exact prepended1168  . intros i naturalI before1169    have typedI := nat.omega.backward with naturalI1170    have shape := natural.zero_or_successor with typedI1171    cases shape with zero | successor1172    . witness oneCellPoints(p[0], p[succ(0)])1173      witness constantSequence(p[0])1174      witness succ(0)1175      rw zero1176      constructor1177      . exact nat.omega.forward at succ(0) with1178          Naturals.constructor.succ at 0 with Naturals.constructor.zero1179      . constructor1180        . exact single1181        . rw [prependRealSequence.zero, initialCellSum]1182          rfl1183    . obtain ⟨j, naturalJ, isNext⟩ := successor1184      have beforeTail : Less(j, N)1185        have shifted : Less(add(j, 1), add(N, 1))1186          rw [add.right_one, add.right_one]1187          rwa isNext at before1188        exact Less.add_right_cancel with shifted1189      obtain ⟨r, s, M, naturalM, tagged, equal⟩ := data with1190        j, nat.omega.forward at j with naturalJ, beforeTail1191      witness r1192      witness s1193      witness M1194      constructor1195      . exact naturalM1196      . constructor1197        . rw isNext1198          have shiftedLeft := shiftedRealSequence.value at p, succ(0), j with points1199          have shiftedRight := shiftedRealSequence.value at p, succ(0), succ(j) with points1200          simp [add] at shiftedLeft1201          simp [add] at shiftedRight1202          rwa [shiftedLeft, shiftedRight] at tagged1203        . rw [isNext, prependRealSequence.succ]1204          exact equal12051206-- PrependSharedTotal1207theorem SharedSubdivisionTotal.prepend_initial (f p q u v : Set) (N M : Nat)1208  requires function : f : ℝ → ℝ1209  requires pointsP : RealSequence(p)1210  requires pointsQ : RealSequence(q)1211  requires first : (p[0]:R) < (p[succ(0)]:R)1212  requires sameStart : p[0] = q[0]1213  requires sameNext : p[succ(0)] = q[succ(0)]1214  requires shared : SharedSubdivisionTotal(f,1215    shiftedRealSequence(p, succ(0)), shiftedRealSequence(q, succ(0)),1216    u, v, N, M)1217  shows SharedSubdivisionTotal(f, p, q,1218    prependRealSequence(initialCellSum(f, p), u),1219    prependRealSequence(initialCellSum(f, q), v), succ(N), succ(M))1220proof1221  rcases shared with ⟨coarseTail, fineTail, equalTail⟩1222  have coarse := CellwiseSubdivisionSums.prepend_initial with function, pointsP, first, coarseTail1223  have firstQ : (q[0]:R) < (q[succ(0)]:R) by rwa [<- sameStart, <- sameNext]1224  have fine := CellwiseSubdivisionSums.prepend_initial with function, pointsQ, firstQ, fineTail1225  have sameInitial : initialCellSum(f, p) = initialCellSum(f, q)1226    simp [initialCellSum]1227  have sequenceU : RealSequence(u)1228    rcases coarseTail with ⟨sequence, data⟩1229    exact sequence1230  have sequenceV : RealSequence(v)1231    rcases fineTail with ⟨sequence, data⟩1232    exact sequence1233  have pointP := RealSequence.value at p, 0 with pointsP1234  have pointNext := RealSequence.value at p, succ(0) with pointsP1235  have onePoints := oneCellPoints.sequence with pointP, pointNext1236  have oneTags := constantSequence.sequence with pointP1237  have firstReal : Real(initialCellSum(f, p))1238    unfold initialCellSum1239    exact riemannSum.real with function, onePoints, oneTags1240  have pointQ := RealSequence.value at q, 0 with pointsQ1241  have pointQNext := RealSequence.value at q, succ(0) with pointsQ1242  have qPoints := oneCellPoints.sequence with pointQ, pointQNext1243  have qTags := constantSequence.sequence with pointQ1244  have secondReal : Real(initialCellSum(f, q))1245    unfold initialCellSum1246    exact riemannSum.real with function, qPoints, qTags1247  have sumP := realPartialSum.prepend at initialCellSum(f, p), u, N with sequenceU1248  have sumQ := realPartialSum.prepend at initialCellSum(f, q), v, M with sequenceV1249  have totals : realPartialSum(prependRealSequence(initialCellSum(f, p), u), succ(N)) =1250      realPartialSum(prependRealSequence(initialCellSum(f, q), v), succ(M))1251    rw [sumP, sumQ, sameInitial, equalTail]1252    rfl1253  refine ⟨coarse, fine, totals⟩12541255-- IndexedSharedTotal1256theorem SharedSubdivisionTotal.exists_insert_indexed (f p : Set) (A B C : Real, k L : Nat)1257  requires function : f : ℝ → ℝ1258  requires partition : IntervalPartition(p, A, B, succ(add(k, L)))1259  requires left : (p[k]:R) < C1260  requires right : C < (p[succ(k)]:R)1261  shows ∃ u, ∃ v, SharedSubdivisionTotal(f, p,1262    indexedInsertedPoints(p, C, k), u, v,1263    succ(add(k, L)), succ(succ(add(k, L))))1264proof1265  induction k generalizing p A1266  | zero =>1267    intros p A realA partition left right1268    have basePartition : IntervalPartition(p, A, B, succ(L)) by rwa add.left_unit at partition1269    have base := SharedSubdivisionTotal.first_cell_inserted at f, p, A, B, C, L with1270      function, basePartition, left, right1271    witness firstCellSubdivisionTerms(f, p, C)1272    witness riemannTerms(f, firstCellInsertedPoints(p, C),1273      leftPartitionTags(firstCellInsertedPoints(p, C)))1274    rwa [indexedInsertedPoints, add.left_unit]1275  | succ(j) using ih =>1276    intros p A realA partition left right1277    have points : RealSequence(p)1278      rcases partition with ⟨points, start, finish, increasing⟩1279      exact points1280    have totalNat : Nat(add(succ(j), L)) by apply add.closed at L, succ(j)1281    have firstBefore := natural.zero_before_successor with totalNat1282    have first := IntervalPartition.cell with partition, firstBefore1283    have tailPartition : IntervalPartition(shiftedRealSequence(p, succ(0)),1284        p[succ(0)], B, succ(add(j, L)))1285      have original : IntervalPartition(p, A, B,1286          add(succ(0), succ(add(j, L))))1287        rw [add, add]1288        rwa add at partition1289      exact IntervalPartition.suffix with original1290    have shifted := shiftedRealSequence.sequence at p, succ(0) with points1291    have leftValue := shiftedRealSequence.value at p, succ(0), j with points1292    have rightValue := shiftedRealSequence.value at p, succ(0), succ(j) with points1293    simp [add] at leftValue1294    simp [add] at rightValue1295    rw <- leftValue at left1296    rw <- rightValue at right1297    have pointOne := RealSequence.value at p, succ(0) with points1298    obtain ⟨u, v, tailShared⟩ := ih with1299      shiftedRealSequence(p, succ(0)), p[succ(0)],1300      pointOne,1301      tailPartition, left, right1302    have inserted := indexedInsertedPoints.sequence at p, C, succ(j) with points1303    have insertedTail := indexedInsertedPoints.sequence at1304      shiftedRealSequence(p, succ(0)), C, j with shifted1305    have newShift := shiftedRealSequence.sequence at1306      indexedInsertedPoints(p, C, succ(j)), succ(0) with inserted1307    have tailCells : ∀ i ∈ ℕ, i < succ(succ(add(j, L))) → indexedInsertedPoints(shiftedRealSequence(p, succ(0)), C, j)[i] = shiftedRealSequence(indexedInsertedPoints(p, C, succ(j)), succ(0))[i] ∧ indexedInsertedPoints(shiftedRealSequence(p, succ(0)), C, j)[succ(i)] = shiftedRealSequence(indexedInsertedPoints(p, C, succ(j)), succ(0))[succ(i)]1308      intros i naturalI before1309      have typedI := nat.omega.backward with naturalI1310      have next := Naturals.constructor.succ with typedI1311      have naturalNext := nat.omega.forward with next1312      have atI := indexedInsertedPoints.successor at p, C, j, i with points1313      have shiftI := shiftedRealSequence.value at1314        indexedInsertedPoints(p, C, succ(j)), succ(0), i with inserted1315      simp [add] at shiftI1316      rw shiftI1317      have atNext := indexedInsertedPoints.successor at p, C, j, succ(i) with points1318      have shiftNext := shiftedRealSequence.value at1319        indexedInsertedPoints(p, C, succ(j)), succ(0), succ(i) with inserted1320      simp [add] at shiftNext1321      rw shiftNext1322      refine ⟨rfl, rfl⟩1323    have moved := SharedSubdivisionTotal.congr_right with tailShared, tailCells1324    have sameStart := indexedInsertedPoints.zero at p, C, succ(j) with points1325    have sameStartP : p[0] = indexedInsertedPoints(p, C, succ(j))[0]1326      rw sameStart1327      rfl1328    have sameNext : p[succ(0)] = indexedInsertedPoints(p, C, succ(j))[succ(0)]1329      have step := indexedInsertedPoints.successor at p, C, j, 0 with points1330      have tailZero := indexedInsertedPoints.zero at1331        shiftedRealSequence(p, succ(0)), C, j with shifted1332      have shiftedZero := shiftedRealSequence.value at p, succ(0), 0 with points1333      simp [add] at shiftedZero1334      rw [tailZero, shiftedZero] at step1335      rw step1336      rfl1337    have lifted := SharedSubdivisionTotal.prepend_initial with1338      function, points, inserted, first, sameStartP, sameNext, moved1339    witness prependRealSequence(initialCellSum(f, p), u)1340    witness prependRealSequence(initialCellSum(f,1341      indexedInsertedPoints(p, C, succ(j))), v)1342    rwa add13431344theorem SharedSubdivisionTotal.exists_insert_at (f p : Set) (A B C : Real, N k : Nat)1345  requires function : f : ℝ → ℝ1346  requires partition : IntervalPartition(p, A, B, N)1347  requires index : Less(k, N)1348  requires left : (p[k]:R) < C1349  requires right : C < (p[succ(k)]:R)1350  shows ∃ u, ∃ v, SharedSubdivisionTotal(f, p,1351    indexedInsertedPoints(p, C, k), u, v, N, succ(N))1352proof1353  obtain ⟨L, naturalL, length⟩ := index1354  rw [<- length, add] at partition1355  obtain ⟨u, v, shared⟩ := SharedSubdivisionTotal.exists_insert_indexed with function, partition, left, right1356  witness u1357  witness v1358  rwa [<- length, add]13591360-- Section: CommonVertices1361theorem IntervalPartition.locate_interior (p : Set) (A B C : Real, N : Nat)1362  requires partition : IntervalPartition(p, A, B, N)1363  requires above : A < C1364  requires below : C < B1365  shows (∃ i ∈ ℕ, i ≤ N ∧ p[i] = C) ∨1366    (∃ k ∈ ℕ, k < N ∧ (p[k]:R) < C ∧ C < (p[succ(k)]:R))1367proof1368  induction N generalizing p A1369  | zero =>1370    intros p A realA partition above1371    have start : p[0] = A1372      rcases partition with ⟨points, start, finish, increasing⟩1373      exact start1374    have finish : p[0] = B1375      rcases partition with ⟨points, start, finish, increasing⟩1376      exact finish1377    rw [<- finish, start] at below1378    have impossible := realLess.transitive with above, below1379    have contradiction := realLess.characterization.forward with impossible1380    have irreflexive := RealLess.irreflexive with contradiction1381    exfalso1382    exact irreflexive1383  | succ(K) using ih =>1384    intros p A realA partition above1385    have points : RealSequence(p)1386      rcases partition with ⟨points, start, finish, increasing⟩1387      exact points1388    have start : p[0] = A1389      rcases partition with ⟨points, start, finish, increasing⟩1390      exact start1391    have pointOne := RealSequence.value at p, succ(0) with points1392    have alternatives : C = p[succ(0)] ∨ C ≠ p[succ(0)] by tauto1393    cases alternatives with equal | distinct1394    . left1395      witness succ(0)1396      constructor1397      . exact nat.omega.forward at succ(0) with1398          Naturals.constructor.succ at 0 with Naturals.constructor.zero1399      . constructor1400        . have zeroLe := Grace.Core.Nat.Order.LessEqual.zero at K1401          have shifted := LessEqual.add_monotone_right at 0, K, 1 with zeroLe1402          rwa [add.right_one, add.right_one] at shifted1403        . rw equal1404          rfl1405    have comparison := realLess.connected_on with C, p[succ(0)], distinct1406    cases comparison with beforeFirst | afterFirst1407    . right1408      witness 01409      constructor1410      . exact nat.omega.forward at 0 with Naturals.constructor.zero1411      . constructor1412        . exact natural.zero_before_successor at K1413        . constructor1414          . rw start1415            exact above1416          . exact beforeFirst1417    . have tail : IntervalPartition(shiftedRealSequence(p, succ(0)),1418          p[succ(0)], B, K)1419        have length : IntervalPartition(p, A, B, add(succ(0), K)) by rwa [add, add.left_unit]1420        exact IntervalPartition.suffix with length1421    have tailPoint := ih with shiftedRealSequence(p, succ(0)),1422      p[succ(0)], pointOne, tail, afterFirst1423    cases tailPoint with atVertex | inCell1424    . obtain ⟨i, naturalI, bound, value⟩ := atVertex1425      left1426      witness succ(i)1427      constructor1428      . exact nat.omega.forward at succ(i) with1429          Naturals.constructor.succ at i with nat.omega.backward at i with naturalI1430      . constructor1431        . have lifted := LessEqual.add_monotone_right at i, K, 1 with bound1432          rwa [add.right_one, add.right_one] at lifted1433          . have shifted := shiftedRealSequence.value at p, succ(0), i with points1434            simp [add] at shifted1435            rw <- shifted1436            rfl1437    . obtain ⟨m, naturalI, bound, left, right⟩ := inCell1438      right1439      witness succ(m)1440      constructor1441      . exact nat.omega.forward at succ(m) with1442          Naturals.constructor.succ at m with nat.omega.backward at m with naturalI1443      . constructor1444        . have lifted := Less.add_LessEqual at m, K, 1, 1 with1445            bound, LessEqual.reflexive at 1 with1446              Naturals.constructor.succ at 0 with Naturals.constructor.zero1447          rwa [add.right_one, add.right_one] at lifted1448        . have shiftedLeft := shiftedRealSequence.value at p, succ(0), m with points1449          have shiftedRight := shiftedRealSequence.value at p, succ(0), succ(m) with points1450          simp [add] at shiftedLeft1451          simp [add] at shiftedRight1452          rw shiftedLeft at left1453          rw shiftedRight at right1454          refine ⟨left, right⟩14551456-- IndexedInsertionVertices1457theorem indexedInsertedPoints.before (p : Set) (C : Real, k i : Nat)1458  requires points : RealSequence(p)1459  requires bounded : i ≤ k1460  shows indexedInsertedPoints(p, C, k)[i] = p[i]1461proof1462  induction k generalizing p i1463  | zero =>1464    intros p i naturalI points bounded1465    have zeroLe := Grace.Core.Nat.Order.LessEqual.zero at i1466    have iZero := LessEqual.antisymmetric with bounded, zeroLe1467    rw [iZero, indexedInsertedPoints]1468    exact firstCellInsertedPoints.zero at p, C with points1469  | succ(j) using ih =>1470    intros p i naturalI points bounded1471    have shape := natural.zero_or_successor at i1472    cases shape with zero | successor1473    . rw zero1474      exact indexedInsertedPoints.zero with points1475    . obtain ⟨m, naturalM, isNext⟩ := successor1476      have before : m ≤ j1477        have shifted : add(m, 1) ≤ add(j, 1)1478          rw [add.right_one, add.right_one]1479          rwa isNext at bounded1480        exact LessEqual.add_right_cancel with shifted1481      have tail := shiftedRealSequence.sequence at p, succ(0) with points1482      have result := ih with shiftedRealSequence(p, succ(0)), m, naturalM, tail, before1483      have step := indexedInsertedPoints.successor at p, C, j, m with points1484      have value := shiftedRealSequence.value at p, succ(0), m with points1485      simp [add] at value1486      rw [result, value] at step1487      rwa isNext14881489theorem indexedInsertedPoints.after (p : Set) (C : Real, k j : Nat)1490  requires points : RealSequence(p)1491  shows indexedInsertedPoints(p, C, k)[succ(succ(add(k, j)))] =1492    p[succ(add(k, j))]1493proof1494  induction k generalizing p1495  | zero =>1496    intros p points1497    rw [add.left_unit, indexedInsertedPoints]1498    exact firstCellInsertedPoints.later with points1499  | succ(m) using ih =>1500    intros p points1501    have shifted := shiftedRealSequence.sequence at p, succ(0) with points1502    have step := indexedInsertedPoints.successor at p, C, m,1503      succ(succ(add(m, j))) with points1504    have result := ih with shiftedRealSequence(p, succ(0)), shifted1505    rw result at step1506    have value := shiftedRealSequence.value at p, succ(0), succ(add(m, j)) with points1507    simp [add] at value1508    rw value at step1509    rwa add15101511theorem indexedInsertedPoints.preserves_vertex (p : Set) (C : Real, N k i : Nat)1512  requires points : RealSequence(p)1513  requires index : k < N1514  requires vertex : i ≤ N1515  shows ∃ j ∈ ℕ, j ≤ succ(N) ∧ indexedInsertedPoints(p, C, k)[j] = p[i]1516proof1517  have cases := Less.trichotomy at i, k with *1518  cases cases with before | rest1519  . have bounded := Less.implies_LessEqual at i, k with before1520    have value := indexedInsertedPoints.before with points, bounded1521    have kLeN := Less.implies_LessEqual at k, N with *1522    have iLeN := LessEqual.transitive with bounded, kLeN1523    have iLeNext := LessEqual.transitive at i, N, succ(N) with1524      *{2}, Naturals.constructor.succ at N with assumption,1525      iLeN, LessEqual.successor at N with assumption1526    witness i1527    refine ⟨nat.omega.forward at i with assumption, iLeNext, value⟩1528  cases rest with equal | after1529  . have bounded : i ≤ k1530      rw equal1531      exact LessEqual.reflexive with assumption1532  have value := indexedInsertedPoints.before with points, bounded1533  have kLeN := Less.implies_LessEqual at k, N with *1534  have iLeN := LessEqual.transitive with bounded, kLeN1535  have iLeNext := LessEqual.transitive at i, N, succ(N) with1536    *{2}, Naturals.constructor.succ at N with assumption,1537    iLeN, LessEqual.successor at N with assumption1538  witness i1539  refine ⟨nat.omega.forward at i with assumption, iLeNext, value⟩1540    obtain ⟨L, naturalL, length⟩ := after1541    have original : i = succ(add(k, L))1542      rw [<- length, add]1543      rfl1544    have shifted := indexedInsertedPoints.after at p, C, k, L with points1545    rw <- original at shifted1546    have nextI := Naturals.constructor.succ at i1547    have lifted := LessEqual.add_monotone_right at i, N, 1 with vertex1548    rw [add.right_one, add.right_one] at lifted1549    witness succ(i)1550    refine ⟨nat.omega.forward at succ(i) with nextI, lifted, shifted⟩15511552-- PartitionVertices1553theorem IntervalPartition.strict_indices (p : Set) (A B : Real, N i j : Nat)1554  requires partition : IntervalPartition(p, A, B, N)1555  requires before : i < j1556  requires bounded : j ≤ N1557  shows (p[i]:R) < (p[j]:R)1558proof1559  have points : RealSequence(p)1560    rcases partition with ⟨points, start, finish, steps⟩1561    exact points1562  have iBefore : i < N by exact Less.transitive_LessEqual at i, j, N with before, bounded1563  have step := IntervalPartition.cell with partition, iBefore1564  have prefix : ∀ k ∈ ℕ, k < j → (p[k]:R) < (p[succ(k)]:R)1565    intros k naturalK below1566    have typedK := nat.omega.backward with naturalK1567    have valid := Less.transitive_LessEqual with below, bounded1568    exact IntervalPartition.cell with partition, valid1569  have monotone := IntervalPartition.prefix_mono with points, prefix1570  have successorLe : succ(i) ≤ j by exact before1571  have nextNatural := Naturals.constructor.succ at i1572  have weak := monotone with succ(i), nat.omega.forward at succ(i) with nextNatural, successorLe1573  have first := RealSequence.value at p, i with points1574  have second := RealSequence.value at p, succ(i) with points1575  have last := RealSequence.value at p, j with points1576  exact realLess.transitive_le with first, second, last, step, weak15771578theorem IntervalPartition.vertex_index_unique (p : Set) (A B : Real, N i j : Nat)1579  requires partition : IntervalPartition(p, A, B, N)1580  requires boundedI : i ≤ N1581  requires boundedJ : j ≤ N1582  requires same : p[i] = p[j]1583  shows i = j1584proof1585  have alternatives := Less.trichotomy at i, j with *1586  cases alternatives with before | rest1587  . have strict := IntervalPartition.strict_indices at p, A, B, N, i, j with1588      partition, before, boundedJ1589    rw same at strict1590    have contradiction := realLess.characterization.forward with strict1591    exfalso1592    exact RealLess.irreflexive with contradiction1593  cases rest with equal | after1594  . exact equal1595  . have strict := IntervalPartition.strict_indices at p, A, B, N, j, i with1596      partition, after, boundedI1597    rw <- same at strict1598    have contradiction := realLess.characterization.forward with strict1599    exfalso1600    exact RealLess.irreflexive with contradiction16011602-- VertexContainment1603predicate VerticesContained (p q : Set) (N M : Nat) :=1604  ∀ i ∈ ℕ, i ≤ N → ∃ j ∈ ℕ, j ≤ M ∧ q[j] = p[i]16051606theorem VerticesContained.reflexive (p : Set) (N : Nat)1607  shows VerticesContained(p, p, N, N)1608proof1609  intros i naturalI bounded1610  witness i1611  refine ⟨naturalI, bounded, rfl⟩16121613theorem VerticesContained.transitive (p q r : Set) (N M L : Nat)1614  requires first : VerticesContained(p, q, N, M)1615  requires second : VerticesContained(q, r, M, L)1616  shows VerticesContained(p, r, N, L)1617proof1618  intros i naturalI bounded1619  obtain ⟨j, naturalJ, jBound, equalP⟩ := first with i, naturalI, bounded1620  obtain ⟨k, naturalK, kBound, equalQ⟩ := second with j, naturalJ, jBound1621  witness k1622  constructor1623  . exact naturalK1624  . constructor1625    . exact kBound1626    . rw equalQ1627      exact equalP16281629theorem VerticesContained.insert_at (p : Set) (C : Real, N k : Nat)1630  requires points : RealSequence(p)1631  requires before : k < N1632  shows VerticesContained(p, indexedInsertedPoints(p, C, k), N, succ(N))1633proof1634  intros i naturalI bounded1635  have typedI := nat.omega.backward with naturalI1636  exact indexedInsertedPoints.preserves_vertex with points, before, bounded16371638-- InsertOrHit1639theorem FinePartition.insert_or_hit (f p : Set) (A B C D : Real, N : Nat)1640  requires function : f : ℝ → ℝ1641  requires fine : FinePartition(p, A, B, N, D)1642  requires above : A < C1643  requires below : C < B1644  shows ∃ q, ∃ M ∈ ℕ, ∃ u, ∃ v,1645    FinePartition(q, A, B, M, D) ∧1646    TaggedPartition(q, leftPartitionTags(q), A, B, M) ∧1647    SharedSubdivisionTotal(f, p, q, u, v, N, M) ∧1648    VerticesContained(p, q, N, M) ∧1649    (∃ i ∈ ℕ, i ≤ M ∧ q[i] = C)1650proof1651  have partition : IntervalPartition(p, A, B, N)1652    rcases fine with ⟨partition, positive, widths⟩1653    exact partition1654  have points : RealSequence(p)1655    rcases partition with ⟨points, start, finish, increasing⟩1656    exact points1657  have location := IntervalPartition.locate_interior with partition, above, below1658  cases location with existing | inside1659  . obtain ⟨i, naturalI, bounded, value⟩ := existing1660    have tagged := IntervalPartition.left_tagged with partition1661    have subdivided := TaggedPartition.trivial_subdivision with function, tagged1662    have shared : SharedSubdivisionTotal(f, p, p,1663        riemannTerms(f, p, leftPartitionTags(p)),1664        riemannTerms(f, p, leftPartitionTags(p)), N, N)1665      refine ⟨subdivided, subdivided, rfl⟩1666    witness p1667    witness N1668    constructor1669    . exact nat.omega.forward at N with assumption1670    . witness riemannTerms(f, p, leftPartitionTags(p))1671      witness riemannTerms(f, p, leftPartitionTags(p))1672      have preserved := VerticesContained.reflexive at p, N1673      refine ⟨fine, tagged, shared, preserved, i, naturalI, bounded, value⟩1674  . obtain ⟨k, naturalK, before, left, right⟩ := inside1675    obtain ⟨tagged, finer⟩ := FinePartition.insert_at_tagged with fine, before, left, right1676    obtain ⟨u, v, shared⟩ := SharedSubdivisionTotal.exists_insert_at with1677      function, partition, before, left, right1678    have point := indexedInsertedPoints.inserted at p, C, k with points1679    have preserved := VerticesContained.insert_at at p, C, N, k with points, before1680    have nextK := Naturals.constructor.succ at k1681    have nextN := Naturals.constructor.succ at N1682    have boundK : succ(k) ≤ N by exact before1683    have boundInserted := LessEqual.transitive at succ(k), N, succ(N) with1684      nextK, assumption, nextN, boundK, LessEqual.successor at N with assumption1685    witness indexedInsertedPoints(p, C, k)1686    witness succ(N)1687    constructor1688    . exact nat.omega.forward at succ(N) with nextN1689    . witness u1690      witness v1691      refine ⟨finer, tagged, shared, preserved, succ(k),1692        nat.omega.forward at succ(k) with nextK, boundInserted, point⟩16931694-- CommonVertices1695predicate PrefixVerticesContained (q r : Set) (m L : Nat) :=1696  ∀ i ∈ ℕ, i ≤ m → ∃ j ∈ ℕ, j ≤ L ∧ r[j] = q[i]16971698theorem PrefixVerticesContained.transitive (q r s : Set) (m L H : Nat)1699  requires prefix : PrefixVerticesContained(q, r, m, L)1700  requires preserved : VerticesContained(r, s, L, H)1701  shows PrefixVerticesContained(q, s, m, H)1702proof1703  intros i naturalI bounded1704  obtain ⟨j, naturalJ, boundJ, equalQ⟩ := prefix with i, naturalI, bounded1705  obtain ⟨h, naturalH, boundH, equalR⟩ := preserved with j, naturalJ, boundJ1706  witness h1707  constructor1708  . exact naturalH1709  . constructor1710    . exact boundH1711    . rw equalR1712      exact equalQ17131714theorem FinePartition.collect_vertices (f p q : Set) (A B D : Real, N M m : Nat)1715  requires function : f : ℝ → ℝ1716  requires fine : FinePartition(p, A, B, N, D)1717  requires source : IntervalPartition(q, A, B, M)1718  shows m ≤ M → ∃ r, ∃ L ∈ ℕ,1719    FinePartition(r, A, B, L, D) ∧1720    VerticesContained(p, r, N, L) ∧1721    PrefixVerticesContained(q, r, m, L)1722proof1723  induction m1724  | zero =>1725    intro prefix1726    have partitionP : IntervalPartition(p, A, B, N)1727      rcases fine with ⟨partition, positive, widths⟩1728      exact partition1729    have startP : p[0] = A1730      rcases partitionP with ⟨points, start, finish, increasing⟩1731      exact start1732    have startQ : q[0] = A1733      rcases source with ⟨points, start, finish, increasing⟩1734      exact start1735    have prefixZero : PrefixVerticesContained(q, p, 0, N)1736      intros i naturalI bounded1737      have typedI := nat.omega.backward with naturalI1738      have zeroLe := Grace.Core.Nat.Order.LessEqual.zero with typedI1739      have equal := LessEqual.antisymmetric with bounded, zeroLe1740      witness 01741      rw equal1742      constructor1743      . exact nat.omega.forward at 0 with Naturals.constructor.zero1744      . constructor1745        . exact Grace.Core.Nat.Order.LessEqual.zero at N1746        . rw [startP, startQ]1747          rfl1748    witness p1749    witness N1750    constructor1751    . exact nat.omega.forward at N with assumption1752    . have preserved := VerticesContained.reflexive at p, N1753      refine ⟨fine, preserved, prefixZero⟩1754  | succ(k) using ih =>1755    intro prefix1756    have kBound := LessEqual.transitive at k, succ(k), M with1757      LessEqual.successor at k with assumption, prefix1758    obtain ⟨r, L, naturalL, fineR, original, processed⟩ := ih with kBound1759    have partitionR : IntervalPartition(r, A, B, L)1760      rcases fineR with ⟨partition, positive, widths⟩1761      exact partition1762    have alternatives := Less.trichotomy at succ(k), M with1763      Naturals.constructor.succ at k with *{2}1764    cases alternatives with interior | rest1765    . have zeroBefore := natural.zero_before_successor at k1766      have sourceStart := IntervalPartition.strict_indices with source, zeroBefore, prefix1767      have sourceEnd := IntervalPartition.strict_indices at q, A, B, M,1768        succ(k), M with source, interior, LessEqual.reflexive at M with assumption1769      have startQ : q[0] = A1770        rcases source with ⟨points, start, finish, increasing⟩1771        exact start1772      have endQ : q[M] = B1773        rcases source with ⟨points, start, finish, increasing⟩1774        exact finish1775      rw startQ at sourceStart1776      rw endQ at sourceEnd1777      have sourcePoints : RealSequence(q)1778        rcases source with ⟨points, start, finish, increasing⟩1779        exact points1780      have sourceValue := RealSequence.value at q, succ(k) with sourcePoints1781      obtain ⟨s, H, naturalH, u, v, fineS, taggedS, shared, preserved, newPoint⟩ :=1782        FinePartition.insert_or_hit at f, r, A, B, q[succ(k)], D, L with1783          sourceValue, function, fineR, sourceStart, sourceEnd1784      have oldVertices := VerticesContained.transitive with original, preserved1785      have oldPrefix := PrefixVerticesContained.transitive with processed, preserved1786      have nextPrefix : PrefixVerticesContained(q, s, succ(k), H)1787        intros i naturalI bounded1788        have typedI := nat.omega.backward with naturalI1789        have cases := nat.le_succ_cases with bounded1790        cases cases with earlier | last1791          exact oldPrefix with i, naturalI, earlier1792        . obtain ⟨j, naturalJ, boundedJ, valueJ⟩ := newPoint1793          witness j1794          constructor1795          . exact naturalJ1796          . constructor1797            . exact boundedJ1798            . rw last1799              exact valueJ1800      witness s1801      witness H1802      refine ⟨naturalH, fineS, oldVertices, nextPrefix⟩1803    . cases rest with endpoint | impossible1804      . have endQ : q[M] = B1805          rcases source with ⟨points, start, finish, increasing⟩1806          exact finish1807      have endR : r[L] = B1808        rcases partitionR with ⟨points, start, finish, increasing⟩1809        exact finish1810      have nextPrefix : PrefixVerticesContained(q, r, succ(k), L)1811        intros i naturalI bounded1812        have typedI := nat.omega.backward with naturalI1813        have cases := nat.le_succ_cases with bounded1814        cases cases with earlier | last1815          exact processed with i, naturalI, earlier1816        . witness L1817          rw last1818          constructor1819          . exact naturalL1820          . constructor1821            . exact LessEqual.reflexive at L1822            . rw [endpoint, endQ]1823              exact endR1824      witness r1825      witness L1826      refine ⟨naturalL, fineR, original, nextPrefix⟩1827      . have weak := Less.implies_LessEqual at M, succ(k) with impossible1828        have equal := LessEqual.antisymmetric with prefix, weak1829        exfalso1830        have contradiction := Less.irreflexive at M1831        apply contradiction1832        rwa equal at impossible18331834theorem FinePartition.common_vertices (f p q : Set) (A B D : Real, N M : Nat)1835  requires function : f : ℝ → ℝ1836  requires fineP : FinePartition(p, A, B, N, D)1837  requires fineQ : FinePartition(q, A, B, M, D)1838  shows ∃ r, ∃ L ∈ ℕ,1839    FinePartition(r, A, B, L, D) ∧1840    VerticesContained(p, r, N, L) ∧1841    VerticesContained(q, r, M, L)1842proof1843  have partitionQ : IntervalPartition(q, A, B, M)1844    rcases fineQ with ⟨partition, positive, widths⟩1845    exact partition1846  obtain ⟨r, L, naturalL, fineR, old, new⟩ :=1847    FinePartition.collect_vertices at f, p, q, A, B, D, N, M, M with1848      function, fineP, partitionQ, LessEqual.reflexive at M with assumption1849  witness r1850  witness L1851  have contained : VerticesContained(q, r, M, L)1852    unfold VerticesContained1853    exact new1854  refine ⟨naturalL, fineR, old, contained⟩18551856-- Section: ArbitrarySharedTotal1857def refinementIndex.candidates (p r : Set, N M i : Nat) : Set :=1858  {j ∈ ℕ | (i ≤ N → j ≤ M ∧ r[j] = p[i]) ∧ (¬(i ≤ N) → j = 0)}18591860def refinementIndex (p r : Set, N M i : Nat) : Set :=1861  leastNatural(refinementIndex.candidates(p, r, N, M, i))18621863theorem refinementIndex.exists (p r : Set, N M i : Nat)1864requires contained : VerticesContained(p, r, N, M)1865shows ∃ j ∈ ℕ, (i ≤ N → j ≤ M ∧ r[j] = p[i]) ∧ (¬(i ≤ N) → j = 0)1866proof1867  have alternatives : i ≤ N ∨ ¬(i ≤ N) by tauto1868  cases alternatives with bounded | beyond1869    obtain ⟨j, naturalJ, jBound, value⟩ := contained with i,1870      nat.omega.forward at i with assumption, bounded1871    witness j1872    constructor1873    . exact naturalJ1874    . constructor1875      . intro again1876        refine ⟨jBound, value⟩1877      . intro impossible1878        exfalso1879        exact impossible with bounded1880  . witness 01881    constructor1882    . exact nat.omega.forward at 0 with Naturals.constructor.zero1883    . constructor1884      . intro bounded1885        exfalso1886        exact beyond with bounded1887      . intro ignored1888        rfl18891890-- Repeated vertices may give several valid indices. Selecting the least one1891-- makes the existing interface deterministic without strengthening its guards.1892theorem refinementIndex.selected (p r : Set, N M i : Nat)1893  requires contained : VerticesContained(p, r, N, M)1894  shows refinementIndex(p, r, N, M, i) ∈ ℕ ∧1895    (i ≤ N → refinementIndex(p, r, N, M, i) ≤ M ∧1896      r[refinementIndex(p, r, N, M, i)] = p[i]) ∧1897    (¬(i ≤ N) → refinementIndex(p, r, N, M, i) = 0)1898proof1899  have exists := refinementIndex.exists at p, r, N, M, i with contained1900  have inhabited : Nonempty(refinementIndex.candidates(p, r, N, M, i)) by simp [refinementIndex.candidates, Nonempty]1901  have naturals : refinementIndex.candidates(p, r, N, M, i) ⊆ ℕ by simp [refinementIndex.candidates, Subset]1902  have member := leastNatural.member at refinementIndex.candidates(p, r, N, M, i) with *1903  have data := refinementIndex.candidates.membership.forward at1904    p, r, N, M, i, leastNatural(refinementIndex.candidates(p, r, N, M, i)) with *1905  simpa [refinementIndex] using data19061907defgraph refinementIndices (p r : Set, N M : Nat) (i ∈ ℕ) : ℕ :=1908  refinementIndex(p, r, N, M, i)1909requires contained : VerticesContained(p, r, N, M)1910proof1911  obtain ⟨natural, bounded, outside⟩ := refinementIndex.selected at p, r, N, M, i with contained1912  exact natural19131914theorem refinementIndices.vertex (p r : Set) (N M i : Nat)1915  requires contained : VerticesContained(p, r, N, M)1916  requires bounded : i ≤ N1917  shows refinementIndices(p, r, N, M)[i] ≤ M ∧1918    r[refinementIndices(p, r, N, M)[i]] = p[i]1919proof1920  obtain ⟨natural, valid, outside⟩ := refinementIndex.selected at p, r, N, M, i with contained1921  have data := valid with bounded1922  have value := refinementIndices.value at p, r, N, M, i with contained1923  rwa value19241925theorem refinementIndices.strict_cell (p r : Set) (A B : Real, N M i : Nat)1926  requires coarse : IntervalPartition(p, A, B, N)1927  requires fine : IntervalPartition(r, A, B, M)1928  requires contained : VerticesContained(p, r, N, M)1929  requires before : i < N1930  shows Less(refinementIndices(p, r, N, M)[i],1931    refinementIndices(p, r, N, M)[succ(i)])1932proof1933  have hFunction : refinementIndices(p, r, N, M) : ℕ → ℕ1934    exact refinementIndices.function with contained1935  have naturalI := nat.omega.forward at i with assumption1936  have nextI := Naturals.constructor.succ at i1937  have naturalNext := nat.omega.forward with nextI1938  have firstNatural := FunctionBetween.apply_closed with hFunction, naturalI1939  have secondNatural := FunctionBetween.apply_closed with hFunction, naturalNext1940  have firstTyped := nat.omega.backward with firstNatural1941  have secondTyped := nat.omega.backward with secondNatural1942  have boundedI := Less.implies_LessEqual with before1943  have boundedNext : succ(i) ≤ N by exact before1944  have firstData := refinementIndices.vertex with contained, boundedI1945  have nextData := refinementIndices.vertex with contained, boundedNext1946  rcases firstData with ⟨firstBound, firstValue⟩1947  rcases nextData with ⟨nextBound, nextValue⟩1948  have coarsePoints : RealSequence(p)1949    rcases coarse with ⟨points, start, finish, increasing⟩1950    exact points1951  have pointI := RealSequence.value at p, i with coarsePoints1952  have pointNext := RealSequence.value at p, succ(i) with coarsePoints1953  have step := IntervalPartition.cell with coarse, before1954  have cases := Less.trichotomy with firstTyped, secondTyped1955  cases cases with increasing | rest1956  . exact increasing1957  cases rest with equal | decreasing1958  . rw equal at firstValue1959    rw [<- firstValue, <- nextValue] at step1960    have contradiction := realLess.characterization.forward with step1961    exfalso1962    exact RealLess.irreflexive with contradiction1963  . have reverse := IntervalPartition.strict_indices at r, A, B, M,1964      refinementIndices(p, r, N, M)[succ(i)],1965      refinementIndices(p, r, N, M)[i] with fine, decreasing, firstBound1966    rw [nextValue, firstValue] at reverse1967    have cycle := realLess.transitive with pointI, pointNext, pointI, step, reverse1968    have contradiction := realLess.characterization.forward with cycle1969    exfalso1970    exact RealLess.irreflexive with contradiction19711972theorem refinementIndices.zero (p r : Set) (A B : Real, N M : Nat)1973  requires coarse : IntervalPartition(p, A, B, N)1974  requires fine : IntervalPartition(r, A, B, M)1975  requires contained : VerticesContained(p, r, N, M)1976  shows refinementIndices(p, r, N, M)[0] = 01977proof1978  have zeroBound := Grace.Core.Nat.Order.LessEqual.zero at N1979  obtain ⟨bounded, value⟩ := refinementIndices.vertex with contained, zeroBound1980  have startP : p[0] = A1981    rcases coarse with ⟨points, start, finish, steps⟩1982    exact start1983  have startR : r[0] = A1984    rcases fine with ⟨points, start, finish, steps⟩1985    exact start1986  rw [startP, <- startR] at value1987  have indexFunction := refinementIndices.function with contained1988  have member := FunctionBetween.apply_closed at refinementIndices(p, r, N, M),1989    ℕ, ℕ, 0 with indexFunction,1990      nat.omega.forward at 0 with Naturals.constructor.zero1991  have typed := nat.omega.backward with member1992  exact IntervalPartition.vertex_index_unique at r, A, B, M,1993    refinementIndices(p, r, N, M)[0], 0 with fine, bounded,1994      Grace.Core.Nat.Order.LessEqual.zero at M with assumption, value19951996theorem refinementIndices.last (p r : Set) (A B : Real, N M : Nat)1997  requires coarse : IntervalPartition(p, A, B, N)1998  requires fine : IntervalPartition(r, A, B, M)1999  requires contained : VerticesContained(p, r, N, M)2000  shows refinementIndices(p, r, N, M)[N] = M2001proof2002  have data := refinementIndices.vertex at p, r, N, M, N with2003    contained, LessEqual.reflexive at N with assumption2004  rcases data with ⟨bounded, value⟩2005  have endP : p[N] = B2006    rcases coarse with ⟨points, start, finish, steps⟩2007    exact finish2008  have endR : r[M] = B2009    rcases fine with ⟨points, start, finish, steps⟩2010    exact finish2011  rw [endP, <- endR] at value2012  have indexFunction := refinementIndices.function with contained2013  have member := FunctionBetween.apply_closed at refinementIndices(p, r, N, M),2014    ℕ, ℕ, N with indexFunction, nat.omega.forward at N with assumption2015  have typed := nat.omega.backward with member2016  exact IntervalPartition.vertex_index_unique at r, A, B, M,2017    refinementIndices(p, r, N, M)[N], M with fine, bounded,2018      LessEqual.reflexive at M with assumption, value20192020-- RefinementSegments2021defunique refinementSegmentCount (p r : Set, A B : Real, N M i : Nat) (d ∈ ℕ) :=2022  (i < N → add(refinementIndices(p, r, N, M)[i], d) =2023    refinementIndices(p, r, N, M)[succ(i)]) ∧2024  (¬(i < N) → d = 0)2025requires coarse : IntervalPartition(p, A, B, N)2026requires fine : IntervalPartition(r, A, B, M)2027requires contained : VerticesContained(p, r, N, M)2028proof2029  have alternatives : i < N ∨ ¬(i < N) by tauto2030  cases alternatives with before | beyond2031  . have strict := refinementIndices.strict_cell at p, r, A, B, N, M, i with2032      coarse, fine, contained, before2033    obtain ⟨L, naturalL, length⟩ := strict2034    have hFunction := refinementIndices.function with contained2035    have naturalI := nat.omega.forward at i with assumption2036    have hMember := FunctionBetween.apply_closed with hFunction, naturalI2037    have hNat := nat.omega.backward with hMember2038    have shape := add.succ_right at L, refinementIndices(p, r, N, M)[i] with hNat2039    witness succ(L)2040    constructor2041    . exact nat.omega.forward at succ(L) with2042        Naturals.constructor.succ at L with naturalL2043    . constructor2044      . intro again2045        rw add at length2046        rwa shape2047      . intro impossible2048        exfalso2049        exact impossible with before2050  . witness 02051    constructor2052    . exact nat.omega.forward at 0 with Naturals.constructor.zero2053    . constructor2054      . intro before2055        exfalso2056        exact beyond with before2057      . intro ignored2058        rfl20592060uniqueness2061  intros d memberD first e memberE second2062  have naturalD := nat.omega.backward with memberD2063  have naturalE := nat.omega.backward with memberE2064  have alternatives : i < N ∨ ¬(i < N) by tauto2065  cases alternatives with before | beyond2066  . have firstValue : add(refinementIndices(p, r, N, M)[i], d) =2067        refinementIndices(p, r, N, M)[succ(i)]2068      tauto2069    have secondValue : add(refinementIndices(p, r, N, M)[i], e) =2070        refinementIndices(p, r, N, M)[succ(i)]2071      tauto2072    have hFunction := refinementIndices.function with contained2073    have hMember := FunctionBetween.apply_closed at refinementIndices(p, r, N, M),2074      ℕ, ℕ, i with hFunction, nat.omega.forward at i with assumption2075    have hNat := nat.omega.backward with hMember2076    have same : add(refinementIndices(p, r, N, M)[i], d) =2077        add(refinementIndices(p, r, N, M)[i], e)2078      cc2079    exact add.left_cancel with hNat, same2080  . have firstZero : d = 02081      tauto2082    have secondZero : e = 0 by tauto2083    cc20842085defgraph refinementSegmentCounts (p r : Set, A B : Real, N M : Nat) (i ∈ ℕ) : ℕ :=2086  refinementSegmentCount(p, r, A, B, N, M, i)2087requires coarse : IntervalPartition(p, A, B, N)2088requires fine : IntervalPartition(r, A, B, M)2089requires contained : VerticesContained(p, r, N, M)2090proof2091  have selected := refinementSegmentCount.selected at p, r, A, B, N, M, i with2092    coarse, fine, contained2093  rcases selected with ⟨natural, valid, outside⟩2094  exact natural20952096theorem refinementSegmentCounts.endpoint (p r : Set) (A B : Real, N M i : Nat)2097  requires coarse : IntervalPartition(p, A, B, N)2098  requires fine : IntervalPartition(r, A, B, M)2099  requires contained : VerticesContained(p, r, N, M)2100  requires before : i < N2101  shows add(refinementIndices(p, r, N, M)[i],2102    refinementSegmentCounts(p, r, A, B, N, M)[i]) =2103      refinementIndices(p, r, N, M)[succ(i)]2104proof2105  have selected := refinementSegmentCount.selected at p, r, A, B, N, M, i with2106    coarse, fine, contained2107  rcases selected with ⟨natural, valid, outside⟩2108  have data := valid with before2109  have value := refinementSegmentCounts.value at p, r, A, B, N, M, i with2110    coarse, fine, contained2111  rwa value21122113-- RefinementSlices2114theorem TaggedPartition.refinement_cell (p r : Set) (A B : Real, N M i : Nat)2115  requires coarse : IntervalPartition(p, A, B, N)2116  requires fine : IntervalPartition(r, A, B, M)2117  requires contained : VerticesContained(p, r, N, M)2118  requires before : i < N2119  shows TaggedPartition(2120    shiftedRealSequence(r, refinementIndices(p, r, N, M)[i]),2121    shiftedRealSequence(leftPartitionTags(r), refinementIndices(p, r, N, M)[i]),2122    p[i], p[succ(i)], refinementSegmentCounts(p, r, A, B, N, M)[i])2123proof2124  have boundedI := Less.implies_LessEqual with before2125  have boundedNext : succ(i) ≤ N by exact before2126  have first := refinementIndices.vertex with contained, boundedI2127  have next := refinementIndices.vertex with contained, boundedNext2128  rcases first with ⟨firstBound, firstValue⟩2129  rcases next with ⟨nextBound, nextValue⟩2130  have naturalI := nat.omega.forward at i with assumption2131  have nextI := Naturals.constructor.succ at i2132  have naturalNext := nat.omega.forward with nextI2133  have indexFunction := refinementIndices.function with contained2134  have firstMember := FunctionBetween.apply_closed with indexFunction, naturalI2135  have nextMember := FunctionBetween.apply_closed with indexFunction, naturalNext2136  have firstNat := nat.omega.backward with firstMember2137  have nextNat := nat.omega.backward with nextMember2138  have segmentFunction := refinementSegmentCounts.function with coarse, fine, contained2139  have segmentMember := FunctionBetween.apply_closed with segmentFunction, naturalI2140  have segmentNat := nat.omega.backward with segmentMember2141  have pointsR : RealSequence(r)2142    rcases fine with ⟨points, start, finish, increasing⟩2143    exact points2144  have endpointReal := RealSequence.value at r,2145    refinementIndices(p, r, N, M)[succ(i)] with pointsR2146  have length := refinementSegmentCounts.endpoint with coarse, fine, contained, before2147  obtain ⟨R, naturalR, finish⟩ := nextBound2148  have partitionPrefix : IntervalPartition(r, A, r[refinementIndices(p, r, N, M)[succ(i)]],2149      refinementIndices(p, r, N, M)[succ(i)])2150    rw <- finish at fine2151    exact IntervalPartition.prefix with fine2152  have taggedFull := IntervalPartition.left_tagged with fine2153  have taggedPrefix : TaggedPartition(r, leftPartitionTags(r), A,2154      r[refinementIndices(p, r, N, M)[succ(i)]],2155      refinementIndices(p, r, N, M)[succ(i)])2156    rw <- finish at taggedFull2157    exact TaggedPartition.prefix with taggedFull2158  have taggedSlice : TaggedPartition(2159      shiftedRealSequence(r, refinementIndices(p, r, N, M)[i]),2160      shiftedRealSequence(leftPartitionTags(r), refinementIndices(p, r, N, M)[i]),2161      r[refinementIndices(p, r, N, M)[i]],2162      r[refinementIndices(p, r, N, M)[succ(i)]],2163      refinementSegmentCounts(p, r, A, B, N, M)[i])2164    have taggedLength : TaggedPartition(r, leftPartitionTags(r), A,2165        r[refinementIndices(p, r, N, M)[succ(i)]],2166        add(refinementIndices(p, r, N, M)[i],2167          refinementSegmentCounts(p, r, A, B, N, M)[i]))2168      rwa length2169    exact TaggedPartition.suffix at r, leftPartitionTags(r), A,2170      r[refinementIndices(p, r, N, M)[succ(i)]],2171      refinementIndices(p, r, N, M)[i],2172      refinementSegmentCounts(p, r, A, B, N, M)[i] with endpointReal, taggedLength2173  rwa [firstValue, nextValue] at taggedSlice21742175-- RefinementCellSums2176defgraph refinementCellSums (f p r : Set, A B : Real, N M : Nat) (i ∈ ℕ) : ℝ :=2177  riemannSum(f,2178    shiftedRealSequence(r, refinementIndices(p, r, N, M)[i]),2179    shiftedRealSequence(leftPartitionTags(r), refinementIndices(p, r, N, M)[i]),2180    refinementSegmentCounts(p, r, A, B, N, M)[i])2181requires function : f : ℝ → ℝ2182requires coarse : IntervalPartition(p, A, B, N)2183requires fine : IntervalPartition(r, A, B, M)2184requires contained : VerticesContained(p, r, N, M)2185proof2186  have points : RealSequence(r)2187    rcases fine with ⟨points, start, finish, increasing⟩2188    exact points2189  have tags : RealSequence(leftPartitionTags(r))2190    unfold RealSequence2191    exact leftPartitionTags.function with points2192  have indexFunction := refinementIndices.function with contained2193  have indexMember := FunctionBetween.apply_closed with indexFunction, member2194  have indexNat := nat.omega.backward with indexMember2195  have segmentFunction := refinementSegmentCounts.function with coarse, fine, contained2196  have segmentMember := FunctionBetween.apply_closed with segmentFunction, member2197  have segmentNat := nat.omega.backward with segmentMember2198  have shiftedPoints := shiftedRealSequence.sequence at r,2199    refinementIndices(p, r, N, M)[i] with points2200  have shiftedTags := shiftedRealSequence.sequence at leftPartitionTags(r),2201    refinementIndices(p, r, N, M)[i] with tags2202  have sum := riemannSum.real at f,2203    shiftedRealSequence(r, refinementIndices(p, r, N, M)[i]),2204    shiftedRealSequence(leftPartitionTags(r), refinementIndices(p, r, N, M)[i]),2205    refinementSegmentCounts(p, r, A, B, N, M)[i] with function, shiftedPoints, shiftedTags2206  exact sum22072208theorem CellwiseSubdivisionSums.refinement (f p r : Set) (A B : Real, N M : Nat)2209  requires function : f : ℝ → ℝ2210  requires coarse : IntervalPartition(p, A, B, N)2211  requires fine : IntervalPartition(r, A, B, M)2212  requires contained : VerticesContained(p, r, N, M)2213  shows CellwiseSubdivisionSums(f, p,2214    refinementCellSums(f, p, r, A, B, N, M), N)2215proof2216  have sequence : RealSequence(refinementCellSums(f, p, r, A, B, N, M))2217    unfold RealSequence2218    exact refinementCellSums.function with function, coarse, fine, contained2219  constructor2220  . exact sequence2221  . intros i naturalI before2222    have typedI := nat.omega.backward with naturalI2223    have segmentFunction := refinementSegmentCounts.function with coarse, fine, contained2224    have segmentMember := FunctionBetween.apply_closed with segmentFunction, naturalI2225    witness shiftedRealSequence(r, refinementIndices(p, r, N, M)[i])2226    witness shiftedRealSequence(leftPartitionTags(r), refinementIndices(p, r, N, M)[i])2227    witness refinementSegmentCounts(p, r, A, B, N, M)[i]2228    constructor2229    . exact segmentMember2230    . constructor2231      . exact TaggedPartition.refinement_cell at p, r, A, B, N, M, i with2232          coarse, fine, contained, before2233      . exact refinementCellSums.value at f, p, r, A, B, N, M, i with2234          function, coarse, fine, contained22352236-- RefinementTotal2237theorem refinementCellSums.prefix_total (f p r : Set) (A B : Real, N M n : Nat)2238  requires function : f : ℝ → ℝ2239  requires coarse : IntervalPartition(p, A, B, N)2240  requires fine : IntervalPartition(r, A, B, M)2241  requires contained : VerticesContained(p, r, N, M)2242  shows n ≤ N → realPartialSum(refinementCellSums(f, p, r, A, B, N, M), n) =2243    riemannSum(f, r, leftPartitionTags(r), refinementIndices(p, r, N, M)[n])2244proof2245  induction n2246  | zero =>2247    intro bounded2248    have start := refinementIndices.zero with coarse, fine, contained2249    rw [start, realPartialSum.zero, riemannSum.zero]2250    rfl2251  | succ(k) using ih =>2252    intro bounded2253    have before : k < N by exact bounded2254    have kBound := Less.implies_LessEqual with before2255    have previous := ih with kBound2256    have endpoint := refinementSegmentCounts.endpoint with coarse, fine, contained, before2257    have indexFunction := refinementIndices.function with contained2258    have naturalK := nat.omega.forward at k with assumption2259    have indexMember := FunctionBetween.apply_closed with indexFunction, naturalK2260    have indexNat := nat.omega.backward with indexMember2261    have segmentFunction := refinementSegmentCounts.function with coarse, fine, contained2262    have segmentMember := FunctionBetween.apply_closed with segmentFunction, naturalK2263    have segmentNat := nat.omega.backward with segmentMember2264    have points : RealSequence(r)2265      rcases fine with ⟨points, start, finish, increasing⟩2266      exact points2267    have tags : RealSequence(leftPartitionTags(r))2268      unfold RealSequence2269      exact leftPartitionTags.function with points2270    have split := riemannSum.split_at at f, r, leftPartitionTags(r),2271      refinementIndices(p, r, N, M)(k),2272      refinementSegmentCounts(p, r, A, B, N, M)(k) with function, points, tags2273    rw endpoint at split2274    have value := refinementCellSums.value at f, p, r, A, B, N, M, k with2275      function, coarse, fine, contained2276    rw [realPartialSum.succ, value, previous]2277    simp [realAddValue, call2]22782279theorem refinementCellSums.total (f p r : Set) (A B : Real, N M : Nat)2280  requires function : f : ℝ → ℝ2281  requires coarse : IntervalPartition(p, A, B, N)2282  requires fine : IntervalPartition(r, A, B, M)2283  requires contained : VerticesContained(p, r, N, M)2284  shows realPartialSum(refinementCellSums(f, p, r, A, B, N, M), N) =2285    riemannSum(f, r, leftPartitionTags(r), M)2286proof2287  have prefix := refinementCellSums.prefix_total at f, p, r, A, B, N, M, N with2288    function, coarse, fine, contained2289  have bound := LessEqual.reflexive at N2290  have total := prefix with bound2291  have last := refinementIndices.last with coarse, fine, contained2292  rwa last at total22932294-- ArbitrarySharedTotal2295theorem FinePartition.shared_subdivision (f p q : Set) (A B D : Real, N M : Nat)2296  requires function : f : ℝ → ℝ2297  requires fineP : FinePartition(p, A, B, N, D)2298  requires fineQ : FinePartition(q, A, B, M, D)2299  shows ∃ u, ∃ v, SharedSubdivisionTotal(f, p, q, u, v, N, M)2300proof2301  obtain ⟨r, L, naturalL, fineR, containedP, containedQ⟩ := FinePartition.common_vertices with2302    function, fineP, fineQ2303  have partitionP : IntervalPartition(p, A, B, N)2304    rcases fineP with ⟨partition, positive, widths⟩2305    exact partition2306  have partitionQ : IntervalPartition(q, A, B, M)2307    rcases fineQ with ⟨partition, positive, widths⟩2308    exact partition2309  have partitionR : IntervalPartition(r, A, B, L)2310    rcases fineR with ⟨partition, positive, widths⟩2311    exact partition2312  have cellsP := CellwiseSubdivisionSums.refinement with function, partitionP, partitionR, containedP2313  have cellsQ := CellwiseSubdivisionSums.refinement with function, partitionQ, partitionR, containedQ2314  have totalP := refinementCellSums.total with function, partitionP, partitionR, containedP2315  have totalQ := refinementCellSums.total with function, partitionQ, partitionR, containedQ2316  witness refinementCellSums(f, p, r, A, B, N, L)2317  witness refinementCellSums(f, q, r, A, B, M, L)2318  constructor2319  . exact cellsP2320  . constructor2321    . exact cellsQ2322    . rw [totalP, totalQ]2323      rfl23242325theorem FineCellOscillation.compare_fine_partitions (f p t q s : Set) (A B D E : Real, N M : Nat)2326  requires function : f : ℝ → ℝ2327  requires oscillation : FineCellOscillation(f, A, B, D, E)2328  requires fineP : FinePartition(p, A, B, N, D)2329  requires fineQ : FinePartition(q, A, B, M, D)2330  requires taggedP : TaggedPartition(p, t, A, B, N)2331  requires taggedQ : TaggedPartition(q, s, A, B, M)2332  shows (riemannSum(f, p, t, N):R) ≤ (riemannSum(f, q, s, M):R) + (E + E) * (B - A) ∧2333    (riemannSum(f, q, s, M):R) ≤ (riemannSum(f, p, t, N):R) + (E + E) * (B - A)2334proof2335  obtain ⟨u, v, shared⟩ := FinePartition.shared_subdivision at f, p, q, A, B, D, N, M2336    with function, fineP, fineQ2337  exact FineCellOscillation.compare_shared_subdivision with2338    function, oscillation, fineP, fineQ, taggedP, taggedQ, shared2339