-- Continuous self-maps of the cube in the sup metric, and their action on
-- convergent sequences of points
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.FixedPoint.CubeContinuity
import CubeSequences

predicate CubeMap (f n : Set) := FunctionBetween(f, unitCube(n), unitCube(n))

predicate CubeContinuousAt (f n x : Set) :=
  ∀ E ∈ ℝ, (0:R) < E → ∃ D ∈ ℝ, (0:R) < D ∧
    (∀ y ∈ unitCube(n), ((∀ i ∈ n, dist(y(i), x(i)) < D) → (∀ i ∈ n, dist(f(y)(i), f(x)(i)) < E)))

predicate CubeContinuous (f n : Set) := CubeMap(f, n) ∧ ∀ x ∈ unitCube(n), CubeContinuousAt(f, n, x)

theorem CubeMap.function (f n : Set)
  requires map : CubeMap(f, n)
  shows f : unitCube(n) → unitCube(n)
proof
  exact map

theorem unitCube.point (n x : Set)
  requires hx : x ∈ unitCube(n)
  shows x : n → ℝ
proof
  have parts := unitCube.membership.forward with hx
  exact functionSpace.mem_iff.forward with parts.left

theorem unitCube.coordinate (n x i : Set)
  requires hx : x ∈ unitCube(n)
  requires hi : i ∈ n
  shows x(i) ∈ closedInterval((0:R), (1:R))
proof
  have parts := unitCube.membership.forward with hx
  exact parts.right with hi

theorem unitCube.coordinate_real (n x i : Set)
  requires hx : x ∈ unitCube(n)
  requires hi : i ∈ n
  shows x(i) ∈ ℝ
proof
  have interval := unitCube.coordinate with hx, hi
  have parts := closedInterval.membership.forward with interval
  exact parts.left

-- A sequence of cube points, as a function into the cube.
theorem PointSequence.into_cube (X n : Set)
  requires sequence : PointSequence(X, n)
  requires inCube : ∀ k ∈ ℕ, X(k) ∈ unitCube(n)
  shows X : ℕ → unitCube(n)
proof
  have function := PointSequence.function with sequence
  exact FunctionBetween.codomain_of_values with function, inCube

def imageSequence (f X n : Set) : Set := compose(f, X, ℕ, unitCube(n), unitCube(n))

theorem imageSequence.sequence (f X n : Set)
  requires map : CubeMap(f, n)
  requires sequence : PointSequence(X, n)
  requires inCube : ∀ k ∈ ℕ, X(k) ∈ unitCube(n)
  shows PointSequence(imageSequence(f, X, n), n)
proof
  have fFunction := CubeMap.function with map
  have XFunction := PointSequence.into_cube with sequence, inCube
  have composed := compose.function with XFunction, fFunction
  have values : ∀ k ∈ ℕ, compose(f, X, ℕ, unitCube(n), unitCube(n))(k) ∈ functionSpace(n, ℝ)
    intros k hk
    have valueIn := FunctionBetween.apply_closed with composed, hk
    have parts := unitCube.membership.forward with valueIn
    exact parts.left
  have same : imageSequence(f, X, n) = compose(f, X, ℕ, unitCube(n), unitCube(n))
    unfold imageSequence
    rfl
  unfold PointSequence
  rw same
  exact FunctionBetween.codomain_of_values with composed, values

theorem imageSequence.value (f X n k : Set)
  requires map : CubeMap(f, n)
  requires sequence : PointSequence(X, n)
  requires inCube : ∀ k ∈ ℕ, X(k) ∈ unitCube(n)
  requires hk : k ∈ ℕ
  shows imageSequence(f, X, n)(k) = f(X(k))
proof
  have fFunction := CubeMap.function with map
  have XFunction := PointSequence.into_cube with sequence, inCube
  have same : imageSequence(f, X, n) = compose(f, X, ℕ, unitCube(n), unitCube(n))
    unfold imageSequence
    rfl
  rw same
  exact compose.apply with XFunction, fFunction, hk

theorem imageSequence.in_cube (f X n k : Set)
  requires map : CubeMap(f, n)
  requires sequence : PointSequence(X, n)
  requires inCube : ∀ k ∈ ℕ, X(k) ∈ unitCube(n)
  requires hk : k ∈ ℕ
  shows imageSequence(f, X, n)(k) ∈ unitCube(n)
proof
  have fFunction := CubeMap.function with map
  have value := imageSequence.value with map, sequence, inCube, hk
  rw value
  exact FunctionBetween.apply_closed with fFunction, (inCube with hk)

