Definitions bundle OAIQ037K011 of the split of OpenAI, The approximation threshold for metric k-median (result family 125)

import Mathlib

section
-- module Solutions.OAIQ037_KM.Compat
namespace OAI

/-! Compatibility with the newer Lean core OpenAI's code was written against: lemmas it uses by
names this environment (Lean 4.33.1, Mathlib 0df444a) does not have yet. Each is the
corresponding `if_pos` / `if_neg` / `dif_pos` / `dif_neg`. The `dite` forms are stated as
`dite p a b`, not with the `if hp : p then …` notation: its eta-expanded lambdas form is a higher-order pattern
that `rw` cannot find (DepthThree, PeriodicTiling 2026-10-25). -/
section OAICompat434
/-- Mathlib's newer case names for `FreeGroup.induction_on` (`one`, where ours says `C1`). -/
@[elab_as_elim]
theorem freeGroupInductionOn {α : Type*} {C : FreeGroup α → Prop} (z : FreeGroup α) (one : C 1)
    (of : ∀ x, C (FreeGroup.of x)) (inv_of : ∀ x, C (FreeGroup.of x) → C (FreeGroup.of x)⁻¹)
    (mul : ∀ x y, C x → C y → C (x * y)) : C z :=
  FreeGroup.induction_on z one of inv_of mul
end OAICompat434

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Analysis_ScalarTransfer
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

section
section
namespace MetricKMedian.ScalarTransfer

noncomputable def T1 (p x : ℝ) : ℝ :=
  1-p-(28/25)*p*(1+x)+(2/5)*p^2*(1-x)*(1+x)
noncomputable def T2 (p x : ℝ) : ℝ :=
  ((1-p)^2-(19/50)*p*(1-x)+p*x)*(1+x)-2*x*(1-p)
noncomputable def Yprime (p k x : ℝ) : ℝ :=
  1-k+p*((8/5)*(1-x)^2-2)

end MetricKMedian.ScalarTransfer


end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Geometry_RationalBrackets
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

section
section
namespace MetricKMedian
open Finset

