-- Closed complex disks: coordinate extraction and passage to the limit (ZF).
-- 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.Complex.Compactness
import PolynomialGrowth
import Real.Analysis.SequentialCompactness

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]

theorem subsequence.comp (u k l : Set)
  requires sequence : RealSequence(u)
  requires first : StrictlyIncreasingNat(k)
  requires second : StrictlyIncreasingNat(l)
  shows subsequence(subsequence(u, k), l) = subsequence(u, compose(k, l, ℕ, ℕ, ℕ))
proof
  have selected := subsequence.sequence at u, k with *
  have composite := StrictlyIncreasingNat.comp at k, l with *
  have left := subsequence.function at subsequence(u, k), l with *
  have right := subsequence.function at u, compose(k, l, ℕ, ℕ, ℕ) with *
  apply FunctionBetween.ext with left, right
  intros n nIn
  have nNat := nat.omega.backward at n with *
  have kFunction := StrictlyIncreasingNat.function at k with *
  have lFunction := StrictlyIncreasingNat.function at l with *
  have ln := FunctionBetween.apply_closed at l, ℕ, ℕ, n with *
  have lnNat := nat.omega.backward at l(n) with *
  have outer := subsequence.value at subsequence(u, k), l, n with *
  have inner := subsequence.value at u, k, l(n) with *
  have flat := subsequence.value at u, compose(k, l, ℕ, ℕ, ℕ), n with *
  have index := compose.apply at k, l, ℕ, ℕ, ℕ, n with *
  rw [outer, inner, flat, index]
  rfl

-- Two extractions give one selector for both coordinates.
theorem closedRectangle.bolzano_weierstrass (u v : Set) (a b c d : Real)
  requires horizontal : RealSequence(u)
  requires vertical : RealSequence(v)
  requires horizontalBounds : TermsIn(u, closedInterval(a, b))
  requires verticalBounds : TermsIn(v, closedInterval(c, d))
  shows ∃ k, StrictlyIncreasingNat(k) ∧
    ∃ x ∈ ℝ, ∃ y ∈ ℝ,
      x ∈ closedInterval(a, b) ∧ y ∈ closedInterval(c, d) ∧
      ConvergesTo(subsequence(u, k), x) ∧ ConvergesTo(subsequence(v, k), y)
proof
  obtain ⟨k, kIncreasing, x, xIn, xBounds, xLimit⟩ := closedInterval.bolzano_weierstrass at u, a, b with *
  have selectedV := subsequence.sequence at v, k with *
  have selectedBounds := TermsIn.subsequence at v, k, closedInterval(c, d) with *
  obtain ⟨l, lIncreasing, y, yIn, yBounds, yLimit⟩ := closedInterval.bolzano_weierstrass at subsequence(v, k), c, d with *
  have preserved := ConvergesTo.subsequence at subsequence(u, k), l, x with *
  have increasing := StrictlyIncreasingNat.comp at k, l with *
  have uFlat := subsequence.comp at u, k, l with *
  have vFlat := subsequence.comp at v, k, l with *
  rw uFlat at preserved
  rw vFlat at yLimit
  refine ⟨compose(k, l, ℕ, ℕ, ℕ), increasing, x, xIn, y, yIn, xBounds, yBounds, preserved, yLimit⟩

-- A coarse coordinate bound avoids square roots entirely.
theorem realLe.self_le_square_add_one (a : Real)
  shows a ≤ a * a + 1
proof
  have squareNonnegative := realMulValue.square_nonnegative at a with *
  have unitNonnegative := realLess.implies_le with realZero.lt_one
  have bounds := realLe.nonnegative_sum_bounds at a * a, realOne with *
  have comparison : a ≤ realOne ∨ ¬(a ≤ realOne) by tauto
  cases comparison with small | large
  . exact realLe.transitive at a, realOne, a * a + 1 with *
  . have strict := realLess.of_not_le at a, realOne with *
    have above := realLess.implies_le at realOne, a with *
    have nonnegative := realLe.transitive at realZero, realOne, a with *
    have multiplied := realLe.mul_right_of_nonnegative at realOne, a, a with *
    rw realMulValue.one_left at multiplied
    exact realLe.transitive at a, a * a, a * a + 1 with *

theorem realSquare.coordinate_bounds (a radius : Real)
  requires squareBound : a * a ≤ radius
  shows -(radius + 1) ≤ a ∧ a ≤ radius + 1
