Counting transfer definition Erdos9796Counting_MEC_Basic

/- Generated by exact skeleton subtraction from Erdos9796Proof.P97.MEC.Basic; source SHA-256 f35255a6cfd027e89b35fa964269c5605d4561cdb60521d52519bc6fdf726fc4 -/
import Definitions.Def_Erdos9796Counting_Adapter
import Mathlib.Geometry.Euclidean.Sphere.Basic
import Mathlib.Geometry.Euclidean.Triangle
import Mathlib.Topology.MetricSpace.ProperSpace
import Mathlib.Topology.Order.Lattice


/-!
# Minimum enclosing circle (Welzl 1991 / Sylvester 1857)

For every nonempty finite point set `A ⊆ ℝ²` we prove that there exists
a **unique** minimum enclosing circle: a centre `c ∈ ℝ²` and radius
`r ≥ 0` such that

* every point of `A` lies in the closed disc of centre `c` and radius `r`,
  i.e. `∀ p ∈ A, dist p c ≤ r`, and
* `r` is minimal among all enclosing pairs `(c', r')`.

This is the geometric content needed by the U1–U7 surplus-cap programme
and by the Dumitrescu lower-bound chain (which both branch on cap
positions relative to the MEC).  Mathlib carries no MEC machinery, so
this file builds the proof from first principles:

* **Existence** is a compactness argument.  Fix `p₀ ∈ A` and let
  `R₀ := A.sup' hA (dist · p₀)`.  Then `(p₀, R₀)` encloses `A`, so any
  optimal centre `c*` must satisfy `dist p₀ c* ≤ R₀`.  The closed ball
  of centre `p₀` and radius `R₀` is compact (`EuclideanSpace ℝ (Fin 2)`
  is a `ProperSpace`).  The map `c ↦ A.sup' hA (dist · c)` is continuous
  and bounded below; `IsCompact.exists_isMinOn` produces a minimiser.

* **Uniqueness** is the classical parallelogram-law / midpoint argument.
  If two centres `c₁, c₂` achieve the optimum radius `r`, then for the
  midpoint `m = midpoint ℝ c₁ c₂`,
  Mathlib's identity
  `dist_sq_add_dist_sq_eq_two_mul_dist_midpoint_sq_add_half_dist_sq`
  yields `dist p m ^ 2 ≤ r² - (dist c₁ c₂ / 2)²` for every `p ∈ A`.
  If `c₁ ≠ c₂`, this forces a strictly smaller enclosing radius
  `r' = √(r² - (d/2)²)`, contradicting minimality.

## Main definitions

* `Problem97.MinEnclosingCircle A` — bundled record packaging the optimal
  centre, radius, the enclosing inequality, and the minimality clause.

## Main theorems

* `Problem97.MinEnclosingCircle.exists` — existence of a MEC for any
  nonempty `Finset ℝ²`.

* `Problem97.MinEnclosingCircle.unique_pair` — uniqueness on the level of
  `(centre, radius)` pairs.

* `Problem97.MEC.exists_unique_minimum_enclosing_circle` — combined
  `∃!` statement at the `ℝ² × ℝ` pair level, the form requested by the
  downstream blueprint obligation `p97-mec-existence`.

* `Problem97.MEC.mec` — `noncomputable` extractor producing the unique
  MEC record from any nonempty `Finset ℝ²`.
-/

open scoped EuclideanGeometry
open Finset

namespace Problem97

/-- A minimum enclosing circle for a finset of plane points. -/
structure MinEnclosingCircle (A : Finset ℝ²) where
  /-- Centre of the minimum enclosing circle. -/
  center : ℝ²
  /-- Radius of the minimum enclosing circle. -/
  radius : ℝ
  /-- The radius is nonnegative. -/
  radius_nn : 0 ≤ radius
  /-- Every point of `A` lies in the closed disc `(center, radius)`. -/
  enclosing : ∀ p ∈ A, dist p center ≤ radius
  /-- The radius is minimal among all enclosing pairs. -/
  minimal : ∀ c' r', (∀ p ∈ A, dist p c' ≤ r') → radius ≤ r'

namespace MinEnclosingCircle

/- ### Auxiliary: per-centre enclosing radius

For a nonempty finset `A`, the function `c ↦ A.sup' hA (dist · c)` returns
the tight enclosing radius given a centre `c`.  It is continuous and the
common backbone of the existence proof. -/

