Grace/Cumulus/FixedPoint/CubeSequences.g17

Open in Workbench Download source

Imports

Real.Analysis.ExtremeValue · Set

Declarations

Source

1-- Sequences of points of the unit cube in n dimensions: coordinate2-- sequences, subsequences, and Bolzano–Weierstrass one coordinate at a time3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.FixedPoint.CubeSequences9import Real.Analysis.ExtremeValue10import Set1112def unitCube (n : Set) : Set := { x ∈ functionSpace(n, ℝ) | ∀ i ∈ n, x(i) ∈ closedInterval((0:R), (1:R)) }1314predicate PointSequence (X n : Set) := FunctionBetween(X, ℕ, functionSpace(n, ℝ))1516theorem PointSequence.function (X n : Set)17  requires sequence : PointSequence(X, n)18  shows X : ℕ → functionSpace(n, ℝ)19proof20  exact sequence2122theorem PointSequence.point (X n k : Set)23  requires sequence : PointSequence(X, n)24  requires hk : k ∈ ℕ25  shows X(k) : n → ℝ26proof27  have function := PointSequence.function with sequence28  have pointIn := FunctionBetween.apply_closed with function, hk29  exact functionSpace.mem_iff.forward with pointIn3031defgraph coordinateSequence (X n i : Set) (k ∈ ℕ) : ℝ := X(k)(i)32requires sequence : PointSequence(X, n)33requires hi : i ∈ n34proof35  have point := PointSequence.point with sequence, member36  exact FunctionBetween.apply_closed with point, hi3738theorem coordinateSequence.sequence (X n i : Set)39  requires sequence : PointSequence(X, n)40  requires hi : i ∈ n41  shows RealSequence(coordinateSequence(X, n, i))42proof43  exact coordinateSequence.function with sequence, hi4445def pointSubsequence (X n k : Set) : Set := compose(X, k, ℕ, ℕ, functionSpace(n, ℝ))4647theorem pointSubsequence.sequence (X n k : Set)48  requires sequence : PointSequence(X, n)49  requires increasing : StrictlyIncreasingNat(k)50  shows PointSequence(pointSubsequence(X, n, k), n)51proof52  have kFunction := increasing.left53  have function := PointSequence.function with sequence54  have same : pointSubsequence(X, n, k) = compose(X, k, ℕ, ℕ, functionSpace(n, ℝ))55    unfold pointSubsequence56    rfl57  unfold PointSequence58  rw same59  exact compose.function with kFunction, function6061theorem pointSubsequence.value (X n k m : Set)62  requires sequence : PointSequence(X, n)63  requires increasing : StrictlyIncreasingNat(k)64  requires hm : m ∈ ℕ65  shows pointSubsequence(X, n, k)(m) = X(k(m))66proof67  have kFunction := increasing.left68  have function := PointSequence.function with sequence69  have same : pointSubsequence(X, n, k) = compose(X, k, ℕ, ℕ, functionSpace(n, ℝ))70    unfold pointSubsequence71    rfl72  rw same73  exact compose.apply with kFunction, function, hm7475theorem coordinateSequence.subsequence (X n k i : Set)76  requires sequence : PointSequence(X, n)77  requires increasing : StrictlyIncreasingNat(k)78  requires hi : i ∈ n79  shows coordinateSequence(pointSubsequence(X, n, k), n, i) = subsequence(coordinateSequence(X, n, i), k)80proof81  have kFunction := increasing.left82  have subSequence := pointSubsequence.sequence with sequence, increasing83  have leftFunction := coordinateSequence.function with subSequence, hi84  have inner := coordinateSequence.sequence with sequence, hi85  have rightFunction := subsequence.function with inner, increasing86  apply FunctionBetween.ext with leftFunction, rightFunction87  intros m hm88  have leftValue := coordinateSequence.value at pointSubsequence(X, n, k), n, i, m with subSequence, hi89  have pointValue := pointSubsequence.value with sequence, increasing, hm90  have rightValue := subsequence.value at coordinateSequence(X, n, i), k, m with inner, increasing91  have indexIn := FunctionBetween.apply_closed with kFunction, hm92  have innerValue := coordinateSequence.value at X, n, i, k(m) with sequence, hi93  rw [leftValue, pointValue, rightValue, innerValue]94  rfl9596theorem coordinateSequence.terms (X n i : Set)97  requires sequence : PointSequence(X, n)98  requires inCube : ∀ k ∈ ℕ, X(k) ∈ unitCube(n)99  requires hi : i ∈ n100  shows TermsIn(coordinateSequence(X, n, i), closedInterval((0:R), (1:R)))101proof102  unfold TermsIn103  intros k hk104  have value := coordinateSequence.value at X, n, i, k with sequence, hi105  rw value106  have parts := unitCube.membership.forward with (inCube with hk)107  exact parts.right with hi108109theorem StrictlyIncreasingNat.comp (k l : Set)110  requires first : StrictlyIncreasingNat(k)111  requires second : StrictlyIncreasingNat(l)112  shows StrictlyIncreasingNat(compose(k, l, ℕ, ℕ, ℕ))113proof114  have kFunction := StrictlyIncreasingNat.function at k with *115  have lFunction := StrictlyIncreasingNat.function at l with *116  have function := compose.function at k, l, ℕ, ℕ, ℕ with *117  rcases first with ⟨kf, kStrict⟩118  rcases second with ⟨lf, lStrict⟩119  refine ⟨function, ?_⟩120  intros m mIn n nIn before121  have lm := FunctionBetween.apply_closed at l, ℕ, ℕ, m with *122  have ln := FunctionBetween.apply_closed at l, ℕ, ℕ, n with *123  have step := lStrict with m, mIn, n, nIn, before124  have result := kStrict with l(m), lm, l(n), ln, step125  rwa [compose.apply, compose.apply]126127-- Bolzano–Weierstrass on the first m coordinates, by induction on m.128theorem unitCube.bolzano_weierstrass_prefix (n m : Nat) (X : Set)129  requires sequence : PointSequence(X, n)130  requires inCube : ∀ k ∈ ℕ, X(k) ∈ unitCube(n)131  shows m ∈ succ(n) → ∃ k, StrictlyIncreasingNat(k) ∧132    ∀ i ∈ m, ∃ L ∈ closedInterval((0:R), (1:R)), ConvergesTo(coordinateSequence(pointSubsequence(X, n, k), n, i), L)133proof134  induction m135  | zero =>136    intro hm137    witness identity(ℕ)138    constructor139    . exact identity.strictly_increasing_nat140    . intros i hi141      exfalso142      rw nat.zero at hi143      simpa using hi144  | succ(j) using ih =>145    intro hm146    have jNat : Nat(j) by typecheck147    have jIn : j ∈ succ(n)148      have less := Less.of_membership with hm149      have below : j < succ(n) by arith150      exact membership.of_Less with below151    have jInN : j ∈ n152      have less := Less.of_membership with hm153      have below : j < n by arith154      exact membership.of_Less with below155    obtain ⟨k, increasing, limits⟩ := ih with jIn156    have subSequence := pointSubsequence.sequence with sequence, increasing157    have subCube : ∀ a ∈ ℕ, pointSubsequence(X, n, k)(a) ∈ unitCube(n)158      intros a ha159      have value := pointSubsequence.value with sequence, increasing, ha160      rw value161      have kFunction := increasing.left162      exact inCube with (FunctionBetween.apply_closed with kFunction, ha)163    have coordinate := coordinateSequence.sequence with subSequence, jInN164    have terms := coordinateSequence.terms with subSequence, subCube, jInN165    obtain ⟨l, lIncreasing, L, LIn, LInterval, converges⟩ := closedInterval.bolzano_weierstrass at coordinateSequence(pointSubsequence(X, n, k), n, j), (0:R), (1:R) with coordinate, terms166    have composed := StrictlyIncreasingNat.comp with increasing, lIncreasing167    witness compose(k, l, ℕ, ℕ, ℕ)168    constructor169    . exact composed170    . intros i hi171      have split := bootstrap.succ.membership.forward with hi172      have nested : pointSubsequence(X, n, compose(k, l, ℕ, ℕ, ℕ)) = pointSubsequence(pointSubsequence(X, n, k), n, l)173        have kFunction := increasing.left174        have lFunction := lIncreasing.left175        have same1 : pointSubsequence(X, n, compose(k, l, ℕ, ℕ, ℕ)) = compose(X, compose(k, l, ℕ, ℕ, ℕ), ℕ, ℕ, functionSpace(n, ℝ))176          unfold pointSubsequence177          rfl178        have same2 : pointSubsequence(pointSubsequence(X, n, k), n, l) = compose(compose(X, k, ℕ, ℕ, functionSpace(n, ℝ)), l, ℕ, ℕ, functionSpace(n, ℝ))179          unfold pointSubsequence180          rfl181        have function := PointSequence.function with sequence182        rw [same1, same2]183        exact compose.associative with lFunction, kFunction, function184      rw under nested185      cases split with below | same186      . obtain ⟨M, MInterval, convergesM⟩ := limits with below187        have MParts := closedInterval.membership.forward with MInterval188        have MReal := MParts.left189        witness M190        constructor191        . exact MInterval192        . have iInN : i ∈ n193            have jLess := Less.of_membership with jInN194            have iNat := natural.member at j with below195            have iLess := Less.of_membership with below196            have less : i < n by arith197            exact membership.of_Less with less198          have same3 := coordinateSequence.subsequence with subSequence, lIncreasing, iInN199          rw under same3200          exact ConvergesTo.subsequence with convergesM, lIncreasing201      . rw under same202        have LParts := closedInterval.membership.forward with LInterval203        have LReal := LParts.left204        witness L205        constructor206        . exact LInterval207        . have same3 := coordinateSequence.subsequence with subSequence, lIncreasing, jInN208          rw under same3209          exact converges210211defunique realLimit (u : Set) (L ∈ ℝ) := ConvergesTo(u, L)212requires convergent : ∃ L ∈ ℝ, ConvergesTo(u, L)213proof214  exact convergent215uniqueness216  intros a ha first b hb second217  exact ConvergesTo.unique with first, second218219defgraph limitPoint (Y n : Set) (i ∈ n) : ℝ := realLimit(coordinateSequence(Y, n, i))220requires convergent : ∀ i ∈ n, ∃ L ∈ ℝ, ConvergesTo(coordinateSequence(Y, n, i), L)221proof222  have selected := realLimit.selected at coordinateSequence(Y, n, i) with (convergent with member)223  exact selected.left224225theorem limitPoint.converges (Y n i : Set)226  requires convergent : ∀ i ∈ n, ∃ L ∈ ℝ, ConvergesTo(coordinateSequence(Y, n, i), L)227  requires hi : i ∈ n228  shows ConvergesTo(coordinateSequence(Y, n, i), limitPoint(Y, n)(i))229proof230  have value := limitPoint.value with convergent, hi231  rw value232  have selected := realLimit.selected at coordinateSequence(Y, n, i) with (convergent with hi)233  exact selected.right234235-- Bolzano–Weierstrass for the cube: every sequence of points has a236-- subsequence converging in every coordinate to a point of the cube.237theorem unitCube.bolzano_weierstrass (n : Nat) (X : Set)238  requires sequence : PointSequence(X, n)239  requires inCube : ∀ k ∈ ℕ, X(k) ∈ unitCube(n)240  shows ∃ k, StrictlyIncreasingNat(k) ∧ ∃ L ∈ unitCube(n),241    ∀ i ∈ n, ConvergesTo(coordinateSequence(pointSubsequence(X, n, k), n, i), L(i))242proof243  have all := unitCube.bolzano_weierstrass_prefix with sequence, inCube244  obtain ⟨k, increasing, limits⟩ := all with (bootstrap.succ.self at n)245  have convergent : ∀ i ∈ n, ∃ L ∈ ℝ, ConvergesTo(coordinateSequence(pointSubsequence(X, n, k), n, i), L)246    intros i hi247    obtain ⟨L, LInterval, converges⟩ := limits with hi248    have parts := closedInterval.membership.forward with LInterval249    refine ⟨L, parts.left, converges⟩250  have limitFunction := limitPoint.function with convergent251  witness k252  constructor253  . exact increasing254  . witness limitPoint(pointSubsequence(X, n, k), n)255    constructor256    . apply unitCube.membership.backward257      constructor258      . exact functionSpace.mem_iff.backward with limitFunction259      . intros i hi260        have converges := limitPoint.converges with convergent, hi261        obtain ⟨L, LInterval, converges2⟩ := limits with hi262        have LParts := closedInterval.membership.forward with LInterval263        have LReal := LParts.left264        have limitReal := FunctionBetween.apply_closed with limitFunction, hi265        have same := ConvergesTo.unique with converges, converges2266        rwa same267    . intros i hi268      exact limitPoint.converges with convergent, hi269