proof
  have upper := realLe.self_le_square_add_one at a with *
  have shifted := realLe.add_right at a * a, radius, realOne with *
  have positiveBound := realLe.transitive at a, a * a + 1, radius + 1 with *
  have negativeUpper := realLe.self_le_square_add_one at -a with *
  have negativeSquare : (-a) * (-a) = a * a by ring
  rw negativeSquare at negativeUpper
  have negativeBound := realLe.transitive at -a, a * a + 1, radius + 1 with *
  have lower := realLe.neg_reverse at -a, radius + 1 with *
  rw realNegValue.involutive at lower
  refine ⟨lower, positiveBound⟩

theorem complexNormSquared.coordinate_bounds (z : Set) (radius : Real)
  requires member : z ∈ complexCarrier
  requires bound : complexNormSquared(z) ≤ radius
  shows Euclidean.x(z) ∈ closedInterval(-(radius + 1), radius + 1) ∧
    Euclidean.y(z) ∈ closedInterval(-(radius + 1), radius + 1)
proof
  have point := complex.point with member
  have coordinates := Euclidean.coordinates at z with *
  have norm : complexNormSquared(z) = Euclidean.x(z) * Euclidean.x(z) + Euclidean.y(z) * Euclidean.y(z)
    unfold complexNormSquared
    unfold Euclidean.normSquared
    unfold Euclidean.dot
    rfl
  have xNonnegative := realMulValue.square_nonnegative at Euclidean.x(z) with *
  have yNonnegative := realMulValue.square_nonnegative at Euclidean.y(z) with *
  have sums := realLe.nonnegative_sum_bounds at Euclidean.x(z) * Euclidean.x(z), Euclidean.y(z) * Euclidean.y(z) with *
  rw norm at bound
  have xBound := realLe.transitive at Euclidean.x(z) * Euclidean.x(z), Euclidean.x(z) * Euclidean.x(z) + Euclidean.y(z) * Euclidean.y(z), radius with *
  have yBound := realLe.transitive at Euclidean.y(z) * Euclidean.y(z), Euclidean.x(z) * Euclidean.x(z) + Euclidean.y(z) * Euclidean.y(z), radius with *
  have xInterval := realSquare.coordinate_bounds at Euclidean.x(z), radius with *
  have yInterval := realSquare.coordinate_bounds at Euclidean.y(z), radius with *
  have xIn : Euclidean.x(z) ∈ ℝ by typecheck
  have yIn : Euclidean.y(z) ∈ ℝ by typecheck
  have lowerReal : Real(-(radius + 1)) by typecheck
  have upperReal : Real(radius + 1) by typecheck
  constructor
  . apply closedInterval.membership.backward at
    -(radius + 1), radius + 1, Euclidean.x(z)
    refine ⟨xIn, xInterval.left, xInterval.right⟩
  . apply closedInterval.membership.backward at
    -(radius + 1), radius + 1, Euclidean.y(z)
    refine ⟨yIn, yInterval.left, yInterval.right⟩

-- Complex sequences use the same set-theoretic function graphs as real ones.
predicate ComplexSequence (u : Set) := FunctionBetween(u, ℕ, complexCarrier)

defgraph complexSequenceX (u : Set) (n ∈ ℕ) : ℝ := Euclidean.x(u(n))
requires sequence : ComplexSequence(u)
proof
  have function : u : ℕ → complexCarrier
    unfold ComplexSequence at sequence
    exact sequence
  have value := FunctionBetween.apply_closed at u, ℕ, complexCarrier, n with *
  have point := complex.point with value
  have real := Euclidean.x.real at u(n) with *
  typecheck

defgraph complexSequenceY (u : Set) (n ∈ ℕ) : ℝ := Euclidean.y(u(n))
requires sequence : ComplexSequence(u)
proof
  have function : u : ℕ → complexCarrier
    unfold ComplexSequence at sequence
    exact sequence
  have value := FunctionBetween.apply_closed at u, ℕ, complexCarrier, n with *
  have point := complex.point with value
  have real := Euclidean.y.real at u(n) with *
  typecheck

predicate ComplexConvergesTo (u a : Set) :=
  ComplexSequence(u) ∧ a ∈ complexCarrier ∧
    ConvergesTo(complexSequenceX(u), Euclidean.x(a)) ∧
    ConvergesTo(complexSequenceY(u), Euclidean.y(a))

def complexSubsequence (u k : Set) : Set := compose(u, k, ℕ, ℕ, complexCarrier)

