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

import Mathlib

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 d (s : Bool) : ℝ := if s then 2/5 else 13/25

end MetricKMedian.ScalarTransfer


end
end

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

 theorem sum_filter_ofFn (n : ℕ) (f : Fin n → ℚ) (p : ℚ → Bool) :
    ((List.ofFn f).filter p).sum=∑ i∈univ.filter (fun i => p (f i)), f i := by
  rw [Finset.sum_filter]
  have he : ((List.ofFn f).filter p).sum=((List.ofFn f).map (fun a => if p a then a else 0)).sum := by
    generalize List.ofFn f=xs
    induction xs with
    | nil => rfl
    | cons a xs ih => cases h : p a <;> simp [h,ih]
  rw [he,List.map_ofFn,List.sum_ofFn]
  rfl

 theorem length_filter_ofFn (n : ℕ) (f : Fin n → ℚ) (p : ℚ → Bool) :
    ((List.ofFn f).filter p).length=(univ.filter (fun i => p (f i))).card := by
  have he : ((List.ofFn f).filter p).length=((List.ofFn f).map (fun a => if p a then (1:ℕ) else 0)).sum := by
    generalize List.ofFn f=xs
    induction xs with
    | nil => rfl
    | cons a xs ih => cases h : p a <;> simp [h,ih,Nat.add_comm]
  rw [he,List.map_ofFn,List.sum_ofFn]
  simp

end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Geometry_NearestFillingFormula
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.Preparation
open Finset
variable {n : ℕ}

def before (d : Fin n → ℚ) (j i : Fin n) : Prop := d j  <  d i ∨ d j=d i ∧ j < i
instance instDecidableBefore (d : Fin n → ℚ) (j i : Fin n) : Decidable (before d j i) := by unfold before; infer_instance
def priorMass (U : Finset (Fin n)) (y d : Fin n → ℚ) (i : Fin n) : ℚ :=
  ∑ j∈U.filter (fun j => before d j i), y j

theorem priorMass_erase (U : Finset (Fin n)) (y d : Fin n → ℚ) (a i : Fin n)
    (ha : a∈U) (hai : before d a i) : priorMass U y d i=priorMass (U.erase a) y d i+y a := by
  have he : (U.erase a).filter (fun j => before d j i)=(U.filter (fun j => before d j i)).erase a := by
    ext j
    simp only [mem_filter,mem_erase,and_assoc]
  unfold priorMass
  rw [he]
  exact (sum_erase_add _ y (mem_filter.mpr ⟨ha,hai⟩)).symm

theorem priorMass_nonneg (U : Finset (Fin n)) (y d : Fin n → ℚ) (i : Fin n)
    (hy : ∀ j∈U, 0 ≤ y j) : 0 ≤ priorMass U y d i :=
  sum_nonneg (fun j hj => hy j (mem_filter.mp hj).1)

end MetricKMedian.Preparation
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_RepresentativeGeometry
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 {J I X : Type*} [DecidableEq J] [PseudoMetricSpace X]

omit [DecidableEq J] in

theorem bundle_disjoint_geometry (s t i : X) {δ Ls Lt : ℝ}
    (hδ : 0 ≤ δ) (hδ1 : δ < 1/2) (hst : 0 < dist s t)
    (hLs : Ls ≤ dist s t) (hLt : Lt ≤ dist s t)
    (hsi : dist s i ≤ δ*Ls) (hti : dist t i ≤ δ*Lt) : False := by
  have hs := hsi.trans (mul_le_mul_of_nonneg_left hLs hδ)
  have ht := hti.trans (mul_le_mul_of_nonneg_left hLt hδ)
  have htri := dist_triangle s i t
  rw [dist_comm i t] at htri
  have hh := mul_lt_mul_of_pos_right hδ1 hst
  linarith only [hs,ht,htri,hh]

omit [DecidableEq J] [PseudoMetricSpace X] in
                                                                   
