-- Subspaces of a metric space: the restricted metric, its balls as traces
-- of balls, open and closed sets, convergence and Cauchy sequences, closed
-- subspaces of complete spaces, restricted maps, and the inclusion isometry
-- 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.Subspace
import Discrete

def subspaceMetric (d S : Set) : Set := restrict(d, S × S)

theorem subspaceMetric.function (X d S : Set)
  requires metric : IsMetric(X, d)
  requires inside : S ⊆ X
  shows subspaceMetric(d, S) : S × S → ℝ
proof
  have function := IsMetric.function with metric
  have product := product.monotone with inside, inside
  unfold subspaceMetric
  exact restrict.domain_function with function, product

theorem subspaceMetric.apply (X d S x y : Set)
  requires metric : IsMetric(X, d)
  requires inside : S ⊆ X
  requires hx : x ∈ S
  requires hy : y ∈ S
  shows subspaceMetric(d, S)(x, y) = d(x, y)
proof
  have function := IsMetric.function with metric
  have product := product.monotone with inside, inside
  have pair := product.pair at x, y, S, S with hx, hy
  unfold call2
  unfold subspaceMetric
  exact restrict.domain_apply with function, product, pair

theorem subspaceMetric.metric (X d S : Set)
  requires metric : IsMetric(X, d)
  requires inside : S ⊆ X
  shows IsMetric(S, subspaceMetric(d, S))
proof
  constructor
  . exact subspaceMetric.function with metric, inside
  . constructor
    . intros x hx y hy
      have value := subspaceMetric.apply with metric, inside, hx, hy
      rw value
      exact IsMetric.nonnegative with metric, (inside with x, hx), (inside with
        y, hy)
    . constructor
      . intros x hx y hy
        have value := subspaceMetric.apply with metric, inside, hx, hy
        rw value
        exact IsMetric.eq_zero_iff with metric, (inside with x, hx),
          (inside with
          y, hy)
      . constructor
        . intros x hx y hy
          have valueXY := subspaceMetric.apply with metric, inside, hx, hy
          have valueYX := subspaceMetric.apply with metric, inside, hy, hx
          rw [valueXY, valueYX]
          exact IsMetric.symmetric with metric, (inside with x, hx),
            (inside with
            y, hy)
        . intros x hx y hy z hz
          have valueXZ := subspaceMetric.apply with metric, inside, hx, hz
          have valueXY := subspaceMetric.apply with metric, inside, hx, hy
          have valueYZ := subspaceMetric.apply with metric, inside, hy, hz
          rw [valueXZ, valueXY, valueYZ]
          exact IsMetric.triangle with metric, (inside with x, hx), (inside with
            y, hy),
            (inside with z, hz)

theorem subspaceMetric.whole (X d : Set)
  requires metric : IsMetric(X, d)
  shows subspaceMetric(d, X) = d
proof
  have function := IsMetric.function with metric
  have restricted := subspaceMetric.function with
    metric, (Subset.reflexive at X)
  apply FunctionBetween.ext with restricted, function
  intros p hp
  obtain ⟨bound, x, hx, y, hy, rfl⟩ := product.membership.forward with hp
  have value := subspaceMetric.apply with
    metric, (Subset.reflexive at X), hx, hy
  unfold call2 at value
  exact value

theorem subspaceMetric.nested (d S T : Set)
  requires inside : T ⊆ S
  shows subspaceMetric(subspaceMetric(d, S), T) = subspaceMetric(d, T)
proof
  have product := product.monotone with inside, inside
  unfold subspaceMetric
  exact restrict.nested with product

-- Balls of the subspace are traces of balls of the space.
theorem subspaceMetric.ball (X d S x : Set, r : Real)
  requires metric : IsMetric(X, d)
  requires inside : S ⊆ X
  requires hx : x ∈ S
  shows ball(S, subspaceMetric(d, S), x, r) = ball(X, d, x, r) ∩ S
proof
  ext y
  constructor
  . intro hy
    have hyS := ball.point with hy
    have near := ball.distance with hy
    have value := subspaceMetric.apply with metric, inside, hx, hyS
    rw value at near
    apply intersection.membership.backward
    exact ⟨(ball.of_distance with (inside with y, hyS), near), hyS⟩
  . intro hy
    have both := intersection.membership.forward with hy
    have near := ball.distance with both.left
    have value := subspaceMetric.apply with metric, inside, hx, both.right
    apply ball.of_distance with both.right
    rw value
    exact near

