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

import Mathlib
import Definitions.Def_OAIQ037K025
import Definitions.Def_OAIQ037K048
import Definitions.Def_OAIQ037K049
import Definitions.Def_OAIQ037K050

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_SequentialParserProgram
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.InputParser
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly Polynomial
section Generic
variable {α : Type} [Coding α] [Inhabited α] (read : List Bool → α × List Bool)
variable (P : PolyProgram enc enc read) (hrest : ∀ xs, (read xs).2.length≤xs.length)
 omit [Inhabited α] in
 include hrest in
 theorem parseFold_size (as : List Unit) (b : State (α:=α)) :
    let out := as.foldl (fun b a => parseStep read (b,a)) b
    out.1.length≤b.1.length ∧
    (enc out.2).length≤(enc b.2).length+as.length*(2*P.sizeBound.eval (enc b.1).length+1) := by
  induction as generalizing b with
  | nil => simp only [List.foldl_nil,List.length_nil,zero_mul,add_zero]; exact ⟨le_rfl,le_rfl⟩
  | cons a as ih =>
    have hh := ih (parseStep read (b,a))
    have hr := hrest b.1
    have hs := P.length_bound b.1
    have he : (enc ((read b.1).1)).length ≤ P.sizeBound.eval (enc b.1).length := by
      change (encodePair enc enc (read b.1)).length≤_ at hs
      rw [encodePair_length] at hs
      omega
    have hp : P.sizeBound.eval (enc (read b.1).2).length≤P.sizeBound.eval (enc b.1).length := by
      apply polynomial_eval_mono
      change (encodeList encodeBool (read b.1).2).length≤(encodeList encodeBool b.1).length
      rw [BooleanLists.length,BooleanLists.length]
      omega
    dsimp only [parseStep] at hh
    simp only [List.foldl_cons,List.length_cons]
    refine ⟨hh.1.trans hr,?_⟩
    have hc : (enc ((read b.1).1::b.2)).length=2*(enc (read b.1).1).length+1+(enc b.2).length := EncodedList.cons_length _ _ _
    rw [hc] at hh
    exact hh.2.trans (by nlinarith)
 omit [Coding α] [Inhabited α] in
 theorem parse_fold_encoded (put : α → List Bool) (hr : ∀ a xs, read (put a++xs)=(a,xs))
    (as : List α) (xs : List Bool) (acc : List α) :
    (List.replicate as.length ()).foldl (fun b a => parseStep read (b,a)) ((as.map put).flatten++xs,acc)=
      (xs,as.reverse++acc) := by
  induction as generalizing acc with
  | nil => simp
  | cons a as ih =>
    simp only [List.length_cons,List.replicate_succ,List.map_cons,List.flatten_cons,List.append_assoc,
      List.foldl_cons,parseStep,hr]
    change (List.replicate as.length ()).foldl (fun b a => parseStep read (b,a)) ((as.map put).flatten++xs,a::acc)=_
    rw [ih]
    simp only [List.reverse_cons,List.append_assoc,List.singleton_append]
end Generic
end MetricKMedian.InputParser
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
noncomputable def thresholdProgram : PolyProgram ethreshold Ratio.encode (fun x : (Row × ℚ) × ℚ => threshold x.1.1 x.1.2 x.2) := by
  let dat := fst (encodePair er Ratio.encode) Ratio.encode
  let xs := dat.comp (fst er Ratio.encode)
  let k := dat.comp (snd er Ratio.encode)
  let a := snd (encodePair er Ratio.encode) Ratio.encode
  let us := (a.fanout xs).comp upperProgram
  let sum := us.comp ratSum
  let card := (us.comp (listLength Ratio.encode 0)).comp ratOfNat
  exact (((sum.fanout k).comp ratSub).fanout card).comp ratDiv
noncomputable def thresholdsProgram : PolyProgram (encodePair er Ratio.encode) er (fun x : Row × ℚ => thresholds x.1 x.2) :=
  (((identity (encodePair er Ratio.encode)).fanout (fst er Ratio.encode)).comp
    (thresholdProgram.listMapWith 0 0)).congr _ (fun _ => rfl)
noncomputable def levelProgram : PolyProgram (encodePair er Ratio.encode) Ratio.encode (fun x : Row × ℚ => level x.1 x.2) :=
  ((thresholdsProgram.fanout (thresholdsProgram.comp (listHead Ratio.encode 0))).comp maxFold).congr _ (fun _ => rfl)
