-- Sequences in a metric space: convergence and its uniqueness, constant
-- sequences and subsequences, Cauchy sequences, their boundedness, and
-- complete spaces
-- 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.Metric.Sequences
import Continuity
import Real.Analysis.SequentialCompactness

predicate SequenceIn (X u : Set) := FunctionBetween(u, ℕ, X)

theorem SequenceIn.function (X u : Set)
  requires sequence : SequenceIn(X, u)
  shows u : ℕ → X
proof
  exact sequence

theorem SequenceIn.term (X u : Set, n : Nat)
  requires sequence : SequenceIn(X, u)
  shows u(n) ∈ X
proof
  have function := SequenceIn.function with sequence
  have member : n ∈ ℕ by simp [Nat]
  exact FunctionBetween.apply_closed with function, member

theorem SequenceIn.term_of_member (X u n : Set)
  requires sequence : SequenceIn(X, u)
  requires hn : n ∈ ℕ
  shows u(n) ∈ X
proof
  have function := SequenceIn.function with sequence
  exact FunctionBetween.apply_closed with function, hn

theorem SequenceIn.compose (X Y u f : Set)
  requires sequence : SequenceIn(X, u)
  requires function : f : X → Y
  shows SequenceIn(Y, compose(f, u, ℕ, X, Y))
proof
  have uFunction := SequenceIn.function with sequence
  exact compose.function with uFunction, function

theorem SequenceIn.subsequence (X u k : Set)
  requires sequence : SequenceIn(X, u)
  requires increasing : StrictlyIncreasingNat(k)
  shows SequenceIn(X, compose(u, k, ℕ, ℕ, X))
proof
  have uFunction := SequenceIn.function with sequence
  have selector := StrictlyIncreasingNat.function with increasing
  exact compose.function with selector, uFunction

-- Two naturals have a common upper bound.
theorem naturalPair.upper_bound (M N : Nat)
  shows ∃ K ∈ ℕ, M ≤ K ∧ N ≤ K
proof
  have order := LessEqual.total at M, N
  cases order with le | ge
  . have member : N ∈ ℕ by simp [Nat]
    exact ⟨N, member, le, (LessEqual.reflexive at N)⟩
  . have member : M ∈ ℕ by simp [Nat]
    exact ⟨M, member, (LessEqual.reflexive at M), ge⟩

-- Convergence

predicate ConvergesIn (X d u x : Set) :=
  SequenceIn(X, u) ∧ x ∈ X ∧
  (∀ ε ∈ ℝ, 0 < ε → ∃ N ∈ ℕ, ∀ n ∈ ℕ, (N ≤ n → d(x, u(n)) < ε))

theorem ConvergesIn.sequence (X d u x : Set)
  requires converges : ConvergesIn(X, d, u, x)
  shows SequenceIn(X, u)
proof
  exact converges.left

theorem ConvergesIn.limit_point (X d u x : Set)
  requires converges : ConvergesIn(X, d, u, x)
  shows x ∈ X
proof
  obtain ⟨sequence, hx, tail⟩ := converges
  exact hx

theorem ConvergesIn.eventually (X d u x : Set, ε : Real)
  requires converges : ConvergesIn(X, d, u, x)
  requires positive : 0 < ε
  shows ∃ N ∈ ℕ, ∀ n ∈ ℕ, (N ≤ n → d(x, u(n)) < ε)
proof
  obtain ⟨sequence, hx, tail⟩ := converges
  have realE : ε ∈ ℝ by typecheck
  exact tail with ε, realE, positive

theorem ConvergesIn.of_eventually (X d u x : Set)
  requires sequence : SequenceIn(X, u)
  requires hx : x ∈ X
  requires tail : ∀ ε ∈ ℝ, 0 < ε → ∃ N ∈ ℕ, ∀ n ∈ ℕ, (N ≤ n → d(x, u(n)) < ε)
  shows ConvergesIn(X, d, u, x)
proof
  exact ⟨sequence, hx, tail⟩