theorem subspaceMetric.closedBall (X d S x : Set, r : Real)
  requires metric : IsMetric(X, d)
  requires inside : S ⊆ X
  requires hx : x ∈ S
  shows closedBall(S, subspaceMetric(d, S), x, r) = closedBall(X, d, x, r) ∩ S
proof
  ext y
  constructor
  . intro hy
    have hyS := closedBall.point with hy
    have near := closedBall.distance with hy
    have value := subspaceMetric.apply with metric, inside, hx, hyS
    rw value at near
    apply intersection.membership.backward
    exact ⟨(closedBall.of_distance with (inside with y, hyS), near), hyS⟩
  . intro hy
    have both := intersection.membership.forward with hy
    have near := closedBall.distance with both.left
    have value := subspaceMetric.apply with metric, inside, hx, both.right
    apply closedBall.of_distance with both.right
    rw value
    exact near

theorem subspaceMetric.open_of_open (X d S U : Set)
  requires metric : IsMetric(X, d)
  requires inside : S ⊆ X
  requires open : MetricOpen(X, d, U)
  shows MetricOpen(S, subspaceMetric(d, S), U ∩ S)
proof
  constructor
  . exact intersection.subset_right at U, S
  . intros x hx
    have both := intersection.membership.forward with hx
    obtain ⟨r, hr, positive, ballInside⟩ :=
      MetricOpen.ball_inside with open, both.left
    refine ⟨r, hr, positive, ?_⟩
    have typedR : Real(r) by exact hr
    have trace := subspaceMetric.ball at X, d, S, x, r with
      metric, inside, both.right
    rw trace
    exact intersection.monotone_left with ballInside

theorem subspaceMetric.closed_of_closed (X d S C : Set)
  requires metric : IsMetric(X, d)
  requires inside : S ⊆ X
  requires closed : MetricClosed(X, d, C)
  shows MetricClosed(S, subspaceMetric(d, S), C ∩ S)
proof
  apply MetricClosed.of_ball_disjoint with (intersection.subset_right at C, S)
  intros x hx outside
  have hxX := inside with x, hx
  have away : ¬x ∈ C
    intro hxC
    apply outside
    exact intersection.membership.backward with ⟨hxC, hx⟩
  obtain ⟨r, hr, positive, disjoint⟩ :=
    MetricClosed.ball_disjoint with closed, hxX, away
  refine ⟨r, hr, positive, ?_⟩
  have typedR : Real(r) by exact hr
  have trace := subspaceMetric.ball at X, d, S, x, r with metric, inside, hx
  rw trace
  have separated := Disjoint.iff.forward with disjoint
  apply Disjoint.iff.backward
  intros y hy hyC
  have inBall := intersection.membership.forward with hy
  have inC := intersection.membership.forward with hyC
  exact separated with y, inBall.left, inC.left

-- Convergence and the Cauchy property are the same in the subspace.
theorem subspaceMetric.converges_iff (X d S u x : Set)
  requires metric : IsMetric(X, d)
  requires inside : S ⊆ X
  requires sequence : SequenceIn(S, u)
  requires hx : x ∈ S
  shows ConvergesIn(S, subspaceMetric(d, S), u, x) ↔ ConvergesIn(X, d, u, x)
proof
  have uFunction := SequenceIn.function with sequence
  have ambient : SequenceIn(X, u)
    have closed : ∀ n ∈ ℕ, u(n) ∈ X
      intros n hn
      exact inside with u(n), (SequenceIn.term_of_member with sequence, hn)
    exact FunctionBetween.codomain_of_values with uFunction, closed
  constructor
  . intro converges
    apply ConvergesIn.of_eventually with ambient, (inside with x, hx)
    intros ε hε positive
    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
    have value := subspaceMetric.apply with metric, inside, hx, term
    have close := near with n, hn, le
    rwa value at close
  . intro converges
    apply ConvergesIn.of_eventually with sequence, hx
    intros ε hε positive
    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
    have value := subspaceMetric.apply with metric, inside, hx, term
    rw value
    exact near with n, hn, le

theorem subspaceMetric.cauchy_iff (X d S u : Set)
  requires metric : IsMetric(X, d)
  requires inside : S ⊆ X
  requires sequence : SequenceIn(S, u)
  shows IsCauchy(S, subspaceMetric(d, S), u) ↔ IsCauchy(X, d, u)
