-- Continuity between metric spaces: the ε–δ definition, its equivalence
-- with topological continuity for the metric topologies, composition,
-- Lipschitz maps, and isometries
-- 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.Continuity
import Closed

predicate MetricContinuousAt (f X d Y e x : Set) :=
  FunctionBetween(f, X, Y) ∧ x ∈ X ∧
  (∀ ε ∈ ℝ, 0 < ε → ∃ δ ∈ ℝ, 0 < δ ∧
    ∀ y ∈ X, (d(x, y) < δ → e(f(x), f(y)) < ε))

predicate IsMetricContinuous (f X d Y e : Set) :=
  FunctionBetween(f, X, Y) ∧ (∀ x ∈ X, MetricContinuousAt(f, X, d, Y, e, x))

theorem MetricContinuousAt.function (f X d Y e x : Set)
  requires continuous : MetricContinuousAt(f, X, d, Y, e, x)
  shows f : X → Y
proof
  exact continuous.left

theorem MetricContinuousAt.point (f X d Y e x : Set)
  requires continuous : MetricContinuousAt(f, X, d, Y, e, x)
  shows x ∈ X
proof
  obtain ⟨function, hx, control⟩ := continuous
  exact hx

theorem MetricContinuousAt.control (f X d Y e x : Set, ε : Real)
  requires continuous : MetricContinuousAt(f, X, d, Y, e, x)
  requires positive : 0 < ε
  shows ∃ δ ∈ ℝ, 0 < δ ∧ ∀ y ∈ X, (d(x, y) < δ → e(f(x), f(y)) < ε)
proof
  obtain ⟨function, hx, control⟩ := continuous
  have realE : ε ∈ ℝ by typecheck
  exact control with ε, realE, positive

theorem MetricContinuousAt.of_control (f X d Y e x : Set)
  requires function : f : X → Y
  requires hx : x ∈ X
  requires control : ∀ ε ∈ ℝ, 0 < ε → ∃ δ ∈ ℝ, 0 < δ ∧
    ∀ y ∈ X, (d(x, y) < δ → e(f(x), f(y)) < ε)
  shows MetricContinuousAt(f, X, d, Y, e, x)
proof
  exact ⟨function, hx, control⟩

-- Continuity at a point in terms of balls: a small ball around x is mapped
-- into any given ball around f(x).
theorem MetricContinuousAt.ball (f X d Y e x : Set, ε : Real)
  requires continuous : MetricContinuousAt(f, X, d, Y, e, x)
  requires positive : 0 < ε
  shows ∃ δ ∈ ℝ, 0 < δ ∧
    ball(X, d, x, δ) ⊆ functionPreimage(f, X, ball(Y, e, f(x), ε))
proof
  have function := MetricContinuousAt.function with continuous
  obtain ⟨δ, hδ, positiveD, maps⟩ :=
    MetricContinuousAt.control with continuous, positive
  refine ⟨δ, hδ, positiveD, ?_⟩
  intros y hy
  have hyX := ball.point with hy
  have near := ball.distance with hy
  have value := FunctionBetween.apply_closed with function, hyX
  have close := maps with y, hyX, near
  apply functionPreimage.membership.backward
  exact ⟨hyX, (ball.of_distance with value, close)⟩

theorem MetricContinuousAt.of_ball (f X d Y e x : Set)
  requires function : f : X → Y
  requires hx : x ∈ X
  requires maps : ∀ ε ∈ ℝ, 0 < ε → ∃ δ ∈ ℝ, 0 < δ ∧
    ball(X, d, x, δ) ⊆ functionPreimage(f, X, ball(Y, e, f(x), ε))
  shows MetricContinuousAt(f, X, d, Y, e, x)
proof
  apply MetricContinuousAt.of_control with function, hx
  intros ε hε positive
  obtain ⟨δ, hδ, positiveD, inside⟩ := maps with ε, hε, positive
  refine ⟨δ, hδ, positiveD, ?_⟩
  intros y hy near
  have member := inside with y, (ball.of_distance with hy, near)
  have parts := functionPreimage.membership.forward with member
  exact ball.distance with parts.right

