Grace/Cumulus/Topology/Real/NestedChoice.g17

Open in Workbench Download source

Imports

Real.Analysis.ArchimedeanLimits · Set.ChoiceFunctions

Declarations

Source

1-- Nested closed intervals chosen by a choice function: each stage centres2-- an interval at a point of a set, shrinks it below 1/(n + 1), keeps it3-- inside the previous one, and keeps out the point of code n4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Topology.Real.NestedChoice10import Real.Analysis.ArchimedeanLimits11import Set.ChoiceFunctions1213-- Section: CenteredIntervals14-- The closed interval of radius E around C.15def centeredInterval (C E : Real) : Set := closedInterval(C - E, C + E)1617theorem centeredInterval.membership (X : Set) (C E : Real)18  shows X ∈ centeredInterval(C, E) ↔19    X ∈ ℝ ∧ C - E ≤ X ∧ X ≤ C + E20proof21  unfold centeredInterval22  exact closedInterval.membership at C - E, C + E, X2324theorem centeredInterval.dist_membership (X : Set) (C E : Real)25  shows X ∈ centeredInterval(C, E) ↔ X ∈ ℝ ∧ dist(X, C) ≤ E26proof27  constructor28  . intro member29    obtain ⟨realX, lower, upper⟩ :=30      centeredInterval.membership.forward with member31    have differenceReal : X - C ∈ ℝ by typecheck32    refine ⟨realX, ?_⟩33    unfold dist34    have split : (0:R) ≤ X - C ∨ ¬((0:R) ≤ X - C) by tauto35    cases split with nonnegative | negative36    . have absolute := abs.of_nonnegative with nonnegative37      rw absolute38      linarith39    . have below := realLess.of_not_le with negative40      have nonpositive := realLess.implies_le with below41      have absolute := abs.of_nonpositive with nonpositive42      rw absolute43      linarith44  . intro near45    obtain ⟨realX, within⟩ := near46    have differenceReal : X - C ∈ ℝ by typecheck47    have upper := abs.upper at X - C48    have lower := abs.upper_neg at X - C49    unfold dist at within50    apply centeredInterval.membership.backward51    refine ⟨realX, ?_, ?_⟩52    . linarith53    . linarith5455theorem centeredInterval.subset_reals (C E : Real)56  shows centeredInterval(C, E) ⊆ ℝ57proof58  unfold centeredInterval59  exact closedInterval.subset_reals at C - E, C + E6061-- An interval around a nearer centre with a smaller radius stays inside.62theorem centeredInterval.nested (C E D R : Real)63  requires inside : dist(D, C) + R ≤ E64  shows centeredInterval(D, R) ⊆ centeredInterval(C, E)65proof66  intros X hX67  obtain ⟨realX, near⟩ := centeredInterval.dist_membership.forward with hX68  have triangle := dist.triangle at X, D, C69  have distXD := dist.real at X, D70  have distDC := dist.real at D, C71  have distXC := dist.real at X, C72  apply centeredInterval.dist_membership.backward73  refine ⟨realX, ?_⟩74  linarith7576-- The endpoints of a nonempty closed interval inside another lie between77-- the endpoints of the larger one.78theorem closedInterval.subset_bounds (A B C D : Real)79  requires ordered : A ≤ B80  requires inside : closedInterval(A, B) ⊆ closedInterval(C, D)81  shows C ≤ A ∧ B ≤ D82proof83  have leftIn := closedInterval.left_mem with ordered84  have rightIn := closedInterval.right_mem with ordered85  obtain ⟨realA, lowerA, upperA⟩ :=86    closedInterval.membership.forward with (inside with A, leftIn)87  obtain ⟨realB, lowerB, upperB⟩ :=88    closedInterval.membership.forward with (inside with B, rightIn)89  exact ⟨lowerA, upperB⟩9091theorem product.projections (q A B : Set)92  requires hq : q ∈ A × B93  shows fst(q) ∈ A ∧ snd(q) ∈ B94proof95  obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with hq96  rw [shape, fst.pair, snd.pair]97  exact ⟨hx, hy⟩9899-- Section: Candidates100-- A candidate pair is a centre with a radius.101def candidateInterval (q : Set) : Set := centeredInterval(fst(q), snd(q))102103-- The candidates at stage n inside the region I: a centre in P, a positive104-- radius at most 1/(n + 1), an interval inside I, and no point of P of105-- code n in the interval.106def shrinkCandidates (P f I : Set, n : Nat) : Set :=107  { q ∈ ℝ × ℝ | fst(q) ∈ P ∧ (0:R) < (snd(q):R) ∧108    (snd(q):R) ≤ harmonicTerms(n) ∧ candidateInterval(q) ⊆ I ∧109    (∀ y ∈ P, y ∈ candidateInterval(q) → f(y) ≠ n) }110111theorem shrinkCandidates.subset (P f I : Set, n : Nat)112  shows shrinkCandidates(P, f, I, n) ⊆ ℝ × ℝ113proof114  intros q hq115  have parts := shrinkCandidates.membership.forward with hq116  exact parts.left117118theorem shrinkCandidates.pair (P f I : Set, n : Nat) (C E : Real)119  requires centre : C ∈ P120  requires positive : 0 < E121  requires small : E ≤ harmonicTerms(n)122  requires inside : centeredInterval(C, E) ⊆ I123  requires avoids : ∀ y ∈ P, y ∈ centeredInterval(C, E) → f(y) ≠ n124  shows (C, E) ∈ shrinkCandidates(P, f, I, n)125proof126  have realC : C ∈ ℝ by typecheck127  have realE : E ∈ ℝ by typecheck128  have pairIn : (C, E) ∈ ℝ × ℝ := product.pair with realC, realE129  have same : candidateInterval((C, E)) = centeredInterval(C, E)130    simp [candidateInterval, fst.pair, snd.pair]131  apply shrinkCandidates.membership.backward132  rw [fst.pair, snd.pair, same]133  refine ⟨pairIn, centre, positive, small, inside, ?_⟩134  intros y hy hIn135  rw same at hIn136  exact avoids with y, hy, hIn137138-- Section: Stages139-- The stages: a choice function on the pairs of reals picks a candidate140-- inside the interval of the previous stage; stage zero lives in the line.141def shrinkStage (P f c : Set, n : Nat) → Set142  | P, f, c, zero => c(shrinkCandidates(P, f, ℝ, 0))143  | P, f, c, succ(k) => c(shrinkCandidates(P, f,144      candidateInterval(shrinkStage(P, f, c, k)), succ(k)))145146def shrinkRegion (P f c : Set, n : Nat) → Set147  | P, f, c, zero => ℝ148  | P, f, c, succ(k) => candidateInterval(shrinkStage(P, f, c, k))149150def shrinkCentre (P f c : Set, n : Nat) : Set := fst(shrinkStage(P, f, c, n))151def shrinkRadius (P f c : Set, n : Nat) : Set := snd(shrinkStage(P, f, c, n))152def shrinkInterval (P f c : Set, n : Nat) : Set :=153  candidateInterval(shrinkStage(P, f, c, n))154155theorem shrinkInterval.centered (P f c : Set, n : Nat)156  shows shrinkInterval(P, f, c, n) =157    centeredInterval(shrinkCentre(P, f, c, n), shrinkRadius(P, f, c, n))158proof159  simp [shrinkInterval, candidateInterval, shrinkCentre, shrinkRadius]160161theorem shrinkStage.equation (P f c : Set, n : Nat)162  shows shrinkStage(P, f, c, n) =163    c(shrinkCandidates(P, f, shrinkRegion(P, f, c, n), n))164proof165  induction n166  | zero =>167    simp [shrinkStage, shrinkRegion]168  | succ(k) using ih =>169    simp [shrinkStage, shrinkRegion]170171theorem shrinkRegion.succ (P f c : Set, k : Nat)172  shows shrinkRegion(P, f, c, succ(k)) = shrinkInterval(P, f, c, k)173proof174  simp [shrinkRegion, shrinkInterval]175176-- The step hypotheses: candidates exist at stage zero in the line, and at177-- every later stage inside any interval around a point of P.178predicate ShrinkSteps (P f : Set) :=179  Nonempty(shrinkCandidates(P, f, ℝ, 0)) ∧180  (∀ n ∈ ℕ, ∀ C ∈ P, ∀ E ∈ ℝ, (0:R) < E →181    Nonempty(shrinkCandidates(P, f, centeredInterval(C, E), succ(n))))182183-- Every stage is a candidate of its region.184theorem shrinkStage.member (P f c : Set, n : Nat)185  requires choice : SubsetChoice(c, ℝ × ℝ)186  requires steps : ShrinkSteps(P, f)187  shows shrinkStage(P, f, c, n) ∈188    shrinkCandidates(P, f, shrinkRegion(P, f, c, n), n)189proof190  induction n191  | zero =>192    have region : shrinkRegion(P, f, c, 0) = ℝ by simp [shrinkRegion]193    have equation := shrinkStage.equation at P, f, c, 0194    rw [equation, region]195    have inhabited := steps.left196    have subset := shrinkCandidates.subset at P, f, ℝ, 0197    exact SubsetChoice.member with choice, subset, inhabited198  | succ(k) using ih =>199    obtain ⟨pairIn, centre, positive, small, inside, avoids⟩ :=200      shrinkCandidates.membership.forward with ih201    have realParts := product.projections with pairIn202    have kNatural : k ∈ ℕ by simp [Nat]203    have inhabited := steps.right with k, kNatural,204      fst(shrinkStage(P, f, c, k)), centre,205      snd(shrinkStage(P, f, c, k)), realParts.right, positive206    have region : shrinkRegion(P, f, c, succ(k)) =207        centeredInterval(fst(shrinkStage(P, f, c, k)),208          snd(shrinkStage(P, f, c, k)))209      simp [shrinkRegion, candidateInterval]210    have equation := shrinkStage.equation at P, f, c, succ(k)211    rw [equation, region]212    have subset := shrinkCandidates.subset at P, f,213      centeredInterval(fst(shrinkStage(P, f, c, k)),214        snd(shrinkStage(P, f, c, k))), succ(k)215    exact SubsetChoice.member with choice, subset, inhabited216217theorem shrinkStage.pair (P f c : Set, n : Nat)218  requires choice : SubsetChoice(c, ℝ × ℝ)219  requires steps : ShrinkSteps(P, f)220  shows shrinkStage(P, f, c, n) ∈ ℝ × ℝ221proof222  have member := shrinkStage.member with choice, steps223  have parts := shrinkCandidates.membership.forward with member224  exact parts.left225226theorem shrinkCentre.member (P f c : Set, n : Nat)227  requires choice : SubsetChoice(c, ℝ × ℝ)228  requires steps : ShrinkSteps(P, f)229  shows shrinkCentre(P, f, c, n) ∈ P230proof231  have member := shrinkStage.member with choice, steps232  have parts := shrinkCandidates.membership.forward with member233  unfold shrinkCentre234  exact parts.right.left235236theorem shrinkCentre.real (P f c : Set, n : Nat)237  requires choice : SubsetChoice(c, ℝ × ℝ)238  requires steps : ShrinkSteps(P, f)239  shows shrinkCentre(P, f, c, n) ∈ ℝ240proof241  have pairIn := shrinkStage.pair with choice, steps242  have parts := product.projections with pairIn243  unfold shrinkCentre244  exact parts.left245246theorem shrinkRadius.real (P f c : Set, n : Nat)247  requires choice : SubsetChoice(c, ℝ × ℝ)248  requires steps : ShrinkSteps(P, f)249  shows shrinkRadius(P, f, c, n) ∈ ℝ250proof251  have pairIn := shrinkStage.pair with choice, steps252  have parts := product.projections with pairIn253  unfold shrinkRadius254  exact parts.right255256theorem shrinkRadius.positive (P f c : Set, n : Nat)257  requires choice : SubsetChoice(c, ℝ × ℝ)258  requires steps : ShrinkSteps(P, f)259  shows (0:R) < (shrinkRadius(P, f, c, n):R)260proof261  have member := shrinkStage.member with choice, steps262  have parts := shrinkCandidates.membership.forward with member263  unfold shrinkRadius264  exact parts.right.right.left265266theorem shrinkRadius.small (P f c : Set, n : Nat)267  requires choice : SubsetChoice(c, ℝ × ℝ)268  requires steps : ShrinkSteps(P, f)269  shows (shrinkRadius(P, f, c, n):R) ≤ harmonicTerms(n)270proof271  have member := shrinkStage.member with choice, steps272  have parts := shrinkCandidates.membership.forward with member273  unfold shrinkRadius274  exact parts.right.right.right.left275276theorem shrinkInterval.nested (P f c : Set, k : Nat)277  requires choice : SubsetChoice(c, ℝ × ℝ)278  requires steps : ShrinkSteps(P, f)279  shows shrinkInterval(P, f, c, succ(k)) ⊆ shrinkInterval(P, f, c, k)280proof281  have member := shrinkStage.member at P, f, c, succ(k) with choice, steps282  have parts := shrinkCandidates.membership.forward with member283  have inside := parts.right.right.right.right.left284  have region := shrinkRegion.succ at P, f, c, k285  rw region at inside286  simp [shrinkInterval]287288theorem shrinkInterval.avoids (P f c : Set, n : Nat)289  requires choice : SubsetChoice(c, ℝ × ℝ)290  requires steps : ShrinkSteps(P, f)291  shows ∀ y ∈ P, y ∈ shrinkInterval(P, f, c, n) → f(y) ≠ n292proof293  have member := shrinkStage.member with choice, steps294  have parts := shrinkCandidates.membership.forward with member295  unfold shrinkInterval296  exact parts.right.right.right.right.right297298-- Section: Endpoints299-- The endpoints of the stage intervals, as real sequences.300defgraph shrinkLeft (P f c : Set) (n ∈ ℕ) : ℝ :=301  (shrinkCentre(P, f, c, n):R) - (shrinkRadius(P, f, c, n):R)302requires choice : SubsetChoice(c, ℝ × ℝ)303requires steps : ShrinkSteps(P, f)304proof305  have typedN := nat.omega.backward with member306  have realCentre := shrinkCentre.real at P, f, c, n with choice, steps307  have realRadius := shrinkRadius.real at P, f, c, n with choice, steps308  typecheck309310defgraph shrinkRight (P f c : Set) (n ∈ ℕ) : ℝ :=311  (shrinkCentre(P, f, c, n):R) + (shrinkRadius(P, f, c, n):R)312requires choice : SubsetChoice(c, ℝ × ℝ)313requires steps : ShrinkSteps(P, f)314proof315  have typedN := nat.omega.backward with member316  have realCentre := shrinkCentre.real at P, f, c, n with choice, steps317  have realRadius := shrinkRadius.real at P, f, c, n with choice, steps318  typecheck319320theorem shrinkInterval.endpoints (P f c : Set, n : Nat)321  requires choice : SubsetChoice(c, ℝ × ℝ)322  requires steps : ShrinkSteps(P, f)323  shows shrinkInterval(P, f, c, n) =324    closedInterval(shrinkLeft(P, f, c)[n], shrinkRight(P, f, c)[n])325proof326  have nNatural : n ∈ ℕ by simp [Nat]327  have left := shrinkLeft.value at P, f, c, n with *328  have right := shrinkRight.value at P, f, c, n with *329  rw [left, right]330  simp [shrinkInterval, candidateInterval, centeredInterval,331    shrinkCentre, shrinkRadius]332333theorem shrinkLeft.le_right (P f c : Set, n : Nat)334  requires choice : SubsetChoice(c, ℝ × ℝ)335  requires steps : ShrinkSteps(P, f)336  shows shrinkLeft(P, f, c)[n] ≤ shrinkRight(P, f, c)[n]337proof338  have nNatural : n ∈ ℕ by simp [Nat]339  have realCentre := shrinkCentre.real with choice, steps340  have realRadius := shrinkRadius.real with choice, steps341  have positive := shrinkRadius.positive with choice, steps342  have left := shrinkLeft.value at P, f, c, n with *343  have right := shrinkRight.value at P, f, c, n with *344  rw [left, right]345  linarith346347-- The stage intervals are nested closed intervals.348theorem shrink.nested (P f c : Set)349  requires choice : SubsetChoice(c, ℝ × ℝ)350  requires steps : ShrinkSteps(P, f)351  shows NestedClosedIntervals(shrinkLeft(P, f, c), shrinkRight(P, f, c))352proof353  have leftSequence : RealSequence(shrinkLeft(P, f, c)) :=354    shrinkLeft.function with choice, steps355  have rightSequence : RealSequence(shrinkRight(P, f, c)) :=356    shrinkRight.function with choice, steps357  have bounds : ∀ n ∈ ℕ,358      shrinkLeft(P, f, c)[n] ≤ shrinkLeft(P, f, c)[succ(n)] ∧359      shrinkRight(P, f, c)[succ(n)] ≤ shrinkRight(P, f, c)[n]360    intros n hn361    have typedN := nat.omega.backward with hn362    have nested := shrinkInterval.nested at P, f, c, n with choice, steps363    have endpointsN := shrinkInterval.endpoints at P, f, c, n with364      choice, steps365    have endpointsS := shrinkInterval.endpoints at P, f, c, succ(n) with366      choice, steps367    rw [endpointsN, endpointsS] at nested368    have ordered := shrinkLeft.le_right at P, f, c, succ(n) with369      choice, steps370    have realLeftN := RealSequence.value at shrinkLeft(P, f, c), n with371      leftSequence372    have realRightN := RealSequence.value at shrinkRight(P, f, c), n with373      rightSequence374    have realLeftS := RealSequence.value at shrinkLeft(P, f, c), succ(n)375      with leftSequence376    have realRightS := RealSequence.value at shrinkRight(P, f, c), succ(n)377      with rightSequence378    exact closedInterval.subset_bounds with ordered, nested379  refine ⟨leftSequence, rightSequence, ?_, ?_, ?_⟩380  . apply StepwiseNondecreasing.nondecreasing with leftSequence381    intros n hn382    have both := bounds with n, hn383    exact realLe.characterization.forward with both.left384  . apply StepwiseNonincreasing.nonincreasing with rightSequence385    intros n hn386    have both := bounds with n, hn387    exact realLe.characterization.forward with both.right388  . intros n hn389    have typedN := nat.omega.backward with hn390    have ordered := shrinkLeft.le_right at P, f, c, n with choice, steps391    exact realLe.characterization.forward with ordered392393-- Cantor's common point of the stage intervals.394theorem shrink.common_point (P f c : Set)395  requires choice : SubsetChoice(c, ℝ × ℝ)396  requires steps : ShrinkSteps(P, f)397  shows ∃ L ∈ ℝ, ∀ n ∈ ℕ, L ∈ shrinkInterval(P, f, c, n)398proof399  have nested := shrink.nested with choice, steps400  obtain ⟨L, realL, inside⟩ :=401    NestedClosedIntervals.nonempty_intersection with nested402  witness L403  refine ⟨realL, ?_⟩404  intros n hn405  have typedN := nat.omega.backward with hn406  have endpoints := shrinkInterval.endpoints at P, f, c, n with choice, steps407  rw endpoints408  exact inside with n, hn409410-- A point of every stage interval is not in P: its code m would have been411-- kept out at stage m.412theorem shrink.escapes (P f c L : Set)413  requires function : f : P → ℕ414  requires choice : SubsetChoice(c, ℝ × ℝ)415  requires steps : ShrinkSteps(P, f)416  requires inside : ∀ n ∈ ℕ, L ∈ shrinkInterval(P, f, c, n)417  shows ¬L ∈ P418proof419  intro member420  have code := FunctionBetween.apply_closed with function, member421  have typedCode := nat.omega.backward with code422  have avoids := shrinkInterval.avoids at P, f, c, f(L) with choice, steps423  have atCode := inside with f(L), code424  have distinct := avoids with L, member, atCode425  apply distinct426  rfl427428-- Section: Archimedes429-- The reciprocals 1/(n + 1) fall below any positive bound.430theorem harmonicTerms.below (E : Real)431  requires positive : 0 < E432  shows ∃ n ∈ ℕ, harmonicTerms(n) < E433proof434  have converges := harmonicTerms.converges_zero435  obtain ⟨N, hN, tail⟩ := ConvergesTo.eventually with converges, positive436  have typedN := nat.omega.backward with hN437  have reflexive := LessEqual.reflexive at N438  have near := tail with N, hN, reflexive439  have sequence := harmonicTerms.sequence440  have termReal := RealSequence.value at harmonicTerms, N with sequence441  obtain ⟨lower, upper⟩ := openBall.order_characterization.forward with near442  witness N443  refine ⟨hN, ?_⟩444  linarith445