theorem ConvergesIn.eventually_ball (X d u x : Set, ε : Real)
  requires converges : ConvergesIn(X, d, u, x)
  requires positive : 0 < ε
  shows ∃ N ∈ ℕ, ∀ n ∈ ℕ, (N ≤ n → u(n) ∈ ball(X, d, x, ε))
proof
  have sequence := ConvergesIn.sequence with converges
  obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, positive
  refine ⟨N, hN, ?_⟩
  intros n hn le
  have term := SequenceIn.term_of_member with sequence, hn
  exact ball.of_distance with term, (near with n, hn, le)

theorem ConvergesIn.unique (X d u x y : Set)
  requires metric : IsMetric(X, d)
  requires first : ConvergesIn(X, d, u, x)
  requires second : ConvergesIn(X, d, u, y)
  shows x = y
proof
  have hx := ConvergesIn.limit_point with first
  have hy := ConvergesIn.limit_point with second
  have sequence := ConvergesIn.sequence with first
  by_contra
  have dxy := IsMetric.real with metric, hx, hy
  have halfPositive := ball.half_positive with metric, hx, hy, this
  have doubled := half.add_self at d(x, y)
  obtain ⟨M, hM, nearX⟩ := ConvergesIn.eventually with first, halfPositive
  obtain ⟨N, hN, nearY⟩ := ConvergesIn.eventually with second, halfPositive
  have natM : Nat(M) by exact hM
  have natN : Nat(N) by exact hN
  obtain ⟨K, hK, leM, leN⟩ := naturalPair.upper_bound at M, N
  have closeX := nearX with K, hK, leM
  have closeY := nearY with K, hK, leN
  have term := SequenceIn.term_of_member with sequence, hK
  have triangle := IsMetric.triangle with metric, hx, term, hy
  have symmetric := IsMetric.symmetric with metric, hy, term
  have dxu := IsMetric.real with metric, hx, term
  have duy := IsMetric.real with metric, term, hy
  have dyu := IsMetric.real with metric, hy, term
  linarith

theorem constantFunction.converges_in (X d x : Set)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  shows ConvergesIn(X, d, constantFunction(ℕ, X, x), x)
proof
  have function := constantFunction.function at ℕ, X, x with hx
  have sequence : SequenceIn(X, constantFunction(ℕ, X, x)) by exact function
  apply ConvergesIn.of_eventually with sequence, hx
  intros ε hε positive
  have zero : 0 ∈ ℕ by exact nat.omega.forward at 0 with
    Naturals.constructor.zero
  refine ⟨0, zero, ?_⟩
  intros n hn le
  have value := constantFunction.apply with hn, hx
  rw value
  have self := IsMetric.self with metric, hx
  rw self
  exact positive

theorem ConvergesIn.subsequence (X d u k x : Set)
  requires converges : ConvergesIn(X, d, u, x)
  requires increasing : StrictlyIncreasingNat(k)
  shows ConvergesIn(X, d, compose(u, k, ℕ, ℕ, X), x)
proof
  have sequence := ConvergesIn.sequence with converges
  have selector := StrictlyIncreasingNat.function with increasing
  have composite := SequenceIn.subsequence with sequence, increasing
  have hx := ConvergesIn.limit_point with converges
  apply ConvergesIn.of_eventually with composite, hx
  intros ε hε positive
  obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, positive
  refine ⟨N, hN, ?_⟩
  intros n hn le
  have natN : Nat(N) by exact hN
  have natn : Nat(n) by exact hn
  have index := StrictlyIncreasingNat.index_le_value at k, n with increasing
  have image := FunctionBetween.apply_closed with selector, hn
  have natImage : Nat(k(n)) by exact image
  have beyond := LessEqual.transitive with le, index
  have uFunction := SequenceIn.function with sequence
  have value := compose.apply with selector, uFunction, hn
  rw value
  exact near with k(n), image, beyond

-- A continuous map sends convergent sequences to convergent sequences.
theorem ConvergesIn.map (f X d Y e u x : Set)
  requires continuous : MetricContinuousAt(f, X, d, Y, e, x)
  requires converges : ConvergesIn(X, d, u, x)
  shows ConvergesIn(Y, e, compose(f, u, ℕ, X, Y), f(x))
