Grace/Cumulus/FixedPoint/CubeContinuity.g17

Open in Workbench Download source

Imports

CubeSequences

Declarations

Source

1-- Continuous self-maps of the cube in the sup metric, and their action on2-- convergent sequences of points3-- 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.CubeContinuity9import CubeSequences1011predicate CubeMap (f n : Set) := FunctionBetween(f, unitCube(n), unitCube(n))1213predicate CubeContinuousAt (f n x : Set) :=14  ∀ E ∈ ℝ, (0:R) < E → ∃ D ∈ ℝ, (0:R) < D ∧15    (∀ y ∈ unitCube(n), ((∀ i ∈ n, dist(y(i), x(i)) < D) → (∀ i ∈ n, dist(f(y)(i), f(x)(i)) < E)))1617predicate CubeContinuous (f n : Set) := CubeMap(f, n) ∧ ∀ x ∈ unitCube(n), CubeContinuousAt(f, n, x)1819theorem CubeMap.function (f n : Set)20  requires map : CubeMap(f, n)21  shows f : unitCube(n) → unitCube(n)22proof23  exact map2425theorem unitCube.point (n x : Set)26  requires hx : x ∈ unitCube(n)27  shows x : n → ℝ28proof29  have parts := unitCube.membership.forward with hx30  exact functionSpace.mem_iff.forward with parts.left3132theorem unitCube.coordinate (n x i : Set)33  requires hx : x ∈ unitCube(n)34  requires hi : i ∈ n35  shows x(i) ∈ closedInterval((0:R), (1:R))36proof37  have parts := unitCube.membership.forward with hx38  exact parts.right with hi3940theorem unitCube.coordinate_real (n x i : Set)41  requires hx : x ∈ unitCube(n)42  requires hi : i ∈ n43  shows x(i) ∈ ℝ44proof45  have interval := unitCube.coordinate with hx, hi46  have parts := closedInterval.membership.forward with interval47  exact parts.left4849-- A sequence of cube points, as a function into the cube.50theorem PointSequence.into_cube (X n : Set)51  requires sequence : PointSequence(X, n)52  requires inCube : ∀ k ∈ ℕ, X(k) ∈ unitCube(n)53  shows X : ℕ → unitCube(n)54proof55  have function := PointSequence.function with sequence56  exact FunctionBetween.codomain_of_values with function, inCube5758def imageSequence (f X n : Set) : Set := compose(f, X, ℕ, unitCube(n), unitCube(n))5960theorem imageSequence.sequence (f X n : Set)61  requires map : CubeMap(f, n)62  requires sequence : PointSequence(X, n)63  requires inCube : ∀ k ∈ ℕ, X(k) ∈ unitCube(n)64  shows PointSequence(imageSequence(f, X, n), n)65proof66  have fFunction := CubeMap.function with map67  have XFunction := PointSequence.into_cube with sequence, inCube68  have composed := compose.function with XFunction, fFunction69  have values : ∀ k ∈ ℕ, compose(f, X, ℕ, unitCube(n), unitCube(n))(k) ∈ functionSpace(n, ℝ)70    intros k hk71    have valueIn := FunctionBetween.apply_closed with composed, hk72    have parts := unitCube.membership.forward with valueIn73    exact parts.left74  have same : imageSequence(f, X, n) = compose(f, X, ℕ, unitCube(n), unitCube(n))75    unfold imageSequence76    rfl77  unfold PointSequence78  rw same79  exact FunctionBetween.codomain_of_values with composed, values8081theorem imageSequence.value (f X n k : Set)82  requires map : CubeMap(f, n)83  requires sequence : PointSequence(X, n)84  requires inCube : ∀ k ∈ ℕ, X(k) ∈ unitCube(n)85  requires hk : k ∈ ℕ86  shows imageSequence(f, X, n)(k) = f(X(k))87proof88  have fFunction := CubeMap.function with map89  have XFunction := PointSequence.into_cube with sequence, inCube90  have same : imageSequence(f, X, n) = compose(f, X, ℕ, unitCube(n), unitCube(n))91    unfold imageSequence92    rfl93  rw same94  exact compose.apply with XFunction, fFunction, hk9596theorem imageSequence.in_cube (f X n k : Set)97  requires map : CubeMap(f, n)98  requires sequence : PointSequence(X, n)99  requires inCube : ∀ k ∈ ℕ, X(k) ∈ unitCube(n)100  requires hk : k ∈ ℕ101  shows imageSequence(f, X, n)(k) ∈ unitCube(n)102proof103  have fFunction := CubeMap.function with map104  have value := imageSequence.value with map, sequence, inCube, hk105  rw value106  exact FunctionBetween.apply_closed with fFunction, (inCube with hk)107108-- Finitely many coordinates converging gives a common tail within any109-- distance, by induction on the number of coordinates.110theorem coordinateSequence.common_tail (n m : Nat) (X x D : Set)111  requires sequence : PointSequence(X, n)112  requires xFunction : x : n → ℝ113  requires DReal : D ∈ ℝ114  requires positive : (0:R) < D115  requires converges : ∀ i ∈ n, ConvergesTo(coordinateSequence(X, n, i), x(i))116  shows m ∈ succ(n) → ∃ N ∈ ℕ, ∀ i ∈ m, ∀ k ∈ ℕ, N ≤ k → dist(X(k)(i), x(i)) < D117proof118  induction m119  | zero =>120    intro hm121    witness 0122    constructor123    . have zeroNat : Nat(0) by typecheck124      exact nat.omega.forward with zeroNat125    . intros i hi126      exfalso127      rw nat.zero at hi128      simpa using hi129  | succ(j) using ih =>130    intro hm131    have jNat : Nat(j) by typecheck132    have jIn : j ∈ succ(n)133      have less := Less.of_membership with hm134      have below : j < succ(n) by arith135      exact membership.of_Less with below136    have jInN : j ∈ n137      have less := Less.of_membership with hm138      have below : j < n by arith139      exact membership.of_Less with below140    obtain ⟨N, NIn, tail⟩ := ih with jIn141    have convergesJ := converges with jInN142    have xReal := FunctionBetween.apply_closed with xFunction, jInN143    obtain ⟨M, MIn, tailJ⟩ := ConvergesTo.eventually with convergesJ, positive144    have NNat := nat.omega.backward with NIn145    have MNat := nat.omega.backward with MIn146    witness N + M147    constructor148    . have sumNat : Nat(N + M) by typecheck149      exact nat.omega.forward with sumNat150    . intros i hi k hk bound151      have kNat := nat.omega.backward with hk152      have split := bootstrap.succ.membership.forward with hi153      cases split with below | same154      . have NBound : N ≤ k by arith155        have forI := tail with below156        exact forI with hk, NBound157      . rw same158        have MBound : M ≤ k by arith159        have inBall := tailJ with hk, MBound160        have value := coordinateSequence.value at X, n, j, k with sequence, jInN161        rw value at inBall162        have parts := openBall.membership.forward with inBall163        exact parts.right164165-- A continuous map sends a coordinatewise convergent sequence of cube points166-- to a sequence converging to the image of the limit.167theorem CubeContinuous.sequential (n : Nat) (f X x : Set)168  requires continuous : CubeContinuous(f, n)169  requires sequence : PointSequence(X, n)170  requires inCube : ∀ k ∈ ℕ, X(k) ∈ unitCube(n)171  requires hx : x ∈ unitCube(n)172  requires converges : ∀ i ∈ n, ConvergesTo(coordinateSequence(X, n, i), x(i))173  shows ∀ i ∈ n, ConvergesTo(coordinateSequence(imageSequence(f, X, n), n, i), f(x)(i))174proof175  obtain ⟨map, pointwise⟩ := continuous176  have fFunction := CubeMap.function with map177  have imageSeq := imageSequence.sequence with map, sequence, inCube178  have xFunction := unitCube.point with hx179  have fxIn := FunctionBetween.apply_closed with fFunction, hx180  have fxFunction := unitCube.point with fxIn181  intros i hi182  have fxReal := FunctionBetween.apply_closed with fxFunction, hi183  unfold ConvergesTo184  constructor185  . exact coordinateSequence.sequence with imageSeq, hi186  . intros E EIn Epos187    have atX := pointwise with hx188    obtain ⟨D, DIn, Dpos, close⟩ := atX with EIn, Epos189    have all := coordinateSequence.common_tail at n, n, X, x, D with sequence, xFunction, DIn, Dpos, converges190    obtain ⟨N, NIn, tail⟩ := all with (bootstrap.succ.self at n)191    witness N192    constructor193    . exact NIn194    . intros k hk bound195      have value := coordinateSequence.value at imageSequence(f, X, n), n, i, k with imageSeq, hi196      have imageValue := imageSequence.value with map, sequence, inCube, hk197      rw [value, imageValue]198      have near : ∀ j ∈ n, dist(X(k)(j), x(j)) < D199        intros j hj200        have forJ := tail with hj201        exact forJ with hk, bound202      have XkIn := inCube with hk203      have images := close with XkIn, near204      have distance := images with hi205      apply openBall.membership.backward206      constructor207      . have fXkIn := FunctionBetween.apply_closed with fFunction, XkIn208        have fXkFunction := unitCube.point with fXkIn209        exact FunctionBetween.apply_closed with fXkFunction, hi210      . exact distance211