theorem outside_mass_bound [DecidableEq I] (F : Finset I) (y d : I → ℝ) {r : ℝ}
    (hy : ∀ i ∈ F, 0 ≤ y i) (hd : ∀ i ∈ F, 0 ≤ d i) :
    r*(∑ i ∈ F.filter (fun i => r < d i), y i) ≤ ∑ i ∈ F, y i*d i := by
  calc
    _ = ∑ i ∈ F.filter (fun i => r < d i), y i*r := by rw [mul_sum]; apply sum_congr rfl; intros; ring
    _ ≤ ∑ i ∈ F.filter (fun i => r < d i), y i*d i := by
      apply sum_le_sum
      intro i hi
      exact mul_le_mul_of_nonneg_left (mem_filter.mp hi).2.le (hy i (mem_filter.mp hi).1)
    _ ≤ ∑ i ∈ F, y i*d i := sum_le_sum_of_subset_of_nonneg (filter_subset _ _) (fun i hi _ => mul_nonneg (hy i hi) (hd i hi))

omit [DecidableEq J] [PseudoMetricSpace X] in
 theorem deficit_small {M δ L V c : ℝ} (hM : 0 < M) (hδ : 0 < δ) (hL : 0 < L)
    (hc : δ*L*c ≤ V) (hsep : M*V ≤ L) : c ≤ 1/(M*δ) := by
  have ha : c ≤ V/(δ*L) := (le_div_iff₀ (mul_pos hδ hL)).mpr (by nlinarith only [hc])
  have hb : V ≤ L/M := (le_div_iff₀ hM).mpr (by nlinarith only [hsep])
  calc
    c ≤ V/(δ*L) := ha
    _ ≤ (L/M)/(δ*L) := div_le_div_of_nonneg_right hb (mul_pos hδ hL).le
    _ = 1/(M*δ) := by field_simp

end MetricKMedian.Preparation
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_RepresentativeBundles
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 {T I X : Type*} [Fintype T] [DecidableEq T] [DecidableEq I]
  [PseudoMetricSpace X]

structure BundleGeometry (F : T → Finset I) (y : I → ℝ) (s : T → X) (i : I → X)
    (V : T → ℝ) (M δ : ℝ) where
  P : T → Finset I
  A : T → Finset I
  p : T → ℝ
  c : T → ℝ
  L : T → ℝ
  next : T → T
  sub : ∀ t, P t ⊆ F t
  missing : ∀ t, A t=F t \ P t
  mass : ∀ t, ∑ a ∈ P t, y a=p t
  deficit_mass : ∀ t, ∑ a ∈ A t, y a=c t
  unit : ∀ t, p t+c t=1
  nonneg : ∀ t, 0 ≤ c t
  small : ∀ t, c t ≤ 1/(M*δ)
  large : ∀ t, 1-1/(M*δ) ≤ p t
  disjoint : Pairwise (fun t u => Disjoint (P t) (P u))
  next_distance : ∀ t, L t=dist (s t) (s (next t))
  closest : ∀ t u, t ≠ u → L t ≤ dist (s t) (s u)
  radius : ∀ t, next t ≠ t → ∀ a ∈ P t, dist (s t) (i a) ≤ δ*L t
  outside_radius : ∀ t, next t ≠ t → ∀ a ∈ A t, δ*L t < dist (s t) (i a)
  self_singleton : ∀ t, next t=t → ∀ u, u=t
  self_zero : ∀ t, next t=t → c t=0
  zero_full : ∀ t, c t=0 → P t=F t
  charge : ∀ t, δ*L t*c t ≤ V t

end MetricKMedian.Preparation
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Geometry_RationalBundleGeometry
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.Preparation.RationalBundles
open Finset
variable {n m : ℕ}

def mass (y : Fin m → ℚ) (P : Fin n → Finset (Fin m)) (t : Fin n) : ℚ := ∑ a ∈ P t, y a

end MetricKMedian.Preparation.RationalBundles
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 Polynomial Finset

structure Input where
  n : ℕ
  m : ℕ
  k : ℕ
  npos : 0 < n
  mpos : 0 < m
  kpos : 0 < k
  kle : k ≤ n
  distance : Fin m → Fin n → ℚ

namespace Input
instance instNeZeroNatN (I : Input) : NeZero I.n := ⟨I.npos.ne'⟩
instance instNeZeroNatM (I : Input) : NeZero I.m := ⟨I.mpos.ne'⟩
end Input

def gradientBound (r L : ℕ) := L*(L*(4*r*(L+1)))^2
def baseBound (r L : ℕ) := 2*r*gradientBound r L*L
def stepsBound (r L : ℕ) := 8*r^2*gradientBound r L*L^2
def exponentBound (r L : ℕ) := baseBound r L+L*(L*L)+L+1
def heightBound (r L : ℕ) := exponentBound r L*(stepsBound r L+1)

