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

import Mathlib
import Definitions.Def_OAIQ037K052
import Definitions.Def_OAIQ037K053
import Definitions.Def_OAIQ037K054
import Definitions.Def_OAIQ037K055

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
noncomputable def nearestRowsProgram : PolyProgram (encodePair ers er) ers (fun x : Rows × Row => nearestRows x.1 x.2) :=
  ((exchange ers er).comp (Nearest.fillingProgram.listMapWith [] [])).congr _ (fun _ => rfl)
noncomputable def rawProgram (r : ℕ) (hr : 0 < r) : PolyProgram Input.encode eo (raw r) := by
  let ds := Program.inputRaw.comp (fst ers Nat.bits)
  let H := (Program.inputRaw.comp (Program.rawPenaltyProgram r)).comp ratOfNat
  let ρ := Program.inputRaw.comp (lossProgram r)
  let y := Program.optimizeProgram r hr
  let tr := (ds.fanout H).comp Program.truncateMatrixProgram
  let xs := (tr.fanout y).comp nearestRowsProgram
  exact (((y.fanout ρ).comp openingProgram).fanout ((ds.fanout xs).comp assignmentsProgram)).congr _ (fun _ => rfl)
end Repair
end MetricKMedian.LPBinary
end

end OAI
end

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

noncomputable def candidateProgram (r : ℕ) (hr : 0 < r) :
    PolyProgram (encodePair Input.encode Ratio.encode) Repair.eo (fun x : Input × ℚ => candidate r x.1 x.2) := by
  let test := ((constant (encodePair Input.encode Ratio.encode) Ratio.encode 0).fanout (snd Input.encode Ratio.encode)).comp ratLT
  exact (ite test ((fst Input.encode Ratio.encode).comp Input.zeroOutputProgram)
    (Input.scaleProgram.comp (Repair.rawProgram r hr))).congr _ (fun _ => by
      simp only [Function.comp_apply,candidate,decide_eq_true_eq])

noncomputable def valueOfProgram (r : ℕ) (hr : 0 < r) :
    PolyProgram (encodePair Input.encode Ratio.encode) Ratio.encode (fun x : Input × ℚ => Repair.value (candidate r x.1 x.2) x.1.rows) :=
  (((candidateProgram r hr).fanout ((fst Input.encode Ratio.encode).comp (Program.inputRaw.comp (fst ers Nat.bits)))).comp Repair.valueProgram).congr _ (fun _ => rfl)

noncomputable def feasibleProgram (r : ℕ) (hr : 0 < r) : PolyProgram Input.encode er (feasible r) := by
  let k := (fst Input.encode Ratio.encode).comp (Program.inputRaw.comp (snd ers Nat.bits))
  let test := (((candidateProgram r hr).fanout k).comp Repair.validProgram)
  let guesses := (Program.inputRaw.comp (fst ers Nat.bits)).comp guessesProgram
  let emptyI : Input := ⟨1,1,1,by decide,by decide,by decide,le_rfl,fun _ _ => 0⟩
  exact (((identity Input.encode).fanout guesses).comp (test.listFilterWith 0 emptyI)).congr _ (fun _ => rfl)

noncomputable def selectedScaleProgram (r : ℕ) (hr : 0 < r) : PolyProgram Input.encode Ratio.encode (selectedScale r) := by
  let xs := feasibleProgram r hr
  let values := (((identity Input.encode).fanout xs).comp ((valueOfProgram r hr).listMapWith 0 0))
  let v := values.comp Program.minimumProgram
  let ec := encodePair Input.encode Ratio.encode
  let I := (fst ec Ratio.encode).comp (fst Input.encode Ratio.encode)
  let q := snd ec Ratio.encode
  let C := (I.fanout q).comp (valueOfProgram r hr)
  let V := (fst ec Ratio.encode).comp (snd Input.encode Ratio.encode)
  let test := (C.fanout V).comp ratEQ
  let emptyI : Input := ⟨1,1,1,by decide,by decide,by decide,le_rfl,fun _ _ => 0⟩
  let filtered := ((((identity Input.encode).fanout v).fanout xs).comp (test.listFilterWith 0 (emptyI,0)))
  exact (filtered.comp Program.minimumProgram).congr _ (fun _ => rfl)

