-- Squared-modulus epsilon/delta continuity over the concrete complex field.
-- 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.Continuity
import PolynomialBounds
import Real.Analysis.Continuity

-- Positive thresholds for squared distances describe the usual complex topology.
predicate ComplexContinuousAt (f a : Set) :=
  FunctionBetween(f, complexCarrier, complexCarrier) ∧ a ∈ complexCarrier ∧
  (∀ e ∈ ℝ, realZero < e → ∃ d ∈ ℝ, realZero < d ∧
    (∀ x ∈ complexCarrier,
      complexNormSquared(complexAdd(x, complexNeg(a))) < d →
      complexNormSquared(complexAdd(f(x), complexNeg(f(a)))) < e))

predicate ComplexContinuous (f : Set) :=
  FunctionBetween(f, complexCarrier, complexCarrier) ∧
  (∀ a ∈ complexCarrier, ComplexContinuousAt(f, a))

-- A bounded nonnegative factor can be absorbed into an explicit epsilon radius.
theorem scaledRadius.product_control (e b t : Real)
  requires epsilon : 0 < e
  requires nonnegative : 0 ≤ t
  requires small : t < scaledRadius(e, limitScale(b))
  shows t * b < e
proof
  have scalePositive := limitScale.positive at b with *
  have upper := abs.upper at b with *
  have larger := abs.lt_limitScale at b with *
  have bLess := realLe.transitive_less at b, abs(b), limitScale(b) with *
  have bLe := realLess.implies_le at b, limitScale(b) with *
  have comparison := realLe.mul_left_of_nonnegative at b, limitScale(b), t with *
  have multiplied := realLess.mul_right_of_positive at t, scaledRadius(e, limitScale(b)), limitScale(b) with *
  have commuted := realMulValue.commutative at scaledRadius(e, limitScale(b)), limitScale(b) with *
  have cancel := scaledRadius.cancel at e, limitScale(b) with *
  rw [commuted, cancel] at multiplied
  have halfLess := half.lt_self at e with *
  have belowHalf := realLe.transitive_less at t * b, t * limitScale(b), half(e) with *
  exact realLess.transitive with *

def complexNeighborhoodRadius (a : Euclidean.Point) : Real :=
  (2:R) * (complexNormSquared(a) + realOne)

theorem complexNeighborhoodRadius.nonnegative (a : Set)
  requires center : a ∈ complexCarrier
  shows realZero ≤ complexNeighborhoodRadius(a)
proof
  have point := complex.point with center
  have normNonnegative := complexNormSquared.nonnegative with center
  have oneNonnegative := realLess.implies_le with realZero.real, realOne.real, realZero.lt_one
  unfold complexNeighborhoodRadius
  exact realLe.two_sum_nonnegative with *

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

theorem complexNormSquared.difference_distance (z w : Set)
  requires first : z ∈ ℂ
  requires second : w ∈ ℂ
  shows complexNormSquared(ℂ[z - w]) = Euclidean.distanceSquared(z, w)
proof
  obtain ⟨a, aReal, b, bReal, zPair⟩ := complexCarrier.cases at z with *
  obtain ⟨c, cReal, d, dReal, wPair⟩ := complexCarrier.cases at w with *
  have firstPoint := Euclidean.pair.point at a, b with *
  have secondPoint := Euclidean.pair.point at c, d with *
  rw [zPair, wPair]
  simp [complexAdd.pair, complexNeg.pair, complexNormSquared.pair, Euclidean.distanceSquared.coordinates, Euclidean.x.pair, Euclidean.y.pair]
  ring

theorem complexNormSquared.nearby_disk (a x : Set)
  requires center : a ∈ ℂ
  requires element : x ∈ ℂ
  requires near : complexNormSquared(ℂ[x - a]) < R[1]
  shows complexNormSquared(x) ≤ complexNeighborhoodRadius(a)
proof
  have field := complexes.is_field
  have ring := IsField.comm_ring with field
  have ordinary := IsCommRing.ring with ring
  have negated := IsRing.neg_closed with ordinary, center
  have displacement := IsRing.add_closed with ordinary, element, negated
  have bound := realLess.implies_le with *
  have addition := complexNormSquared.add_bound at a, ℂ[x - a] with *
  have sum : ℂ[a + (x - a)] = x by ring
  rw sum at addition
  have translated := realLe.add_left at complexNormSquared(ℂ[x - a]), realOne, complexNormSquared(a) with *
  have doubled := realLe.double_bound with bound
  unfold complexNeighborhoodRadius
  exact realLe.transitive with *

