-- Coordinate convergence and squared-distance continuity describe the same limits.
-- 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.SequentialContinuity
import Compactness

theorem realSquare.abs_lt_of_lt_square (a e : Real)
  requires positive : realZero < e
  requires small : a * a < e * e
  shows abs(a) < e
proof
  have nonnegative := abs.nonnegative at a with *
  have eNonnegative := realLess.implies_le at realZero, e with *
  have squareNonnegative := realMulValue.square_nonnegative at a with *
  have squareAbs := abs.of_nonnegative at a * a with *
  have multiplicative := abs.mul at a, a with *
  have square : abs(a) * abs(a) = a * a by cc
  have comparison : e ≤ abs(a) ∨ ¬(e ≤ abs(a)) by tauto
  cases comparison with large | notLarge
  . have first := realLe.mul_left_of_nonnegative at e, abs(a), e with *
    have second := realLe.mul_right_of_nonnegative at e, abs(a), abs(a) with *
    have bound := realLe.transitive at e * e, e * abs(a), abs(a) * abs(a) with *
    rw square at bound
    have impossible := realLess.transitive_le at a * a, e * e, a * a with *
    have irrefl := realLess.irreflexive_on
    exfalso
    exact irrefl with a * a, impossible
  . exact realLess.of_not_le at e, abs(a) with *

def complexDistanceSequence (u a : Set) : Set :=
  addSequence(
    mulSequence(subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a))), subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a)))),
    mulSequence(subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a))), subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a)))))

def complexMappedSequence (f u : Set) : Set := compose(f, u, ℕ, complexCarrier, complexCarrier)

section Complexes
notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)
notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)

theorem complexNormSquared.difference_coordinates (z a : Set)
  requires first : z ∈ ℂ
  requires second : a ∈ ℂ
  shows complexNormSquared(ℂ[z - a]) = R[(Euclidean.x(z) - Euclidean.x(a)) * (Euclidean.x(z) - Euclidean.x(a)) + (Euclidean.y(z) - Euclidean.y(a)) * (Euclidean.y(z) - Euclidean.y(a))]
proof
  have zPoint := complex.point with first
  have aPoint := complex.point with second
  rw [complexNormSquared.difference_distance, Euclidean.distanceSquared.coordinates]
  ring

theorem complexNormSquared.small_coordinates (z a : Set) (e : Real)
  requires first : z ∈ ℂ
  requires second : a ∈ ℂ
  requires positive : R[0] < e
  requires small : complexNormSquared(ℂ[z - a]) < R[e * e]
  shows Euclidean.x(z) ∈ openBall(Euclidean.x(a), e) ∧ Euclidean.y(z) ∈ openBall(Euclidean.y(a), e)
proof
  have zPoint := complex.point with first
  have aPoint := complex.point with second
  have ax := Euclidean.x.real at a with *
  have ay := Euclidean.y.real at a with *
  have xx := realMulValue.square_nonnegative at R[Euclidean.x(z) - Euclidean.x(a)] with *
  have yy := realMulValue.square_nonnegative at R[Euclidean.y(z) - Euclidean.y(a)] with *
  have sums := realLe.nonnegative_sum_bounds at R[(Euclidean.x(z) - Euclidean.x(a)) * (Euclidean.x(z) - Euclidean.x(a))], R[(Euclidean.y(z) - Euclidean.y(a)) * (Euclidean.y(z) - Euclidean.y(a))] with *
  rw complexNormSquared.difference_coordinates at small
  have xSmall := realLe.transitive_less at R[(Euclidean.x(z) - Euclidean.x(a)) * (Euclidean.x(z) - Euclidean.x(a))], R[(Euclidean.x(z) - Euclidean.x(a)) * (Euclidean.x(z) - Euclidean.x(a)) + (Euclidean.y(z) - Euclidean.y(a)) * (Euclidean.y(z) - Euclidean.y(a))], R[e * e] with *
  have ySmall := realLe.transitive_less at R[(Euclidean.y(z) - Euclidean.y(a)) * (Euclidean.y(z) - Euclidean.y(a))], R[(Euclidean.x(z) - Euclidean.x(a)) * (Euclidean.x(z) - Euclidean.x(a)) + (Euclidean.y(z) - Euclidean.y(a)) * (Euclidean.y(z) - Euclidean.y(a))], R[e * e] with *
  have xAbs := realSquare.abs_lt_of_lt_square at R[Euclidean.x(z) - Euclidean.x(a)], e with *
  have yAbs := realSquare.abs_lt_of_lt_square at R[Euclidean.y(z) - Euclidean.y(a)], e with *
  have xIn : Euclidean.x(z) ∈ ℝ by typecheck
  have yIn : Euclidean.y(z) ∈ ℝ by typecheck
  constructor
  . apply openBall.membership.backward
    constructor
    . exact xIn
    . unfold dist
      unfold realSubValue
      exact xAbs
  . apply openBall.membership.backward
    constructor
    . exact yIn
    . unfold dist
      unfold realSubValue
      exact yAbs