noncomputable def stepsPolynomial (r : ℕ) : Polynomial ℕ := 8*C r^2*(X*(X*(4*C r*(X+1)))^2)*X^2
noncomputable def heightPolynomial (r : ℕ) : Polynomial ℕ :=
  (2*C r*(X*(X*(4*C r*(X+1)))^2)*X+X*(X*X)+X+1)*(stepsPolynomial r+1)
 theorem stepsPolynomial_eval (r L : ℕ) : (stepsPolynomial r).eval L=stepsBound r L := by
  simp only [stepsPolynomial,stepsBound,gradientBound,eval_add,eval_mul,eval_pow,eval_ofNat,eval_C,eval_X,eval_one]
 theorem heightPolynomial_eval (r L : ℕ) : (heightPolynomial r).eval L=heightBound r L := by
  simp only [heightPolynomial,heightBound,exponentBound,baseBound,gradientBound,eval_add,eval_mul,eval_pow,eval_ofNat,eval_C,eval_X,eval_one,stepsPolynomial_eval]
end MetricKMedian.LPBinary
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
theorem range_ofFn (n : ℕ) : List.range n=List.ofFn (fun i : Fin n => i.val) := by
  apply List.ext_getElem
  · simp
  · intros; simp

end MetricKMedian.LPBinary
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 Function

theorem head_ofFn {α : Type} {n : ℕ} [NeZero n] (f : Fin n → α) (a : α) :
    (List.ofFn f).head?.getD a=f ⟨0,NeZero.pos n⟩ := by
  cases n with
  | zero => exact (NeZero.ne 0 rfl).elim
  | succ n => rw [List.ofFn_succ]; rfl

end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_NearestListProgram
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 Function Finset

theorem sum_map_filter_ofFn {α : Type} {n : ℕ} (f : Fin n → α) (p : α → Bool) (v : α → ℚ) :
    (((List.ofFn f).filter p).map v).sum=∑ i ∈ univ.filter (fun i => p (f i)), v (f i) := by
  rw [Finset.sum_filter]
  have he (xs : List α) : ((xs.filter p).map v).sum=(xs.map (fun a => if p a then v a else 0)).sum := by
    induction xs with
    | nil => rfl
    | cons a xs ih => cases h : p a <;> simp [h,ih]
  rw [he,List.map_ofFn,List.sum_ofFn]
  rfl

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 Function Finset

def bounded (q : ℚ) : Bool := decide (0 ≤ q ∧ q ≤ 1)

theorem all_ofFn {α : Type} {n : ℕ} (f : Fin n → α) (p : α → Bool) :
    (List.ofFn f).all p=true ↔ ∀ i, p (f i)=true := by
  simp only [List.all_eq_true,List.mem_ofFn,forall_exists_index,forall_apply_eq_imp_iff]

end MetricKMedian.LPBinary.Repair
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_PreparationStars
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.SupplierStars
open Finset
variable {I T : Type} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T]

def outside (P : T → Finset I) : Finset I := univ.filter (fun i => ∀ t, i ∉ P t)

 theorem target_card_sum {E : Type} [Fintype E] (D : E → Finset T) (w : E → ℝ) :
    (∑ e, ((D e).card:ℝ)*w e)=∑ t, ∑ e, if t ∈ D e then w e else 0 := by
  rw [sum_comm]
  apply sum_congr rfl
  intro e _
  simp only [sum_ite_mem,univ_inter,sum_const,nsmul_eq_mul]

end MetricKMedian.Preparation.SupplierStars
end
end

end OAI
end

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

namespace OAI

namespace MetricKMedian.PhysicalBatchLaw
open Finset
variable {E : Type*} [Fintype E] [DecidableEq E]

noncomputable def unbalanced (Z : Finset E) (ω : E → Bool) : Finset E :=
  univ.filter (fun e => ω e=true ∧ e ∉ Z)

end MetricKMedian.PhysicalBatchLaw

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseBernoulliFeatures
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 d : ℕ}

def without (f : Fin d → Fin (n+1)) (i : Fin n) : Fin d → Fin (n+1) :=
  fun a => if (f a).val=i.val then ⟨n,Nat.lt_succ_self n⟩ else f a