noncomputable def selectedProgram (r : ℕ) (hr : 0 < r) : PolyProgram Input.encode Repair.eo (selected r) :=
  ((((identity Input.encode).fanout (selectedScaleProgram r hr)).comp (candidateProgram r hr))).congr _ (fun _ => rfl)

end Scale
end MetricKMedian.LPBinary
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.SparseIntegerLaw
open Finset
variable {α β : Type}

theorem bindCompress_spec {d : ℕ} (μ : SparseIntegerLaw α) (κ : Fin μ.length → SparseIntegerLaw β)
    (v : β → Fin d → ℚ) :
    let ν := μ.bindCompress κ v
    ν.length ≤ d+1 ∧
    (∀ i : Fin ν.length, ∃ a : Fin μ.length, ∃ b : Fin (κ a).length,
      ν.states[i.val]=(κ a).states[b.val]) ∧
    ∀ j, ν.moment (fun z => v z j)=
      ∑ a, μ.law.rational.weight a*(κ a).moment (fun z => v z j) := by
  have h := (μ.bindIndexed κ).compressAuto_correct v
  refine ⟨h.1,?_,fun j => (h.2.2 j).trans (bindIndexed_moment μ κ _)⟩
  intro i
  obtain ⟨b,hb⟩ := h.2.1 i
  let z := (finSigmaFinEquiv (n := fun a => (κ a).length)).symm b
  refine ⟨z.1,z.2,?_⟩
  exact hb.trans (by
    simp only [bindIndexed,Vector.getElem_ofFn]
    congr 3)

end MetricKMedian.SparseIntegerLaw

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_LastFractionProgram
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.RoundingList.Last
open Binary Binary.Automatic Binary.Automatic.Poly Finset

def active (p : Row) : Bool := decide (0<(RoundingList.fractional p).length)
@[fun_prop] theorem active_poly : Poly active := by unfold active; fun_prop
 theorem active_list {n : ℕ} (p : Vector ℚ n) : active p.toList=decide (RationalWeightedStep.fractional p).Nonempty := by
  simp only [active,fractional_list,List.length_map,Finset.length_sort,card_pos]
 theorem first_list {n : ℕ} (p : Vector ℚ n) (h : (RationalWeightedStep.fractional p).Nonempty) :
    first p.toList=(RationalLastFraction.pick p h).val := by
  unfold first indices
  rw [Vector.length_toList]
  apply findIdx_min _ h
  intro i
  simp [frac,RationalWeightedStep.fractional,RationalWeightedStep.point]

def probability (p : Row) : ℚ := if active p then p[first p]?.getD 0 else 0
@[fun_prop] theorem probability_poly : Poly probability := by unfold probability; fun_prop
 theorem probability_list {n : ℕ} (p : Vector ℚ n) : probability p.toList=RationalLastFraction.probability p := by
  unfold probability RationalLastFraction.probability
  rw [active_list]
  by_cases h : (RationalWeightedStep.fractional p).Nonempty
  · simp only [decide_eq_true h,ite_true,dite_eq_left h,first_list p h,List.getElem?_eq_getElem
      (show (RationalLastFraction.pick p h).val<p.toList.length by simp),
      Option.getD_some,Vector.getElem_toList,RationalWeightedStep.point]
  · simp only [decide_eq_false h,Bool.false_eq_true,ite_false,dite_eq_right h]

def endpoint (b : Bool) (p : Row) : Row := if active p then
  (indices p).map (fun k => if k=first p then (if b then 0 else 1) else p[k]?.getD 0)
  else p
