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

import Mathlib
import Definitions.Def_MetricKMedian
import Definitions.Def_OAIQ037K027
import Definitions.Def_OAIQ037K028
import Definitions.Def_OAIQ037K029
import Definitions.Def_OAIQ037K030
import Definitions.Def_OAIQ037K032
import Definitions.Def_OAIQ037K033
import Definitions.Def_OAIQ037K034

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

namespace OAI

namespace MetricKMedian.IntegerBranching
open Finset
variable {n : ℕ}

theorem branch_moment (μ : IntegerLaw (Fin n)) (p : Fin n → ℚ)
    (hp : ∀ i, 0 ≤ p i ∧ p i ≤ 1) (f : Fin n → Fin 2 → ℚ) :
    (∑ a, (branch μ p hp).rational.weight a*f a.1 a.2)=
      ∑ i, μ.rational.weight i*(p i*f i 0+(1-p i)*f i 1) := by
  have hD : (RationalScaling.denominator p:ℚ) ≠ 0 := by
    exact_mod_cast (RationalScaling.denominator_pos p).ne'
  have hM : (μ.denominator:ℚ) ≠ 0 := by exact_mod_cast μ.denominator_pos.ne'
  simp only [IntegerLaw.rational,branch,Vector.getElem_ofFn,Fin.eta]
  rw [Fintype.sum_prod_type]
  simp only [Fin.sum_univ_two,branchNumerator]
  norm_num only [show (1:Fin 2) ≠ 0 by decide,ite_true,ite_false]
  simp only [Int.cast_mul,Int.cast_sub,RationalScaling.numerator_cast]
  apply sum_congr rfl
  intro i _
  field_simp

end MetricKMedian.IntegerBranching

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_LPListFacts
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.LPBinary
open Finset
abbrev ers := Binary.encodeList er

end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_LPBinaryInput
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.LPBinary
open Binary Polynomial Finset

namespace Input
abbrev encode (I : Input) := encodePair ers Nat.bits I.raw

end Input

end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_SimplexListProgram
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.LPBinary
open Finset

namespace Program
open Binary Binary.PolyProgram
abbrev ethreshold := encodePair (encodePair er Ratio.encode) Ratio.encode
end Program
end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_DualListCompiler
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.LPBinary.Program
open Binary Binary.PolyProgram Function
abbrev epoint := encodePair er er
abbrev edual := encodePair epoint Ratio.encode

noncomputable def candidatesProgram : PolyProgram (encodePair er Ratio.encode) er (fun x : Row × ℚ => Dual.candidates x.1 x.2) := by
  let consH := (exchange er Ratio.encode).comp (listCons Ratio.encode)
  exact (((constant (encodePair er Ratio.encode) Ratio.encode 0).fanout consH).comp (listCons Ratio.encode)).congr _ (fun _ => rfl)

end MetricKMedian.LPBinary.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_TruncatedListOperations
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.LPBinary
open Finset

namespace Truncated

 theorem objective_ofFn {n m : ℕ} (d : Fin m → Fin n → ℚ) (y : Fin n → ℚ) (H : ℚ) :
    objective (List.ofFn (fun j => List.ofFn (d j))) (List.ofFn y) H=TruncatedLP.objective d y H := by
  simp only [objective,matrix_ofFn,List.map_ofFn,List.sum_ofFn,TruncatedLP.objective]
  apply sum_congr rfl
  intro j _
  exact Dual.value_ofFn _ _ _
 theorem component_ofFn {n m : ℕ} (d : Fin m → Fin n → ℚ) (y : Fin n → ℚ) (H : ℚ) (i : Fin n) :
    component (List.ofFn (fun j => List.ofFn (d j))) (List.ofFn y) H i.val=TruncatedLP.gradient d y H i := by
  simp only [component,matrix_ofFn,List.map_ofFn,List.sum_ofFn,TruncatedLP.gradient]
  apply sum_congr rfl
  intro j _
  simp only [Function.comp_apply,Dual.best_ofFn,Gaussian.ListOperation.get_ofFn,FractionalDual.gradient]
 theorem gradient_ofFn {n m : ℕ} (d : Fin m → Fin n → ℚ) (y : Fin n → ℚ) (H : ℚ) :
    gradient (List.ofFn (fun j => List.ofFn (d j))) (List.ofFn y) H=List.ofFn (TruncatedLP.gradient d y H) := by
  simp only [gradient,List.length_ofFn]
  rw [range_ofFn,List.map_ofFn]
  congr 1
  funext i
  exact component_ofFn d y H i
 theorem next_ofFn {n m : ℕ} [NeZero n] (d : Fin m → Fin n → ℚ) (y : Fin n → ℚ) (H k rate : ℚ) :
    next (List.ofFn (fun j => List.ofFn (d j))) (List.ofFn y) H k rate=
      List.ofFn (ProjectedSubgradient.point (ProjectedSubgradient.next k rate (fun y => TruncatedLP.gradient d y H) (Vector.ofFn y))) := by
  simp only [next,gradient_ofFn,Gaussian.ListOperation.zip_ofFn,List.map_ofFn,project_ofFn]
  congr 1
  funext i
  simp only [ProjectedSubgradient.next_apply,ProjectedSubgradient.point_ofFn]
  simp only [ProjectedSubgradient.point_ofFn_apply,Function.comp_def]