proof
  have function := MetricContinuousAt.function with continuous
  have sequence := ConvergesIn.sequence with converges
  have hx := ConvergesIn.limit_point with converges
  have composite := SequenceIn.compose with sequence, function
  have image := FunctionBetween.apply_closed with function, hx
  apply ConvergesIn.of_eventually with composite, image
  intros ε hε positive
  obtain ⟨δ, hδ, positiveD, maps⟩ :=
    MetricContinuousAt.control with continuous, positive
  obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, positiveD
  refine ⟨N, hN, ?_⟩
  intros n hn le
  have term := SequenceIn.term_of_member with sequence, hn
  have uFunction := SequenceIn.function with sequence
  have value := compose.apply with uFunction, function, hn
  rw value
  exact maps with u(n), term, (near with n, hn, le)

theorem ConvergesIn.eventually_in_open (X d u x U : Set)
  requires converges : ConvergesIn(X, d, u, x)
  requires open : MetricOpen(X, d, U)
  requires hxU : x ∈ U
  shows ∃ N ∈ ℕ, ∀ n ∈ ℕ, (N ≤ n → u(n) ∈ U)
proof
  have sequence := ConvergesIn.sequence with converges
  obtain ⟨r, hr, positive, inside⟩ := MetricOpen.ball_inside with open, hxU
  obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, positive
  refine ⟨N, hN, ?_⟩
  intros n hn le
  have term := SequenceIn.term_of_member with sequence, hn
  exact inside with u(n), (ball.of_distance with term, (near with n, hn, le))

-- Limits of sequences in a closed set stay in the set.
theorem ConvergesIn.limit_in_closed (X d u x C : Set)
  requires closed : MetricClosed(X, d, C)
  requires terms : ∀ n ∈ ℕ, u(n) ∈ C
  requires converges : ConvergesIn(X, d, u, x)
  shows x ∈ C
proof
  have sequence := ConvergesIn.sequence with converges
  have hx := ConvergesIn.limit_point with converges
  apply MetricClosed.of_balls_meet with closed, hx
  intros r hr positive
  obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, positive
  have natN : Nat(N) by exact hN
  have term := SequenceIn.term_of_member with sequence, hN
  have close := near with N, hN, (LessEqual.reflexive at N)
  witness u(N)
  apply intersection.membership.backward
  exact ⟨(ball.of_distance with term, close), (terms with N, hN)⟩

theorem ConvergesIn.limit_in_closure (X d u x A : Set)
  requires metric : IsMetric(X, d)
  requires hA : A ⊆ X
  requires terms : ∀ n ∈ ℕ, u(n) ∈ A
  requires converges : ConvergesIn(X, d, u, x)
  shows x ∈ closure(X, metricTopology(X, d), A)
proof
  have sequence := ConvergesIn.sequence with converges
  have hx := ConvergesIn.limit_point with converges
  apply metricClosure.of_balls_meet with metric, hA, hx
  intros r hr positive
  obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, positive
  have natN : Nat(N) by exact hN
  have term := SequenceIn.term_of_member with sequence, hN
  have close := near with N, hN, (LessEqual.reflexive at N)
  witness u(N)
  apply intersection.membership.backward
  exact ⟨(ball.of_distance with term, close), (terms with N, hN)⟩

-- Cauchy sequences

predicate IsCauchy (X d u : Set) :=
  SequenceIn(X, u) ∧
  (∀ ε ∈ ℝ, 0 < ε → ∃ N ∈ ℕ, ∀ m ∈ ℕ, ∀ n ∈ ℕ,
    (N ≤ m → N ≤ n → d(u(m), u(n)) < ε))

theorem IsCauchy.sequence (X d u : Set)
  requires cauchy : IsCauchy(X, d, u)
  shows SequenceIn(X, u)
proof
  exact cauchy.left