@[fun_prop] theorem endpoint_poly (b : Bool) : Poly (endpoint b) := by
  unfold endpoint
  have he : Poly (fun p : Row => (indices p).map (fun k => if k=first p then (if b then (0:ℚ) else 1) else p[k]?.getD 0)) := by
    apply list_map <;> fun_prop
  fun_prop
 theorem endpoint_list {n : ℕ} (p : Vector ℚ n) (b : Fin 2) : endpoint (decide (b=1)) p.toList=(RationalLastFraction.endpoint p b).toList := by
  unfold endpoint RationalLastFraction.endpoint
  rw [active_list]
  by_cases h : (RationalWeightedStep.fractional p).Nonempty
  · simp only [decide_eq_true h,ite_true,dite_eq_left h,first_list p h,indices,Vector.length_toList,range_finRange,
      ← List.ofFn_eq_map,List.map_ofFn,Function.comp_def,Vector.toList_ofFn]
    apply congrArg List.ofFn
    funext i
    simp only [Fin.val_inj,List.getElem?_eq_getElem (show i.val<p.toList.length by simp),Option.getD_some,Vector.getElem_toList,RationalWeightedStep.point]
    fin_cases b <;> simp
  · simp only [decide_eq_false h,Bool.false_eq_true,ite_false,dite_eq_right h]
end MetricKMedian.RoundingList.Last

namespace MetricKMedian.RoundingProgram.WeightedRound
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly SparseIntegerLaw.BinarySparse

def lastRaw (x : Row × Data Row) : Row × Data Row :=
  (x.1,(branchLawData (x.2.1,x.2.2.map RoundingList.Last.probability),
    x.2.2.flatMap (fun p => [RoundingList.Last.endpoint false p,RoundingList.Last.endpoint true p])))
@[fun_prop] theorem lastRaw_poly : Poly lastRaw := by
  unfold lastRaw
  have hp : Poly (fun x : Row × Data Row => x.2.2.map RoundingList.Last.probability) := by apply list_map <;> fun_prop
  have he : Poly (fun x : Row × Data Row => x.2.2.flatMap (fun p => [RoundingList.Last.endpoint false p,RoundingList.Last.endpoint true p])) := by
    apply list_flatMap <;> fun_prop
  exact pair (by fun_prop) (pair (comp (⟨branchLawProgram⟩ : Poly branchLawData) (pair (by fun_prop) hp)) he)
end MetricKMedian.RoundingProgram.WeightedRound
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
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Row Table setView)
abbrev Raw := Row × ℚ
def Input.raw (x : Input) : Raw := (setView x.D,x.q)
abbrev Input.encode (x : Input) := enc x.raw

def prepare (x : Raw) : List ℚ × List ℚ := (x.1.map (fun _ => 1),x.1.map (fun b => if b then x.2 else 0))
@[fun_prop] theorem prepare_poly : Poly prepare := by
  unfold prepare
  apply pair <;> apply list_map <;> fun_prop
end MetricKMedian.SparseTargetSubset.Program
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
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Row Table setView indices)
abbrev Raw := List Unit × (Table × List ℚ)
def Input.raw (x : Input) : Raw :=
  (List.replicate x.n (),(List.ofFn (fun e => setView (x.D e)),List.ofFn x.q))
abbrev Input.encode (x : Input) := enc x.raw

def prepare (x : Raw) : List SparseTargetSubset.Program.Raw :=
  (indices x.2.2).map (fun e => (x.2.1[e]?.getD [],x.2.2[e]?.getD 0))
@[fun_prop] theorem prepare_poly : Poly prepare := by unfold prepare; apply list_map <;> fun_prop
 theorem prepare_input (x : Input) : prepare x.raw=x.columns.map SparseTargetSubset.Program.Input.raw := by
  simp only [prepare,Input.raw,indices,List.length_ofFn,RoundingList.range_finRange,← List.ofFn_eq_map,
    List.map_ofFn,Function.comp_def,List.getElem?_ofFn,dite_eq_left (Fin.isLt _),Option.getD_some,Fin.eta,Input.columns]
  rfl
noncomputable def columnsProgram : PolyProgram Input.encode (encodeList SparseTargetSubset.Program.Input.encode) Input.columns :=
  prepare_poly.program.recode Input.raw (fun _ => rfl) (fun x => by
    change encodeList enc (prepare x.raw)=_
    rw [prepare_input,RoundingProgram.encodeList_map])

def Input.result (x : Input) : Data Table :=
  (((law x.D x.q).law.denominator,List.ofFn (law x.D x.q).law.numerator),
    (law x.D x.q).states.toList.map SparseGraph.ListOperation.view)
