-- Sequences of points of the unit cube in n dimensions: coordinate
-- sequences, subsequences, and Bolzano–Weierstrass one coordinate at a time
-- 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.CubeSequences
import Real.Analysis.ExtremeValue
import Set

def unitCube (n : Set) : Set := { x ∈ functionSpace(n, ℝ) | ∀ i ∈ n, x(i) ∈ closedInterval((0:R), (1:R)) }

predicate PointSequence (X n : Set) := FunctionBetween(X, ℕ, functionSpace(n, ℝ))

theorem PointSequence.function (X n : Set)
  requires sequence : PointSequence(X, n)
  shows X : ℕ → functionSpace(n, ℝ)
proof
  exact sequence

theorem PointSequence.point (X n k : Set)
  requires sequence : PointSequence(X, n)
  requires hk : k ∈ ℕ
  shows X(k) : n → ℝ
proof
  have function := PointSequence.function with sequence
  have pointIn := FunctionBetween.apply_closed with function, hk
  exact functionSpace.mem_iff.forward with pointIn

defgraph coordinateSequence (X n i : Set) (k ∈ ℕ) : ℝ := X(k)(i)
requires sequence : PointSequence(X, n)
requires hi : i ∈ n
proof
  have point := PointSequence.point with sequence, member
  exact FunctionBetween.apply_closed with point, hi

theorem coordinateSequence.sequence (X n i : Set)
  requires sequence : PointSequence(X, n)
  requires hi : i ∈ n
  shows RealSequence(coordinateSequence(X, n, i))
proof
  exact coordinateSequence.function with sequence, hi

def pointSubsequence (X n k : Set) : Set := compose(X, k, ℕ, ℕ, functionSpace(n, ℝ))

theorem pointSubsequence.sequence (X n k : Set)
  requires sequence : PointSequence(X, n)
  requires increasing : StrictlyIncreasingNat(k)
  shows PointSequence(pointSubsequence(X, n, k), n)
proof
  have kFunction := increasing.left
  have function := PointSequence.function with sequence
  have same : pointSubsequence(X, n, k) = compose(X, k, ℕ, ℕ, functionSpace(n, ℝ))
    unfold pointSubsequence
    rfl
  unfold PointSequence
  rw same
  exact compose.function with kFunction, function

theorem pointSubsequence.value (X n k m : Set)
  requires sequence : PointSequence(X, n)
  requires increasing : StrictlyIncreasingNat(k)
  requires hm : m ∈ ℕ
  shows pointSubsequence(X, n, k)(m) = X(k(m))
proof
  have kFunction := increasing.left
  have function := PointSequence.function with sequence
  have same : pointSubsequence(X, n, k) = compose(X, k, ℕ, ℕ, functionSpace(n, ℝ))
    unfold pointSubsequence
    rfl
  rw same
  exact compose.apply with kFunction, function, hm

theorem coordinateSequence.subsequence (X n k i : Set)
  requires sequence : PointSequence(X, n)
  requires increasing : StrictlyIncreasingNat(k)
  requires hi : i ∈ n
  shows coordinateSequence(pointSubsequence(X, n, k), n, i) = subsequence(coordinateSequence(X, n, i), k)
proof
  have kFunction := increasing.left
  have subSequence := pointSubsequence.sequence with sequence, increasing
  have leftFunction := coordinateSequence.function with subSequence, hi
  have inner := coordinateSequence.sequence with sequence, hi
  have rightFunction := subsequence.function with inner, increasing
  apply FunctionBetween.ext with leftFunction, rightFunction
  intros m hm
  have leftValue := coordinateSequence.value at pointSubsequence(X, n, k), n, i, m with subSequence, hi
  have pointValue := pointSubsequence.value with sequence, increasing, hm
  have rightValue := subsequence.value at coordinateSequence(X, n, i), k, m with inner, increasing
  have indexIn := FunctionBetween.apply_closed with kFunction, hm
  have innerValue := coordinateSequence.value at X, n, i, k(m) with sequence, hi
  rw [leftValue, pointValue, rightValue, innerValue]
  rfl