theorem IsMetricContinuous.function (f X d Y e : Set)
  requires continuous : IsMetricContinuous(f, X, d, Y, e)
  shows f : X → Y
proof
  exact continuous.left

theorem IsMetricContinuous.at (f X d Y e x : Set)
  requires continuous : IsMetricContinuous(f, X, d, Y, e)
  requires hx : x ∈ X
  shows MetricContinuousAt(f, X, d, Y, e, x)
proof
  exact continuous.right with x, hx

theorem IsMetricContinuous.of_pointwise (f X d Y e : Set)
  requires function : f : X → Y
  requires pointwise : ∀ x ∈ X, MetricContinuousAt(f, X, d, Y, e, x)
  shows IsMetricContinuous(f, X, d, Y, e)
proof
  exact ⟨function, pointwise⟩

theorem identity.metric_continuous_at (X d x : Set)
  requires hx : x ∈ X
  shows MetricContinuousAt(identity(X), X, d, X, d, x)
proof
  have function := identity.function at X
  apply MetricContinuousAt.of_control with function, hx
  intros ε hε positive
  refine ⟨ε, hε, positive, ?_⟩
  intros y hy near
  have fixedX := identity.apply with hx
  have fixedY := identity.apply with hy
  rwa [fixedX, fixedY]

theorem identity.metric_continuous (X d : Set)
  shows IsMetricContinuous(identity(X), X, d, X, d)
proof
  apply IsMetricContinuous.of_pointwise with (identity.function at X)
  intros x hx
  exact identity.metric_continuous_at with hx

theorem constantFunction.metric_continuous_at (X d Y e x c : Set)
  requires metric : IsMetric(Y, e)
  requires hx : x ∈ X
  requires hc : c ∈ Y
  shows MetricContinuousAt(constantFunction(X, Y, c), X, d, Y, e, x)
proof
  have function := constantFunction.function at X, Y, c with hc
  apply MetricContinuousAt.of_control with function, hx
  intros ε hε positive
  refine ⟨ε, hε, positive, ?_⟩
  intros y hy near
  have valueX := constantFunction.apply with hx, hc
  have valueY := constantFunction.apply with hy, hc
  rw [valueX, valueY]
  have self := IsMetric.self with metric, hc
  rw self
  exact positive

theorem constantFunction.metric_continuous (X d Y e c : Set)
  requires metric : IsMetric(Y, e)
  requires hc : c ∈ Y
  shows IsMetricContinuous(constantFunction(X, Y, c), X, d, Y, e)
proof
  have function := constantFunction.function at X, Y, c with hc
  apply IsMetricContinuous.of_pointwise with function
  intros x hx
  exact constantFunction.metric_continuous_at with metric, hx, hc

theorem MetricContinuousAt.compose (g f X d Y e Z k x : Set)
  requires first : MetricContinuousAt(f, X, d, Y, e, x)
  requires second : MetricContinuousAt(g, Y, e, Z, k, f(x))
  shows MetricContinuousAt(compose(g, f, X, Y, Z), X, d, Z, k, x)
proof
  have fFunction := MetricContinuousAt.function with first
  have gFunction := MetricContinuousAt.function with second
  have hx := MetricContinuousAt.point with first
  have composite := compose.function with fFunction, gFunction
  apply MetricContinuousAt.of_control with composite, hx
  intros ε hε positive
  obtain ⟨η, hη, positiveH, mapsG⟩ :=
    MetricContinuousAt.control with second, positive
  obtain ⟨δ, hδ, positiveD, mapsF⟩ :=
    MetricContinuousAt.control with first, positiveH
  refine ⟨δ, hδ, positiveD, ?_⟩
  intros y hy near
  have valueX := compose.apply with fFunction, gFunction, hx
  have valueY := compose.apply with fFunction, gFunction, hy
  rw [valueX, valueY]
  have middle := mapsF with y, hy, near
  have imageY := FunctionBetween.apply_closed with fFunction, hy
  exact mapsG with f(y), imageY, middle