theorem IsCauchy.eventually (X d u : Set, ε : Real)
  requires cauchy : IsCauchy(X, d, u)
  requires positive : 0 < ε
  shows ∃ N ∈ ℕ, ∀ m ∈ ℕ, ∀ n ∈ ℕ, (N ≤ m → N ≤ n → d(u(m), u(n)) < ε)
proof
  obtain ⟨sequence, tail⟩ := cauchy
  have realE : ε ∈ ℝ by typecheck
  exact tail with ε, realE, positive

theorem IsCauchy.of_eventually (X d u : Set)
  requires sequence : SequenceIn(X, u)
  requires tail : ∀ ε ∈ ℝ, 0 < ε → ∃ N ∈ ℕ, ∀ m ∈ ℕ, ∀ n ∈ ℕ,
    (N ≤ m → N ≤ n → d(u(m), u(n)) < ε)
  shows IsCauchy(X, d, u)
proof
  exact ⟨sequence, tail⟩

theorem ConvergesIn.cauchy (X d u x : Set)
  requires metric : IsMetric(X, d)
  requires converges : ConvergesIn(X, d, u, x)
  shows IsCauchy(X, d, u)
proof
  have sequence := ConvergesIn.sequence with converges
  have hx := ConvergesIn.limit_point with converges
  apply IsCauchy.of_eventually with sequence
  intros ε hε positive
  have halfPositive := half.positive with positive
  have doubled := half.add_self at ε
  obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, halfPositive
  refine ⟨N, hN, ?_⟩
  intros m hm n hn leM leN
  have termM := SequenceIn.term_of_member with sequence, hm
  have termN := SequenceIn.term_of_member with sequence, hn
  have closeM := near with m, hm, leM
  have closeN := near with n, hn, leN
  have triangle := IsMetric.triangle_from with metric, hx, termM, termN
  have dxm := IsMetric.real with metric, hx, termM
  have dxn := IsMetric.real with metric, hx, termN
  have dmn := IsMetric.real with metric, termM, termN
  linarith

theorem IsCauchy.subsequence (X d u k : Set)
  requires cauchy : IsCauchy(X, d, u)
  requires increasing : StrictlyIncreasingNat(k)
  shows IsCauchy(X, d, compose(u, k, ℕ, ℕ, X))
proof
  have sequence := IsCauchy.sequence with cauchy
  have selector := StrictlyIncreasingNat.function with increasing
  have composite := SequenceIn.subsequence with sequence, increasing
  apply IsCauchy.of_eventually with composite
  intros ε hε positive
  obtain ⟨N, hN, near⟩ := IsCauchy.eventually with cauchy, positive
  refine ⟨N, hN, ?_⟩
  intros m hm n hn leM leN
  have natN : Nat(N) by exact hN
  have natM : Nat(m) by exact hm
  have natn : Nat(n) by exact hn
  have indexM := StrictlyIncreasingNat.index_le_value at k, m with increasing
  have indexN := StrictlyIncreasingNat.index_le_value at k, n with increasing
  have imageM := FunctionBetween.apply_closed with selector, hm
  have imageN := FunctionBetween.apply_closed with selector, hn
  have natImageM : Nat(k(m)) by exact imageM
  have natImageN : Nat(k(n)) by exact imageN
  have beyondM := LessEqual.transitive with leM, indexM
  have beyondN := LessEqual.transitive with leN, indexN
  have uFunction := SequenceIn.function with sequence
  have valueM := compose.apply with selector, uFunction, hm
  have valueN := compose.apply with selector, uFunction, hn
  rw [valueM, valueN]
  exact near with k(m), imageM, k(n), imageN, beyondM, beyondN

-- A Cauchy sequence with a convergent subsequence converges.
theorem IsCauchy.converges_of_subsequence (X d u k x : Set)
  requires metric : IsMetric(X, d)
  requires cauchy : IsCauchy(X, d, u)
  requires increasing : StrictlyIncreasingNat(k)
  requires converges : ConvergesIn(X, d, compose(u, k, ℕ, ℕ, X), x)
  shows ConvergesIn(X, d, u, x)