theorem rational_bracket (B : Finset ℚ) (r : ℝ) (lo hi : ℚ)
    (hlo : lo ∈ B) (hhi : hi ∈ B) (hlor : (lo:ℝ) < r) (hrhi : r < (hi:ℝ))
    (hnot : ∀ q ∈ B, (q:ℝ) ≠ r) :
    ∃ a ∈ B, ∃ b ∈ B, (a:ℝ) < r ∧ r < (b:ℝ) ∧
      ∀ q ∈ B, q ≤ a ∨ b ≤ q := by
  classical
  let A : Finset ℚ := B.filter (fun q : ℚ => (q:ℝ) < r)
  let C : Finset ℚ := B.filter (fun q : ℚ => r < (q:ℝ))
  have hA : A.Nonempty := ⟨lo,mem_filter.mpr ⟨hlo,hlor⟩⟩
  have hC : C.Nonempty := ⟨hi,mem_filter.mpr ⟨hhi,hrhi⟩⟩
  let a := A.max' hA
  let b := C.min' hC
  have ha := mem_filter.mp (max'_mem A hA)
  have hb := mem_filter.mp (min'_mem C hC)
  refine ⟨a,ha.1,b,hb.1,ha.2,hb.2,?_⟩
  intro q hq
  rcases lt_or_gt_of_ne (hnot q hq) with hqlo | hqhi
  · exact Or.inl (le_max' A q (mem_filter.mpr ⟨hq,hqlo⟩))
  · exact Or.inr (min'_le C q (mem_filter.mpr ⟨hq,hqhi⟩))

theorem same_interval_cuts (B : Finset ℚ) (a b : ℚ)
    (hgap : ∀ q ∈ B, q ≤ a ∨ b ≤ q) (x y : ℝ)
    (hx : (a:ℝ) < x ∧ x < (b:ℝ)) (hy : (a:ℝ) < y ∧ y < (b:ℝ)) :
    ∀ q ∈ B, (x ≤ (q:ℝ) ↔ y ≤ (q:ℝ)) ∧ ((q:ℝ) ≤ x ↔ (q:ℝ) ≤ y) := by
  intro q hq
  rcases hgap q hq with hq | hq
  · have hq' : (q:ℝ) ≤ a := by exact_mod_cast hq
    exact ⟨iff_of_false (not_le_of_gt (hq'.trans_lt hx.1))
      (not_le_of_gt (hq'.trans_lt hy.1)),iff_of_true (hq'.trans hx.1.le) (hq'.trans hy.1.le)⟩
  · have hq' : (b:ℝ) ≤ q := by exact_mod_cast hq
    exact ⟨iff_of_true (hx.2.le.trans hq') (hy.2.le.trans hq'),
      iff_of_false (not_le_of_gt (hx.2.trans_le hq')) (not_le_of_gt (hy.2.trans_le hq'))⟩

end MetricKMedian
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_NearestAssignmentGeometry
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

section
section
namespace MetricKMedian.Preparation
open Finset
variable {I T X : Type} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T]
  [PseudoMetricSpace X]

noncomputable def relevantRadius (c L R : ℝ) : ℝ := if 0 < c then L else R

end MetricKMedian.Preparation
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_PreparationParameters
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

section
section
namespace MetricKMedian.Preparation

noncomputable def parameterEnvelopeFar (a : ℝ) : ℝ :=
  max (1/(1-a)) (1+2*a/(1-a^2-a))*((1+a)/(1-a))+(a^2+1+a)*a^5
noncomputable def parameterEnvelopeNear (a : ℝ) : ℝ :=
  1/(1-a)+9*(a^2+1+a)*a^2
noncomputable def parameterEnvelope (a : ℝ) : ℝ :=
  max (parameterEnvelopeFar a) (parameterEnvelopeNear a)/(1-8*a^8)

end MetricKMedian.Preparation
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_SupplierAllocation
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

section
section
namespace MetricKMedian.Preparation
open Finset
variable {I T E : Type} [Fintype I] [DecidableEq I]
  [Fintype T] [DecidableEq T] [Fintype E]

def supplierOutside (σ : E → I ⊕ T) (q : E → ℝ) (i : I) : ℝ :=
  ∑ e, if σ e=Sum.inl i then q e else 0

def supplierBundle (σ : E → I ⊕ T) (q : E → ℝ) (t : T) : ℝ :=
  ∑ e, if σ e=Sum.inr t then q e else 0

end MetricKMedian.Preparation
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Probability_BernoulliSquare
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

namespace MetricKMedian.SparseBernoulli
open Finset
variable {n m : ℕ}

def pairSet (S : Fin m → Finset (Fin n)) (a : Fin (m*m)) : Finset (Fin n) :=
  S (finProdFinEquiv.symm a).1 ∪ S (finProdFinEquiv.symm a).2

def pairCoefficient (c : Fin m → ℚ) (a : Fin (m*m)) : ℚ :=
  c (finProdFinEquiv.symm a).1*c (finProdFinEquiv.symm a).2

end MetricKMedian.SparseBernoulli

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_SourceBalance
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

section
section
namespace MetricKMedian.SourceBalance
open Finset
variable {I : Type*} [Fintype I]

noncomputable def negative (m : I → ℝ) : Finset I := univ.filter (fun i => 1 < m i)
noncomputable def nonzero (m : I → ℝ) : Finset I := univ.filter (fun i => m i ≠ 1)
noncomputable def amount (m : I → ℝ) : ℝ := ∑ i, max (1-m i) 0

end MetricKMedian.SourceBalance
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_CountSource
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

section
section
namespace MetricKMedian.SourceBalance
open Finset
variable {I : Type*} [Fintype I]

noncomputable def bias (m : I → ℝ) (p φ : ℝ) (i : I) : ℝ :=
  if 1 < m i then (1+φ)*p else p

end MetricKMedian.SourceBalance

end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_Taper
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

section
section
namespace MetricKMedian.Taper

noncomputable def marginal (P d r : ℝ) : ℝ := min 1 (max (1-r*d) 0/P)

theorem marginal_nonneg {P d r : ℝ} (hP : 0 < P) : 0 ≤ marginal P d r :=
  le_min (by norm_num) (div_nonneg (le_max_right _ _) hP.le)

theorem marginal_le_one (P d r : ℝ) : marginal P d r ≤ 1 := min_le_left _ _

theorem marginal_antitone {P d : ℝ} (hP : 0 < P) (hd : 0 ≤ d) : Antitone (marginal P d) := by
  intro r s hrs
  apply min_le_min_left
  apply div_le_div_of_nonneg_right _ hP.le
  apply max_le_max_right
  nlinarith only [mul_le_mul_of_nonneg_right hrs hd]

theorem marginal_one {P d r : ℝ} (hP : 0 < P) (h : r*d ≤ 1-P) : marginal P d r=1 := by
  apply min_eq_left
  apply (le_div_iff₀ hP).mpr
  have hh := le_max_left (1-r*d) 0
  linarith only [h, hh]

theorem marginal_zero {P d r : ℝ} (h : 1 ≤ r*d) : marginal P d r=0 := by
  simp only [marginal, max_eq_right (by linarith : 1-r*d ≤ 0), zero_div]
  norm_num

theorem marginal_at_zero_distance {P r : ℝ} (hP : 0 < P) (hP1 : P ≤ 1) : marginal P 0 r=1 := by
  apply marginal_one hP
  simpa only [mul_zero] using sub_nonneg.mpr hP1

theorem lower_comparison {P d r : ℝ} (hP : 0 < P) (h : marginal P d r < 1) :
    1-P*marginal P d r ≤ r*d := by
  have hright : max (1-r*d) 0/P < 1 := by
    by_contra hn
    have heq : marginal P d r=1 := min_eq_left (le_of_not_gt hn)
    rw [heq] at h
    exact lt_irrefl _ h
  have heq : marginal P d r=max (1-r*d) 0/P := min_eq_right hright.le
  rw [heq, mul_div_cancel₀ _ (ne_of_gt hP)]
  have hh := le_max_left (1-r*d) 0
  linarith only [hh]

theorem upper_comparison {P d r : ℝ} (hP : 0 < P) (h : 0 < marginal P d r) :
    r*d ≤ 1-P*marginal P d r := by
  have hrd : r*d < 1 := by
    by_contra hn
    rw [marginal_zero (le_of_not_gt hn)] at h
    exact lt_irrefl _ h
  have hh : marginal P d r ≤ (1-r*d)/P := by
    unfold marginal
    rw [max_eq_left (by linarith only [hrd])]
    exact min_le_right _ _
  have hb := (le_div_iff₀ hP).mp hh
  nlinarith only [hb]

variable {I : Type*} [Fintype I]

noncomputable def mass (g P : ℝ) (d : I → ℝ) (r : ℝ) : ℝ := ∑ i, g*marginal P (d i) r

noncomputable def colocatedMass (g : ℝ) (d : I → ℝ) : ℝ := ∑ i, if d i=0 then g else 0

theorem mass_antitone {g P : ℝ} {d : I → ℝ} (hg : 0 ≤ g) (hP : 0 < P)
    (hd : ∀ i, 0 ≤ d i) : Antitone (mass g P d) := by
  intro r s hrs
  exact Finset.sum_le_sum (fun i _ => mul_le_mul_of_nonneg_left (marginal_antitone hP (hd i) hrs) hg)

theorem continuous_mass {g P : ℝ} {d : I → ℝ} : Continuous (mass g P d) := by
  unfold mass marginal
  fun_prop

theorem exists_full_inverse {P : ℝ} (hP : 0 < P) (hP1 : P ≤ 1/2)
    (d : I → ℝ) (hd : ∀ i, 0 ≤ d i) :
    ∃ r > 0, ∀ i, marginal P (d i) r=1 := by
  let D := ∑ i, d i
  have hD : 0 ≤ D := Finset.sum_nonneg (fun i _ => hd i)
  have hden : 0 < 2*(1+D) := by linarith only [hD]
  refine ⟨1/(2*(1+D)), one_div_pos.mpr hden, ?_⟩
  intro i
  apply marginal_one hP
  have hi : d i ≤ D := Finset.single_le_sum (fun t _ => hd t) (Finset.mem_univ i)
  have hh : (1/(2*(1+D)))*d i ≤ 1/2 := by
    rw [one_div_mul_eq_div]
    apply (div_le_iff₀ hden).mpr
    linarith only [hi]
  linarith only [hh, hP1]

end MetricKMedian.Taper
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_TaperGraph
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

section
section
namespace MetricKMedian.Taper
open Finset
variable {I X : Type*} [Fintype I] [DecidableEq I] [PseudoMetricSpace X]

structure GraphData (Δ : ℕ) (g P : ℝ) (location : I → X) (own : I → Finset I) where
  radius : I → ℝ
  marginal : I → I → ℝ
  radius_nonneg : ∀ i, 0 ≤ radius i
  marginal_nonneg : ∀ h i, 0 ≤ marginal h i
  marginal_le_one : ∀ h i, marginal h i ≤ 1
  incoming_mass : ∀ i, ∑ h, g*marginal h i=1
  incoming_count : ∀ i, ∑ h, marginal h i=Δ
  own_certain : ∀ i h, h ∈ own i → marginal h i=1
  lower : ∀ h i, marginal h i < 1 →
    radius i*(1-P*marginal h i) ≤ dist (location i) (location h)
  upper : ∀ h i, 0 < marginal h i →
    dist (location i) (location h) ≤ radius i*(1-P*marginal h i)
  minimal : ∀ i R, 0 < R →
    1 ≤ mass g P (fun h => dist (location i) (location h)) (1/R) → radius i ≤ R

def GraphData.Good {Δ : ℕ} {g P : ℝ} {location : I → X} {own : I → Finset I}
    (D : GraphData Δ g P location own) (G : I → Finset I) : Prop :=
  (∀ i, (G i).card=Δ) ∧ (∀ i, own i ⊆ G i) ∧
    (∀ h i, h ∈ G i → 0 < D.marginal h i)

end MetricKMedian.Taper
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_WeightedRounding
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

section
section
namespace MetricKMedian.WeightedRounding

variable {I : Type*} [Fintype I] [DecidableEq I]

noncomputable def indicator (S : Finset I) (i : I) : ℝ := if i ∈ S then 1 else 0

end MetricKMedian.WeightedRounding
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_RationalTaperAffine
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

section
section
namespace MetricKMedian.Taper
open Finset

theorem marginal_piecewise {P d r : ℝ} (hP : 0 < P) :
    marginal P d r=if r*d ≤ 1-P then 1 else
      if 1 ≤ r*d then 0 else (1-r*d)/P := by
  split_ifs with hs hz
  · exact marginal_one hP hs
  · exact marginal_zero hz
  · have hp : 0 ≤ 1-r*d := by linarith
    have hh : (1-r*d)/P ≤ 1 := (div_le_one₀ hP).mpr (by linarith)
    exact (congrArg (min 1) (congrArg (fun a => a/P) (max_eq_left hp))).trans (min_eq_right hh)

end MetricKMedian.Taper
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Reduction_RationalThreshold
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

section
section
namespace MetricKMedian.Reduction
open Finset

def deletionChoices {I : Type} [DecidableEq I] (T : Finset I) (c : ℕ) : Finset (Finset I) :=
  (range (c+1)).biUnion (fun m => T.powersetCard m)

end MetricKMedian.Reduction
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_BoundedEnumerationProgram
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI


                                                 
section
namespace MetricKMedian.Reduction.Enumeration
open Finset
def words {α : Type} : ℕ → List α → List (List α)
  | 0,_ => [[]]
  | c+1,xs => []::xs.flatMap (fun a => (words c xs).map (List.cons a))
end MetricKMedian.Reduction.Enumeration
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseCountStatistic
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

section
section
namespace MetricKMedian.SparseBernoulli
open Finset
variable {n : ℕ}

def countSets (a : Fin (n+n*n)) : Finset (Fin n) :=
  (finSumFinEquiv.symm a).elim (fun i => {i})
    (fun ij => {(finProdFinEquiv.symm ij).1} ∪ {(finProdFinEquiv.symm ij).2})

def countCoefficients (b : Fin n → ℚ) (c : Fin n → Fin n → ℚ) (a : Fin (n+n*n)) : ℚ :=
  (finSumFinEquiv.symm a).elim b
    (fun ij => (1/2)*c (finProdFinEquiv.symm ij).1 (finProdFinEquiv.symm ij).2)

end MetricKMedian.SparseBernoulli
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_GridClipping
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

section
section
namespace MetricKMedian.Preparation
open Finset WeightedRounding
variable {E T Ω : Type} [Fintype E] [DecidableEq T]

theorem grid_clip {Δ : ℕ} {g : ℝ} (hg : 0 < g) (heven : Even Δ)
    (hunit : g*(Δ:ℝ)=1) (Z : ℕ) :
    min (g*(Z:ℝ)) (1/2)=g*(min Z (Δ/2):ℕ) ∧
    1-min (g*(Z:ℝ)) (1/2)=g*(Δ-min Z (Δ/2):ℕ) ∧
    (1/2:ℝ) ≤ g*(Δ-min Z (Δ/2):ℕ) ∧
    g*(Δ-min Z (Δ/2):ℕ) ≤ 1 := by
  have htwo : Δ/2+Δ/2=Δ := by
    obtain ⟨n,hn⟩ := heven
    omega
  have hhalf : g*(Δ/2:ℕ)= (1/2:ℝ) := by
    have hh : (Δ/2:ℕ)+(Δ/2:ℕ)=(Δ:ℝ) := by exact_mod_cast htwo
    have he := congrArg (fun x : ℝ => g*x) hh
    rw [mul_add,hunit] at he
    linarith only [he]
  have hle : min Z (Δ/2) ≤ Δ := (min_le_right _ _).trans (Nat.div_le_self _ _)
  have hc : min (g*(Z:ℝ)) (1/2)=g*(min Z (Δ/2):ℕ) := by
    rw [← hhalf,Nat.cast_min,mul_min_of_nonneg _ _ hg.le]
  have hm : 1-min (g*(Z:ℝ)) (1/2)=g*(Δ-min Z (Δ/2):ℕ) := by
    rw [hc,Nat.cast_sub hle,mul_sub,hunit]
  refine ⟨hc,hm,?_,?_⟩
  · rw [← hm]
    have hc' : min (g*(Z:ℝ)) (1/2) ≤ (1/2:ℝ) := min_le_right _ _
    linarith only [hc']
  · rw [← hm]
    have hz : 0 ≤ min (g*(Z:ℝ)) (1/2) := le_min (mul_nonneg hg.le (Nat.cast_nonneg _)) (by norm_num)
    linarith only [hz]

end MetricKMedian.Preparation
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseCountRun
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

section
section
namespace MetricKMedian.SparseCounts
open Finset
variable {n m : ℕ}

def target (q : Fin n → Fin m → ℚ) (t : ℕ) (h : Fin n) (i : Fin m) : ℚ :=
  if i.val<t then q h i else 0

theorem target_succ_eq (q : Fin n → Fin m → ℚ) (t : ℕ) (ht : t < m) (h : Fin n) :
    target q (t+1) h ⟨t,ht⟩=q h ⟨t,ht⟩ := by simp [target]

theorem target_succ_ne (q : Fin n → Fin m → ℚ) (t : ℕ) (ht : t < m)
    (h : Fin n) (i : Fin m) (hi : i≠⟨t,ht⟩) : target q (t+1) h i=target q t h i := by
  have hv : i.val≠t := fun he => hi (Fin.ext he)
  have hh : i.val<t+1 ↔ i.val<t := by omega
  simp only [target,hh]

end MetricKMedian.SparseCounts
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_RestrictionProgram
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI


                                          
section
namespace MetricKMedian.Reduction.Enumeration
open Finset
 theorem mem_orderList {n : ℕ} (T : Finset (Fin n)) (i : Fin n) : i∈List.ofFn (T.orderEmbOfFin rfl) ↔ i∈T := by
  simp only [List.mem_ofFn]
  constructor
  · rintro ⟨a,rfl⟩; exact T.orderEmbOfFin_mem rfl a
  · intro hi
    have h : i ∈ Set.range (T.orderEmbOfFin rfl) := by rw [T.range_orderEmbOfFin rfl]; exact hi
    exact h
 def pairs {n : ℕ} (T : Finset (Fin n)) : List (Fin n × Fin n) :=
  (List.ofFn (T.orderEmbOfFin rfl)).flatMap (fun i => (List.ofFn (T.orderEmbOfFin rfl)).map (fun j => (i,j)))
end MetricKMedian.Reduction.Enumeration
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Reduction_RationalLocalChoice
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

section
section
namespace MetricKMedian.Reduction
open Finset

def pickSingleton {X : Type*} [LinearOrder X] (K : Finset X) (w : X → ℚ) : Finset X :=
  if hK : K.Nonempty then
    let m := (K.image w).min' (hK.image w)
    let A := K.filter (fun a => w a=m)
    have hA : A.Nonempty := by
      obtain ⟨a,ha,he⟩ := mem_image.mp (min'_mem (K.image w) (hK.image w))
      exact ⟨a,mem_filter.mpr ⟨ha,he⟩⟩
    {A.min' hA}
  else ∅

end MetricKMedian.Reduction
end
end

end OAI
end