end MetricKMedian.SparseBernoulli

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseBernoulliSubsets
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 d : ℕ}

def tuple (S : Finset (Fin n)) : Fin d → Fin (n+1) :=
  fun a => if h : a.val<S.card then (S.orderEmbOfFin rfl ⟨a.val,h⟩).castSucc
    else ⟨n,Nat.lt_succ_self n⟩

end MetricKMedian.SparseBernoulli

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseGraphRun
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.SparseGraph
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]

end MetricKMedian.SparseGraph
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseTargetSubset
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.SparseTargetSubset
open Finset
variable {n : ℕ}

def initial (D : Finset (Fin n)) (q : ℚ) : Vector ℚ n :=
  Vector.ofFn (fun i => if i∈D then q else 0)

end MetricKMedian.SparseTargetSubset
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_TargetSubsetProgram
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.SparseTargetSubset.Program
structure Input where
  n : ℕ
  D : Finset (Fin n)
  q : ℚ
  feasible : 0≤q ∧ q≤1
end MetricKMedian.SparseTargetSubset.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_ExceptionalStar
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 {E T : Type*} [Fintype E] [DecidableEq E] [Fintype T] [DecidableEq T]

noncomputable def upperBit (q : ℝ) : ℝ := if 0 < q then 1 else 0

 theorem upperBit_bounds {q : ℝ} (_hq0 : 0 ≤ q) (hq1 : q ≤ 1) :
    q ≤ upperBit q ∧ upperBit q ≤ 1 := by
  unfold upperBit
  split_ifs with h
  · exact ⟨hq1, le_rfl⟩
  · exact ⟨le_of_not_gt h, zero_le_one⟩

end MetricKMedian.Preparation
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseStarActivation
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.SparseStarActivation
open Finset
variable {n m : ℕ}

def upper (q : ℚ) : ℚ := if 0 < q then 1 else 0

end MetricKMedian.SparseStarActivation
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_StarActivationProgram
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.SparseStarActivation.Program
structure Input where
  n : ℕ
  m : ℕ
  D : Fin m → Finset (Fin n)
  q : Fin m → ℚ
  feasible : ∀ e, 0≤q e ∧ q e≤1

def Input.column (x : Input) (e : Fin x.m) : SparseTargetSubset.Program.Input :=
  ⟨x.n,x.D e,x.q e,x.feasible e⟩
def Input.columns (x : Input) := List.ofFn x.column

def dummy : SparseTargetSubset.Program.Input := ⟨0,∅,0,by norm_num⟩
end MetricKMedian.SparseStarActivation.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseSignedPreparation
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.SparseSignedPreparation
open Finset
variable {n m : ℕ}

abbrev State (n m : ℕ) := Vector ℚ m × ((Fin m → Finset (Fin n)) × (Fin m → Bool))

def signed (D : Fin m → Finset (Fin n)) (c : Fin m → ℚ) : Fin m → ℚ :=
  fun e => c e-((D e).card:ℚ)

end MetricKMedian.SparseSignedPreparation
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_RationalRetain
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.RationalRetain
open Finset

def keep : {n : ℕ} → (Fin n → ℕ) → ℕ → (Fin n → ℕ)
  | 0,_,_ => Fin.elim0
  | n+1,q,k => Fin.cons (min (q 0) k) (keep (fun i : Fin n => q i.succ) (k-min (q 0) k))

end MetricKMedian.RationalRetain
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseGridRounding
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.SparseGridRounding
open Finset
variable {n : ℕ}

def base (q : Fin n → ℚ) (i : Fin n) : ℕ := ⌊q i⌋₊
def fraction (q : Fin n → ℚ) : Vector ℚ n := Vector.ofFn (fun i => q i-(base q i:ℚ))

end MetricKMedian.SparseGridRounding
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseOuterLaw
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.SparseOuterLaw
open Finset
open SparseGridRounding (base fraction)
open SparseSignedPreparation (State)
variable {n m : ℕ}

def activation (D : Fin m → Finset (Fin n)) (q : Fin m → ℚ)
    (z : State n m) (e : Fin m) (i : Fin n) : ℚ :=
  (if i∈D e then (base q e:ℚ) else 0)+(if i∈z.2.1 e then 1 else 0)

end MetricKMedian.SparseOuterLaw
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseOuterCounts
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.SparseOuterLaw
open Finset
open SparseGridRounding (base fraction)
open SparseSignedPreparation (State)
variable {n m : ℕ}