theorem complexDistanceSequence.converges_zero (u a : Set)
  requires converges : ComplexConvergesTo(u, a)
  shows ConvergesTo(complexDistanceSequence(u, a), R[0])
proof
  rcases converges with ⟨sequence, member, horizontal, vertical⟩
  have point := complex.point with member
  have xConstant := constantSequence.converges at Euclidean.x(a) with *
  have yConstant := constantSequence.converges at Euclidean.y(a) with *
  have xDiff := ConvergesTo.sub at complexSequenceX(u), constantSequence(Euclidean.x(a)), Euclidean.x(a), Euclidean.x(a) with *
  have yDiff := ConvergesTo.sub at complexSequenceY(u), constantSequence(Euclidean.y(a)), Euclidean.y(a), Euclidean.y(a) with *
  unfold realSubValue at xDiff
  unfold realSubValue at yDiff
  have xx := ConvergesTo.mul at subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a))), subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a))), R[Euclidean.x(a) - Euclidean.x(a)], R[Euclidean.x(a) - Euclidean.x(a)] with *
  have yy := ConvergesTo.mul at subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a))), subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a))), R[Euclidean.y(a) - Euclidean.y(a)], R[Euclidean.y(a) - Euclidean.y(a)] with *
  have sum := ConvergesTo.add at mulSequence(subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a))), subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a)))), mulSequence(subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a))), subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a)))), R[(Euclidean.x(a) - Euclidean.x(a)) * (Euclidean.x(a) - Euclidean.x(a))], R[(Euclidean.y(a) - Euclidean.y(a)) * (Euclidean.y(a) - Euclidean.y(a))] with *
  have zero : R[(Euclidean.x(a) - Euclidean.x(a)) * (Euclidean.x(a) - Euclidean.x(a)) + (Euclidean.y(a) - Euclidean.y(a)) * (Euclidean.y(a) - Euclidean.y(a))] = R[0]
    ring
  rw zero at sum
  unfold complexDistanceSequence
  exact sum

theorem complexDistanceSequence.value (u a : Set) (n : Nat)
  requires sequence : ComplexSequence(u)
  requires center : a ∈ ℂ
  shows complexDistanceSequence(u, a)(n) = complexNormSquared(ℂ[u(n) - a])
proof
  have point := complex.point with center
  have horizontal := complexSequenceX.sequence with *
  have vertical := complexSequenceY.sequence with *
  have xConstant := constantSequence.sequence at Euclidean.x(a) with *
  have yConstant := constantSequence.sequence at Euclidean.y(a) with *
  have xDiff := subSequence.sequence at complexSequenceX(u), constantSequence(Euclidean.x(a)) with *
  have yDiff := subSequence.sequence at complexSequenceY(u), constantSequence(Euclidean.y(a)) with *
  have xx := mulSequence.sequence at subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a))), subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a))) with *
  have yy := mulSequence.sequence at subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a))), subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a))) with *
  have xReal := RealSequence.value at complexSequenceX(u), n with *
  have yReal := RealSequence.value at complexSequenceY(u), n with *
  have cxReal := RealSequence.value at constantSequence(Euclidean.x(a)), n with *
  have cyReal := RealSequence.value at constantSequence(Euclidean.y(a)), n with *
  have dxReal := RealSequence.value at subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a))), n with *
  have dyReal := RealSequence.value at subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a))), n with *
  have xxReal := RealSequence.value at mulSequence(subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a))), subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a)))), n with *
  have yyReal := RealSequence.value at mulSequence(subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a))), subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a)))), n with *
  have function : u : ℕ → ℂ by exact sequence
  have member := FunctionBetween.apply_closed at u, ℕ, ℂ, n with *
  unfold complexDistanceSequence
  rw [addSequence.value, mulSequence.value, mulSequence.value, subSequence.value, subSequence.value, constantSequence.value, constantSequence.value, complexSequenceX.value, complexSequenceY.value, complexNormSquared.difference_coordinates]
  simp [realSubValue]

theorem ComplexConvergesTo.eventually_squared_distance (u a : Set) (e : Real)
  requires converges : ComplexConvergesTo(u, a)
  requires positive : R[0] < e
  shows ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n → complexNormSquared(ℂ[u(n) - a]) < e
proof
  have distanceLimit := complexDistanceSequence.converges_zero with *
  have distanceSequence := ConvergesTo.sequence at complexDistanceSequence(u, a), R[0] with *
  obtain ⟨N, natural, close⟩ := ConvergesTo.eventually at complexDistanceSequence(u, a), R[0], e with *
  rcases converges with ⟨sequence, member, horizontal, vertical⟩
  refine ⟨N, natural, ?_⟩
  intros n nIn after
  have nNat := nat.omega.backward at n with *
  have termReal := RealSequence.value with *
  have near := close with n, nIn, after
  have interval := openBall.order_characterization.forward with *
  have upper := interval.right
  rwa [realAddValue.zero_left, complexDistanceSequence.value] at upper