theorem IsMetricContinuous.compose (g f X d Y e Z k : Set)
  requires first : IsMetricContinuous(f, X, d, Y, e)
  requires second : IsMetricContinuous(g, Y, e, Z, k)
  shows IsMetricContinuous(compose(g, f, X, Y, Z), X, d, Z, k)
proof
  have fFunction := IsMetricContinuous.function with first
  have gFunction := IsMetricContinuous.function with second
  apply IsMetricContinuous.of_pointwise with (compose.function with
    fFunction, gFunction)
  intros x hx
  have image := FunctionBetween.apply_closed with fFunction, hx
  have atX := IsMetricContinuous.at with first, hx
  have atImage := IsMetricContinuous.at with second, image
  exact MetricContinuousAt.compose with atX, atImage

-- ε–δ continuity is continuity for the metric topologies.
theorem IsMetricContinuous.continuous_map (f X d Y e : Set)
  requires metricD : IsMetric(X, d)
  requires metricE : IsMetric(Y, e)
  requires continuous : IsMetricContinuous(f, X, d, Y, e)
  shows ContinuousMap(f, X, metricTopology(X, d), Y, metricTopology(Y, e))
proof
  have function := IsMetricContinuous.function with continuous
  constructor
  . exact function
  . intros V hV
    apply metricTopology.of_open
    constructor
    . exact functionPreimage.subset at f, X, V
    . intros x hx
      have parts := functionPreimage.membership.forward with hx
      obtain ⟨ε, hε, positive, ballInside⟩ :=
        metricTopology.ball_inside with hV, parts.right
      have atX := IsMetricContinuous.at with continuous, parts.left
      obtain ⟨δ, hδ, positiveD, maps⟩ :=
        MetricContinuousAt.ball with atX, positive
      refine ⟨δ, hδ, positiveD, ?_⟩
      intros y hy
      have preimage := functionPreimage.membership.forward with (maps with
        y, hy)
      apply functionPreimage.membership.backward
      exact ⟨preimage.left, (ballInside with f(y), preimage.right)⟩

theorem ContinuousMap.metric_continuous (f X d Y e : Set)
  requires metricD : IsMetric(X, d)
  requires metricE : IsMetric(Y, e)
  requires continuous :
    ContinuousMap(f, X, metricTopology(X, d), Y, metricTopology(Y, e))
  shows IsMetricContinuous(f, X, d, Y, e)
proof
  have function := ContinuousMap.function with continuous
  apply IsMetricContinuous.of_pointwise with function
  intros x hx
  apply MetricContinuousAt.of_ball with function, hx
  intros ε hε positive
  have image := FunctionBetween.apply_closed with function, hx
  have openBall := ball.member_topology at Y, e, f(x), ε with metricE, image
  have preimageOpen := ContinuousMap.preimage with continuous, openBall
  have center := ball.center with metricE, image, positive
  have inPreimage : x ∈ functionPreimage(f, X, ball(Y, e, f(x), ε)) :=
    functionPreimage.membership.backward with ⟨hx, center⟩
  exact metricTopology.ball_inside with preimageOpen, inPreimage

theorem IsMetricContinuous.iff_continuous_map (f X d Y e : Set)
  requires metricD : IsMetric(X, d)
  requires metricE : IsMetric(Y, e)
  shows IsMetricContinuous(f, X, d, Y, e) ↔
    ContinuousMap(f, X, metricTopology(X, d), Y, metricTopology(Y, e))
proof
  constructor
  . intro continuous
    exact IsMetricContinuous.continuous_map with metricD, metricE, continuous
  . intro continuous
    exact ContinuousMap.metric_continuous with metricD, metricE, continuous

-- Lipschitz maps

predicate IsLipschitz (f X d Y e : Set) (K : Real) :=
  FunctionBetween(f, X, Y) ∧ 0 ≤ K ∧
  (∀ x ∈ X, ∀ y ∈ X, e(f(x), f(y)) ≤ realMul(K, d(x, y)))

theorem IsLipschitz.function (f X d Y e : Set) (K : Real)
  requires lipschitz : IsLipschitz(f, X, d, Y, e, K)
  shows f : X → Y
proof
  exact lipschitz.left