theorem coordinateSequence.terms (X n i : Set)
  requires sequence : PointSequence(X, n)
  requires inCube : ∀ k ∈ ℕ, X(k) ∈ unitCube(n)
  requires hi : i ∈ n
  shows TermsIn(coordinateSequence(X, n, i), closedInterval((0:R), (1:R)))
proof
  unfold TermsIn
  intros k hk
  have value := coordinateSequence.value at X, n, i, k with sequence, hi
  rw value
  have parts := unitCube.membership.forward with (inCube with hk)
  exact parts.right with hi

theorem StrictlyIncreasingNat.comp (k l : Set)
  requires first : StrictlyIncreasingNat(k)
  requires second : StrictlyIncreasingNat(l)
  shows StrictlyIncreasingNat(compose(k, l, ℕ, ℕ, ℕ))
proof
  have kFunction := StrictlyIncreasingNat.function at k with *
  have lFunction := StrictlyIncreasingNat.function at l with *
  have function := compose.function at k, l, ℕ, ℕ, ℕ with *
  rcases first with ⟨kf, kStrict⟩
  rcases second with ⟨lf, lStrict⟩
  refine ⟨function, ?_⟩
  intros m mIn n nIn before
  have lm := FunctionBetween.apply_closed at l, ℕ, ℕ, m with *
  have ln := FunctionBetween.apply_closed at l, ℕ, ℕ, n with *
  have step := lStrict with m, mIn, n, nIn, before
  have result := kStrict with l(m), lm, l(n), ln, step
  rwa [compose.apply, compose.apply]

-- Bolzano–Weierstrass on the first m coordinates, by induction on m.
theorem unitCube.bolzano_weierstrass_prefix (n m : Nat) (X : Set)
  requires sequence : PointSequence(X, n)
  requires inCube : ∀ k ∈ ℕ, X(k) ∈ unitCube(n)
  shows m ∈ succ(n) → ∃ k, StrictlyIncreasingNat(k) ∧
    ∀ i ∈ m, ∃ L ∈ closedInterval((0:R), (1:R)), ConvergesTo(coordinateSequence(pointSubsequence(X, n, k), n, i), L)
proof
  induction m
  | zero =>
    intro hm
    witness identity(ℕ)
    constructor
    . exact identity.strictly_increasing_nat
    . 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 ⟨k, increasing, limits⟩ := ih with jIn
    have subSequence := pointSubsequence.sequence with sequence, increasing
    have subCube : ∀ a ∈ ℕ, pointSubsequence(X, n, k)(a) ∈ unitCube(n)
      intros a ha
      have value := pointSubsequence.value with sequence, increasing, ha
      rw value
      have kFunction := increasing.left
      exact inCube with (FunctionBetween.apply_closed with kFunction, ha)
    have coordinate := coordinateSequence.sequence with subSequence, jInN
    have terms := coordinateSequence.terms with subSequence, subCube, jInN
    obtain ⟨l, lIncreasing, L, LIn, LInterval, converges⟩ := closedInterval.bolzano_weierstrass at coordinateSequence(pointSubsequence(X, n, k), n, j), (0:R), (1:R) with coordinate, terms
    have composed := StrictlyIncreasingNat.comp with increasing, lIncreasing
    witness compose(k, l, ℕ, ℕ, ℕ)
    constructor
    . exact composed
    . intros i hi
      have split := bootstrap.succ.membership.forward with hi
      have nested : pointSubsequence(X, n, compose(k, l, ℕ, ℕ, ℕ)) = pointSubsequence(pointSubsequence(X, n, k), n, l)
        have kFunction := increasing.left
        have lFunction := lIncreasing.left
        have same1 : pointSubsequence(X, n, compose(k, l, ℕ, ℕ, ℕ)) = compose(X, compose(k, l, ℕ, ℕ, ℕ), ℕ, ℕ, functionSpace(n, ℝ))
          unfold pointSubsequence
          rfl
        have same2 : pointSubsequence(pointSubsequence(X, n, k), n, l) = compose(compose(X, k, ℕ, ℕ, functionSpace(n, ℝ)), l, ℕ, ℕ, functionSpace(n, ℝ))
          unfold pointSubsequence
          rfl
        have function := PointSequence.function with sequence
        rw [same1, same2]
        exact compose.associative with lFunction, kFunction, function
      rw under nested
      cases split with below | same
      . obtain ⟨M, MInterval, convergesM⟩ := limits with below
        have MParts := closedInterval.membership.forward with MInterval
        have MReal := MParts.left
        witness M
        constructor
        . exact MInterval
        . have iInN : i ∈ n
            have jLess := Less.of_membership with jInN
            have iNat := natural.member at j with below
            have iLess := Less.of_membership with below
            have less : i < n by arith
            exact membership.of_Less with less
          have same3 := coordinateSequence.subsequence with subSequence, lIncreasing, iInN
          rw under same3
          exact ConvergesTo.subsequence with convergesM, lIncreasing
      . rw under same
        have LParts := closedInterval.membership.forward with LInterval
        have LReal := LParts.left
        witness L
        constructor
        . exact LInterval
        . have same3 := coordinateSequence.subsequence with subSequence, lIncreasing, jInN
          rw under same3
          exact converges