theorem ComplexConvergesTo.of_squared_distance (u a : Set)
  requires sequence : ComplexSequence(u)
  requires center : a ∈ ℂ
  requires close : ∀ e ∈ ℝ, R[0] < e → ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n → complexNormSquared(ℂ[u(n) - a]) < e
  shows ComplexConvergesTo(u, a)
proof
  have point := complex.point with center
  have horizontal := complexSequenceX.sequence with *
  have vertical := complexSequenceY.sequence with *
  have function : u : ℕ → ℂ by exact sequence
  have both : ∀ e ∈ ℝ, R[0] < e → ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n →
      complexSequenceX(u)(n) ∈ openBall(Euclidean.x(a), e) ∧ complexSequenceY(u)(n) ∈ openBall(Euclidean.y(a), e)
    intros e eIn positive
    have squarePositive := realMulValue.positive with *
    obtain ⟨N, natural, small⟩ := close with R[e * e], squarePositive
    refine ⟨N, natural, ?_⟩
    intros n nIn after
    have nNat := nat.omega.backward at n with *
    have member := FunctionBetween.apply_closed at u, ℕ, ℂ, n with *
    have distance := small with n, nIn, after
    have coordinates := complexNormSquared.small_coordinates with *
    rwa [complexSequenceX.value, complexSequenceY.value]
  unfold ComplexConvergesTo
  refine ⟨sequence, center, ?_⟩
  constructor
  . unfold ConvergesTo
    refine ⟨horizontal, ?_⟩
    intros e eIn positive
    obtain ⟨N, natural, closeBoth⟩ := both with e, eIn, positive
    refine ⟨N, natural, ?_⟩
    intros n nIn after
    have near := closeBoth with n, nIn, after
    exact near.left
  . unfold ConvergesTo
    refine ⟨vertical, ?_⟩
    intros e eIn positive
    obtain ⟨N, natural, closeBoth⟩ := both with e, eIn, positive
    refine ⟨N, natural, ?_⟩
    intros n nIn after
    have near := closeBoth with n, nIn, after
    exact near.right

theorem complexMappedSequence.sequence (f u : Set)
  requires function : f : ℂ → ℂ
  requires sequence : ComplexSequence(u)
  shows ComplexSequence(complexMappedSequence(f, u))
proof
  have uFunction : u : ℕ → ℂ by exact sequence
  unfold ComplexSequence
  unfold complexMappedSequence
  exact compose.function with *

theorem complexMappedSequence.value (f u : Set) (n : Nat)
  requires function : f : ℂ → ℂ
  requires sequence : ComplexSequence(u)
  shows complexMappedSequence(f, u)(n) = f(u(n))
proof
  have uFunction : u : ℕ → ℂ by exact sequence
  unfold complexMappedSequence
  exact compose.apply with *

theorem ComplexContinuousAt.converges (f u a : Set)
  requires continuous : ComplexContinuousAt(f, a)
  requires converges : ComplexConvergesTo(u, a)
  shows ComplexConvergesTo(complexMappedSequence(f, u), f(a))
proof
  have convergesAgain := converges
  rcases converges with ⟨sequence, center, horizontal, vertical⟩
  rcases continuous with ⟨function, centerAgain, local⟩
  have mapped := complexMappedSequence.sequence with *
  have image := FunctionBetween.apply_closed with *
  have uFunction : u : ℕ → ℂ by exact sequence
  apply ComplexConvergesTo.of_squared_distance with mapped, image
  intros e eIn positive
  obtain ⟨d, dIn, dPositive, nearImage⟩ := local with e, eIn, positive
  obtain ⟨N, natural, nearInput⟩ := ComplexConvergesTo.eventually_squared_distance at u, a, d with *
  refine ⟨N, natural, ?_⟩
  intros n nIn after
  have nNat := nat.omega.backward at n with *
  have member := FunctionBetween.apply_closed at u, ℕ, ℂ, n with *
  have near := nearInput with n, nIn, after
  rw complexMappedSequence.value
  exact nearImage with u(n), member, near

theorem complexPolynomial.converges (u a : Set) (cs : List(ℂ))
  requires converges : ComplexConvergesTo(u, a)
  shows ComplexConvergesTo(complexMappedSequence(complexPolynomial(cs), u), complexPolynomial(cs)(a))
proof
  have center : a ∈ ℂ
    rcases converges with ⟨sequence, center, horizontal, vertical⟩
    exact center
  have continuous := complexPolynomial.continuous_at with *
  exact ComplexContinuousAt.converges with *

theorem complexPolynomial.norm_converges (u a : Set) (cs : List(ℂ))
  requires converges : ComplexConvergesTo(u, a)
  shows ConvergesTo(complexNormSequence(complexMappedSequence(complexPolynomial(cs), u)), complexNormSquared(complexPolynomial(cs)(a)))
proof
  have mapped := complexPolynomial.converges with *
  exact ComplexConvergesTo.norm_squared with *

end Complexes