end MetricKMedian.SparseStarActivation.Program
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

def boolState (x : (Row × Row) × List Bool) : Row :=
  (List.range x.1.1.length).map (fun i => if x.1.1[i]?.getD 0<0 then x.1.2[i]?.getD 0
    else if x.2[i]?.getD false then 1 else 0)
@[fun_prop] theorem boolState_poly : Poly boolState := by
  unfold boolState
  apply list_map
  · fun_prop
  · exact comp (f:=fun xs : Row => List.range xs.length) (g:=fun x : (Row × Row) × List Bool => x.1.1) list_indices (by fun_prop)

 theorem boolState_list {n : ℕ} (u : Fin n → ℚ) (p : Vector ℚ n) (q : Fin n → Bool) :
    boolState ((List.ofFn u,p.toList),List.ofFn q)=(RationalSignedTerminal.state u p q).toList := by
  rw [point_toList]
  apply List.ext_getElem
  · simp only [boolState,List.length_map,List.length_range,List.length_ofFn,Vector.length_toList]
  · intro i hi hi'
    have hi'' : i<n := by simpa only [boolState,List.length_map,List.length_range,List.length_ofFn] using hi
    simp only [boolState,List.getElem_map,List.getElem_range,List.getElem?_ofFn,dite_eq_left hi'',Option.getD_some,
      RationalSignedTerminal.state,Vector.toList_ofFn,List.getElem_ofFn,SparseBernoulli.flag]

def result (x : Input true) : Data Row :=
  let μ := RationalSignedTerminal.terminal x.β x.p x.feasible
  ((μ.law.denominator,List.ofFn μ.law.numerator),μ.states.toList.map Vector.toList)

end Terminal
end MetricKMedian.RoundingProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_SignedPreparationProgram
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.SparseSignedPreparation.Program
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Row Table setView)
abbrev StateRaw := QRow × (Table × Row)
def view {n m : ℕ} (s : SparseSignedPreparation.State n m) : StateRaw :=
  (s.1.toList,(SparseGraph.ListOperation.view s.2.1,List.ofFn s.2.2))
abbrev KernelRaw := List Unit × (Table × QRow)
def KernelInput.raw (x : KernelInput) : KernelRaw :=
  (List.replicate x.n (),(List.ofFn (fun e => setView (x.D e)),x.p.toList))
abbrev KernelInput.encode (x : KernelInput) := enc x.raw

noncomputable def starInputProgram : PolyProgram KernelInput.encode SparseStarActivation.Program.Input.encode KernelInput.star :=
  (identity enc).recode KernelInput.raw (fun _ => rfl) (fun x => by
    simp only [SparseStarActivation.Program.Input.encode,SparseStarActivation.Program.Input.raw,
      KernelInput.star,point_list]; rfl)
noncomputable def bernoulliInputProgram : PolyProgram KernelInput.encode SparseBernoulli.Program.Input.encode KernelInput.bernoulli :=
  ((snd enc enc).comp (snd enc enc)).recode KernelInput.raw (fun _ => rfl) (fun x => by
    simp only [SparseBernoulli.Program.Input.encode,KernelInput.bernoulli,point_list]; rfl)

def attach (x : QRow × Data (Table × Row)) : Data StateRaw := (x.2.1,x.2.2.map (fun s => (x.1,s)))
@[fun_prop] theorem attach_poly : Poly attach := by
  unfold attach; apply pair
  · fun_prop
  · apply list_map <;> fun_prop

def KernelInput.result (x : KernelInput) : Data StateRaw :=
  ((SparseIntegerLaw.BinarySparse.raw (kernel x.D x.p x.feasible)).1,(kernel x.D x.p x.feasible).states.toList.map view)
 theorem kernel_raw (x : KernelInput) :
    attach (x.p.toList,prodData (x.star.result,
       (((SparseBernoulli.run (d:=2) (RationalWeightedStep.point x.p) x.feasible x.m).law.denominator,
         List.ofFn (SparseBernoulli.run (d:=2) (RationalWeightedStep.point x.p) x.feasible x.m).law.numerator),
       (SparseBernoulli.run (d:=2) (RationalWeightedStep.point x.p) x.feasible x.m).states.toList.map List.ofFn)))=x.result := by
  simp only [KernelInput.star,SparseStarActivation.Program.Input.result,attach,prodData,
    KernelInput.result,kernel,SparseIntegerLaw.BinarySparse.raw,SparseIntegerLaw.prod,
    states_list,List.flatMap_def,List.map_ofFn,Function.comp_def,
    RoundingList.ofFn_product,Vector.toList_ofFn,view]
  rfl