end Truncated
end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_TruncatedListCompiler
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.LPBinary.Program
open Binary Binary.PolyProgram Function
abbrev etrunc := encodePair (encodePair ers er) Ratio.encode
abbrev enext := encodePair etrunc (encodePair Ratio.encode Ratio.encode)

end MetricKMedian.LPBinary.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_LPBinaryStart
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.LPBinary
open Binary Binary.PolyProgram Function
abbrev ec := encodePair ers (encodePair Ratio.encode (encodePair Ratio.encode Ratio.encode))
abbrev es := encodePair ec er
abbrev ei := encodePair ers Nat.bits

def start (r : ℕ) (I : Input) : State := (rawContext r I.raw,rawInitial I.raw)
def update (s : State) : State := (s.1,Truncated.next s.1.1 s.2 s.1.2.1 s.1.2.2.1 s.1.2.2.2)

namespace Program
noncomputable def inputRaw : PolyProgram Input.encode ei Input.raw :=
  (identity ei).recode Input.raw (fun _ => rfl) (fun _ => rfl)
end Program

theorem start_eq (r : ℕ) (I : Input) : start r I=(rawContext r I.raw,I.iterate r 0) := by
  unfold start
  congr 1
  simp only [rawInitial,Input.raw,Input.rows,head_ofFn,List.length_ofFn,range_ofFn,List.map_ofFn,Input.iterate,Input.vector,ProjectedSubgradient.trajectory_zero]
  congr 1
  funext i
  simp only [ProjectedSubgradient.initial,ProjectedSubgradient.point_ofFn_apply]
  simp only [Fin.ext_iff,Function.comp_apply,Fin.val_zero]

theorem update_eq (r : ℕ) (I : Input) (t : ℕ) :
    update (rawContext r I.raw,I.iterate r t)=(rawContext r I.raw,I.iterate r (t+1)) := by
  unfold update
  congr 1
  change Truncated.next I.rows (I.iterate r t) (TruncatedLP.penalty r I.k) I.k (rawRate r I.raw)=I.iterate r (t+1)
  rw [rawRate_eq]
  unfold Input.rows Input.iterate
  rw [Truncated.next_ofFn]
  have he : Vector.ofFn (ProjectedSubgradient.point (I.vector r t))=I.vector r t := by ext index hindex; simp
  rw [he]
  rfl