def activationCount (D : Fin m → Finset (Fin n)) (q : Fin m → ℚ)
    (z : State n m) (e : Fin m) (i : Fin n) : ℕ :=
  (if i∈D e then base q e else 0)+(if i∈z.2.1 e then 1 else 0)

theorem activationCount_cast (D : Fin m → Finset (Fin n)) (q : Fin m → ℚ)
    (z : State n m) (e : Fin m) (i : Fin n) :
    (activationCount D q z e i:ℚ)=activation D q z e i := by
  simp only [activationCount,activation,Nat.cast_add,Nat.cast_ite,Nat.cast_zero,Nat.cast_one]

end MetricKMedian.SparseOuterLaw
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseCountFeatures
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 : ℕ}

abbrev Table (n m : ℕ) := Fin m → (Fin n → ℕ)

def edge (G : Table n m) (h : Fin n) (i : Fin m) : ℚ := (G i h:ℚ)

def edgeCode (G : Table n m) (a : Fin (n*m)) : ℚ :=
  edge G (finProdFinEquiv.symm a).1 (finProdFinEquiv.symm a).2

def features (G : Table n m) (a : Fin (n*m+(n*m)*(n*m))) : ℚ :=
  Sum.elim (edgeCode G) (fun ij : Fin ((n*m)*(n*m)) =>
    edgeCode G (finProdFinEquiv.symm ij).1*edgeCode G (finProdFinEquiv.symm ij).2)
    (finSumFinEquiv.symm a)

@[simp] theorem features_single (G : Table n m) (h : Fin n) (i : Fin m) :
    features G (finSumFinEquiv (Sum.inl (finProdFinEquiv (h,i))))=edge G h i := by
  simp only [features,edgeCode,Equiv.symm_apply_apply,Sum.elim_inl]

@[simp] theorem features_pair (G : Table n m) (h k : Fin n) (i j : Fin m) :
    features G (finSumFinEquiv (Sum.inr (finProdFinEquiv
      (finProdFinEquiv (h,i),finProdFinEquiv (k,j)))))=edge G h i*edge G k j := by
  simp only [features,edgeCode,Equiv.symm_apply_apply,Sum.elim_inr]

def next (G : Table n m) (S : (Fin n → ℕ)) (i : Fin m) : Table n m :=
  Function.update G i S

@[simp] theorem edge_next (G : Table n m) (S : (Fin n → ℕ)) (h : Fin n) (i j : Fin m) :
    edge (next G S i) h j=if j=i then (S h:ℚ) else edge G h j := by
  by_cases hji : j=i <;> simp [edge,next,hji]

end MetricKMedian.SparseCounts
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseRescaledInner
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.SparseRescaledInner
open Finset
variable {n t : ℕ}

def piece (P : Fin t → Finset (Fin n)) (y : Fin n → ℚ) (p : Fin t → ℚ)
    (K : Fin t → ℕ) : Fin n → Fin t → ℚ :=
  fun i j => if i∈P j then (K j:ℚ)*y i/p j else 0

theorem piece_nonnegative (P : Fin t → Finset (Fin n)) (y : Fin n → ℚ) (p : Fin t → ℚ)
    (K : Fin t → ℕ) (hy : ∀ i,0 ≤ y i) (hp : ∀ j,0 < p j) :
    ∀ i j,0 ≤ piece P y p K i j := by
  intro i j
  dsimp only [piece]
  split_ifs
  · exact div_nonneg (mul_nonneg (Nat.cast_nonneg _) (hy i)) (hp j).le
  · exact le_rfl

end MetricKMedian.SparseRescaledInner
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparsePreparedLaw
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.SparsePrepared
open Finset SparseOuterLaw
open SparseSignedPreparation (State)
variable {n m f : ℕ}

def requests (D : Fin m → Finset (Fin n)) (q : Fin m → ℚ) (Δ : ℕ)
    (z : State n m) : Fin n → Fin m → ℕ :=
  fun j => RationalRetain.keep (fun e => activationCount D q z e j) (Δ/2)

def total (D : Fin m → Finset (Fin n)) (q : Fin m → ℚ) (Δ : ℕ)
    (z : State n m) : Fin n → ℕ :=
  fun j => Δ-min (∑ e,activationCount D q z e j) (Δ/2)