theorem complexPolynomial.cons_continuous_at (a c : Set) (cs : List(complexCarrier))
  requires center : a ∈ ℂ
  requires coefficient : c ∈ ℂ
  shows ComplexContinuousAt(complexPolynomial(c :: cs), a)
proof
  have function := complexPolynomial.function at c :: cs with *
  have point := complex.point with center
  have radiusNonnegative := complexNeighborhoodRadius.nonnegative with center
  obtain ⟨b, bIn, bNonnegative, estimate⟩ := complexPolynomial.difference_bound_on_disk at a, c, complexNeighborhoodRadius(a), cs with *
  unfold ComplexContinuousAt
  refine ⟨function, center, ?_⟩
  intros e eIn epsilon
  have scalePositive := limitScale.positive at b with *
  have scaledPositive := scaledRadius.positive at e, limitScale(b) with *
  have unitPositive := realZero.lt_one
  obtain ⟨d, dIn, dPositive, dUnit, dScaled⟩ := positiveRadius.common at realOne, scaledRadius(e, limitScale(b)) with *
  refine ⟨d, dIn, dPositive, ?_⟩
  intros x member close
  have field := complexes.is_field
  have ring := IsField.comm_ring with field
  have ordinary := IsCommRing.ring with ring
  have negated := IsRing.neg_closed with ordinary, center
  have displacement := IsRing.add_closed with ordinary, member, negated
  have displacementNonnegative := complexNormSquared.nonnegative with displacement
  have near := realLess.transitive_le at complexNormSquared(ℂ[x - a]), d, realOne with *
  have inside := complexNormSquared.nearby_disk with *
  have bound := estimate with x, member, inside
  have small := realLess.transitive_le at complexNormSquared(ℂ[x - a]), d, scaledRadius(e, limitScale(b)) with *
  have controlled := scaledRadius.product_control with epsilon, small
  have imageX := FunctionBetween.apply_closed at complexPolynomial(c :: cs), complexCarrier, complexCarrier, x with *
  have imageA := FunctionBetween.apply_closed at complexPolynomial(c :: cs), complexCarrier, complexCarrier, a with *
  have negImage := IsRing.neg_closed with ordinary, imageA
  have imageDifference := IsRing.add_closed with ordinary, imageX, negImage
  exact realLe.transitive_less with *

theorem complexFunction.constant_continuous_at (f a z : Set)
  requires function : f : ℂ → ℂ
  requires center : a ∈ ℂ
  requires value : z ∈ ℂ
  requires constant : ∀ x ∈ ℂ, f(x) = z
  shows ComplexContinuousAt(f, a)
proof
  unfold ComplexContinuousAt
  refine ⟨function, center, ?_⟩
  intros e eIn epsilon
  have unitIn : realOne ∈ ℝ by typecheck
  refine ⟨realOne, unitIn, realZero.lt_one, ?_⟩
  intros x member close
  have xValue := constant with x, member
  have aValue := constant with a, center
  rw [xValue, aValue]
  have field := complexes.is_field
  have ring := IsField.comm_ring with field
  have cancel : ℂ[z - z] = ℂ[0] by ring
  rwa [cancel, complexNormSquared.zero]

theorem complexPolynomial.continuous_at (a : Set) (cs : List(complexCarrier))
  requires center : a ∈ ℂ
  shows ComplexContinuousAt(complexPolynomial(cs), a)
proof
  have shape := List.cases with *
  cases shape with emptyShape | nonemptyShape
  . rw emptyShape
    have empty : List(complexCarrier, []) by typecheck
    have function := complexPolynomial.function at [] with *
    have field := complexes.is_field
    have ring := IsField.comm_ring with field
    have unit : ℂ[1] ∈ ℂ by typecheck
    have constant : ∀ x ∈ ℂ, complexPolynomial([])(x) = ℂ[1]
      intros x member
      rw [complexPolynomial.value, monicValue]
      rfl
    exact complexFunction.constant_continuous_at with *
  . obtain ⟨c, coefficient, tail, list, consShape⟩ := nonemptyShape
    rw consShape
    exact complexPolynomial.cons_continuous_at with *

theorem complexPolynomial.continuous (cs : List(complexCarrier))
  shows ComplexContinuous(complexPolynomial(cs))
proof
  have function := complexPolynomial.function at cs with *
  unfold ComplexContinuous
  refine ⟨function, ?_⟩
  intros a center
  exact complexPolynomial.continuous_at with *

end Complexes