theorem IsLipschitz.nonnegative (f X d Y e : Set) (K : Real)
  requires lipschitz : IsLipschitz(f, X, d, Y, e, K)
  shows 0 ≤ K
proof
  obtain ⟨function, nonnegative, bound⟩ := lipschitz
  exact nonnegative

theorem IsLipschitz.bound (f X d Y e x y : Set) (K : Real)
  requires lipschitz : IsLipschitz(f, X, d, Y, e, K)
  requires hx : x ∈ X
  requires hy : y ∈ X
  shows e(f(x), f(y)) ≤ realMul(K, d(x, y))
proof
  obtain ⟨function, nonnegative, bound⟩ := lipschitz
  exact bound with x, hx, y, hy

-- The modulus ε / (K + 1) works for every Lipschitz constant K ≥ 0.
theorem Lipschitz.modulus (K ε : Real)
  requires nonnegative : 0 ≤ K
  requires positive : 0 < ε
  shows 0 < ε / (K + 1) ∧ K * (ε / (K + 1)) < ε
proof
  have successorPositive : (0:R) < K + 1 by linarith
  have nonzero : K + 1 ≠ 0
    intro zero
    rw zero at successorPositive
    exact realLess.not_self with successorPositive
  have quotientReal := realDiv.real at ε, K + 1 with *
  have cancel := realDiv.mul_left at ε, K + 1 with *{2}, nonzero
  have inversePositive := realInvValue.positive with successorPositive
  have inverseReal := realInvValue.real at K + 1
  have asProduct := realDiv.eq_mul_inv at ε, K + 1 with *
  have quotientPositive : 0 < ε / (K + 1)
    rw asProduct
    exact realMulValue.positive with positive, inversePositive
  constructor
  . exact quotientPositive
  . have expand : K * (ε / (K + 1)) = ε - ε / (K + 1) by
      linear_combination cancel
    rw expand
    linarith

theorem IsLipschitz.continuous_at (f X d Y e x : Set) (K : Real)
  requires metricD : IsMetric(X, d)
  requires metricE : IsMetric(Y, e)
  requires lipschitz : IsLipschitz(f, X, d, Y, e, K)
  requires hx : x ∈ X
  shows MetricContinuousAt(f, X, d, Y, e, x)
proof
  have function := IsLipschitz.function with lipschitz
  have imageX := FunctionBetween.apply_closed with function, hx
  have nonnegative := IsLipschitz.nonnegative with lipschitz
  apply MetricContinuousAt.of_control with function, hx
  intros ε hε positive
  obtain ⟨positiveD, small⟩ := Lipschitz.modulus with nonnegative, positive
  have quotientReal : ε / (K + 1) ∈ ℝ by typecheck
  refine ⟨ε / (K + 1), quotientReal, positiveD, ?_⟩
  intros y hy near
  have bound := IsLipschitz.bound with lipschitz, hx, hy
  have imageY := FunctionBetween.apply_closed with function, hy
  have dxy := IsMetric.real with metricD, hx, hy
  have exy := IsMetric.real with metricE, imageX, imageY
  have le := realLess.implies_le with near
  have scaled := realLe.mul_left_of_nonnegative with le, nonnegative
  linarith

theorem IsLipschitz.continuous (f X d Y e : Set) (K : Real)
  requires metricD : IsMetric(X, d)
  requires metricE : IsMetric(Y, e)
  requires lipschitz : IsLipschitz(f, X, d, Y, e, K)
  shows IsMetricContinuous(f, X, d, Y, e)
proof
  apply IsMetricContinuous.of_pointwise with (IsLipschitz.function with lipschitz)
  intros x hx
  exact IsLipschitz.continuous_at with metricD, metricE, lipschitz, hx

theorem IsLipschitz.identity (X d : Set)
  requires metric : IsMetric(X, d)
  shows IsLipschitz(identity(X), X, d, X, d, (1:R))