proof
  have sequence := IsCauchy.sequence with cauchy
  have selector := StrictlyIncreasingNat.function with increasing
  have hx := ConvergesIn.limit_point with converges
  apply ConvergesIn.of_eventually with sequence, hx
  intros ε hε positive
  have halfPositive := half.positive with positive
  have doubled := half.add_self at ε
  obtain ⟨M, hM, close⟩ := IsCauchy.eventually with cauchy, halfPositive
  obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, halfPositive
  have natM : Nat(M) by exact hM
  have natN : Nat(N) by exact hN
  obtain ⟨K, hK, leM, leN⟩ := naturalPair.upper_bound at M, N
  refine ⟨K, hK, ?_⟩
  intros n hn le
  have natK : Nat(K) by exact hK
  have natn : Nat(n) by exact hn
  have index := StrictlyIncreasingNat.index_le_value at k, n with increasing
  have image := FunctionBetween.apply_closed with selector, hn
  have natImage : Nat(k(n)) by exact image
  have aboveM := LessEqual.transitive with leM, le
  have aboveN := LessEqual.transitive with leN, le
  have imageAboveM := LessEqual.transitive with aboveM, index
  have imageAboveN := LessEqual.transitive with aboveN, index
  have uFunction := SequenceIn.function with sequence
  have value := compose.apply with selector, uFunction, hn
  have nearImage := near with n, hn, aboveN
  rw value at nearImage
  have closePair := close with k(n), image, n, hn, imageAboveM, aboveM
  have term := SequenceIn.term_of_member with sequence, hn
  have termImage := SequenceIn.term_of_member with sequence, image
  have triangle := IsMetric.triangle with metric, hx, termImage, term
  have dxi := IsMetric.real with metric, hx, termImage
  have din := IsMetric.real with metric, termImage, term
  have dxn := IsMetric.real with metric, hx, term
  linarith

-- Finitely many initial terms stay within a bounded distance of the first.
theorem SequenceIn.prefix_bound (X d u : Set, N : Nat)
  requires metric : IsMetric(X, d)
  requires sequence : SequenceIn(X, u)
  shows ∃ B ∈ ℝ, 0 ≤ B ∧ ∀ n ∈ ℕ, (n ≤ N → d(u(0), u(n)) ≤ B)
proof
  induction N
  | zero =>
    have zero : 0 ∈ ℕ by exact nat.omega.forward at 0 with
      Naturals.constructor.zero
    have term := SequenceIn.term_of_member at X, u, 0 with sequence, zero
    have self := IsMetric.self at X, d, u(0) with metric, term
    have zeroReal : (0:R) ∈ ℝ by typecheck
    have reflexive : (0:R) ≤ 0 by linarith
    refine ⟨(0:R), zeroReal, reflexive, ?_⟩
    intros n hn le
    have natN : Nat(n) by exact hn
    have equal := LessEqual.antisymmetric with
      le, (Grace.Core.Nat.Order.LessEqual.zero at n)
    rw equal
    rw self
    exact reflexive
  | k + 1 using ih =>
    obtain ⟨B, hB, nonnegativeB, bound⟩ := ih
    have zero : 0 ∈ ℕ by exact nat.omega.forward at 0 with
      Naturals.constructor.zero
    have natNext : Nat(k + 1) by typecheck
    have next : k + 1 ∈ ℕ by exact nat.omega.forward with natNext
    have term0 := SequenceIn.term_of_member at X, u, 0 with sequence, zero
    have termNext := SequenceIn.term_of_member at X, u, k + 1 with
      sequence, next
    have distance := IsMetric.real at X, d, u(0), u(k + 1) with
      metric, term0, termNext
    have nonnegative := IsMetric.nonnegative at X, d, u(0), u(k + 1) with
      metric, term0, termNext
    have sumReal : B + d(u(0), u(k + 1)) ∈ ℝ by typecheck
    have sumNonnegative : (0:R) ≤ B + d(u(0), u(k + 1)) by linarith
    refine ⟨B + d(u(0), u(k + 1)), sumReal, sumNonnegative, ?_⟩
    intros n hn le
    have natN : Nat(n) by exact hn
    have order := Less.trichotomy at n, k + 1 with natN
    rcases order with below | equal | above
    . have le2 : n ≤ k by arith
      have earlier := bound with n, hn, le2
      have termN := SequenceIn.term_of_member at X, u, n with sequence, hn
      have distanceN := IsMetric.real at X, d, u(0), u(n) with
        metric, term0, termN
      linarith
    . rw equal
      linarith
    . exfalso
      have cycle : n < n by arith
      exact Less.irreflexive with cycle