noncomputable def projectProgram : PolyProgram (encodePair er Ratio.encode) er (fun x : Row × ℚ => project x.1 x.2) := by
  let sub := ((exchange Ratio.encode Ratio.encode).comp ratSub).comp positivePart
  exact ((levelProgram.fanout (fst er Ratio.encode)).comp (sub.listMapWith 0 0)).congr _ (fun _ => rfl)
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

noncomputable def maximumProgram : PolyProgram er Ratio.encode maximum :=
  (((identity er).fanout (listHead Ratio.encode 0)).comp maxFold).congr _ (fun _ => rfl)

noncomputable def dualAffineProgram : PolyProgram edual Ratio.encode (fun x : (Row × Row) × ℚ => Dual.affine x.1.1 x.1.2 x.2) := by
  let t := snd epoint Ratio.encode
  let zip := (fst epoint Ratio.encode).comp (listZip Ratio.encode Ratio.encode 0 0)
  let ec := encodePair Ratio.encode (encodePair Ratio.encode Ratio.encode)
  let q := snd Ratio.encode (encodePair Ratio.encode Ratio.encode)
  let d := q.comp (fst Ratio.encode Ratio.encode)
  let y := q.comp (snd Ratio.encode Ratio.encode)
  let s := ((fst Ratio.encode (encodePair Ratio.encode Ratio.encode)).fanout d).comp ratSub
  let weighted := (y.fanout (s.comp positivePart)).comp ratMul
  let sum := (((t.fanout zip).comp (weighted.listMapWith (0,0) 0)).comp ratSum)
  exact ((t.fanout sum).comp ratSub).congr _ (fun _ => rfl)

noncomputable def dualValueProgram : PolyProgram edual Ratio.encode (fun x : (Row × Row) × ℚ => Dual.value x.1.1 x.1.2 x.2) := by
  let dat := fst epoint Ratio.encode
  let ts := (((dat.comp (fst er er)).fanout (snd epoint Ratio.encode)).comp candidatesProgram)
  exact (((dat.fanout ts).comp (dualAffineProgram.listMapWith 0 0)).comp maximumProgram).congr _ (fun _ => rfl)

noncomputable def dualBestProgram : PolyProgram edual Ratio.encode (fun x : (Row × Row) × ℚ => Dual.best x.1.1 x.1.2 x.2) := by
  let dat := fst epoint Ratio.encode
  let ts := (((dat.comp (fst er er)).fanout (snd epoint Ratio.encode)).comp candidatesProgram)
  let context := dat.fanout dualValueProgram
  let c := fst edual Ratio.encode
  let dy := c.comp (fst epoint Ratio.encode)
  let v := c.comp (snd epoint Ratio.encode)
  let a := snd edual Ratio.encode
  let test := (((dy.fanout a).comp dualAffineProgram).fanout v).comp ratEQ
  exact (((context.fanout ts).comp (test.listFilterWith 0 (([],[]),0))).comp maximumProgram).congr _ (fun _ => rfl)

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

noncomputable def objectiveProgram : PolyProgram etrunc Ratio.encode (fun x : (Rows × Row) × ℚ => Truncated.objective x.1.1 x.1.2 x.2) := by
  let dat := fst (encodePair ers er) Ratio.encode
  let ys := dat.comp (snd ers er)
  let H := snd (encodePair ers er) Ratio.encode
  let matrix := ((dat.comp (fst ers er)).fanout H).comp truncateMatrixProgram
  let ec := encodePair er Ratio.encode
  let c := fst ec er
  let y := c.comp (fst er Ratio.encode)
  let h := c.comp (snd er Ratio.encode)
  let row := snd ec er
  let value := ((row.fanout y).fanout h).comp dualValueProgram
  exact ((((ys.fanout H).fanout matrix).comp (value.listMapWith [] 0)).comp ratSum).congr _ (fun _ => rfl)

noncomputable def componentProgram : PolyProgram (encodePair etrunc Nat.bits) Ratio.encode
    (fun x : ((Rows × Row) × ℚ) × ℕ => Truncated.component x.1.1.1 x.1.1.2 x.1.2 x.2) := by
  let t := fst etrunc Nat.bits
  let dat := t.comp (fst (encodePair ers er) Ratio.encode)
  let ys := dat.comp (snd ers er)
  let H := t.comp (snd (encodePair ers er) Ratio.encode)
  let i := snd etrunc Nat.bits
  let matrix := ((dat.comp (fst ers er)).fanout H).comp truncateMatrixProgram
  let ec := encodePair (encodePair er Ratio.encode) Nat.bits
  let c := fst ec er
  let yh := c.comp (fst (encodePair er Ratio.encode) Nat.bits)
  let y := yh.comp (fst er Ratio.encode)
  let h := yh.comp (snd er Ratio.encode)
  let idx := c.comp (snd (encodePair er Ratio.encode) Nat.bits)
  let row := snd ec er
  let best := ((row.fanout y).fanout h).comp dualBestProgram
  let distance := (row.fanout idx).comp (listGetD Ratio.encode 0)
  let coord := (((best.fanout distance).comp ratSub).comp positivePart).comp ratNeg
  exact (((((ys.fanout H).fanout i).fanout matrix).comp (coord.listMapWith [] 0)).comp ratSum).congr _ (fun _ => rfl)