proof
  have uFunction := SequenceIn.function with sequence
  have ambient : SequenceIn(X, u)
    have closed : ∀ n ∈ ℕ, u(n) ∈ X
      intros n hn
      exact inside with u(n), (SequenceIn.term_of_member with sequence, hn)
    exact FunctionBetween.codomain_of_values with uFunction, closed
  constructor
  . intro cauchy
    apply IsCauchy.of_eventually with ambient
    intros ε hε positive
    obtain ⟨N, hN, close⟩ := IsCauchy.eventually with cauchy, positive
    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 value := subspaceMetric.apply with metric, inside, termM, termN
    have near := close with m, hm, n, hn, leM, leN
    rwa value at near
  . intro cauchy
    apply IsCauchy.of_eventually with sequence
    intros ε hε positive
    obtain ⟨N, hN, close⟩ := IsCauchy.eventually with cauchy, positive
    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 value := subspaceMetric.apply with metric, inside, termM, termN
    rw value
    exact close with m, hm, n, hn, leM, leN

-- A closed subspace of a complete space is complete.
theorem IsComplete.closed_subspace (X d S : Set)
  requires complete : IsComplete(X, d)
  requires closed : MetricClosed(X, d, S)
  shows IsComplete(S, subspaceMetric(d, S))
proof
  have metric := IsComplete.metric with complete
  have inside := MetricClosed.subset with closed
  apply IsComplete.of_limits with (subspaceMetric.metric with metric, inside)
  intros u cauchy
  have sequence := IsCauchy.sequence with cauchy
  have bridge := subspaceMetric.cauchy_iff at X, d, S, u with
    metric, inside, sequence
  have ambient := bridge.forward with cauchy
  obtain ⟨x, hx, converges⟩ := IsComplete.limit with complete, ambient
  have terms : ∀ n ∈ ℕ, u(n) ∈ S
    intros n hn
    exact SequenceIn.term_of_member with sequence, hn
  have hxS := ConvergesIn.limit_in_closed with closed, terms, converges
  have same := subspaceMetric.converges_iff at X, d, S, u, x with
    metric, inside, sequence, hxS
  exact ⟨x, hxS, (same.backward with converges)⟩

theorem IsBounded.subspace (X d S T : Set)
  requires metric : IsMetric(X, d)
  requires inside : S ⊆ X
  requires bounded : IsBounded(X, d, T)
  requires hT : T ⊆ S
  shows IsBounded(S, subspaceMetric(d, S), T)
proof
  obtain ⟨insideT, r, hr, bound⟩ := bounded
  refine ⟨hT, r, hr, ?_⟩
  intros x hx y hy
  have value :=
    subspaceMetric.apply with metric, inside, (hT with x, hx), (hT with y, hy)
  rw value
  exact bound with x, hx, y, hy

-- Restricting a continuous map to a subspace keeps it continuous.
theorem IsMetricContinuous.restrict (f X d Y e S : Set)
  requires metric : IsMetric(X, d)
  requires inside : S ⊆ X
  requires continuous : IsMetricContinuous(f, X, d, Y, e)
  shows IsMetricContinuous(restrict(f, S), S, subspaceMetric(d, S), Y, e)
proof
  have function := IsMetricContinuous.function with continuous
  have restricted := restrict.domain_function with function, inside
  apply IsMetricContinuous.of_pointwise with restricted
  intros x hx
  have hxX := inside with x, hx
  have atX := IsMetricContinuous.at with continuous, hxX
  apply MetricContinuousAt.of_control with restricted, hx
  intros ε hε positive
  obtain ⟨δ, hδ, positiveD, maps⟩ :=
    MetricContinuousAt.control with atX, positive
  refine ⟨δ, hδ, positiveD, ?_⟩
  intros y hy near
  have valueX := restrict.domain_apply with function, inside, hx
  have valueY := restrict.domain_apply with function, inside, hy
  have distance := subspaceMetric.apply with metric, inside, hx, hy
  rw distance at near
  rw [valueX, valueY]
  exact maps with y, (inside with y, hy), near

theorem inclusionMap.isometry (X d S : Set)
  requires metric : IsMetric(X, d)
  requires inside : S ⊆ X
  shows IsIsometry(inclusionMap(S, X), S, subspaceMetric(d, S), X, d)
proof
  have function := inclusionMap.function at S, X with inside
  constructor
  . exact function
  . intros x hx y hy
    have valueX := inclusionMap.value at S, X, x with inside, hx
    have valueY := inclusionMap.value at S, X, y with inside, hy
    rw [valueX, valueY]
    have value := subspaceMetric.apply with metric, inside, hx, hy
    symm at value
    exact value

theorem inclusionMap.metric_continuous (X d S : Set)
  requires metric : IsMetric(X, d)
  requires inside : S ⊆ X
  shows IsMetricContinuous(inclusionMap(S, X), S, subspaceMetric(d, S), X, d)
proof
  exact IsIsometry.continuous with (inclusionMap.isometry with metric, inside)