abbrev Raw := List Unit × (Table × (QRow × QRow))
def Input.raw (x : Input) : Raw :=
  (List.replicate x.n (),(List.ofFn (fun e => setView (x.D e)),(List.ofFn x.c,x.p.toList)))
abbrev Input.encode (x : Input) := enc x.raw

def beta (x : Raw) : QRow :=
  (SparseGraph.ListOperation.indices x.2.2.1).map (fun e => x.2.2.1[e]?.getD 0-
    (Completion.Rational.BestProgram.card (x.2.1[e]?.getD []):ℚ))
@[fun_prop] theorem beta_poly : Poly beta := by unfold beta; apply list_map <;> fun_prop
 theorem beta_input (x : Input) : beta x.raw=List.ofFn (SparseSignedPreparation.signed x.D x.c) := by
  simp only [beta,Input.raw,SparseGraph.ListOperation.indices,List.length_ofFn,RoundingList.range_finRange,
    ← List.ofFn_eq_map,List.map_ofFn,Function.comp_def,List.getElem?_ofFn,dite_eq_left (Fin.isLt _),Option.getD_some,Fin.eta]
  congr 1
  funext e
  rw [Completion.Rational.BestProgram.card_view]
  rfl

def inputRows (x : Raw × QRow × Data QRow) : List KernelRaw :=
  x.2.2.2.map (fun p => (x.1.1,(x.1.2.1,p)))
@[fun_prop] theorem inputRows_poly : Poly inputRows := by unfold inputRows; apply list_map <;> fun_prop

end MetricKMedian.SparseSignedPreparation.Program
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
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (setView indices)
abbrev StateRaw := SparseSignedPreparation.Program.StateRaw

abbrev KernelRaw := BaseRaw × StateRaw

def KernelInput.base (x : KernelInput) : BaseRaw :=
  (List.ofFn (fun e => setView (x.D e)),(List.ofFn x.q,(List.ofFn (fun j => setView (x.P j)),
    (List.ofFn x.y,(List.ofFn x.p,x.Δ)))))
def KernelInput.raw (x : KernelInput) : KernelRaw := (x.base,SparseSignedPreparation.Program.view x.z)
abbrev KernelInput.encode (x : KernelInput) := enc x.raw

def activationData (x : KernelRaw) (e j : ℕ) : ℕ :=
  (if (x.1.1[e]?.getD [])[j]?.getD false then ⌊x.1.2.1[e]?.getD 0⌋₊ else 0)+
    if (x.2.2.1[e]?.getD [])[j]?.getD false then 1 else 0
def totalData (x : KernelRaw) (j : ℕ) : ℕ :=
  x.1.2.2.2.2.2-min ((indices x.1.2.1).map (fun e => activationData x e j)).sum (x.1.2.2.2.2.2/2)
def pieces (x : KernelRaw) : List (List ℚ) :=
  (indices x.1.2.2.2.2.1).map (fun j => (indices x.1.2.2.2.1).map (fun i =>
    if (x.1.2.2.1[j]?.getD [])[i]?.getD false then
      (totalData x j:ℚ)*x.1.2.2.2.1[i]?.getD 0/x.1.2.2.2.2.1[j]?.getD 0 else 0))
@[fun_prop] theorem activationData_poly : Poly (fun x : KernelRaw × (ℕ × ℕ) => activationData x.1 x.2.1 x.2.2) := by
  unfold activationData; fun_prop
@[fun_prop] theorem totalData_poly : Poly (fun x : KernelRaw × ℕ => totalData x.1 x.2) := by
  unfold totalData
  have h : Poly (fun x : KernelRaw × ℕ => ((indices x.1.1.2.1).map (fun e => activationData x.1 e x.2)).sum) := by
    apply comp nat_list_sum
    apply list_map <;> fun_prop
  fun_prop