noncomputable def gradientProgram : PolyProgram etrunc er (fun x : (Rows × Row) × ℚ => Truncated.gradient x.1.1 x.1.2 x.2) := by
  let ys := (fst (encodePair ers er) Ratio.encode).comp (snd ers er)
  let ids := ys.comp (listIndices Ratio.encode 0)
  exact (((identity etrunc).fanout ids).comp (componentProgram.listMapWith 0 0)).congr _ (fun _ => rfl)

noncomputable def nextProgram : PolyProgram enext er
    (fun x : ((Rows × Row) × ℚ) × (ℚ × ℚ) => Truncated.next x.1.1.1 x.1.1.2 x.1.2 x.2.1 x.2.2) := by
  let t := fst etrunc (encodePair Ratio.encode Ratio.encode)
  let kr := snd etrunc (encodePair Ratio.encode Ratio.encode)
  let ys := (t.comp (fst (encodePair ers er) Ratio.encode)).comp (snd ers er)
  let grad := t.comp gradientProgram
  let zip := (ys.fanout grad).comp (listZip Ratio.encode Ratio.encode 0 0)
  let rate := kr.comp (snd Ratio.encode Ratio.encode)
  let coords := snd Ratio.encode (encodePair Ratio.encode Ratio.encode)
  let y := coords.comp (fst Ratio.encode Ratio.encode)
  let g := coords.comp (snd Ratio.encode Ratio.encode)
  let rg := ((fst Ratio.encode (encodePair Ratio.encode Ratio.encode)).fanout g).comp ratMul
  let coord := (y.fanout rg).comp ratSub
  let update := (rate.fanout zip).comp (coord.listMapWith (0,0) 0)
  exact ((update.fanout (kr.comp (fst Ratio.encode Ratio.encode))).comp projectProgram).congr _ (fun _ => rfl)
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

namespace Program
noncomputable def updateProgram : PolyProgram es es update := by
  let c := fst ec er
  let ds := c.comp (fst ers (encodePair Ratio.encode (encodePair Ratio.encode Ratio.encode)))
  let hkr := c.comp (snd ers (encodePair Ratio.encode (encodePair Ratio.encode Ratio.encode)))
  let h := hkr.comp (fst Ratio.encode (encodePair Ratio.encode Ratio.encode))
  let kr := hkr.comp (snd Ratio.encode (encodePair Ratio.encode Ratio.encode))
  let args := (((ds.fanout (snd ec er)).fanout h).fanout kr)
  exact (c.fanout (args.comp nextProgram)).congr _ (fun _ => rfl)
end Program

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

namespace Program
noncomputable def statesProgram (r : ℕ) (hr : 0 < r) : PolyProgram Input.encode (encodeList es) (states r) :=
  (updateProgram.iteratesFrom (startProgram r) (stepsProgram r) (([],(0,(0,0))),[])
    (stepsPolynomial r) (statePolynomial r)
    (fun I => by rw [stepsPolynomial_eval,rawSteps_eq]; exact steps_bound I r)
    (state_size r hr)).congr _ (fun _ => rfl)
noncomputable def valueProgram : PolyProgram es Ratio.encode value := by
  let c := fst ec er
  let ds := c.comp (fst ers (encodePair Ratio.encode (encodePair Ratio.encode Ratio.encode)))
  let H := (c.comp (snd ers (encodePair Ratio.encode (encodePair Ratio.encode Ratio.encode)))).comp (fst Ratio.encode (encodePair Ratio.encode Ratio.encode))
  exact (((ds.fanout (snd ec er)).fanout H).comp objectiveProgram).congr _ (fun _ => rfl)