/-- The tight enclosing radius given a centre `c`. -/
 noncomputable def radF (A : Finset ℝ²) (hA : A.Nonempty) (c : ℝ²) : ℝ :=
  A.sup' hA (fun p => dist p c)

 lemma radF_continuous (A : Finset ℝ²) (hA : A.Nonempty) :
    Continuous (radF A hA) := by
  -- `Continuous.finset_sup'` over a `Finset ℝ²`, sup of finitely many continuous
  -- distance maps `c ↦ dist p c`.
  have h :=
    Continuous.finset_sup' (L := ℝ) hA (s := A)
      (f := fun p (c : ℝ²) => dist p c)
      (fun _ _ => continuous_const.dist continuous_id)
  -- `Finset.sup'_apply` turns `(A.sup' hA F) c` into `A.sup' hA (F · c)`.
  have e : radF A hA = A.sup' hA (fun p (c : ℝ²) => dist p c) := by
    funext c
    exact (Finset.sup'_apply hA (fun p (c : ℝ²) => dist p c) c).symm
  rw [e]; exact h

 lemma radF_upper (A : Finset ℝ²) (hA : A.Nonempty)
    (c : ℝ²) {p : ℝ²} (hp : p ∈ A) : dist p c ≤ radF A hA c :=
  Finset.le_sup' (f := fun p => dist p c) hp

 lemma radF_nn (A : Finset ℝ²) (hA : A.Nonempty) (c : ℝ²) :
    0 ≤ radF A hA c := by
  have hA' := hA
  obtain ⟨p, hp⟩ := hA'
  exact (dist_nonneg).trans (radF_upper A hA c hp)

 lemma radF_le_iff (A : Finset ℝ²) (hA : A.Nonempty)
    {c : ℝ²} {r : ℝ} :
    radF A hA c ≤ r ↔ ∀ p ∈ A, dist p c ≤ r := by
  exact Finset.sup'_le_iff hA _

/-- **Existence of a minimum enclosing circle.**  For any nonempty
finset `A ⊆ ℝ²`, there is a record packaging the optimal centre, radius,
enclosing inequality, and minimality clause. -/
theorem exists_mec (A : Finset ℝ²) (hA : A.Nonempty) :
    Nonempty (MinEnclosingCircle A) := by
  classical
  -- Auxiliary continuous radius function.
  have hf_cont : Continuous (radF A hA) := radF_continuous A hA
  -- Pick a reference point and the trivial bound `R₀ = radF A hA p₀`.
  have hA' := hA
  obtain ⟨p₀, hp₀⟩ := hA'
  set R₀ := radF A hA p₀ with hR₀_def
  have hR₀_nn : 0 ≤ R₀ := radF_nn A hA p₀
  -- The closed ball about `p₀` of radius `R₀` is compact and nonempty.
  have hcompact : IsCompact (Metric.closedBall p₀ R₀) :=
    ProperSpace.isCompact_closedBall p₀ R₀
  have hp0_in : p₀ ∈ Metric.closedBall p₀ R₀ := Metric.mem_closedBall_self hR₀_nn
  -- A minimiser of `radF A hA` exists on this compact set.
  obtain ⟨cMin, hcMin_mem, hcMin_min⟩ :=
    hcompact.exists_isMinOn ⟨p₀, hp0_in⟩ hf_cont.continuousOn
  refine ⟨{
    center := cMin
    radius := radF A hA cMin
    radius_nn := radF_nn A hA cMin
    enclosing := fun p hp => radF_upper A hA cMin hp
    minimal := ?_ }⟩
  intro c' r' hencl
  -- For any candidate `(c', r')`, `radF A hA c' ≤ r'`.
  have hfc' : radF A hA c' ≤ r' := (radF_le_iff A hA).mpr hencl
  by_cases hcase : c' ∈ Metric.closedBall p₀ R₀
  · -- Minimality of `cMin` directly applies on the ball.
    have hle : radF A hA cMin ≤ radF A hA c' := hcMin_min hcase
    linarith
  · -- Outside the ball: `dist p₀ c' > R₀`, so `radF A hA c' > R₀ ≥ radF A hA cMin`.
    rw [Metric.mem_closedBall, not_le] at hcase
    have h1 : dist p₀ c' ≤ radF A hA c' := radF_upper A hA c' hp₀
    have h2 : radF A hA cMin ≤ R₀ := hcMin_min hp0_in
    have h3 : dist c' p₀ = dist p₀ c' := dist_comm _ _
    linarith

/- ### Uniqueness

If two `(centre, radius)` pairs both attain the minimum enclosing radius,
they must coincide.  The radius agreement is immediate from the
minimality clauses; the centre agreement uses the parallelogram-law
identity at the midpoint. -/











end MinEnclosingCircle

namespace MEC



/-- **The (noncomputable) minimum enclosing circle of a nonempty finset.**

Extracted from the existence proof by `Classical.choice`.  Downstream
consumers can use `(mec A hA).center`, `(mec A hA).radius`, etc. -/
noncomputable def mec (A : Finset ℝ²) (hA : A.Nonempty) :
    MinEnclosingCircle A :=
  (Problem97.MinEnclosingCircle.exists_mec A hA).some











end MEC

end Problem97