theorem IsCauchy.bounded (X d u : Set)
  requires metric : IsMetric(X, d)
  requires cauchy : IsCauchy(X, d, u)
  shows ∃ r ∈ ℝ, ∀ n ∈ ℕ, d(u(0), u(n)) < r
proof
  have sequence := IsCauchy.sequence with cauchy
  have one : (0:R) < 1 by linarith
  obtain ⟨N, hN, close⟩ := IsCauchy.eventually with cauchy, one
  have natN : Nat(N) by exact hN
  obtain ⟨B, hB, nonnegativeB, bound⟩ :=
    SequenceIn.prefix_bound at X, d, u, N with
    metric, sequence
  have zero : 0 ∈ ℕ by exact nat.omega.forward at 0 with
    Naturals.constructor.zero
  have term0 := SequenceIn.term_of_member with sequence, zero
  have termN := SequenceIn.term_of_member with sequence, hN
  have d0N := IsMetric.real with metric, term0, termN
  have nonnegative := IsMetric.nonnegative with metric, term0, termN
  have radiusReal : B + d(u(0), u(N)) + 1 ∈ ℝ by typecheck
  refine ⟨B + d(u(0), u(N)) + 1, radiusReal, ?_⟩
  intros n hn
  have natn : Nat(n) by exact hn
  have termn := SequenceIn.term_of_member with sequence, hn
  have d0n := IsMetric.real with metric, term0, termn
  have order := LessEqual.total at n, N
  cases order with le | ge
  . have early := bound with n, hn, le
    linarith
  . have late := close with N, hN, n, hn, (LessEqual.reflexive at N), ge
    have dNn := IsMetric.real with metric, termN, termn
    have triangle := IsMetric.triangle with metric, term0, termN, termn
    linarith

-- Complete spaces

predicate IsComplete (X d : Set) :=
  IsMetric(X, d) ∧ (∀ u, IsCauchy(X, d, u) → ∃ x ∈ X, ConvergesIn(X, d, u, x))

theorem IsComplete.metric (X d : Set)
  requires complete : IsComplete(X, d)
  shows IsMetric(X, d)
proof
  exact complete.left

theorem IsComplete.limit (X d u : Set)
  requires complete : IsComplete(X, d)
  requires cauchy : IsCauchy(X, d, u)
  shows ∃ x ∈ X, ConvergesIn(X, d, u, x)
proof
  exact complete.right with u, cauchy

theorem IsComplete.of_limits (X d : Set)
  requires metric : IsMetric(X, d)
  requires limits : ∀ u, IsCauchy(X, d, u) → ∃ x ∈ X, ConvergesIn(X, d, u, x)
  shows IsComplete(X, d)
proof
  exact ⟨metric, limits⟩

-- In a complete space a Cauchy sequence converges exactly to the limit of
-- any convergent subsequence; conversely convergence is characterized by
-- the Cauchy property.
theorem IsComplete.cauchy_iff_converges (X d u : Set)
  requires complete : IsComplete(X, d)
  shows IsCauchy(X, d, u) ↔ ∃ x ∈ X, ConvergesIn(X, d, u, x)
proof
  have metric := IsComplete.metric with complete
  constructor
  . intro cauchy
    exact IsComplete.limit with complete, cauchy
  . intro data
    obtain ⟨x, hx, converges⟩ := data
    exact ConvergesIn.cauchy with metric, converges