def closedComplexDisk (radius : Real) : Set :=
  { z ∈ complexCarrier | complexNormSquared(z) ≤ radius }

theorem complexSequenceX.sequence (u : Set)
  requires sequence : ComplexSequence(u)
  shows RealSequence(complexSequenceX(u))
proof
  unfold RealSequence
  exact complexSequenceX.function with *

theorem complexSequenceY.sequence (u : Set)
  requires sequence : ComplexSequence(u)
  shows RealSequence(complexSequenceY(u))
proof
  unfold RealSequence
  exact complexSequenceY.function with *

theorem complexSubsequence.sequence (u k : Set)
  requires sequence : ComplexSequence(u)
  requires increasing : StrictlyIncreasingNat(k)
  shows ComplexSequence(complexSubsequence(u, k))
proof
  have selector := StrictlyIncreasingNat.function with increasing
  have function : u : ℕ → complexCarrier by exact sequence
  unfold ComplexSequence
  unfold complexSubsequence
  exact compose.function with *

theorem complexSubsequence.value (u k : Set) (n : Nat)
  requires sequence : ComplexSequence(u)
  requires increasing : StrictlyIncreasingNat(k)
  shows complexSubsequence(u, k)(n) = u(k(n))
proof
  have selector := StrictlyIncreasingNat.function with increasing
  have function : u : ℕ → complexCarrier by exact sequence
  unfold complexSubsequence
  exact compose.apply with *

theorem complexSequenceX.subsequence (u k : Set)
  requires sequence : ComplexSequence(u)
  requires increasing : StrictlyIncreasingNat(k)
  shows complexSequenceX(complexSubsequence(u, k)) = subsequence(complexSequenceX(u), k)
proof
  have selected := complexSubsequence.sequence with *
  have horizontal := complexSequenceX.sequence at u with *
  have left := complexSequenceX.function at complexSubsequence(u, k) with *
  have right := subsequence.function with *
  apply FunctionBetween.ext with left, right
  intros n member
  have natural := nat.omega.backward at n with *
  have selector := StrictlyIncreasingNat.function with increasing
  have kn := FunctionBetween.apply_closed at k, ℕ, ℕ, n with *
  have knNat := nat.omega.backward at k(n) with *
  rw [complexSequenceX.value, complexSubsequence.value, subsequence.value, complexSequenceX.value]
  rfl

theorem complexSequenceY.subsequence (u k : Set)
  requires sequence : ComplexSequence(u)
  requires increasing : StrictlyIncreasingNat(k)
  shows complexSequenceY(complexSubsequence(u, k)) = subsequence(complexSequenceY(u), k)
proof
  have selected := complexSubsequence.sequence with *
  have vertical := complexSequenceY.sequence at u with *
  have left := complexSequenceY.function at complexSubsequence(u, k) with *
  have right := subsequence.function with *
  apply FunctionBetween.ext with left, right
  intros n member
  have natural := nat.omega.backward at n with *
  have selector := StrictlyIncreasingNat.function with increasing
  have kn := FunctionBetween.apply_closed at k, ℕ, ℕ, n with *
  have knNat := nat.omega.backward at k(n) with *
  rw [complexSequenceY.value, complexSubsequence.value, subsequence.value, complexSequenceY.value]
  rfl

theorem ComplexSequence.disk_coordinate_bounds (u : Set) (radius : Real)
  requires sequence : ComplexSequence(u)
  requires terms : TermsIn(u, closedComplexDisk(radius))
  shows TermsIn(complexSequenceX(u), closedInterval(-(radius + 1), radius + 1)) ∧
    TermsIn(complexSequenceY(u), closedInterval(-(radius + 1), radius + 1))
proof
  have coordinates : ∀ n ∈ ℕ,
      complexSequenceX(u)(n) ∈ closedInterval(-(radius + 1), radius + 1) ∧
      complexSequenceY(u)(n) ∈ closedInterval(-(radius + 1), radius + 1)
    intros n member
    have natural := nat.omega.backward at n with *
    have term := terms with n, member
    have disk := closedComplexDisk.membership.forward with term
    have bounds := complexNormSquared.coordinate_bounds at u(n), radius with *
    rwa [complexSequenceX.value, complexSequenceY.value]
  constructor
    intros n member
    have both := coordinates with n, member
    exact both.left
    intros n member
    have both := coordinates with n, member
    exact both.right

