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

Open in Workbench Download source

Imports

RiemannSums · HeineCantor · Sequences · ExtremeValue

Declarations

Source

1-- Real analysis: CommonRefinementComparison2-- 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.CommonRefinementComparison8import RiemannSums9import HeineCantor10import Sequences11import ExtremeValue1213-- Section: SplitCellEstimate14theorem dist.le_interval_width (A B C : Real)15  requires lower : A ≤ B16  requires upper : B ≤ C17  shows dist(A, B) ≤ C - A18proof19  have nonnegative : (0:R) ≤ B - A by linarith20  have absolute := abs.of_nonnegative with nonnegative21  have distanceShape : dist(B, A) = B - A22    simp [dist]23  have symmetry := dist.symmetric at A, B with *24  have differenceLe : B - A ≤ C - A by linarith25  rwa [symmetry, distanceShape]2627-- A tag stays within one cell width of the left endpoint.28theorem TaggedPartition.tag_left_distance_le_width (p t : Set) (A B : Real, N i : Nat)29  requires tagged : TaggedPartition(p, t, A, B, N)30  requires beforeEnd : i < N31  shows dist(p[i], t[i]) ≤ (p[succ(i)]:R) - (p[i]:R)32proof33  obtain ⟨lower, upper⟩ := TaggedPartition.tag_bounds with tagged, beforeEnd34  rcases tagged with ⟨partition, tagSequence, cells⟩35  rcases partition with ⟨points, left, right, increasing⟩36  have pointI := RealSequence.value at p, i with points37  have pointNext := RealSequence.value at p, succ(i) with points38  have tagI := RealSequence.value at t, i with tagSequence39  exact dist.le_interval_width with pointI, tagI, pointNext, lower, upper4041-- A fine cell keeps its tag within the same strict mesh bound.42theorem FinePartition.tag_left_distance (p t : Set) (A B : Real, N i : Nat, D : Real)43  requires tagged : TaggedPartition(p, t, A, B, N)44  requires fine : FinePartition(p, A, B, N, D)45  requires beforeEnd : i < N46  shows dist(p[i], t[i]) < D47proof48  have near := TaggedPartition.tag_left_distance_le_width with tagged, beforeEnd49  have width := FinePartition.cell_width with fine, beforeEnd50  rcases tagged with ⟨partition, tags, cells⟩51  rcases partition with ⟨points, left, right, increasing⟩52  have pointI := RealSequence.value at p, i with points53  have pointNext := RealSequence.value at p, succ(i) with points54  have tagI := RealSequence.value at t, i with tags55  exact realLe.transitive_less with near, width5657-- FineCellDistance58theorem FinePartition.cell_points_distance (p : Set) (A B X Y : Real, N i : Nat, D : Real)59  requires fine : FinePartition(p, A, B, N, D)60  requires before : i < N61  requires xCell : X ∈ closedInterval(p[i], p[succ(i)])62  requires yCell : Y ∈ closedInterval(p[i], p[succ(i)])63  shows dist(X, Y) < D + D64proof65  have partition : IntervalPartition(p, A, B, N)66    rcases fine with ⟨partition, positive, widths⟩67    exact partition68  have points : RealSequence(p)69    rcases partition with ⟨points, left, right, increasing⟩70    exact points71  have pointI := RealSequence.value at p, i with points72  have pointNext := RealSequence.value at p, succ(i) with points73  have xBounds := closedInterval.membership.forward with xCell74  have yBounds := closedInterval.membership.forward with yCell75  rcases xBounds with ⟨realX, lowerX, upperX⟩76  rcases yBounds with ⟨realY, lowerY, upperY⟩77  have typedX : Real(X) by exact realX78  have typedY : Real(Y) by exact realY79  have width := FinePartition.cell_width with fine, before80  have nearX := dist.le_interval_width with pointI, typedX, pointNext, lowerX, upperX81  have nearY := dist.le_interval_width with pointI, typedY, pointNext, lowerY, upperY82  have triangle := dist.triangle with typedX, pointI, typedY83  have symmetryX := dist.symmetric with pointI, typedX84  rw symmetryX at nearX85  have distanceXReal := dist.real with typedX, pointI86  have distanceYReal := dist.real with pointI, typedY87  have widthReal := realSubValue.real with pointNext, pointI88  have sumLe := realLe.add with nearX, nearY89  have sumLess := realLess.add at90    p[succ(i)] - p[i], D, p[succ(i)] - p[i], D with91      widthReal, assumption, widthReal, assumption, width, width92  have chain := realLe.transitive with triangle, sumLe93  exact realLe.transitive_less with chain, sumLess9495-- FineCellOscillation96predicate FineCellOscillation (f : Set) (A B D E : Real) :=97  ∀ p, ∀ N ∈ ℕ, ∀ i ∈ ℕ, ∀ X ∈ ℝ, ∀ Y ∈ ℝ,98    FinePartition(p, A, B, N, D) → i < N →99    X ∈ closedInterval(p[i], p[succ(i)]) →100    Y ∈ closedInterval(p[i], p[succ(i)]) →101    X ∈ closedInterval(A, B) → Y ∈ closedInterval(A, B) →102    f(X) ∈ openBall(f(Y), E)103104theorem UniformContinuousOn.fine_cell_oscillation (f : Set) (A B E : Real)105  requires uniform : UniformContinuousOn(f, closedInterval(A, B))106  requires positive : 0 < E107  shows ∃ D ∈ ℝ, 0 < D ∧ FineCellOscillation(f, A, B, D, E)108proof109  rcases uniform with ⟨function, subset, control⟩110  obtain ⟨R, realR, positiveR, maps⟩ := control with E, positive111  have typedR : Real(R) by exact realR112  have halfReal := half.real with typedR113  have halfPositive := half.positive with positiveR114  have halfMember : half(R) ∈ ℝ by exact halfReal115  witness half(R)116  constructor117  . exact halfMember118  . constructor119    . exact halfPositive120      intros p N naturalN i naturalI X realX Y realY fine before xCell yCell xGlobal yGlobal121      have typedN := nat.omega.backward with naturalN122      have typedI := nat.omega.backward with naturalI123      have near := FinePartition.cell_points_distance with fine, before, xCell, yCell124      have double := half.add_self with typedR125      rw double at near126      have data : X ∈ ℝ ∧ dist(X, Y) < R by refine ⟨realX, near⟩127      have ball := openBall.membership.backward with data128      exact maps with X, realX, xGlobal, Y, realY, yGlobal, ball129130theorem ContinuousOn.fine_cell_oscillation (f : Set) (A B E : Real)131  requires continuous : ContinuousOn(f, closedInterval(A, B))132  requires positive : 0 < E133  shows ∃ D ∈ ℝ, 0 < D ∧ FineCellOscillation(f, A, B, D, E)134proof135  have uniform := closedInterval.heine_cantor with continuous136  exact UniformContinuousOn.fine_cell_oscillation with uniform, positive137138-- Interval endpoints are enough to supply the global membership required by139-- the uniform modulus; callers need not repeat it for each pair of tags.140theorem FineCellOscillation.of_cell_endpoints (f p : Set) (A B D E X Y : Real, N i : Nat)141  requires oscillation : FineCellOscillation(f, A, B, D, E)142  requires fine : FinePartition(p, A, B, N, D)143  requires before : i < N144  requires left : A ≤ (p[i]:R)145  requires right : (p[succ(i)]:R) ≤ B146  requires xCell : X ∈ closedInterval(p[i], p[succ(i)])147  requires yCell : Y ∈ closedInterval(p[i], p[succ(i)])148  shows f(X) ∈ openBall(f(Y), E)149proof150  have partition : IntervalPartition(p, A, B, N)151    rcases fine with ⟨partition, positive, widths⟩152    exact partition153  have points : RealSequence(p)154    rcases partition with ⟨points, start, finish, increasing⟩155    exact points156  have pointI := RealSequence.value at p, i with points157  have pointNext := RealSequence.value at p, succ(i) with points158  have nested := closedInterval.nested with pointI, pointNext, left, right159  have xGlobal := nested with X, xCell160  have yGlobal := nested with Y, yCell161  have xData := closedInterval.membership.forward with xCell162  have yData := closedInterval.membership.forward with yCell163  rcases xData with ⟨realX, lowerX, upperX⟩164  rcases yData with ⟨realY, lowerY, upperY⟩165  have naturalN : N ∈ ℕ by simp [Nat]166  have naturalI : i ∈ ℕ by simp [Nat]167  exact oscillation with p, N, naturalN, i, naturalI,168    X, realX, Y, realY, fine, before, xCell, yCell, xGlobal, yGlobal169170theorem FineCellOscillation.on_cell (f p : Set) (A B D E X Y : Real, N i : Nat)171  requires oscillation : FineCellOscillation(f, A, B, D, E)172  requires fine : FinePartition(p, A, B, N, D)173  requires before : i < N174  requires xCell : X ∈ closedInterval(p[i], p[succ(i)])175  requires yCell : Y ∈ closedInterval(p[i], p[succ(i)])176  shows f(X) ∈ openBall(f(Y), E)177proof178  have partition : IntervalPartition(p, A, B, N)179    rcases fine with ⟨partition, positive, widths⟩180    exact partition181  have indexLe := Less.implies_LessEqual with before182  have successorLe : succ(i) ≤ N by exact before183  have leftBounds := IntervalPartition.point_bounds with partition, indexLe184  have rightBounds := IntervalPartition.point_bounds with partition, successorLe185  rcases leftBounds with ⟨left, upperLeft⟩186  rcases rightBounds with ⟨lowerRight, right⟩187  exact FineCellOscillation.of_cell_endpoints with oscillation, fine, before, left, right, xCell, yCell188189-- FineCellTermBound190theorem FineCellOscillation.weighted_tags (f p t s : Set) (A B D E : Real, N i : Nat)191  requires function : f : ℝ → ℝ192  requires oscillation : FineCellOscillation(f, A, B, D, E)193  requires fine : FinePartition(p, A, B, N, D)194  requires taggedT : TaggedPartition(p, t, A, B, N)195  requires taggedS : TaggedPartition(p, s, A, B, N)196  requires before : i < N197  shows (f(t[i]):R) * ((p[succ(i)]:R) - (p[i]:R)) <198    (f(s[i]):R) * ((p[succ(i)]:R) - (p[i]:R)) + E * ((p[succ(i)]:R) - (p[i]:R))199proof200  have partition : IntervalPartition(p, A, B, N)201    rcases fine with ⟨partition, positive, widths⟩202    exact partition203  have points : RealSequence(p)204    rcases partition with ⟨points, start, finish, increasing⟩205    exact points206  have tagsT : RealSequence(t)207    rcases taggedT with ⟨partitionT, tags, cells⟩208    exact tags209  have tagsS : RealSequence(s)210    rcases taggedS with ⟨partitionS, tags, cells⟩211    exact tags212  have pointI := RealSequence.value at p, i with points213  have pointNext := RealSequence.value at p, succ(i) with points214  have tagT := RealSequence.value at t, i with tagsT215  have tagS := RealSequence.value at s, i with tagsS216  have memberT := TaggedPartition.cell with taggedT, before217  have memberS := TaggedPartition.cell with taggedS, before218  have near := FineCellOscillation.on_cell with oscillation, fine, before, memberT, memberS219  have tagTMember : t[i] ∈ ℝ by exact tagT220  have tagSMember : s[i] ∈ ℝ by exact tagS221  have fT := FunctionBetween.apply_closed with function, tagTMember222  have fS := FunctionBetween.apply_closed with function, tagSMember223  obtain ⟨lower, upper⟩ := openBall.order_characterization.forward with near224  have width := IntervalPartition.positive_width with partition, before225  have scaled := realLess.mul_right_of_positive with upper, width226  have distribute : (f(s[i]) + E) * (p[succ(i)] - p[i]) =227      f(s[i]) * (p[succ(i)] - p[i]) + E * (p[succ(i)] - p[i])228    ring229  rwa distribute at scaled230231-- SplitCellEstimate232theorem real.weighted_split_upper (V W Z X C Y E : Real)233  requires left : X ≤ C234  requires right : C ≤ Y235  requires nearLeft : V ≤ W + E236  requires nearRight : V ≤ Z + E237  shows V * (Y - X) ≤ W * (C - X) + Z * (Y - C) + E * (Y - X)238proof239  have leftWidth : 0 ≤ C - X by linarith240  have rightWidth : 0 ≤ Y - C by linarith241  have leftScaled := realLe.mul_right_of_nonnegative with nearLeft, leftWidth242  have rightScaled := realLe.mul_right_of_nonnegative with nearRight, rightWidth243  have added := realLe.add with leftScaled, rightScaled244  have algebra : V * (C - X) + V * (Y - C) = V * (Y - X) by ring245  have other : (W + E) * (C - X) + (Z + E) * (Y - C) =246      W * (C - X) + Z * (Y - C) + E * (Y - X)247    ring248  rwa [algebra, other] at added249250-- Sampling each half of a fine cell changes its contribution by at most251-- epsilon times the original width. The new sample points need only lie in252-- the old cell, which refinement preserves.253theorem FineCellOscillation.split_upper (f p : Set) (A B D E T S R C : Real, N i : Nat)254  requires function : f : ℝ → ℝ255  requires oscillation : FineCellOscillation(f, A, B, D, E)256  requires fine : FinePartition(p, A, B, N, D)257  requires before : i < N258  requires tCell : T ∈ closedInterval(p[i], p[succ(i)])259  requires sCell : S ∈ closedInterval(p[i], p[succ(i)])260  requires rCell : R ∈ closedInterval(p[i], p[succ(i)])261  requires cCell : C ∈ closedInterval(p[i], p[succ(i)])262  shows f(T) * ((p[succ(i)]:R) - (p[i]:R)) ≤263    f(S) * (C - (p[i]:R)) +264      f(R) * ((p[succ(i)]:R) - C) +265        E * ((p[succ(i)]:R) - (p[i]:R))266proof267  have partition : IntervalPartition(p, A, B, N)268    rcases fine with ⟨partition, positive, widths⟩269    exact partition270  have points : RealSequence(p)271    rcases partition with ⟨points, start, finish, steps⟩272    exact points273  have pointI := RealSequence.value at p, i with points274  have pointNext := RealSequence.value at p, succ(i) with points275  obtain ⟨realC, lower, upper⟩ := closedInterval.membership.forward with cCell276  have tBounds := closedInterval.membership.forward with tCell277  have sBounds := closedInterval.membership.forward with sCell278  have rBounds := closedInterval.membership.forward with rCell279  rcases tBounds with ⟨realTMember, lowerT, upperT⟩280  rcases sBounds with ⟨realSMember, cellLowerS, cellUpperS⟩281  rcases rBounds with ⟨realRMember, cellLowerR, cellUpperR⟩282  have nearS := FineCellOscillation.on_cell with oscillation, fine, before, tCell, sCell283  have nearR := FineCellOscillation.on_cell with oscillation, fine, before, tCell, rCell284  have boundsS := openBall.order_characterization.forward with nearS285  have boundsR := openBall.order_characterization.forward with nearR286  rcases boundsS with ⟨lowerS, upperS⟩287  rcases boundsR with ⟨lowerR, upperR⟩288  have weakS := realLess.implies_le with upperS289  have weakR := realLess.implies_le with upperR290  have tValue := FunctionBetween.apply_closed with function, realTMember291  have sValue := FunctionBetween.apply_closed with function, realSMember292  have rValue := FunctionBetween.apply_closed with function, realRMember293  exact real.weighted_split_upper with lower, upper, weakS, weakR294295-- A finite tagged subdivision of a fine cell stays close to any sample of296-- that original cell. This formulation does not require an insertion order.297theorem FineCellOscillation.subdivision_bounds (f p q s : Set) (A B D E T : Real, N i M : Nat)298  requires function : f : ℝ → ℝ299  requires oscillation : FineCellOscillation(f, A, B, D, E)300  requires fine : FinePartition(p, A, B, N, D)301  requires before : i < N302  requires sample : T ∈ closedInterval(p[i], p[succ(i)])303  requires subdivided : TaggedPartition(q, s, p[i], p[succ(i)], M)304  shows (f(T):R) * ((p[succ(i)]:R) - (p[i]:R)) ≤305      (riemannSum(f, q, s, M):R) + E * ((p[succ(i)]:R) - (p[i]:R)) ∧306    (riemannSum(f, q, s, M):R) ≤307      (f(T):R) * ((p[succ(i)]:R) - (p[i]:R)) +308        E * ((p[succ(i)]:R) - (p[i]:R))309proof310  have partition : IntervalPartition(p, A, B, N)311    rcases fine with ⟨partition, positive, widths⟩312    exact partition313  have points : RealSequence(p)314    rcases partition with ⟨points, start, finish, steps⟩315    exact points316  have pointI := RealSequence.value at p, i with points317  have pointNext := RealSequence.value at p, succ(i) with points318  obtain ⟨realTMember, lowerT, upperT⟩ := closedInterval.membership.forward with sample319  have valueMember := FunctionBetween.apply_closed with function, realTMember320  have valueReal : Real(f(T)) by exact valueMember321  have lower : ∀ j ∈ ℕ, j < M →322      f(T) - E ≤ (f(s[j]):R)323    intros j naturalJ lessJ324    have qPartition : IntervalPartition(q, p[i], p[succ(i)], M)325      rcases subdivided with ⟨qPartition, tags, cells⟩326      exact qPartition327    have inSubcell := TaggedPartition.cell with subdivided, lessJ328    have included := IntervalPartition.cell_subset with qPartition, lessJ329    have inCell := included with s[j], inSubcell330    have realTag : Real(s[j])331      rcases subdivided with ⟨qPartition, tags, cells⟩332      exact RealSequence.value with tags333    have near := FineCellOscillation.on_cell with oscillation, fine, before, inCell, sample334    obtain ⟨lowerBound, upperBound⟩ := openBall.order_characterization.forward with near335    have memberTag : s[j] ∈ ℝ by exact realTag336    have image := FunctionBetween.apply_closed with function, memberTag337    exact realLess.implies_le with lowerBound338  have upper : ∀ k ∈ ℕ, k < M →339      (f(s[k]):R) ≤ f(T) + E340    intros k naturalK lessK341    have qPartition : IntervalPartition(q, p[i], p[succ(i)], M)342      rcases subdivided with ⟨qPartition, tags, cells⟩343      exact qPartition344    have inSubcell := TaggedPartition.cell with subdivided, lessK345    have included := IntervalPartition.cell_subset with qPartition, lessK346    have inCell := included with s[k], inSubcell347    have realTag : Real(s[k])348      rcases subdivided with ⟨qPartition, tags, cells⟩349      exact RealSequence.value with tags350    have near := FineCellOscillation.on_cell with oscillation, fine, before, inCell, sample351    obtain ⟨lowerBound, upperBound⟩ := openBall.order_characterization.forward with near352    exact realLess.implies_le with upperBound353  obtain ⟨below, above⟩ := riemannSum.between_constants with function, subdivided, lower, upper354  have leftAlgebra : (f(T) - E) * (p[succ(i)] - p[i]) =355      f(T) * (p[succ(i)] - p[i]) - E * (p[succ(i)] - p[i])356    ring357  have rightAlgebra : (f(T) + E) * (p[succ(i)] - p[i]) =358      f(T) * (p[succ(i)] - p[i]) + E * (p[succ(i)] - p[i])359    ring360  rw leftAlgebra at below361  rw rightAlgebra at above362  have widthReal := realSubValue.real with pointNext, pointI363  have productReal := realMulValue.real with valueReal, widthReal364  have errorReal := realMulValue.real at E, p[succ(i)] - p[i] with assumption, widthReal365  have leftReal := realSubValue.real with productReal, errorReal366  have sumReal : Real(riemannSum(f, q, s, M))367    have qPartition : IntervalPartition(q, p[i], p[succ(i)], M)368      rcases subdivided with ⟨qPartition, tags, cells⟩369      exact qPartition370    rcases qPartition with ⟨qPoints, start, finish, steps⟩371    rcases subdivided with ⟨another, tags, cells⟩372    exact riemannSum.real with function, qPoints, tags373  have shifted := realLe.add_right with leftReal, sumReal, errorReal, below374  have cancel : (f(T) * (p[succ(i)] - p[i]) - E * (p[succ(i)] - p[i])) +375      E * (p[succ(i)] - p[i]) = f(T) * (p[succ(i)] - p[i])376    ring377  rw cancel at shifted378  have first : f(T) * (p[succ(i)] - p[i]) ≤ riemannSum(f, q, s, M) + E * (p[succ(i)] - p[i]) by exact shifted379  refine ⟨first, above⟩380381-- Section: CommonRefinementComparison382theorem realPartialSum.cell_error_prefix (u v p : Set) (E : Real, N n : Nat)383  requires sequenceU : RealSequence(u)384  requires sequenceV : RealSequence(v)385  requires points : RealSequence(p)386  requires errors : ∀ i ∈ ℕ, i < N → (u[i]:R) ≤ (v[i]:R) + E * ((p[succ(i)]:R) - (p[i]:R))387  shows n ≤ N → (realPartialSum(u, n):R) ≤ (realPartialSum(v, n):R) + E * ((p[n]:R) - (p[0]:R))388proof389  induction n390  | zero =>391    intro bounded392    rw [realPartialSum.zero, realPartialSum.zero]393    have point0 := RealSequence.value at p, 0 with points394    have self := realSubValue.self with point0395    rw self396    have zeroProduct : E * (0:R) = (0:R) by ring397    rw zeroProduct398    have zeroSum : (0:R) + (0:R) = (0:R) by ring399    rw zeroSum400    exact realLe.reflexive with realZero.real401  | succ(k) using ih =>402    intro bounded403    have before : k < N by exact bounded404    have kLeNext := LessEqual.successor at k405    have kLeN := LessEqual.transitive at k, succ(k), N with406      assumption, Naturals.constructor.succ at k with *{2}, kLeNext, bounded407    have prefix := ih with kLeN408    have point0 := RealSequence.value at p, 0 with points409    have pointK := RealSequence.value at p, k with points410    have pointNext := RealSequence.value at p, succ(k) with points411    have termU := RealSequence.value at u, k with sequenceU412    have termV := RealSequence.value at v, k with sequenceV413    have sumU := realPartialSum.real at u, k with sequenceU414    have sumV := realPartialSum.real at v, k with sequenceV415    have prefixWidth := realSubValue.real with pointK, point0416    have cellWidth := realSubValue.real with pointNext, pointK417    have prefixError := realMulValue.real at E, p[k] - p[0] with assumption, prefixWidth418    have cellError := realMulValue.real at E, p[succ(k)] - p[k] with assumption, cellWidth419    have firstRhs := realAddValue.real with sumV, prefixError420    have secondRhs := realAddValue.real with termV, cellError421    have bound := errors with k, nat.omega.forward at k with assumption, before422    have added := realLe.add with sumU, firstRhs, termU, secondRhs, prefix, bound423    have rearrange : (realPartialSum(v, k) + E * (p[k] - p[0])) +424        (v[k] + E * (p[succ(k)] - p[k])) =425      (realPartialSum(v, k) + v[k]) + E * (p[succ(k)] - p[0])426      ring427    rw rearrange at added428    rw [realPartialSum.succ, realPartialSum.succ]429    unfold realAddValue430    unfold call2 at added431    unfold call2432    exact added433434-- Only cells of the partition are compared; arbitrary sequence tails do not435-- affect the resulting bound.436theorem realPartialSum.cell_error_on_partition (u v p : Set) (A B E : Real, N : Nat)437  requires sequenceU : RealSequence(u)438  requires sequenceV : RealSequence(v)439  requires partition : IntervalPartition(p, A, B, N)440  requires errors : ∀ i ∈ ℕ, i < N →441    (u[i]:R) ≤ (v[i]:R) + E * ((p[succ(i)]:R) - (p[i]:R))442  shows (realPartialSum(u, N):R) ≤ (realPartialSum(v, N):R) + E * (B - A)443proof444  rcases partition with ⟨points, start, finish, increasing⟩445  have result := realPartialSum.cell_error_prefix at u, v, p, E, N, N with446    sequenceU, sequenceV, points, errors,447    LessEqual.reflexive at N with assumption448  rwa [start, finish] at result449450-- CellwiseSubdivision451predicate CellwiseSubdivisionSums (f p u : Set) (N : Nat) :=452  RealSequence(u) ∧453  (∀ i ∈ ℕ, i < N → ∃ q, ∃ s, ∃ M ∈ ℕ,454    TaggedPartition(q, s, p[i], p[succ(i)], M) ∧455      u[i] = riemannSum(f, q, s, M))456457theorem FineCellOscillation.cellwise_subdivision_bounds (f p t u : Set) (A B D E : Real, N : Nat)458  requires function : f : ℝ → ℝ459  requires oscillation : FineCellOscillation(f, A, B, D, E)460  requires fine : FinePartition(p, A, B, N, D)461  requires tagged : TaggedPartition(p, t, A, B, N)462  requires subdivided : CellwiseSubdivisionSums(f, p, u, N)463  shows (riemannSum(f, p, t, N):R) ≤464      (realPartialSum(u, N):R) + E * (B - A) ∧465    (realPartialSum(u, N):R) ≤466      (riemannSum(f, p, t, N):R) + E * (B - A)467proof468  have partition : IntervalPartition(p, A, B, N)469    rcases fine with ⟨partition, positive, widths⟩470    exact partition471  have points : RealSequence(p)472    rcases partition with ⟨points, start, finish, increasing⟩473    exact points474  have tags : RealSequence(t)475    rcases tagged with ⟨partitionT, tags, cells⟩476    exact tags477  rcases subdivided with ⟨sequenceU, cellData⟩478  have terms : RealSequence(riemannTerms(f, p, t))479    unfold RealSequence480    exact riemannTerms.function with function, points, tags481  have local : ∀ i ∈ ℕ, i < N → ((riemannTerms(f, p, t)[i]:R) ≤ (u[i]:R) + E * ((p[succ(i)]:R) - (p[i]:R)) ∧ (u[i]:R) ≤ (riemannTerms(f, p, t)[i]:R) + E * ((p[succ(i)]:R) - (p[i]:R)))482    intros i naturalI before483    obtain ⟨q, s, M, naturalM, taggedSub, equal⟩ := cellData with i, naturalI, before484    have typedM := nat.omega.backward with naturalM485    have sample := TaggedPartition.cell with tagged, before486    have estimates := FineCellOscillation.subdivision_bounds with487      function, oscillation, fine, before, sample, taggedSub488    rcases estimates with ⟨first, second⟩489    have term := riemannTerms.value at f, p, t, i with function, points, tags490    constructor491    . rw [term, equal]492      unfold realMulValue493      unfold call2494      unfold call2 at first495      exact first496    . rw [term, equal]497      unfold realMulValue498      unfold call2499      unfold call2 at second500      exact second501  have upperErrors : ∀ j ∈ ℕ, j < N →502    (riemannTerms(f, p, t)[j]:R) ≤ (u[j]:R) + E * ((p[succ(j)]:R) - (p[j]:R))503    intros j naturalJ beforeJ504    obtain ⟨first, second⟩ := local with j, naturalJ, beforeJ505    exact first506  have lowerErrors : ∀ k ∈ ℕ, k < N →507    (u[k]:R) ≤ (riemannTerms(f, p, t)[k]:R) + E * ((p[succ(k)]:R) - (p[k]:R))508    intros k naturalK beforeK509    obtain ⟨first, second⟩ := local with k, naturalK, beforeK510    exact second511  have first := realPartialSum.cell_error_on_partition with terms, sequenceU, partition, upperErrors512  have second := realPartialSum.cell_error_on_partition with sequenceU, terms, partition, lowerErrors513  constructor514  . unfold riemannSum515    exact first516  . unfold riemannSum517    exact second518519-- CommonRefinementComparison520predicate SharedSubdivisionTotal (f p q u v : Set) (N M : Nat) :=521  CellwiseSubdivisionSums(f, p, u, N) ∧522  CellwiseSubdivisionSums(f, q, v, M) ∧523  realPartialSum(u, N) = realPartialSum(v, M)524525theorem FineCellOscillation.compare_shared_subdivision (f p t q s u v : Set) (A B D E : Real, N M : Nat)526  requires function : f : ℝ → ℝ527  requires oscillation : FineCellOscillation(f, A, B, D, E)528  requires fineP : FinePartition(p, A, B, N, D)529  requires fineQ : FinePartition(q, A, B, M, D)530  requires taggedP : TaggedPartition(p, t, A, B, N)531  requires taggedQ : TaggedPartition(q, s, A, B, M)532  requires shared : SharedSubdivisionTotal(f, p, q, u, v, N, M)533  shows (riemannSum(f, p, t, N):R) ≤ (riemannSum(f, q, s, M):R) + (E + E) * (B - A) ∧534    (riemannSum(f, q, s, M):R) ≤ (riemannSum(f, p, t, N):R) + (E + E) * (B - A)535proof536  rcases shared with ⟨cellsP, cellsQ, equalTotals⟩537  have boundP := FineCellOscillation.cellwise_subdivision_bounds with538    function, oscillation, fineP, taggedP, cellsP539  have boundQ := FineCellOscillation.cellwise_subdivision_bounds with540    function, oscillation, fineQ, taggedQ, cellsQ541  rcases boundP with ⟨pToU, uToP⟩542  rcases boundQ with ⟨qToV, vToQ⟩543  have partitionP : IntervalPartition(p, A, B, N)544    rcases fineP with ⟨partition, positive, widths⟩545    exact partition546  have partitionQ : IntervalPartition(q, A, B, M)547    rcases fineQ with ⟨partition, positive, widths⟩548    exact partition549  have pointsP : RealSequence(p)550    rcases partitionP with ⟨points, start, finish, increasing⟩551    exact points552  have pointsQ : RealSequence(q)553    rcases partitionQ with ⟨points, start, finish, increasing⟩554    exact points555  have tagsP : RealSequence(t)556    rcases taggedP with ⟨partition, tags, cells⟩557    exact tags558  have tagsQ : RealSequence(s)559    rcases taggedQ with ⟨partition, tags, cells⟩560    exact tags561  have sumP := riemannSum.real at f, p, t, N with function, pointsP, tagsP562  have sumQ := riemannSum.real at f, q, s, M with function, pointsQ, tagsQ563  rcases cellsP with ⟨sequenceU, dataU⟩564  rcases cellsQ with ⟨sequenceV, dataV⟩565  have totalU := realPartialSum.real at u, N with sequenceU566  have totalV := realPartialSum.real at v, M with sequenceV567  have width := realSubValue.real at B, A with *568  have err := realMulValue.real at E, B - A with assumption, width569  have sumPErr := realAddValue.real with sumP, err570  have sumQErr := realAddValue.real with sumQ, err571  have firstShift := realLe.add_right with totalV, sumQErr, err, vToQ572  rw ← equalTotals at firstShift573  have firstChain := realLe.transitive with pToU, firstShift574  have secondShift := realLe.add_right with totalU, sumPErr, err, uToP575  rw equalTotals at secondShift576  have secondChain := realLe.transitive with qToV, secondShift577  have firstShape : (riemannSum(f, q, s, M) + E * (B - A)) + E * (B - A) =578      riemannSum(f, q, s, M) + (E + E) * (B - A)579    ring580  have secondShape : (riemannSum(f, p, t, N) + E * (B - A)) + E * (B - A) =581      riemannSum(f, p, t, N) + (E + E) * (B - A)582    ring583  rw firstShape at firstChain584  rw secondShape at secondChain585  refine ⟨firstChain, secondChain⟩586587-- Section: OneCellComparison588def oneCellPoint (A B : Real, n : Nat) → Set589  | A, B, zero => A590  | A, B, succ(k) => B591592theorem oneCellPoint.real (A B : Real, n : Nat)593  shows Real(oneCellPoint(A, B, n))594proof595  induction n596  | zero =>597    rwa oneCellPoint598  | succ(k) using ih =>599    rwa oneCellPoint600601-- A checked parameterized graph. The closure proof is the only graph-specific602-- obligation; defgraph derives membership, function, and application laws.603defgraph oneCellPoints (A B : Real) (n ∈ ℕ) : ℝ := oneCellPoint(A, B, n)604proof605  have realPoint := oneCellPoint.real at A, B, n with606    *{3}607  exact realPoint608609theorem oneCellPoints.sequence (A B : Real)610  shows RealSequence(oneCellPoints(A, B))611proof612  unfold RealSequence613  exact oneCellPoints.function with *{2}614615theorem Nat.lt_one_zero (i : Nat)616  requires before : i < succ(0)617  shows i = 0618proof619  have zeroNatural := Naturals.constructor.zero620  have oneNatural := Naturals.constructor.succ with zeroNatural621  have member := membership.of_Less at i, succ(0) with622    assumption, oneNatural, before623  have alternatives := membership.successor_forward{n := 0} with member624  cases alternatives with empty | equal625  . exfalso626    rw nat.zero at empty627    simp628  . exact equal629630theorem oneCellPoints.zero (A B : Real)631  shows oneCellPoints(A, B)[0] = A632proof633  have value := oneCellPoints.value at A, B, 0 with634    *{2}, Naturals.constructor.zero635  rwa oneCellPoint at value636637theorem oneCellPoints.one (A B : Real)638  shows oneCellPoints(A, B)[succ(0)] = B639proof640  have zeroNatural := Naturals.constructor.zero641  have oneNatural := Naturals.constructor.succ with zeroNatural642  have value := oneCellPoints.value at A, B, succ(0) with643    *{2}, oneNatural644  rwa oneCellPoint at value645646-- OneCellPartition647theorem oneCellPoints.partition (A B : Real)648  requires ordered : A < B649  shows IntervalPartition(oneCellPoints(A, B), A, B, succ(0))650proof651  constructor652  . exact oneCellPoints.sequence with *{2}653  . constructor654    . exact oneCellPoints.zero with *{2}655    . constructor656      . exact oneCellPoints.one with *{2}657      . intros i naturalI before658        have typedI := nat.omega.backward with naturalI659        have atZero := Nat.lt_one_zero with typedI, before660        rwa [atZero, oneCellPoints.zero, oneCellPoints.one]661662theorem oneCellPoints.tagged (A B : Real)663  requires ordered : A < B664  shows TaggedPartition(oneCellPoints(A, B), constantSequence(A), A, B, succ(0))665proof666  constructor667  . exact oneCellPoints.partition with ordered668  . constructor669    . exact constantSequence.sequence at A670    . intros i naturalI before671      have typedI := nat.omega.backward with naturalI672      have atZero := Nat.lt_one_zero with typedI, before673      rw [atZero, constantSequence.value, oneCellPoints.zero, oneCellPoints.one]674      have le := realLess.implies_le with ordered675      exact closedInterval.left_mem with *676677-- OneCellTaggedValue678theorem oneCellPoints.tagged_at (A B T : Real)679  requires ordered : A < B680  requires tag : T ∈ closedInterval(A, B)681  shows TaggedPartition(oneCellPoints(A, B), constantSequence(T), A, B, succ(0))682proof683  constructor684  . exact oneCellPoints.partition with ordered685  . constructor686    . exact constantSequence.sequence at T687    . intros i naturalI before688      have typedI := nat.omega.backward with naturalI689      have atZero := Nat.lt_one_zero with typedI, before690      rwa [atZero, constantSequence.value, oneCellPoints.zero, oneCellPoints.one]691692theorem riemannSum.one_cell_tag (f : Set) (A B T : Real)693  requires function : f : ℝ → ℝ694  shows riemannSum(f, oneCellPoints(A, B), constantSequence(T), succ(0)) =695    f(T) * (B - A)696proof697  have pointSequence := oneCellPoints.sequence at A, B with *698  have tagSequence := constantSequence.sequence at T699  have step := riemannSum.succ at700    f, oneCellPoints(A, B), constantSequence(T), 0 with701      function, pointSequence, tagSequence702  rw [riemannSum.zero, oneCellPoints.zero, oneCellPoints.one, constantSequence.value] at step703  rw step704  have realT : T ∈ ℝ705    have typedT : Real(T) by assumption706    exact typedT707  have imageMember := FunctionBetween.apply_closed with function, realT708  have imageReal : Real(f(T)) by exact imageMember709  have width := realSubValue.real at B, A with *710  have product := realMulValue.real with imageReal, width711  have zero := realAddValue.zero_left with product712  unfold realAddValue713  unfold realMulValue714  unfold call2 at zero715  simp [call2]716717-- TrivialSubdivision718theorem TaggedPartition.trivial_subdivision (f p t : Set) (A B : Real, N : Nat)719  requires function : f : ℝ → ℝ720  requires tagged : TaggedPartition(p, t, A, B, N)721  shows CellwiseSubdivisionSums(f, p, riemannTerms(f, p, t), N)722proof723  have partition : IntervalPartition(p, A, B, N)724    rcases tagged with ⟨partition, tags, cells⟩725    exact partition726  have points : RealSequence(p)727    rcases partition with ⟨points, start, finish, increasing⟩728    exact points729  have tags : RealSequence(t)730    rcases tagged with ⟨partitionT, tags, cells⟩731    exact tags732  constructor733  . unfold RealSequence734    exact riemannTerms.function with function, points, tags735  . intros i naturalI before736    have typedI := nat.omega.backward with naturalI737    have pointI := RealSequence.value at p, i with points738    have pointNext := RealSequence.value at p, succ(i) with points739    have tagI := RealSequence.value at t, i with tags740    have increasing := IntervalPartition.cell with partition, before741    have cell := TaggedPartition.cell with tagged, before742    have single := oneCellPoints.tagged_at with increasing, cell743    witness oneCellPoints(p[i], p[succ(i)])744    witness constantSequence(t[i])745    witness succ(0)746    constructor747    . have zeroNat := Naturals.constructor.zero748      have oneNat := Naturals.constructor.succ with zeroNat749      exact nat.omega.forward with oneNat750    . constructor751      . exact single752      . have term := riemannTerms.value at f, p, t, i with function, points, tags753        have singleValue := riemannSum.one_cell_tag at f, p[i], p[succ(i)], t[i] with function754        rw [term, singleValue]755        unfold realMulValue756        unfold call2757        rfl758759-- OneCellCommonRefinement760theorem SharedSubdivisionTotal.one_cell (f q s : Set) (A B T : Real, M : Nat)761  requires function : f : ℝ → ℝ762  requires tagged : TaggedPartition(q, s, A, B, M)763  shows SharedSubdivisionTotal(f, oneCellPoints(A, B), q,764    constantSequence(riemannSum(f, q, s, M)), riemannTerms(f, q, s), succ(0), M)765proof766  have partition : IntervalPartition(q, A, B, M)767    rcases tagged with ⟨partition, tags, cells⟩768    exact partition769  have points : RealSequence(q)770    rcases partition with ⟨points, start, finish, increasing⟩771    exact points772  have tags : RealSequence(s)773    rcases tagged with ⟨partitionS, tags, cells⟩774    exact tags775  have sumReal := riemannSum.real with function, points, tags776  have trivial := TaggedPartition.trivial_subdivision with function, tagged777  have terms : RealSequence(riemannTerms(f, q, s))778    unfold RealSequence779    exact riemannTerms.function with function, points, tags780  have totalReal := realPartialSum.real with terms781  have coarse : CellwiseSubdivisionSums(f, oneCellPoints(A, B),782      constantSequence(riemannSum(f, q, s, M)), succ(0))783    constructor784    . exact constantSequence.sequence with sumReal785    . intros i naturalI before786      have typedI := nat.omega.backward with naturalI787      have zero := Nat.lt_one_zero with typedI, before788      witness q789      witness s790      witness M791      constructor792      . exact nat.omega.forward at M with assumption793      . constructor794        . rw [zero, oneCellPoints.zero, oneCellPoints.one]795          exact tagged796        . rw [zero, constantSequence.value]797          rfl798  have total : realPartialSum(constantSequence(riemannSum(f, q, s, M)), succ(0)) =799      realPartialSum(riemannTerms(f, q, s), M)800    rw [realPartialSum.succ, realPartialSum.zero, constantSequence.value]801    unfold riemannSum802    have zero := realAddValue.zero_left with totalReal803    unfold realAddValue804    unfold call2 at zero805    exact zero806  refine ⟨coarse, trivial, total⟩807808-- OneCellFine809theorem oneCellPoints.fine (A B D : Real)810  requires ordered : A < B811  requires positive : (0:R) < D812  requires width : B - A < D813  shows FinePartition(oneCellPoints(A, B), A, B, succ(0), D)814proof815  constructor816  . exact oneCellPoints.partition with ordered817  . constructor818    . exact positive819    . intros i naturalI before820      have typedI := nat.omega.backward with naturalI821      have atZero := Nat.lt_one_zero with typedI, before822      rwa [atZero, oneCellPoints.zero, oneCellPoints.one]823824-- OneCellComparison825theorem FineCellOscillation.compare_one_cell (f q s : Set) (A B D E T : Real, M : Nat)826  requires function : f : ℝ → ℝ827  requires oscillation : FineCellOscillation(f, A, B, D, E)828  requires ordered : A < B829  requires width : B - A < D830  requires fine : FinePartition(q, A, B, M, D)831  requires tagged : TaggedPartition(q, s, A, B, M)832  requires tag : T ∈ closedInterval(A, B)833  shows (f(T):R) * (B - A) ≤ (riemannSum(f, q, s, M):R) + (E + E) * (B - A) ∧834    (riemannSum(f, q, s, M):R) ≤ f(T) * (B - A) + (E + E) * (B - A)835proof836  have positive : (0:R) < D837    rcases fine with ⟨partition, positive, widths⟩838    exact positive839  have coarse := oneCellPoints.fine with ordered, positive, width840  have coarseTagged := oneCellPoints.tagged_at with ordered, tag841  have shared := SharedSubdivisionTotal.one_cell at f, q, s, A, B, T, M with842    function, tagged843  have comparison := FineCellOscillation.compare_shared_subdivision with844    function, oscillation, coarse, fine, coarseTagged, tagged, shared845  have value := riemannSum.one_cell_tag at f, A, B, T with function846  rwa value at comparison847848-- Section: AffineCofinality849def intervalMidpoint (A B : Real) : Real := A + half(B - A)850851theorem intervalMidpoint.real (A B : Real)852  shows Real(intervalMidpoint(A, B))853proof854  unfold intervalMidpoint855  have width := realSubValue.real at B, A with *856  have halfWidth := half.real with width857  exact realAddValue.real with assumption, halfWidth858859theorem intervalMidpoint.left_width (A B : Real)860  shows intervalMidpoint(A, B) - A = half(B - A)861proof862  unfold intervalMidpoint863  ring864865theorem intervalMidpoint.right_width (A B : Real)866  shows B - intervalMidpoint(A, B) = half(B - A)867proof868  have width := realSubValue.real at B, A with *869  have doubled := half.add_self with width870  have cancellation : (half(B - A) + half(B - A)) - half(B - A) = half(B - A) by ring871  rw doubled at cancellation872  unfold intervalMidpoint873  have reassociated : B - (A + half(B - A)) = (B - A) - half(B - A) by ring874  rwa reassociated875876theorem intervalMidpoint.between (A B : Real)877  requires ordered : A < B878  shows A < intervalMidpoint(A, B) ∧ intervalMidpoint(A, B) < B879proof880  have positive := realLess.iff_pos_sub.forward with ordered881  have halfPositive := half.positive with positive882  have left := intervalMidpoint.left_width at A, B with *883  have right := intervalMidpoint.right_width at A, B with *884  constructor885  . have positiveLeft := halfPositive886    rw ← left at positiveLeft887    exact realLess.iff_pos_sub.backward with positiveLeft888  . have positiveRight := halfPositive889    rw ← right at positiveRight890    exact realLess.iff_pos_sub.backward with positiveRight891892-- TwoCellPoints893def twoCellPoint (A M B : Real, n : Nat) → Set894  | A, M, B, zero => A895  | A, M, B, succ(k) => oneCellPoint(M, B, k)896897theorem twoCellPoint.real (A M B : Real, n : Nat)898  shows Real(twoCellPoint(A, M, B, n))899proof900  induction n901  | zero =>902    rwa twoCellPoint903  | succ(k) using ih =>904    rw twoCellPoint905    exact oneCellPoint.real with *{3}906907-- A checked parameterized graph. The closure proof is the only graph-specific908-- obligation; defgraph derives membership, function, and application laws.909defgraph twoCellPoints (A M B : Real) (n ∈ ℕ) : ℝ := twoCellPoint(A, M, B, n)910proof911  have realPoint := twoCellPoint.real at A, M, B, n with912    *{4}913  exact realPoint914915theorem twoCellPoints.sequence (A M B : Real)916  shows RealSequence(twoCellPoints(A, M, B))917proof918  unfold RealSequence919  exact twoCellPoints.function with *{3}920921theorem Nat.lt_two_cases (i : Nat)922  requires before : i < succ(succ(0))923  shows i = 0 ∨ i = succ(0)924proof925  have zeroNatural := Naturals.constructor.zero926  have oneNatural := Naturals.constructor.succ with zeroNatural927  have twoNatural := Naturals.constructor.succ with oneNatural928  have member := membership.of_Less at i, succ(succ(0)) with929    assumption, twoNatural, before930  have alternatives := membership.successor_forward{n := succ(0)} at i with member931  cases alternatives with earlier | equal932  . have cases := membership.successor_forward{n := 0} at i with earlier933    cases cases with empty | zero934    . exfalso935      rw nat.zero at empty936      simp937    . left938      exact zero939  . right940    exact equal941942theorem twoCellPoints.zero (A M B : Real)943  shows twoCellPoints(A, M, B)[0] = A944proof945  have value := twoCellPoints.value at A, M, B, 0 with946    *{3}, Naturals.constructor.zero947  rwa twoCellPoint at value948949theorem twoCellPoints.one (A M B : Real)950  shows twoCellPoints(A, M, B)[succ(0)] = M951proof952  have zeroNatural := Naturals.constructor.zero953  have oneNatural := Naturals.constructor.succ with zeroNatural954  have value := twoCellPoints.value at A, M, B, succ(0) with955    *{3}, oneNatural956  rwa [twoCellPoint, oneCellPoint] at value957958theorem twoCellPoints.two (A M B : Real)959  shows twoCellPoints(A, M, B)[succ(succ(0))] = B960proof961  have zeroNatural := Naturals.constructor.zero962  have oneNatural := Naturals.constructor.succ with zeroNatural963  have twoNatural := Naturals.constructor.succ with oneNatural964  have value := twoCellPoints.value at A, M, B, succ(succ(0)) with965    *{3}, twoNatural966  rwa [twoCellPoint, oneCellPoint] at value967968-- TwoCellPartition969theorem twoCellPoints.partition (A M B : Real)970  requires left : A < M971  requires right : M < B972  shows IntervalPartition(twoCellPoints(A, M, B), A, B, succ(succ(0)))973proof974  constructor975  . exact twoCellPoints.sequence at A, M, B with976      *{3}977  . constructor978    . exact twoCellPoints.zero at A, M, B with979        *{3}980    . constructor981      . exact twoCellPoints.two at A, M, B with982          *{3}983      . intros i naturalI before984        have typedI := nat.omega.backward with naturalI985        have cases := Nat.lt_two_cases with typedI, before986        cases cases with first | second987        . rw [first, twoCellPoints.zero, twoCellPoints.one]988          exact left989        . rw [second, twoCellPoints.one, twoCellPoints.two]990          exact right991992theorem twoCellPoints.tagged (A M B : Real)993  requires left : A < M994  requires right : M < B995  shows TaggedPartition(twoCellPoints(A, M, B), twoCellPoints(A, M, B),996    A, B, succ(succ(0)))997proof998  have partition := twoCellPoints.partition with left, right999  have sequence := twoCellPoints.sequence at A, M, B with1000    *{3}1001  constructor1002  . exact partition1003  . constructor1004    . exact sequence1005    . intros i naturalI before1006      have typedI := nat.omega.backward with naturalI1007      have cell := IntervalPartition.cell with partition, before1008      have le := realLess.implies_le with cell1009      have realI := RealSequence.value with sequence1010      have realNext := RealSequence.value at twoCellPoints(A, M, B), succ(i) with sequence1011      exact closedInterval.left_mem with realI, realNext, le10121013-- TwoCellFine1014theorem twoCellPoints.fine (A B D : Real)1015  requires ordered : A < B1016  requires positive : (0:R) < D1017  requires halfWidth : half(B - A) < D1018  shows FinePartition(twoCellPoints(A, intervalMidpoint(A, B), B),1019    A, B, succ(succ(0)), D)1020proof1021  obtain ⟨left, right⟩ := intervalMidpoint.between with ordered1022  have middle := intervalMidpoint.real at A, B with *1023  constructor1024  . exact twoCellPoints.partition at A, intervalMidpoint(A, B), B with1025      assumption, middle, assumption, left, right1026  . constructor1027    . exact positive1028    . intros i naturalI before1029      have typedI := nat.omega.backward with naturalI1030      have cases := Nat.lt_two_cases with typedI, before1031      cases cases with first | second1032      . rw [first, twoCellPoints.zero, twoCellPoints.one, intervalMidpoint.left_width]1033        exact halfWidth1034      . rw [second, twoCellPoints.one, twoCellPoints.two, intervalMidpoint.right_width]1035        exact halfWidth10361037-- LargeMeshPartitions1038theorem FineTaggedPartitionsExist.large_mesh (A B D : Real)1039  requires ordered : A < B1040  requires positive : (0:R) < D1041  requires width : B - A < D1042  shows ∃ p, ∃ t, ∃ N ∈ ℕ,1043    TaggedPartition(p, t, A, B, N) ∧ FinePartition(p, A, B, N, D)1044proof1045  witness oneCellPoints(A, B)1046  witness constantSequence(A)1047  witness succ(0)1048  constructor1049  . have naturalZero := Naturals.constructor.zero1050    have naturalOne := Naturals.constructor.succ with naturalZero1051    exact nat.omega.forward with naturalOne1052  . constructor1053    . exact oneCellPoints.tagged with ordered1054    . exact oneCellPoints.fine at A, B, D with1055        *{3}, ordered, positive, width10561057-- HalfMeshPartitions1058theorem FineTaggedPartitionsExist.half_mesh (A B D : Real)1059  requires ordered : A < B1060  requires positive : (0:R) < D1061  requires halfWidth : half(B - A) < D1062  shows ∃ p, ∃ t, ∃ N ∈ ℕ,1063    TaggedPartition(p, t, A, B, N) ∧ FinePartition(p, A, B, N, D)1064proof1065  have midpointReal := intervalMidpoint.real at A, B with *1066  obtain ⟨left, right⟩ := intervalMidpoint.between with ordered1067  witness twoCellPoints(A, intervalMidpoint(A, B), B)1068  witness twoCellPoints(A, intervalMidpoint(A, B), B)1069  witness succ(succ(0))1070  constructor1071  . have naturalZero := Naturals.constructor.zero1072    have naturalOne := Naturals.constructor.succ with naturalZero1073    have naturalTwo := Naturals.constructor.succ with naturalOne1074    exact nat.omega.forward with naturalTwo1075  . constructor1076    . exact twoCellPoints.tagged at A, intervalMidpoint(A, B), B with1077        assumption, midpointReal, assumption, left, right1078    . exact twoCellPoints.fine at A, B, D with1079        *{3}, ordered, positive, halfWidth10801081-- SubdivisionScale1082theorem dyadicRadius.eventually_scaled_below (W D : Real)1083  requires positive : (0:R) < D1084  shows ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n → W * dyadicRadius(n) < D1085proof1086  have constant := constantSequence.converges at W1087  have scaled := ConvergesTo.mul with constant, dyadicRadii.converges_zero1088  have zero := realMulValue.zero_right at W1089  rw zero at scaled1090  obtain ⟨N, naturalN, near⟩ := ConvergesTo.eventually with scaled, positive1091  witness N1092  constructor1093  . exact naturalN1094  . intros n memberN afterN1095    have typedN := nat.omega.backward with memberN1096    have nearN := near with n, memberN, afterN1097    have constantValue := constantSequence.value at W, n with1098      assumption, typedN1099    have radiusValue := dyadicRadii.value with typedN1100    have constantSequenceReal := constantSequence.sequence at W1101    have valueReal := RealSequence.value with constantSequenceReal1102    have radiusReal := RealSequence.value with dyadicRadii.sequence1103    have productValue := mulSequence.value with1104      constantSequenceReal, dyadicRadii.sequence, valueReal, radiusReal1105    rw [constantValue, radiusValue] at productValue1106    rw productValue at nearN1107    obtain ⟨lower, upper⟩ := openBall.order_characterization.forward with nearN1108    have zeroAdd := realAddValue.zero_left at D1109    rwa zeroAdd at upper11101111-- DyadicCofinality1112theorem FinePartitionsExist.of_dyadic (A B W : Real)1113  requires family : ∀ n ∈ ℕ,1114    ∃ p, ∃ N ∈ ℕ,1115      FinePartition(p, A, B, N, W * dyadicRadius(n))1116  shows FinePartitionsExist(A, B)1117proof1118  intros D realD positiveD1119  have typedD : Real(D) by exact realD1120  obtain ⟨n, naturalN, eventually⟩ :=1121    dyadicRadius.eventually_scaled_below at W, D with1122      assumption, typedD, positiveD1123  have typedN := nat.omega.backward with naturalN1124  have reflexive := LessEqual.reflexive with typedN1125  have small := eventually with n, naturalN, reflexive1126  have weak := realLess.implies_le with small1127  obtain ⟨p, N, naturalCells, fine⟩ := family with n, naturalN1128  have relaxed := FinePartition.weaken with fine, weak1129  witness p1130  witness N1131  refine ⟨naturalCells, relaxed⟩11321133-- The sole remaining geometric obligation is to construct the dyadic family.1134theorem FineTaggedPartitionsExist.of_dyadic (A B W : Real)1135  requires family : ∀ n ∈ ℕ,1136    ∃ p, ∃ t, ∃ N ∈ ℕ,1137      TaggedPartition(p, t, A, B, N) ∧1138        FinePartition(p, A, B, N, W * dyadicRadius(n))1139  shows FineTaggedPartitionsExist(A, B)1140proof1141  intros D realD positiveD1142  have typedD : Real(D) by exact realD1143  obtain ⟨n, naturalN, eventually⟩ :=1144    dyadicRadius.eventually_scaled_below at W, D with1145      assumption, typedD, positiveD1146  have typedN := nat.omega.backward with naturalN1147  have reflexive := LessEqual.reflexive with typedN1148  have small := eventually with n, naturalN, reflexive1149  have weak := realLess.implies_le with small1150  obtain ⟨p, t, N, naturalCells, tagged, fine⟩ := family with n, naturalN1151  have typedCells := nat.omega.backward with naturalCells1152  have relaxed := FinePartition.weaken with fine, weak1153  witness p1154  witness t1155  witness N1156  refine ⟨naturalCells, tagged, relaxed⟩11571158-- AffineCofinality1159theorem FinePartitionsExist.positive_interval (A B : Real)1160  requires ordered : A < B1161  shows FinePartitionsExist(A, B)1162proof1163  have family : ∀ n ∈ ℕ,1164      ∃ p, ∃ N ∈ ℕ,1165        FinePartition(p, A, B, N, (B - A) * dyadicRadius(n))1166    intros n naturalN1167    have typedN := nat.omega.backward with naturalN1168    witness affinePoints(A, (B - A) * dyadicRadius(succ(n)))1169    witness dyadicCellCount(succ(n))1170    constructor1171    . have next := Naturals.constructor.succ at n with typedN1172      have count := dyadicCellCount.nat with next1173      exact nat.omega.forward with count1174    . exact affinePoints.dyadic_fine at A, B, n with1175        *{2}, typedN, ordered1176  exact FinePartitionsExist.of_dyadic with family11771178theorem FineTaggedPartitionsExist.positive_interval (A B : Real)1179  requires ordered : A < B1180  shows FineTaggedPartitionsExist(A, B)1181proof1182  have fine := FinePartitionsExist.positive_interval with ordered1183  exact FinePartitionsExist.tagged with fine1184