-- Finitely many coordinates converging gives a common tail within any
-- distance, by induction on the number of coordinates.
theorem coordinateSequence.common_tail (n m : Nat) (X x D : Set)
  requires sequence : PointSequence(X, n)
  requires xFunction : x : n → ℝ
  requires DReal : D ∈ ℝ
  requires positive : (0:R) < D
  requires converges : ∀ i ∈ n, ConvergesTo(coordinateSequence(X, n, i), x(i))
  shows m ∈ succ(n) → ∃ N ∈ ℕ, ∀ i ∈ m, ∀ k ∈ ℕ, N ≤ k → dist(X(k)(i), x(i)) < D
proof
  induction m
  | zero =>
    intro hm
    witness 0
    constructor
    . have zeroNat : Nat(0) by typecheck
      exact nat.omega.forward with zeroNat
    . intros i hi
      exfalso
      rw nat.zero at hi
      simpa using hi
  | succ(j) using ih =>
    intro hm
    have jNat : Nat(j) by typecheck
    have jIn : j ∈ succ(n)
      have less := Less.of_membership with hm
      have below : j < succ(n) by arith
      exact membership.of_Less with below
    have jInN : j ∈ n
      have less := Less.of_membership with hm
      have below : j < n by arith
      exact membership.of_Less with below
    obtain ⟨N, NIn, tail⟩ := ih with jIn
    have convergesJ := converges with jInN
    have xReal := FunctionBetween.apply_closed with xFunction, jInN
    obtain ⟨M, MIn, tailJ⟩ := ConvergesTo.eventually with convergesJ, positive
    have NNat := nat.omega.backward with NIn
    have MNat := nat.omega.backward with MIn
    witness N + M
    constructor
    . have sumNat : Nat(N + M) by typecheck
      exact nat.omega.forward with sumNat
    . intros i hi k hk bound
      have kNat := nat.omega.backward with hk
      have split := bootstrap.succ.membership.forward with hi
      cases split with below | same
      . have NBound : N ≤ k by arith
        have forI := tail with below
        exact forI with hk, NBound
      . rw same
        have MBound : M ≤ k by arith
        have inBall := tailJ with hk, MBound
        have value := coordinateSequence.value at X, n, j, k with sequence, jInN
        rw value at inBall
        have parts := openBall.membership.forward with inBall
        exact parts.right

-- A continuous map sends a coordinatewise convergent sequence of cube points
-- to a sequence converging to the image of the limit.
theorem CubeContinuous.sequential (n : Nat) (f X x : Set)
  requires continuous : CubeContinuous(f, n)
  requires sequence : PointSequence(X, n)
  requires inCube : ∀ k ∈ ℕ, X(k) ∈ unitCube(n)
  requires hx : x ∈ unitCube(n)
  requires converges : ∀ i ∈ n, ConvergesTo(coordinateSequence(X, n, i), x(i))
  shows ∀ i ∈ n, ConvergesTo(coordinateSequence(imageSequence(f, X, n), n, i), f(x)(i))
proof
  obtain ⟨map, pointwise⟩ := continuous
  have fFunction := CubeMap.function with map
  have imageSeq := imageSequence.sequence with map, sequence, inCube
  have xFunction := unitCube.point with hx
  have fxIn := FunctionBetween.apply_closed with fFunction, hx
  have fxFunction := unitCube.point with fxIn
  intros i hi
  have fxReal := FunctionBetween.apply_closed with fxFunction, hi
  unfold ConvergesTo
  constructor
  . exact coordinateSequence.sequence with imageSeq, hi
  . intros E EIn Epos
    have atX := pointwise with hx
    obtain ⟨D, DIn, Dpos, close⟩ := atX with EIn, Epos
    have all := coordinateSequence.common_tail at n, n, X, x, D with sequence, xFunction, DIn, Dpos, converges
    obtain ⟨N, NIn, tail⟩ := all with (bootstrap.succ.self at n)
    witness N
    constructor
    . exact NIn
    . intros k hk bound
      have value := coordinateSequence.value at imageSequence(f, X, n), n, i, k with imageSeq, hi
      have imageValue := imageSequence.value with map, sequence, inCube, hk
      rw [value, imageValue]
      have near : ∀ j ∈ n, dist(X(k)(j), x(j)) < D
        intros j hj
        have forJ := tail with hj
        exact forJ with hk, bound
      have XkIn := inCube with hk
      have images := close with XkIn, near
      have distance := images with hi
      apply openBall.membership.backward
      constructor
      . have fXkIn := FunctionBetween.apply_closed with fFunction, XkIn
        have fXkFunction := unitCube.point with fXkIn
        exact FunctionBetween.apply_closed with fXkFunction, hi
      . exact distance