proof
  have one : (0:R) ≤ 1 by linarith
  unfold IsLipschitz
  constructor
  . exact identity.function at X
  . constructor
    . exact one
    . intros x hx y hy
      have fixedX := identity.apply with hx
      have fixedY := identity.apply with hy
      have dxy := IsMetric.real with metric, hx, hy
      have unit := realMulValue.one_left at d(x, y)
      rw [fixedX, fixedY, unit]
      exact realLe.reflexive

theorem IsLipschitz.constant (X d Y e c : Set)
  requires metricD : IsMetric(X, d)
  requires metricE : IsMetric(Y, e)
  requires hc : c ∈ Y
  shows IsLipschitz(constantFunction(X, Y, c), X, d, Y, e, (0:R))
proof
  have zero : (0:R) ≤ 0 by linarith
  unfold IsLipschitz
  constructor
  . exact constantFunction.function at X, Y, c with hc
  . constructor
    . exact zero
    . intros x hx y hy
      have valueX := constantFunction.apply with hx, hc
      have valueY := constantFunction.apply with hy, hc
      have dxy := IsMetric.real with metricD, hx, hy
      have self := IsMetric.self with metricE, hc
      have annihilate := realMulValue.zero_left at d(x, y)
      rw [valueX, valueY, self, annihilate]
      exact realLe.reflexive

theorem IsLipschitz.compose (g f X d Y e Z k : Set) (K L : Real)
  requires metricD : IsMetric(X, d)
  requires metricE : IsMetric(Y, e)
  requires metricK : IsMetric(Z, k)
  requires first : IsLipschitz(f, X, d, Y, e, K)
  requires second : IsLipschitz(g, Y, e, Z, k, L)
  shows IsLipschitz(compose(g, f, X, Y, Z), X, d, Z, k, L * K)
proof
  have fFunction := IsLipschitz.function with first
  have gFunction := IsLipschitz.function with second
  have nonnegativeK := IsLipschitz.nonnegative with first
  have nonnegativeL := IsLipschitz.nonnegative with second
  have product := realMulValue.nonnegative with nonnegativeL, nonnegativeK
  unfold IsLipschitz
  constructor
  . exact compose.function with fFunction, gFunction
  . constructor
    . exact product
    . intros x hx y hy
      have valueX := compose.apply with fFunction, gFunction, hx
      have valueY := compose.apply with fFunction, gFunction, hy
      rw [valueX, valueY]
      have imageX := FunctionBetween.apply_closed with fFunction, hx
      have imageY := FunctionBetween.apply_closed with fFunction, hy
      have inner := IsLipschitz.bound with first, hx, hy
      have outer := IsLipschitz.bound with second, imageX, imageY
      have dxy := IsMetric.real with metricD, hx, hy
      have exy := IsMetric.real with metricE, imageX, imageY
      have outerX := FunctionBetween.apply_closed with gFunction, imageX
      have outerY := FunctionBetween.apply_closed with gFunction, imageY
      have kxy := IsMetric.real with metricK, outerX, outerY
      have scaled := realLe.mul_left_of_nonnegative with inner, nonnegativeL
      have regroup : L * (K * d(x, y)) = (L * K) * d(x, y) by ring
      rw regroup at scaled
      linarith

-- Isometries

predicate IsIsometry (f X d Y e : Set) :=
  FunctionBetween(f, X, Y) ∧ (∀ x ∈ X, ∀ y ∈ X, e(f(x), f(y)) = d(x, y))

theorem IsIsometry.function (f X d Y e : Set)
  requires isometry : IsIsometry(f, X, d, Y, e)
  shows f : X → Y
proof
  exact isometry.left

theorem IsIsometry.distance (f X d Y e x y : Set)
  requires isometry : IsIsometry(f, X, d, Y, e)
  requires hx : x ∈ X
  requires hy : y ∈ X
  shows e(f(x), f(y)) = d(x, y)
proof
  exact isometry.right with x, hx, y, hy

theorem IsIsometry.lipschitz (f X d Y e : Set)
  requires metric : IsMetric(X, d)
  requires isometry : IsIsometry(f, X, d, Y, e)
  shows IsLipschitz(f, X, d, Y, e, (1:R))