-- A polynomial inequality defining the disk is preserved by coordinate limits.
theorem ConvergesTo.sum_squares_le (u v : Set) (a b radius : Real)
  requires horizontal : ConvergesTo(u, a)
  requires vertical : ConvergesTo(v, b)
  requires bounds : ∀ n ∈ ℕ, (u(n):R) * u(n) + (v(n):R) * v(n) ≤ radius
  shows a * a + b * b ≤ radius
proof
  have uSequence := ConvergesTo.sequence at u, a with *
  have vSequence := ConvergesTo.sequence at v, b with *
  have uSquare := ConvergesTo.mul at u, u, a, a with *
  have vSquare := ConvergesTo.mul at v, v, b, b with *
  have sum := ConvergesTo.add at mulSequence(u, u), mulSequence(v, v), a * a, b * b with *
  have uSquareSequence := mulSequence.sequence at u, u with *
  have vSquareSequence := mulSequence.sequence at v, v with *
  have bounded : BoundedAboveBy(addSequence(mulSequence(u, u), mulSequence(v, v)), radius)
    intros n member
    have natural := nat.omega.backward at n with *
    have uReal := RealSequence.value at u, n with *
    have vReal := RealSequence.value at v, n with *
    have uSquareReal := RealSequence.value at mulSequence(u, u), n with *
    have vSquareReal := RealSequence.value at mulSequence(v, v), n with *
    rw [addSequence.value, mulSequence.value, mulSequence.value]
    have bound := bounds with n, member
    exact realLe.characterization.forward with bound
  exact ConvergesTo.le_constant with *

theorem closedComplexDisk.contains_limit (u a : Set) (radius : Real)
  requires converges : ComplexConvergesTo(u, a)
  requires terms : TermsIn(u, closedComplexDisk(radius))
  shows a ∈ closedComplexDisk(radius)
proof
  rcases converges with ⟨sequence, member, horizontal, vertical⟩
  have point := complex.point with member
  have bounds : ∀ n ∈ ℕ,
      (complexSequenceX(u)(n):R) * complexSequenceX(u)(n) + (complexSequenceY(u)(n):R) * complexSequenceY(u)(n) ≤ radius
    intros n nIn
    have natural := nat.omega.backward at n with *
    have term := terms with n, nIn
    have disk := closedComplexDisk.membership.forward with term
    have bound := disk.right
    rw [complexSequenceX.value, complexSequenceY.value]
    unfold complexNormSquared at bound
    unfold Euclidean.normSquared at bound
    unfold Euclidean.dot at bound
    exact bound
  have limit := ConvergesTo.sum_squares_le with horizontal, vertical, bounds
  apply closedComplexDisk.membership.backward
  constructor
  . exact member
  . unfold complexNormSquared
    unfold Euclidean.normSquared
    unfold Euclidean.dot
    exact limit

theorem TermsIn.complex_subsequence (u k S : Set)
  requires sequence : ComplexSequence(u)
  requires increasing : StrictlyIncreasingNat(k)
  requires terms : TermsIn(u, S)
  shows TermsIn(complexSubsequence(u, k), S)
proof
  intros n member
  have natural := nat.omega.backward at n with *
  have selector := StrictlyIncreasingNat.function with increasing
  have kn := FunctionBetween.apply_closed with *
  rw complexSubsequence.value
  exact terms with k(n), kn

-- Every sequence in a closed disk has a subsequence converging inside that disk.
-- The radius need not be nonnegative: the empty-disk case is vacuous.
theorem closedComplexDisk.bolzano_weierstrass (u : Set) (radius : Real)
  requires sequence : ComplexSequence(u)
  requires terms : TermsIn(u, closedComplexDisk(radius))
  shows ∃ k, StrictlyIncreasingNat(k) ∧ ∃ a ∈ closedComplexDisk(radius),
    ComplexConvergesTo(complexSubsequence(u, k), a)
proof
  have horizontal := complexSequenceX.sequence at u with *
  have vertical := complexSequenceY.sequence at u with *
  have bounds := ComplexSequence.disk_coordinate_bounds at u, radius with *
  obtain ⟨k, increasing, x, xIn, y, yIn, xBounds, yBounds, xLimit, yLimit⟩ := closedRectangle.bolzano_weierstrass at complexSequenceX(u), complexSequenceY(u), -(radius + 1), radius + 1, -(radius + 1), radius + 1 with *
  have pair := complexCarrier.pair at x, y with *
  have selected := complexSubsequence.sequence at u, k with *
  have horizontalSelected := complexSequenceX.subsequence at u, k with *
  have verticalSelected := complexSequenceY.subsequence at u, k with *
  have converges : ComplexConvergesTo(complexSubsequence(u, k), (x, y))
    unfold ComplexConvergesTo
    refine ⟨selected, pair, ?_⟩
    constructor
    . rw [horizontalSelected, Euclidean.x.pair]
      exact xLimit
    . rw [verticalSelected, Euclidean.y.pair]
      exact yLimit
  have selectedTerms := TermsIn.complex_subsequence at u, k, closedComplexDisk(radius) with *
  have member := closedComplexDisk.contains_limit at complexSubsequence(u, k), (x, y), radius with *
  refine ⟨k, increasing, (x, y), member, converges⟩