end MetricKMedian.SparsePrepared
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_PreparedDataOperations
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.SparsePrepared.Program
abbrev QRow := List ℚ
abbrev BTable := List (List Bool)

abbrev BaseRaw := BTable × (QRow × (BTable × (QRow × (QRow × ℕ))))
structure KernelInput where
  n : ℕ
  m : ℕ
  f : ℕ
  D : Fin m → Finset (Fin n)
  q : Fin m → ℚ
  P : Fin n → Finset (Fin f)
  y : Fin f → ℚ
  p : Fin n → ℚ
  Δ : ℕ
  z : SparseSignedPreparation.State n m
  hy : ∀ i,0≤y i
  hp : ∀ j,0<p j

end MetricKMedian.SparsePrepared.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_CountRunHeight
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
variable {n m : ℕ}

theorem next_bound (G : Table n m) (S : Fin n → ℕ) (i : Fin m) (U : ℕ)
    (hG : ∀ j h,G j h≤U) (hS : ∀ h,S h≤U) : ∀ j h,next G S i j h≤U := by
  intro j h
  by_cases hj : j=i
  · subst j; simpa only [next,Function.update_self] using hS h
  · simpa only [next,Function.update_of_ne hj] using hG j h

def stepHeight (n m N L H : ℕ) :=
  let d := n*m+(n*m)*(n*m)
  L+((2*(d+1)*(d+1+(H+H)*((d+1)*N+1)))*((d+1)*N+1))*((d+1)*N)

end MetricKMedian.SparseCounts
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_CountListOperations
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.ListOperation

def indices {α : Type} (xs : List α) : List ℕ := List.range xs.length
end MetricKMedian.SparseCounts.ListOperation
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_CountRunProgram
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 Function Polynomial

def supportBound (L : ℕ) := L*L+(L*L)*(L*L)+1
def heightBound (L : ℕ) := SparseCounts.stepHeight L L L L L*L
def graphSize (L : ℕ) := L*(2*(L*(2*(L+1)+1))+1)
def sizeBound (L : ℕ) :=
  2*(3*L+2)+1+(2*(2*(heightBound L+4)+1+supportBound L*(2*(heightBound L+4)+1))+1+
    supportBound L*(2*graphSize L+1))
noncomputable def SPoly : Polynomial ℕ := X*X+(X*X)*(X*X)+1
noncomputable def HPoly : Polynomial ℕ := (X+(2*SPoly*(SPoly+(X+X)*(SPoly*X+1)))*(SPoly*X+1)*(SPoly*X))*X
noncomputable def APoly : Polynomial ℕ := X*(2*(X*(2*(X+1)+1))+1)
noncomputable def sizePolynomial : Polynomial ℕ :=
  2*(3*X+2)+1+(2*(2*(HPoly+4)+1+SPoly*(2*(HPoly+4)+1))+1+SPoly*(2*APoly+1))
theorem sizePolynomial_eval (L : ℕ) : sizePolynomial.eval L=sizeBound L := by
  simp only [sizePolynomial,sizeBound,heightBound,supportBound,graphSize,HPoly,SPoly,APoly,
    SparseCounts.stepHeight,eval_add,eval_mul,eval_ofNat,eval_X,eval_one]

end MetricKMedian.SparseCounts.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_GridRoundingProgram
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.SparseGridRounding.Program
structure Input where
  n : ℕ
  q : Fin n → ℚ
  nonnegative : ∀ i, 0≤q i
abbrev Input.raw (x : Input) := List.ofFn x.q

def fractionRow (q : List ℚ) : List ℚ := q.map (fun x => x-(⌊x⌋₊:ℚ))
end MetricKMedian.SparseGridRounding.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_BundlesProgram
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.SparseBundles.Program
open Function
open SparseCounts.Program

structure QInput where
  n : ℕ
  m : ℕ
  q : Fin n → Fin m → ℚ
  feasible : ∀ h i, 0≤q h i

def QInput.raw (x : QInput) : List Unit × List (List ℚ) :=
  (List.replicate x.n (),List.ofFn fun i => List.ofFn fun h => x.q h i)

def QInput.column (x : QInput) (i : Fin x.m) : SparseGridRounding.Program.Input :=
  ⟨x.n,fun h => x.q h i,fun h => x.feasible h i⟩