defunique realLimit (u : Set) (L ∈ ℝ) := ConvergesTo(u, L)
requires convergent : ∃ L ∈ ℝ, ConvergesTo(u, L)
proof
  exact convergent
uniqueness
  intros a ha first b hb second
  exact ConvergesTo.unique with first, second

defgraph limitPoint (Y n : Set) (i ∈ n) : ℝ := realLimit(coordinateSequence(Y, n, i))
requires convergent : ∀ i ∈ n, ∃ L ∈ ℝ, ConvergesTo(coordinateSequence(Y, n, i), L)
proof
  have selected := realLimit.selected at coordinateSequence(Y, n, i) with (convergent with member)
  exact selected.left

theorem limitPoint.converges (Y n i : Set)
  requires convergent : ∀ i ∈ n, ∃ L ∈ ℝ, ConvergesTo(coordinateSequence(Y, n, i), L)
  requires hi : i ∈ n
  shows ConvergesTo(coordinateSequence(Y, n, i), limitPoint(Y, n)(i))
proof
  have value := limitPoint.value with convergent, hi
  rw value
  have selected := realLimit.selected at coordinateSequence(Y, n, i) with (convergent with hi)
  exact selected.right

-- Bolzano–Weierstrass for the cube: every sequence of points has a
-- subsequence converging in every coordinate to a point of the cube.
theorem unitCube.bolzano_weierstrass (n : Nat) (X : Set)
  requires sequence : PointSequence(X, n)
  requires inCube : ∀ k ∈ ℕ, X(k) ∈ unitCube(n)
  shows ∃ k, StrictlyIncreasingNat(k) ∧ ∃ L ∈ unitCube(n),
    ∀ i ∈ n, ConvergesTo(coordinateSequence(pointSubsequence(X, n, k), n, i), L(i))
proof
  have all := unitCube.bolzano_weierstrass_prefix with sequence, inCube
  obtain ⟨k, increasing, limits⟩ := all with (bootstrap.succ.self at n)
  have convergent : ∀ i ∈ n, ∃ L ∈ ℝ, ConvergesTo(coordinateSequence(pointSubsequence(X, n, k), n, i), L)
    intros i hi
    obtain ⟨L, LInterval, converges⟩ := limits with hi
    have parts := closedInterval.membership.forward with LInterval
    refine ⟨L, parts.left, converges⟩
  have limitFunction := limitPoint.function with convergent
  witness k
  constructor
  . exact increasing
  . witness limitPoint(pointSubsequence(X, n, k), n)
    constructor
    . apply unitCube.membership.backward
      constructor
      . exact functionSpace.mem_iff.backward with limitFunction
      . intros i hi
        have converges := limitPoint.converges with convergent, hi
        obtain ⟨L, LInterval, converges2⟩ := limits with hi
        have LParts := closedInterval.membership.forward with LInterval
        have LReal := LParts.left
        have limitReal := FunctionBetween.apply_closed with limitFunction, hi
        have same := ConvergesTo.unique with converges, converges2
        rwa same
    . intros i hi
      exact limitPoint.converges with convergent, hi