theorem update_iterate (r : ℕ) (I : Input) (t : ℕ) :
    update^[t] (start r I)=(rawContext r I.raw,I.iterate r t) := by
  induction t with
  | zero => exact start_eq r I
  | succ t ih => rw [Function.iterate_succ_apply',ih,update_eq]
end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_LPBinaryTrajectory
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.LPBinary
open Binary Binary.PolyProgram Polynomial Function

def states (r : ℕ) (I : Input) : List State := Iteration.iterates update (start r I) (rawSteps r I.raw)

theorem states_eq (r : ℕ) (I : Input) :
    states r I=List.ofFn (fun t : Fin (rawSteps r I.raw) => (rawContext r I.raw,I.iterate r t.val)) := by
  rw [states,Iteration.iterates_eq,range_ofFn,List.map_ofFn]
  congr 1
  funext t
  exact update_iterate r I t.val

def value (s : State) : ℚ := Truncated.objective s.1.1 s.2 s.1.2.1
def choose (ss : List State) : State := selectMinimum value ss (([],(0,(0,0))),[])
def result (r : ℕ) (I : Input) : Row := (choose (states r I)).2

 theorem value_eq (r : ℕ) (I : Input) (t : ℕ) :
    value (rawContext r I.raw,I.iterate r t)=
      TruncatedLP.objective I.distance (ProjectedSubgradient.point (I.vector r t)) (TruncatedLP.penalty r I.k) := by
  unfold value
  change Truncated.objective I.rows (I.iterate r t) (TruncatedLP.penalty r I.k)=_
  exact Truncated.objective_ofFn _ _ _

 theorem result_eq (r : ℕ) (hr : 0 < r) (I : Input) :
    result r I=List.ofFn (ProjectedSubgradient.point (TruncatedLP.optimize I.distance r I.k (TruncatedLP.penalty r I.k) hr I.kpos (TruncatedLP.penalty_pos r I.k hr))) := by
  let T := TruncatedLP.steps (n:=I.n) (m:=I.m) r I.k (TruncatedLP.penalty r I.k)
  have hT : 0 < T := TruncatedLP.steps_pos _ _ _ hr I.kpos (TruncatedLP.penalty_pos r I.k hr)
  let : NeZero T := ⟨hT.ne'⟩
  unfold result choose
  have hs := states_eq r I
  rw [rawSteps_eq] at hs
  rw [hs,selectMinimum_ofFn]
  simp only [value_eq]
  unfold TruncatedLP.optimize
  simp only [Input.iterate,Input.vector]
end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_ApproximationListProgram
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.LPBinary
open Binary Binary.PolyProgram Function Finset
namespace Repair
abbrev eo := encodePair er ers

theorem assignments_ofFn {n m : ℕ} (d x : Fin m → Fin n → ℚ) :
    assignments (List.ofFn (fun j => List.ofFn (d j))) (List.ofFn (fun j => List.ofFn (x j)))=
      List.ofFn (fun j => List.ofFn (TruncatedLP.repairedAssignment d x j)) := by
  simp only [assignments,Gaussian.ListOperation.zip_ofFn,List.map_ofFn,Function.comp_def,assignment,weights_ofFn,List.sum_ofFn]
  rfl

end Repair
end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_FractionalListChecks
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.LPBinary.Repair
open Binary Binary.PolyProgram Function Finset

theorem valid_encodeData {n m : ℕ} (a : TruncatedLP.FractionalData n m) (k : ℕ) :
    valid (encodeData a) k=decide (a.Valid k) := by
  apply Bool.eq_iff_iff.mpr
  rw [decide_eq_true_eq]
  simp only [valid,encodeData,Bool.and_eq_true,all_ofFn,bounded,dominated,Gaussian.ListOperation.zip_ofFn,
    decide_eq_true_eq,List.sum_ofFn,TruncatedLP.FractionalData.Valid,ProjectedSubgradient.point]
  tauto

end MetricKMedian.LPBinary.Repair
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_ZeroCostBranch
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
namespace Instance

def zeroOutput (I : Instance) : Finset (Fin I.n) :=
  if I.clients.Nonempty then I.clients else {I.facilities.min' I.facilities_nonempty}

theorem zeroOutput_spec (I : Instance) (h : I.zeroTest) :
    I.zeroOutput ⊆ I.facilities ∧ I.zeroOutput.Nonempty ∧ I.zeroOutput.card ≤ I.k ∧
      cost I I.zeroOutput=0 := by
  by_cases hJ : I.clients.Nonempty
  · simp only [zeroOutput,ite_eq_left hJ]
    exact ⟨h.1,hJ,h.2,(I.cost_eq_zero_iff I.clients hJ).mpr Subset.rfl⟩
  · simp only [zeroOutput,ite_eq_right hJ]
    refine ⟨singleton_subset_iff.mpr (min'_mem _ _),singleton_nonempty _,?_,?_⟩
    · simpa only [card_singleton] using I.k_pos
    · have hj : I.clients=∅ := not_nonempty_iff_eq_empty.mp hJ
      simp only [cost,hj,sum_empty]

theorem nonzero_clients (I : Instance) (h : ¬I.zeroTest) : I.clients.Nonempty := by
  by_contra hn
  apply h
  have hj : I.clients=∅ := not_nonempty_iff_eq_empty.mp hn
  simp only [zeroTest,hj,empty_subset,card_empty,Nat.zero_le,and_self]

end Instance
end MetricKMedian
end
end

end OAI
end

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

namespace OAI

namespace MetricKMedian.SparseIntegerLaw
open Finset
variable {α : Type}

theorem branch_moment (μ : SparseIntegerLaw α) (p : α → ℚ)
    (hp : ∀ a, 0 ≤ p a ∧ p a ≤ 1) (next : α → Fin 2 → α) (f : α → ℚ) :
    (μ.branch p hp next).moment f=
      μ.moment (fun a => p a*f (next a 0)+(1-p a)*f (next a 1)) := by
  let ρ := IntegerBranching.branch μ.law (fun i => p μ.states[i.val])
    (fun i => hp μ.states[i.val])
  have h := ρ.reindex_moment finProdFinEquiv
    (fun a => f (next μ.states[a.1.val] a.2))
  have h' := IntegerBranching.branch_moment μ.law (fun i => p μ.states[i.val])
    (fun i => hp μ.states[i.val]) (fun i b => f (next μ.states[i.val] b))
  unfold moment branch
  simp only [Vector.getElem_ofFn]
  convert h.trans h' using 1
  all_goals try with_reducible_and_instances rfl

end MetricKMedian.SparseIntegerLaw

end OAI
end

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

namespace OAI

namespace MetricKMedian.SparseIntegerLaw
open Finset
variable {α : Type}

 theorem moment_congr (μ : SparseIntegerLaw α) (f g : α → ℚ)
    (h : ∀ i : Fin μ.length, f μ.states[i.val]=g μ.states[i.val]) :
    μ.moment f=μ.moment g := by
  apply sum_congr rfl
  intro i _
  rw [h i]

 theorem dirac_moment (a : α) (f : α → ℚ) : (dirac a).moment f=f a := by
  change (∑ _i : Fin 1, ((1:ℤ):ℚ)/1*f a)=f a
  simp

end MetricKMedian.SparseIntegerLaw

end OAI
end

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

namespace OAI

namespace MetricKMedian.SparseIntegerLaw
open Finset
variable {α : Type}

theorem moment_mul (μ : SparseIntegerLaw α) (c : ℚ) (f : α → ℚ) :
    μ.moment (fun a => c*f a)=c*μ.moment f := by
  simp only [moment,mul_left_comm,mul_sum]

end MetricKMedian.SparseIntegerLaw

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_CountStepProgram
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.SparseCounts.Program
open Binary Binary.PolyProgram Function
open SparseIntegerLaw.BinarySparse
open ListOperation (Row Table er et)

structure Input where
  n : ℕ
  m : ℕ
  columns : Fin m → SparseIntegerLaw ((Fin n → ℕ))
end MetricKMedian.SparseCounts.Program
end

end OAI
end

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

namespace OAI

namespace MetricKMedian.RationalLaw
open Finset
variable {α : Type} {β : α → Type} [Fintype α] [∀ a, Fintype (β a)]

theorem sigma_moment (μ : RationalLaw α) (κ : ∀ a, RationalLaw (β a)) (f : Sigma β → ℚ) :
    (∑ z, (μ.sigma κ).weight z*f z)=
      ∑ a, μ.weight a*∑ b, (κ a).weight b*f ⟨a,b⟩ := by
  rw [Fintype.sum_sigma]
  simp only [sigma,mul_sum,mul_assoc]

end MetricKMedian.RationalLaw
namespace MetricKMedian.SparseIntegerLaw
open Finset
variable {α β : Type}

theorem bindIndexed_moment (μ : SparseIntegerLaw α) (κ : Fin μ.length → SparseIntegerLaw β)
    (f : β → ℚ) :
    (μ.bindIndexed κ).moment f=∑ a, μ.law.rational.weight a*(κ a).moment f := by
  let ρ := μ.law.rational.sigma (fun a => (κ a).law.rational)
  have h := ρ.integer.reindex_moment finSigmaFinEquiv
    (fun z => f (κ z.1).states[z.2.val])
  have h' := μ.law.rational.sigma_moment (fun a => (κ a).law.rational)
    (fun z => f (κ z.1).states[z.2.val])
  simp only [RationalLaw.integer_weight] at h
  unfold moment bindIndexed
  simp only [Vector.getElem_ofFn]
  convert h.trans h' using 1
  all_goals try with_reducible_and_instances rfl

end MetricKMedian.SparseIntegerLaw

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseSupport
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.SparseIntegerLaw
open Finset
variable {α : Type}

theorem zero_indicator (μ : SparseIntegerLaw α) (P : α → Prop) [DecidablePred P]
    (hz : μ.moment (fun x => if P x then 1 else 0)=0)
    (a : Fin μ.length) (ha : 0 < μ.law.rational.weight a) : ¬P μ.states[a.val] := by
  intro hpa
  have hs := single_le_sum (s := univ)
    (f := fun i : Fin μ.length => μ.law.rational.weight i*(if P μ.states[i.val] then 1 else 0))
    (fun i _ => mul_nonneg (μ.law.rational.nonneg _) (by split_ifs <;> norm_num)) (mem_univ a)
  change _ ≤ μ.moment (fun x => if P x then 1 else 0) at hs
  rw [hz,ite_eq_left hpa,mul_one] at hs
  exact (not_lt_of_ge hs) ha

theorem one_indicator (μ : SparseIntegerLaw α) (P : α → Prop) [DecidablePred P]
    (hz : μ.moment (fun x => if P x then 1 else 0)=1)
    (a : Fin μ.length) (ha : 0 < μ.law.rational.weight a) : P μ.states[a.val] := by
  by_contra hn
  have hs := single_le_sum (s := univ)
    (f := fun i : Fin μ.length => μ.law.rational.weight i*(if P μ.states[i.val] then 0 else 1))
    (fun i _ => mul_nonneg (μ.law.rational.nonneg _) (by split_ifs <;> norm_num)) (mem_univ a)
  have hsum : (∑ i : Fin μ.length, μ.law.rational.weight i*(if P μ.states[i.val] then 0 else 1))=0 := by
    have hh : ∀ i : Fin μ.length,
        μ.law.rational.weight i*(if P μ.states[i.val] then 0 else 1)=
          μ.law.rational.weight i-μ.law.rational.weight i*(if P μ.states[i.val] then 1 else 0) := by
      intro i
      split_ifs <;> ring
    simp_rw [hh]
    rw [sum_sub_distrib,μ.law.rational.total]
    change 1-μ.moment (fun x => if P x then 1 else 0)=0
    rw [hz,sub_self]
  rw [hsum,ite_eq_right hn,mul_one] at hs
  exact (not_lt_of_ge hs) ha

end MetricKMedian.SparseIntegerLaw
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_ScaleListProgram
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.LPBinary
open Binary Binary.PolyProgram Function Finset
namespace Scale

theorem guesses_mem {n m : ℕ} (d : Fin m → Fin n → ℚ) (q : ℚ) :
    q ∈ guesses (List.ofFn (fun j => List.ofFn (d j))) ↔ q ∈ Normalization.matrixGuesses d := by
  unfold guesses Normalization.matrixGuesses
  simp only [List.mem_flatMap,List.mem_flatten,mem_biUnion,mem_univ,true_and]
  constructor
  · rintro ⟨v,⟨xs,hxs,hv⟩,hq⟩
    obtain ⟨j,rfl⟩ := List.mem_ofFn.mp hxs
    obtain ⟨i,rfl⟩ := List.mem_ofFn.mp hv
    by_cases h : 0 < d j i
    · simp only [ite_eq_left h,List.length_ofFn,Dyadic.powers_eq,List.mem_map,List.mem_range] at hq
      obtain ⟨z,⟨t,ht,rfl⟩,he⟩ := hq
      exact ⟨(j,i),by simp only [ite_eq_left h,mem_image,mem_range]; exact ⟨t,ht,he⟩⟩
    · simp only [ite_eq_right h,List.not_mem_nil] at hq
  · rintro ⟨⟨j,i⟩,hq⟩
    by_cases h : 0 < d j i
    · simp only [ite_eq_left h,mem_image,mem_range] at hq
      obtain ⟨t,ht,rfl⟩ := hq
      refine ⟨d j i,⟨List.ofFn (d j),List.mem_ofFn.mpr ⟨j,rfl⟩,List.mem_ofFn.mpr ⟨i,rfl⟩⟩,?_⟩
      simp only [ite_eq_left h,List.length_ofFn,Dyadic.powers_eq,List.mem_map,List.mem_range]
      exact ⟨(2:ℚ)^t,⟨t,ht,rfl⟩,rfl⟩
    · simp only [ite_eq_right h,notMem_empty] at hq

end Scale
end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_InstanceDataProgram
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.InstanceProgram
open Finset Preparation Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
open MaskProgram
def lpInput (I : Nonzero) : LPBinary.Input :=
  ⟨I.val.facilities.card,I.val.clients.card,I.val.k,card_pos.mpr I.val.facilities_nonempty,
    card_pos.mpr (I.val.nonzero_clients I.property),I.val.k_pos,I.val.k_le,I.val.indexedDistance⟩
end MetricKMedian.InstanceProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_SignedTerminalProgram
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.RoundingProgram
open Binary Binary.PolyProgram Function SparseIntegerLaw.BinarySparse
open Binary.Automatic Binary.Automatic.Poly
namespace Terminal

abbrev ber := SparseBernoulli.Program.er

end Terminal
end MetricKMedian.RoundingProgram
end

end OAI
end