@[fun_prop] theorem pieces_poly : Poly pieces := by
  unfold pieces
  apply list_map
  · apply list_map <;> fun_prop
  · fun_prop

theorem activationData_view (x : KernelInput) (e : Fin x.m) (j : Fin x.n) :
    activationData x.raw e.val j.val=SparseOuterLaw.activationCount x.D x.q x.z e j := by
  simp only [activationData,KernelInput.raw,KernelInput.base,SparseSignedPreparation.Program.view,
    SparseGraph.ListOperation.view,setView,List.getElem?_ofFn,dite_eq_left (Fin.isLt _),Option.getD_some,
    decide_eq_true_eq,Fin.eta,SparseOuterLaw.activationCount,SparseGridRounding.base]

theorem totalData_view (x : KernelInput) (j : Fin x.n) :
    totalData x.raw j.val=total x.D x.q x.Δ x.z j := by
  unfold totalData
  simp only [KernelInput.raw,KernelInput.base,indices,List.length_ofFn,RoundingList.range_finRange,
    ← List.ofFn_eq_map,List.map_ofFn,Function.comp_def]
  change x.Δ-min ((List.ofFn (fun e => activationData x.raw e.val j.val)).sum) (x.Δ/2)=_
  simp only [activationData_view,List.sum_ofFn,total]

theorem pieces_view (x : KernelInput) : pieces x.raw=
    List.ofFn (fun j => List.ofFn (fun i => SparseRescaledInner.piece x.P x.y x.p (total x.D x.q x.Δ x.z) i j)) := by
  simp only [pieces,KernelInput.raw,KernelInput.base,indices,List.length_ofFn,RoundingList.range_finRange,
    ← List.ofFn_eq_map,List.map_ofFn,Function.comp_def,List.getElem?_ofFn,dite_eq_left (Fin.isLt _),
    Option.getD_some,setView,decide_eq_true_eq,Fin.eta]
  change (List.ofFn (fun j : Fin x.n => List.ofFn (fun i : Fin x.f => if i∈x.P j then
    (totalData x.raw j.val:ℚ)*x.y i/x.p j else 0)))=_
  simp only [totalData_view,SparseRescaledInner.piece]
end MetricKMedian.SparsePrepared.Program
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
open Binary Binary.Automatic Binary.Automatic.Poly
def dimensions (x : List Unit × List (SparseIntegerLaw.BinarySparse.Data Row)) : List Unit :=
  let bs := x.1.flatMap (fun _ => x.2.map (fun _ => (0:ℚ)))
  RoundingList.dimensions bs

end MetricKMedian.SparseCounts.ListOperation
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
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly SparseIntegerLaw.BinarySparse
abbrev Input.encode (x : Input) := enc x.raw

@[fun_prop] theorem fractionRow_poly : Poly fractionRow := by unfold fractionRow; apply list_map <;> fun_prop
 theorem fractionRow_list {n : ℕ} (q : Fin n → ℚ) : fractionRow (List.ofFn q)=(fraction q).toList := by
  simp only [fractionRow,List.map_ofFn,fraction,base,Function.comp_def,Vector.toList_ofFn]
noncomputable def cardinalInputProgram : PolyProgram Input.encode SparseCardinalRounding.Program.encodeInput Input.cardinal :=
  fractionRow_poly.program.recode Input.raw (fun _ => rfl) (fun x => by
    rw [fractionRow_list]
    change enc ((fraction x.q).toList)=enc (List.ofFn (RationalWeightedStep.point (fraction x.q)))
    rw [ofFn_point])

def counts (x : List ℚ × List Bool) : List ℕ :=
  (SparseGraph.ListOperation.indices x.1).map (fun i => ⌊x.1[i]?.getD 0⌋₊+if x.2[i]?.getD false then 1 else 0)