noncomputable def chooseProgram : PolyProgram (encodeList es) es choose := by
  let a0 : State := (([],(0,(0,0))),[])
  let vals := valueProgram.listMap a0
  let mn := vals.comp minimumProgram
  let val := (snd Ratio.encode es).comp valueProgram
  let pred := ((fst Ratio.encode es).fanout val).comp ratEQ
  let filt := ((mn.fanout (identity (encodeList es))).comp (pred.listFilterWith a0 0))
  exact (filt.comp (listHead es a0)).congr _ (fun ss => by
    change (ss.filter (fun a => decide (minimum (ss.map value)=value a))).head?.getD a0=choose ss
    unfold choose selectMinimum
    apply congrArg (fun xs : List State => xs.head?.getD a0)
    exact List.filter_congr (fun a _ => decide_eq_decide.mpr eq_comm))

noncomputable def optimizeProgram (r : ℕ) (hr : 0 < r) : PolyProgram Input.encode er (result r) :=
  (((statesProgram r hr).comp chooseProgram).comp (snd ec er)).congr _ (fun _ => rfl)
end Program

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
noncomputable def assignmentProgram : PolyProgram (encodePair er er) er (fun x : Row × Row => assignment x.1 x.2) := by
  let coord := (exchange Ratio.encode Ratio.encode).comp ratDiv
  let norm := ((ratSum.fanout (identity er)).comp (coord.listMapWith 0 0))
  exact (weightsProgram.comp norm).congr _ (fun _ => rfl)
noncomputable def assignmentsProgram : PolyProgram (encodePair ers ers) ers (fun x : Rows × Rows => assignments x.1 x.2) :=
  ((listZip er er [] []).comp (assignmentProgram.listMap ([],[]))).congr _ (fun _ => 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

noncomputable def validProgram : PolyProgram (encodePair eo Nat.bits) encodeBool (fun x : Output × ℕ => valid x.1 x.2) := by
  let a := fst eo Nat.bits
  let ys := a.comp (fst er ers)
  let xs := a.comp (snd er ers)
  let k := ((snd eo Nat.bits).comp ratOfNat).fanout (constant (encodePair eo Nat.bits) Ratio.encode 1) |>.comp ratAdd
  let yb := ys.comp (boundedProgram.listAll 0)
  let rowDom := (exchange er er).comp dominatedProgram
  let dom := (ys.fanout xs).comp (rowDom.listAllWith [])
  let one := ((ratSum.fanout (constant er Ratio.encode 1)).comp ratEQ).listAll []
  let sums := xs.comp one
  let cap := ((ys.comp ratSum).fanout k).comp ratLE
  exact (((((yb.fanout dom).comp boolAnd).fanout sums).comp boolAnd).fanout cap |>.comp boolAnd).congr _ (fun _ => rfl)
noncomputable def dotProgram : PolyProgram (encodePair er er) Ratio.encode (fun x : Row × Row => dot x.1 x.2) :=
  ((listZipWith Ratio.encode Ratio.encode 0 0 ratMul).comp ratSum).congr _ (fun _ => rfl)
noncomputable def valueProgram : PolyProgram (encodePair eo ers) Ratio.encode (fun x : Output × Rows => value x.1 x.2) := by
  let xs := (fst eo ers).comp (snd er ers)
  let ds := snd eo ers
  exact (((xs.fanout ds).comp (listZipWith er er [] [] dotProgram)).comp ratSum).congr _ (fun _ => rfl)
end MetricKMedian.LPBinary.Repair
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 : ℕ}

def step (μ : SparseIntegerLaw (Table n m)) (ν : SparseIntegerLaw ((Fin n → ℕ)))
    (i : Fin m) : SparseIntegerLaw (Table n m) :=
  μ.prodCompress ν (fun G S => next G S i) features

end MetricKMedian.SparseCounts
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 run (ν : Fin m → SparseIntegerLaw ((Fin n → ℕ))) : ℕ → SparseIntegerLaw (Table n m)
  | 0 => .dirac (fun _ _ => 0)
  | t+1 => if ht : t < m then step (run ν t) (ν ⟨t,ht⟩) ⟨t,ht⟩ else run ν t

end MetricKMedian.SparseCounts
end
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 Binary Binary.PolyProgram Function Polynomial
open SparseIntegerLaw.DependentProgram SparseIntegerLaw.BinarySparse
open ListOperation (Row Table et)

def Input.state (x : Input) (t : ℕ) : State := ⟨⟨x,t⟩,run x.columns t⟩