predicate ComplexSequentiallyCompact (S : Set) :=
  S ⊆ complexCarrier ∧
    (∀ u, ComplexSequence(u) → TermsIn(u, S) →
      ∃ k, StrictlyIncreasingNat(k) ∧ ∃ a ∈ S,
        ComplexConvergesTo(complexSubsequence(u, k), a))

theorem closedComplexDisk.sequentially_compact (radius : Real)
  shows ComplexSequentiallyCompact(closedComplexDisk(radius))
proof
  constructor
    intros z member
    have disk := closedComplexDisk.membership.forward with member
    exact disk.left
  . intros u sequence terms
    exact closedComplexDisk.bolzano_weierstrass with *

defgraph complexNormSequence (u : Set) (n ∈ ℕ) : ℝ := complexNormSquared(u(n))
requires sequence : ComplexSequence(u)
proof
  have function : u : ℕ → complexCarrier by exact sequence
  have value := FunctionBetween.apply_closed with *
  typecheck

theorem complexNormSequence.coordinates (u : Set)
  requires sequence : ComplexSequence(u)
  shows complexNormSequence(u) = addSequence(
    mulSequence(complexSequenceX(u), complexSequenceX(u)),
    mulSequence(complexSequenceY(u), complexSequenceY(u)))
proof
  have horizontal := complexSequenceX.sequence with *
  have vertical := complexSequenceY.sequence with *
  have xx := mulSequence.sequence at complexSequenceX(u), complexSequenceX(u) with *
  have yy := mulSequence.sequence at complexSequenceY(u), complexSequenceY(u) with *
  have sum := addSequence.sequence at mulSequence(complexSequenceX(u), complexSequenceX(u)), mulSequence(complexSequenceY(u), complexSequenceY(u)) with *
  have left := complexNormSequence.function at u with *
  have right : addSequence(mulSequence(complexSequenceX(u), complexSequenceX(u)), mulSequence(complexSequenceY(u), complexSequenceY(u))) : ℕ → ℝ
    exact sum
  apply FunctionBetween.ext with left, right
  intros n member
  have natural := nat.omega.backward at n with *
  have xReal := RealSequence.value at complexSequenceX(u), n with *
  have yReal := RealSequence.value at complexSequenceY(u), n with *
  have xxReal := RealSequence.value at mulSequence(complexSequenceX(u), complexSequenceX(u)), n with *
  have yyReal := RealSequence.value at mulSequence(complexSequenceY(u), complexSequenceY(u)), n with *
  rw [complexNormSequence.value, addSequence.value, mulSequence.value, mulSequence.value, complexSequenceX.value, complexSequenceY.value]
  unfold complexNormSquared
  unfold Euclidean.normSquared
  unfold Euclidean.dot
  rfl

theorem ComplexConvergesTo.norm_squared (u a : Set)
  requires converges : ComplexConvergesTo(u, a)
  shows ConvergesTo(complexNormSequence(u), complexNormSquared(a))
proof
  rcases converges with ⟨sequence, member, horizontal, vertical⟩
  have point := complex.point with member
  have xx := ConvergesTo.mul at complexSequenceX(u), complexSequenceX(u), Euclidean.x(a), Euclidean.x(a) with *
  have yy := ConvergesTo.mul at complexSequenceY(u), complexSequenceY(u), Euclidean.y(a), Euclidean.y(a) with *
  have sum := ConvergesTo.add at mulSequence(complexSequenceX(u), complexSequenceX(u)), mulSequence(complexSequenceY(u), complexSequenceY(u)), Euclidean.x(a) * Euclidean.x(a), Euclidean.y(a) * Euclidean.y(a) with *
  rw complexNormSequence.coordinates
  unfold complexNormSquared
  unfold Euclidean.normSquared
  unfold Euclidean.dot
  exact sum