@[fun_prop] theorem counts_poly : Poly counts := by unfold counts; apply list_map <;> fun_prop
 theorem counts_view {n : ℕ} (q : Fin n → ℚ) (p : Vector ℚ n) :
    counts (List.ofFn q,SparseGraph.ListOperation.setView (SparseCardinalRounding.selected p))=List.ofFn (SparseGridRounding.count q p) := by
  simp only [counts,SparseGraph.ListOperation.indices,List.length_ofFn,RoundingList.range_finRange,← List.ofFn_eq_map,
    List.map_ofFn,Function.comp_def,SparseGraph.ListOperation.setView,List.getElem?_ofFn,dite_eq_left (Fin.isLt _),
    Option.getD_some,Fin.eta,SparseCardinalRounding.selected,Finset.mem_filter,Finset.mem_univ,true_and,decide_eq_true_eq]
  rfl
def post (x : List ℚ × Data (List Bool)) : Data (List ℕ) := (x.2.1,x.2.2.map (fun b => counts (x.1,b)))
@[fun_prop] theorem post_poly : Poly post := by
  unfold post; apply pair
  · fun_prop
  · apply list_map <;> fun_prop

def Input.result (x : Input) : Data (List ℕ) :=
  ((SparseIntegerLaw.BinarySparse.raw (law x.q)).1,(law x.q).states.toList.map List.ofFn)
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 Binary Binary.PolyProgram Function SparseIntegerLaw.BinarySparse
open SparseIntegerLaw.DependentProgram SparseCounts.Program

noncomputable def columnsProgram : PolyProgram QInput.encode (encodeList SparseGridRounding.Program.Input.encode) QInput.columns :=
  (snd (encodeList (fun _ : Unit => [])) qt).recode QInput.raw (fun _ => rfl) (fun x => by
    change qt (List.ofFn (fun i => List.ofFn (x.column i).q))=
      encodeList SparseGridRounding.Program.Input.encode (List.ofFn x.column)
    rw [show List.ofFn (fun i => List.ofFn (x.column i).q)=
      (List.ofFn x.column).map (fun c => List.ofFn c.q) by rw [List.map_ofFn]; rfl]
    exact RoundingProgram.encodeList_map qr (fun c : SparseGridRounding.Program.Input => List.ofFn c.q) _)

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
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly SparseIntegerLaw.BinarySparse

def bundleData (x : KernelRaw) : List Unit × List (List ℚ) := (x.1.2.2.2.1.map (fun _ => ()),pieces x)
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 Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly Polynomial
open SparseGraph.ListOperation (Row Table setView indices)
open MaskProgram

 theorem any_view {n : ℕ} (U : Finset (Fin n)) : (setView U).any id=decide U.Nonempty := by
  apply Bool.eq_iff_iff.mpr
  simp only [setView,List.any_eq_true,List.mem_ofFn,id_eq,decide_eq_true_eq]
  constructor
  · rintro ⟨b,⟨i,rfl⟩,hi⟩; exact ⟨i,of_decide_eq_true hi⟩
  · rintro ⟨i,hi⟩; exact ⟨_,⟨i,rfl⟩,decide_eq_true hi⟩

end MetricKMedian.Preparation.RationalRepresentatives.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
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Table setView)
abbrev Raw := SparseSignedPreparation.Program.Raw
def Input.raw (x : Input) : Raw :=
  (List.replicate x.n (),(List.ofFn (fun e => setView (x.D e)),(List.ofFn x.c,List.ofFn x.q)))
abbrev Input.encode (x : Input) := enc x.raw
def post (x : Raw) : Raw := (x.1,(x.2.1,(x.2.2.1,SparseGridRounding.Program.fractionRow x.2.2.2)))
@[fun_prop] theorem post_poly : Poly post := by unfold post; fun_prop
noncomputable def signedProgram : PolyProgram Input.encode SparseSignedPreparation.Program.Input.encode Input.signed :=
  post_poly.program.recode Input.raw (fun _ => rfl) (fun x => by
    simp only [post,Input.raw,SparseGridRounding.Program.fractionRow_list,
      SparseSignedPreparation.Program.Input.encode,SparseSignedPreparation.Program.Input.raw,Input.signed])
end MetricKMedian.SparseOuterLaw.Program
end

end OAI
end