theorem state_next (x : Input) (t : ℕ) : State.step (x.state t)=x.state (t+1) := by
  have he (ht : t < x.m) : update ⟨x,t⟩=(fun G S => next G S ⟨t,ht⟩) := by
    funext G S i
    by_cases h : i=⟨t,ht⟩
    · subst i; simp only [update,next,Function.update_self,ite_true]
    · have hv : i.val≠t := fun hh => h (Fin.ext hh)
      simp only [update,next,Function.update_of_ne h,ite_eq_right hv]
  unfold State.step Input.state
  by_cases ht : t < x.m
  · rw [ite_eq_left ht]
    change (⟨⟨x,t+1⟩,((run x.columns t).prod (column ⟨x,t⟩) (update ⟨x,t⟩)).compressAuto features⟩ : State)=_
    rw [run,dite_eq_left ht]
    simp only [column,dite_eq_left ht,he ht,SparseCounts.step,SparseIntegerLaw.prodCompress]
  · rw [ite_eq_right ht,run,dite_eq_right ht]
    rfl

theorem state_iterate (x : Input) (t : ℕ) : (State.step)^[t] x.start=x.state t := by
  induction t with
  | zero => rfl
  | succ t ih => rw [Function.iterate_succ_apply',ih,state_next]

end MetricKMedian.SparseCounts.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 Binary Binary.PolyProgram Function Finset
namespace Scale

noncomputable def guessesProgram : PolyProgram ers er guesses := by
  let e := encodePair er Ratio.encode
  let q := snd er Ratio.encode
  let ps := fst er Ratio.encode
  let times := ratMul.listMapWith 0 0
  let pos := ((constant e Ratio.encode 0).fanout q).comp ratLT
  let body := ite pos (constant e er []) ((q.fanout ps).comp times)
  let powers := (listLength er []).comp Dyadic.program
  exact ((powers.fanout (listFlatten Ratio.encode 0)).comp (body.listFlatMapWith 0 0)).congr _ (fun _ => by
    simp only [Function.comp_apply,guesses,decide_eq_true_eq])

end Scale
end MetricKMedian.LPBinary
end

end OAI
end

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

abbrev law (q : Fin n → Fin m → ℚ) : SparseIntegerLaw (SparseCounts.Table n m) :=
  SparseCounts.run (fun j => SparseGridRounding.law (fun i => q i j)) m

end MetricKMedian.SparseBundles
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 : ℕ}

abbrev law (P : Fin t → Finset (Fin n)) (y : Fin n → ℚ) (p : Fin t → ℚ)
    (K : Fin t → ℕ) := SparseBundles.law (piece P y p K)

end MetricKMedian.SparseRescaledInner
end
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 : ℕ}

noncomputable def law (q : Fin n → Fin m → ℚ) : FiniteLaw (Fin m → Finset (Fin n)) :=
  (SparseBundles.law q).realIndex.map
    (fun a => encode q (SparseBundles.law q).states[a.val])

end MetricKMedian.SparseBundleEncoding

namespace MetricKMedian.SparseRescaledInner
open Finset
variable {n t : ℕ}

noncomputable def encodedLaw (P : Fin t → Finset (Fin n)) (y : Fin n → ℚ)
    (p : Fin t → ℚ) (K : Fin t → ℕ) : FiniteLaw (Fin t → Finset (Fin n)) :=
  SparseBundleEncoding.law (piece P y p K)

end MetricKMedian.SparseRescaledInner
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 law (D : Fin m → Finset (Fin n)) (q : Fin m → ℚ) :
    SparseIntegerLaw (Fin m → Finset (Fin n)) :=
  SparseGraph.run (fun e => SparseTargetSubset.law (D e) (q e)) m

end MetricKMedian.SparseStarActivation
end
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
open RationalWeightedStep (point fractional)
variable {n m : ℕ}

def kernel (D : Fin m → Finset (Fin n)) (q : Vector ℚ m)
    (hq : ∀ e, 0 ≤ point q e ∧ point q e ≤ 1) : SparseIntegerLaw (State n m) :=
  (SparseStarActivation.law D (point q)).prod
    (SparseBernoulli.run (d := 2) (point q) hq m) (fun S ω => (q,S,ω))

end MetricKMedian.SparseSignedPreparation
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 kernel (D : Fin m → Finset (Fin n)) (q : Fin m → ℚ) (Δ : ℕ)
    (P : Fin n → Finset (Fin f)) (y : Fin f → ℚ) (p : Fin n → ℚ) (z : State n m) :
    SparseIntegerLaw (State n m × SparseCounts.Table f n) :=
  (SparseRescaledInner.law P y p (total D q Δ z)).map (fun G => (z,G))

end MetricKMedian.SparsePrepared
end
end

end OAI
end