def QInput.columns (x : QInput) : List SparseGridRounding.Program.Input := List.ofFn x.column
def emptyColumn : SparseGridRounding.Program.Input := ⟨0,Fin.elim0,fun i => Fin.elim0 i⟩
end MetricKMedian.SparseBundles.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_PreparedKernelProgram
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.SparsePrepared.Program

def KernelInput.bundles (x : KernelInput) : SparseBundles.Program.QInput :=
  ⟨x.f,x.n,SparseRescaledInner.piece x.P x.y x.p (total x.D x.q x.Δ x.z),
    SparseRescaledInner.piece_nonnegative x.P x.y x.p _ x.hy x.hp⟩
end MetricKMedian.SparsePrepared.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_OuterLawProgram
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.SparseOuterLaw.Program
structure Input where
  n : ℕ
  m : ℕ
  D : Fin m → Finset (Fin n)
  c : Fin m → ℚ
  q : Fin m → ℚ
  c_unit : ∀ e,0 ≤ c e ∧ c e≤1
  q_nonnegative : ∀ e,0≤q e
end MetricKMedian.SparseOuterLaw.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_PreparedLawProgram
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.SparsePrepared.Program
structure Input where
  n : ℕ
  m : ℕ
  f : ℕ
  D : Fin m → Finset (Fin n)
  c : Fin m → ℚ
  q : Fin m → ℚ
  P : Fin n → Finset (Fin f)
  y : Fin f → ℚ
  p : Fin n → ℚ
  Δ : ℕ
  hy : ∀ i,0≤y i
  hp : ∀ j,0<p j
  hc : ∀ e,0 ≤ c e ∧ c e≤1
  hq : ∀ e,0≤q e

def Input.outer (x : Input) : SparseOuterLaw.Program.Input := ⟨x.n,x.m,x.D,x.c,x.q,x.hc,x.hq⟩
def dummy : KernelInput :=
  ⟨0,0,0,Fin.elim0,Fin.elim0,Fin.elim0,Fin.elim0,Fin.elim0,0,(#v[],Fin.elim0,Fin.elim0),(fun i => Fin.elim0 i),(fun i => Fin.elim0 i)⟩
end MetricKMedian.SparsePrepared.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_RepresentativeProgram
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.Preparation.RationalRepresentatives.Program
open Finset Polynomial

structure Input where
  n : ℕ
  R : Fin n → ℚ
  d : Fin n → Fin n → ℚ
  M : ℚ
  U : Finset (Fin n)
abbrev Cut (x : Input) := Finset (Fin x.n) × Finset (Fin x.n)
structure State where
  input : Input
  cut : Cut input
end MetricKMedian.Preparation.RationalRepresentatives.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseBundleEncoding
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.SparseBundleEncoding
open Finset
variable {n m : ℕ}

def decode (q : Fin n → Fin m → ℚ) (ξ : Fin m → Finset (Fin n)) :
    SparseCounts.Table n m :=
  fun j i => SparseGridRounding.base (fun i => q i j) i + if i ∈ ξ j then 1 else 0

end MetricKMedian.SparseBundleEncoding

end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseOuterMoments
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.SparseOuterLaw
open Finset
open SparseGridRounding (base)
open SparseSignedPreparation (State)
variable {n m : ℕ}

def targetMean (D : Fin m → Finset (Fin n)) (q : Fin m → ℚ) (i : Fin n) : ℚ :=
  ∑ e, if i∈D e then q e else 0

def deficit (D : Fin m → Finset (Fin n)) (q : Fin m → ℚ) (g : ℚ)
    (z : State n m) (i : Fin n) : ℚ := g*∑ e, activation D q z e i

end MetricKMedian.SparseOuterLaw
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_SupplierListOperations
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.Preparation.RationalSuppliers.Program
open Finset

theorem finSum_symm_castLE {m n : ℕ} (h : m ≤ m+n) (i : Fin m) :
    (finSumFinEquiv.symm (Fin.castLE h i) : Fin m ⊕ Fin n)=.inl i :=
  finSumFinEquiv_symm_apply_castAdd i

end MetricKMedian.Preparation.RationalSuppliers.Program
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 Function Finset
namespace Input

def scale (I : Input) (B : ℚ) : Input := { I with distance := fun j i => I.distance j i/B }
end Input
end MetricKMedian.LPBinary
end

end OAI
end