proof
  have one : (0:R) ≤ 1 by linarith
  unfold IsLipschitz
  constructor
  . exact IsIsometry.function with isometry
  . constructor
    . exact one
    . intros x hx y hy
      have preserved := IsIsometry.distance with isometry, hx, hy
      have dxy := IsMetric.real with metric, hx, hy
      have unit := realMulValue.one_left at d(x, y)
      rw [preserved, unit]
      exact realLe.reflexive

theorem IsIsometry.continuous_at (f X d Y e x : Set)
  requires isometry : IsIsometry(f, X, d, Y, e)
  requires hx : x ∈ X
  shows MetricContinuousAt(f, X, d, Y, e, x)
proof
  have function := IsIsometry.function with isometry
  apply MetricContinuousAt.of_control with function, hx
  intros ε hε positive
  refine ⟨ε, hε, positive, ?_⟩
  intros y hy near
  have preserved := IsIsometry.distance with isometry, hx, hy
  rwa preserved

theorem IsIsometry.continuous (f X d Y e : Set)
  requires isometry : IsIsometry(f, X, d, Y, e)
  shows IsMetricContinuous(f, X, d, Y, e)
proof
  apply IsMetricContinuous.of_pointwise with (IsIsometry.function with isometry)
  intros x hx
  exact IsIsometry.continuous_at with isometry, hx

theorem IsIsometry.injective (f X d Y e : Set)
  requires metricD : IsMetric(X, d)
  requires metricE : IsMetric(Y, e)
  requires isometry : IsIsometry(f, X, d, Y, e)
  shows InjectiveBetween(f, X, Y)
proof
  have function := IsIsometry.function with isometry
  constructor
  . exact function
  . intros x hx y hy z hz first second
    have valueX := FunctionBetween.apply_value with function, hx, first
    have valueY := FunctionBetween.apply_value with function, hy, second
    have preserved := IsIsometry.distance with isometry, hx, hy
    have self := IsMetric.self with metricE, hz
    have zero : d(x, y) = (0:R)
      rw ← preserved
      rw [valueX, valueY]
      exact self
    exact IsMetric.eq_of_zero with metricD, hx, hy, zero

theorem IsIsometry.compose (g f X d Y e Z k : Set)
  requires first : IsIsometry(f, X, d, Y, e)
  requires second : IsIsometry(g, Y, e, Z, k)
  shows IsIsometry(compose(g, f, X, Y, Z), X, d, Z, k)
proof
  have fFunction := IsIsometry.function with first
  have gFunction := IsIsometry.function with second
  refine ⟨(compose.function with fFunction, gFunction), ?_⟩
  intros x hx y hy
  have valueX := compose.apply with fFunction, gFunction, hx
  have valueY := compose.apply with fFunction, gFunction, hy
  rw [valueX, valueY]
  have imageX := FunctionBetween.apply_closed with fFunction, hx
  have imageY := FunctionBetween.apply_closed with fFunction, hy
  have inner := IsIsometry.distance with first, hx, hy
  have outer := IsIsometry.distance with second, imageX, imageY
  rw outer
  exact inner

theorem identity.isometry (X d : Set)
  shows IsIsometry(identity(X), X, d, X, d)
proof
  refine ⟨(identity.function at X), ?_⟩
  intros x hx y hy
  have fixedX := identity.apply with hx
  have fixedY := identity.apply with hy
  rw [fixedX, fixedY]
  rfl

-- An isometry maps a ball onto the ball of the image inside the image.
theorem IsIsometry.ball_image (f X d Y e x y : Set, r : Real)
  requires isometry : IsIsometry(f, X, d, Y, e)
  requires hx : x ∈ X
  requires hy : y ∈ X
  shows y ∈ ball(X, d, x, r) ↔ f(y) ∈ ball(Y, e, f(x), r)
proof
  have function := IsIsometry.function with isometry
  have preserved := IsIsometry.distance with isometry, hx, hy
  have image := FunctionBetween.apply_closed with function, hy
  constructor
  . intro member
    have near := ball.distance with member
    apply ball.of_distance with image
    rwa preserved
  . intro member
    have near := ball.distance with member
    apply ball.of_distance with hy
    rwa preserved at near