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

import Mathlib
import Definitions.Def_OAIQ037K057
import Definitions.Def_OAIQ037K058
import Definitions.Def_OAIQ037K059
import Definitions.Def_OAIQ037K060

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseSignedPartial
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.SparseSignedPartial
open Finset RationalSignedStep
open RationalWeightedStep (point fractional)
open SparseWeightedPartial (features features_single features_pair)
variable {n : ℕ}

theorem run_terminal (β : Fin n → ℚ) (p : Vector ℚ n)
    (hp : ∀ i, 0 ≤ point p i ∧ point p i ≤ 1) (a : Fin (run β p n).length) :
    ¬Active β (run β p n).states[a.val] := by
  rcases (run_invariants β p hp n a).2.2 with h | h
  · intro ha
    have hi := (pair β (run β p n).states[a.val] ha).property.1
    have hc := card_pos.mpr ⟨_,hi⟩
    omega
  · exact h

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

theorem run_length (ν : Fin m → SparseIntegerLaw ((Fin n → ℕ))) (t : ℕ) :
    (run ν t).length ≤ n*m+(n*m)*(n*m)+1 := by
  induction t with
  | zero => change 1 ≤ _; omega
  | succ t ih =>
    rw [run]
    split_ifs with ht
    · exact ((run ν t).prodCompress_spec (ν ⟨t,ht⟩)
        (fun G S => next G S ⟨t,ht⟩) features).1
    · exact ih

end MetricKMedian.SparseCounts
end
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
open Binary
variable {n m : ℕ}

theorem run_bound (ν : Fin m → SparseIntegerLaw (Fin n → ℕ)) (U : ℕ)
    (hν : ∀ i, ∀ a : Fin (ν i).length, ∀ h, (ν i).states[a.val] h≤U) (t : ℕ) :
    ∀ a : Fin (run ν t).length, ∀ i h,(run ν t).states[a.val] i h≤U := by
  induction t with
  | zero =>
    intro a i h
    change (Vector.replicate 1 (fun _ : Fin m => fun _ : Fin n => (0:ℕ)))[a.val] i h≤U
    simp only [Vector.getElem_replicate]
    exact Nat.zero_le _
  | succ t ih =>
    let P := fun μ : SparseIntegerLaw (Table n m) => ∀ a : Fin μ.length, ∀ i h,μ.states[a.val] i h≤U
    change P (run ν (t+1))
    rw [run]
    split_ifs with ht
    · intro a i h
      obtain ⟨j,k,hjk⟩ := ((run ν t).prodCompress_spec (ν ⟨t,ht⟩)
        (fun G S => next G S ⟨t,ht⟩) features).2.1 a
      change (step (run ν t) (ν ⟨t,ht⟩) ⟨t,ht⟩).states[a.val]=_ at hjk
      rw [hjk]
      exact next_bound _ _ _ U (ih j) (hν _ k) i h
    · exact ih

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
open Binary Binary.Automatic Binary.Automatic.Poly
def nextTable (x : (ℕ × Table) × Row) : Table :=
  (indices x.1.2).map (fun i => if i=x.1.1 then x.2 else x.1.2[i]?.getD [])
@[fun_prop] theorem nextTable_poly : Poly nextTable := by
  unfold nextTable
  apply list_map <;> fun_prop
@[fun_prop] theorem dimensions_poly : Poly dimensions := by
  unfold dimensions
  apply comp RoundingList.dimensions_poly
  apply list_flatMap
  · apply list_map <;> fun_prop
  · fun_prop

 theorem edges_view {n m : ℕ} (G : SparseCounts.Table n m) :
    edges (List.replicate n (),view G)=List.ofFn (edgeCode G) := by
  simp only [edges,indices,List.length_replicate,RoundingList.range_finRange,view,
    List.flatMap_def,List.map_map,Function.comp_def]
  rw [← List.ofFn_eq_map]
  simp only [List.map_ofFn,Function.comp_def,List.getElem?_ofFn,dite_eq_left (Fin.isLt _),Option.getD_some]
  rw [RoundingList.ofFn_product]
  rfl

 theorem featureList_view {n m : ℕ} (G : SparseCounts.Table n m) :
    featureList (List.replicate n (),view G)=List.ofFn (features G) := by
  simp only [featureList,edges_view,RoundingList.features,List.flatMap_def,List.map_ofFn,
    Function.comp_def,RoundingList.ofFn_product]
  rw [List.ofFn_add]
  congr 1
  · congr 1; funext i
    have hi : (Fin.castAdd ((n*m)*(n*m)) i : Fin (n*m+(n*m)*(n*m)))=finSumFinEquiv (Sum.inl i) := rfl
    change edgeCode G i = features G (Fin.castAdd ((n*m)*(n*m)) i)
    rw [hi]
    simp only [features,Equiv.symm_apply_apply,Sum.elim_inl]
  · congr 1; funext i
    have hi : (Fin.natAdd (n*m) i : Fin (n*m+(n*m)*(n*m)))=finSumFinEquiv (Sum.inr i) := by apply Fin.ext; simp [finSumFinEquiv]
    rw [hi]
    simp only [features,Equiv.symm_apply_apply,Sum.elim_inr]

end MetricKMedian.SparseCounts.ListOperation
end

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.DependentProgram SparseIntegerLaw.BinarySparse
open ListOperation (Row Table er et)
abbrev InputRaw := List Unit × List (Data Row)
abbrev ei : InputRaw → List Bool := Binary.Automatic.enc

def columnRaw {n : ℕ} (μ : SparseIntegerLaw ((Fin n → ℕ))) : Data Row :=
  ((μ.law.denominator,List.ofFn μ.law.numerator),μ.states.toList.map ListOperation.setView)
def Input.raw (x : Input) : InputRaw := (List.replicate x.n (),List.ofFn fun i => columnRaw (x.columns i))
abbrev Input.encode (x : Input) := ei x.raw
def Context.raw (c : Context) : InputRaw × ℕ := (c.input.raw,c.t)
abbrev Context.encode (c : Context) := encodePair ei Nat.bits c.raw
abbrev view (c : Context) (G : T c) := ListOperation.view G
abbrev State.encode := Bundle.encode Context.encode et view

def rawColumn (x : InputRaw × ℕ) : Data Row :=
  if x.2 < x.1.2.length then x.1.2[x.2]?.getD ((1,[1]),[])
  else ((1,[1]),[x.1.1.map (fun _ => 0)])

noncomputable def activeProgram : PolyProgram State.encode encodeBool
    (fun x : State => decide (x.ctx.t<x.ctx.input.m)) := by
  let raw : PolyProgram (encodePair ei Nat.bits) encodeBool
      (fun x : InputRaw × ℕ => decide (x.2<x.1.2.length)) := Binary.Automatic.Poly.program (by fun_prop)
  let ctx : PolyProgram Context.encode encodeBool (fun c => decide (c.t < c.input.m)) := raw.recode Context.raw (fun _ => rfl)
    (fun c => by simp only [Context.raw,Input.raw,List.length_ofFn])
  exact (contextProgram Context.encode et view).comp ctx
end MetricKMedian.SparseCounts.Program
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)
local notation "erB" => ListOperation.er

noncomputable def startProgram : PolyProgram Input.encode State.encode Input.start := by
  let raw : PolyProgram ei (encodePair (encodePair ei Nat.bits) (ed et))
      (fun x : InputRaw => ((x,0),(((1:ℤ),[(1:ℤ)]),[x.2.map (fun _ => x.1.map (fun _ => (0:ℕ)))]))) := by
    apply Binary.Automatic.Poly.program
    have hs : Binary.Automatic.Poly (fun x : InputRaw => x.2.map (fun _ => x.1.map (fun _ => (0:ℕ)))) := by
      apply Binary.Automatic.Poly.list_map
      · apply Binary.Automatic.Poly.list_map <;> fun_prop
      · fun_prop
    fun_prop
  exact raw.recode Input.raw (fun _ => rfl) (fun x => by
    simp only [State.encode,Bundle.encode,Bundle.raw,Input.start,SparseIntegerLaw.dirac,
      List.map_const',Input.raw,List.length_ofFn,List.map_replicate,
      Vector.toList_replicate,List.ofFn_const,view,ListOperation.view]
    rfl)

noncomputable def countProgram : PolyProgram Input.encode Nat.bits Input.m :=
  ((snd (encodeList (fun _ : Unit => [])) (encodeList (ed erB))).comp (listLength (ed erB) ((1,[1]),[]))).recode
    Input.raw (fun _ => rfl) (fun x => by simp only [Function.comp_def,Input.raw,List.length_ofFn])

theorem input_bounds (x : Input) :
    x.n≤x.encode.length ∧ x.m≤x.encode.length ∧
    (∀ i, (x.columns i).length≤x.encode.length) ∧
    (∀ i, (x.columns i).law.denominator≤(2:ℤ)^x.encode.length) := by
  let L := x.encode.length
  have he : L=2*(encodeList (fun _ : Unit => []) x.raw.1).length+1+
      (encodeList (ed erB) x.raw.2).length := encodePair_length _ _ _
  have hn := EncodedList.length_le (fun _ : Unit => []) x.raw.1
  have hm := EncodedList.length_le (ed erB) x.raw.2
  simp only [Input.raw,List.length_ofFn,List.length_replicate] at hn hm he
  have hcol (i : Fin x.m) : (ed erB (columnRaw (x.columns i))).length≤L := by
    have h := EncodedList.member_length (ed erB) x.raw.2 (columnRaw (x.columns i))
      (List.mem_ofFn.mpr ⟨i,rfl⟩)
    simp only [Input.raw] at h
    omega
  have hc (i : Fin x.m) : (ed erB (columnRaw (x.columns i))).length=
      2*(2*(Signed.encode (x.columns i).law.denominator).length+1+
        (encodeList Signed.encode (List.ofFn (x.columns i).law.numerator)).length)+1+
      (encodeList erB ((x.columns i).states.toList.map ListOperation.setView)).length := by
    simp only [columnRaw,ed,el,IntegerLaw.ListPivot.el,encodePair_length]
  refine ⟨by change x.n≤L; omega,by change x.m≤L; omega,?_,?_⟩
  · intro i
    have h := EncodedList.length_le Signed.encode (List.ofFn (x.columns i).law.numerator)
    simp only [List.length_ofFn] at h
    have hh := hcol i
    rw [hc i] at hh
    change (x.columns i).length≤L
    omega
  · intro i
    have hh := hcol i
    rw [hc i] at hh
    have hl : (Signed.encode (x.columns i).law.denominator).length≤L := by omega
    exact (le_abs_self _).trans ((Signed.height_length _).trans (pow_le_pow_right₀ (by norm_num) hl))

theorem entry_bound (x : Input) : ∀ i, ∀ a : Fin (x.columns i).length, ∀ h,
    (x.columns i).states[a.val] h≤2^x.encode.length := by
  intro i a h
  have he := encodePair_length (encodeList (fun _ : Unit => [])) (encodeList (ed erB)) x.raw
  have hcol := EncodedList.member_length (ed erB) x.raw.2 (columnRaw (x.columns i))
    (List.mem_ofFn.mpr ⟨i,rfl⟩)
  have hs := encodePair_length el (encodeList erB) (columnRaw (x.columns i))
  have hrow := EncodedList.member_length erB ((x.columns i).states.toList.map ListOperation.setView)
    (ListOperation.setView (x.columns i).states[a.val]) (by
      apply List.mem_map.mpr
      exact ⟨(x.columns i).states[a.val], by simp, rfl⟩)
  have hv := EncodedList.member_length Nat.bits (ListOperation.setView (x.columns i).states[a.val])
    ((x.columns i).states[a.val] h) (List.mem_ofFn.mpr ⟨h,rfl⟩)
  have hl : ((x.columns i).states[a.val] h).bits.length≤x.encode.length := by
    change x.encode.length=_ at he
    change (ed erB (columnRaw (x.columns i))).length=
      2*(el ((x.columns i).law.denominator,List.ofFn (x.columns i).law.numerator)).length+1+
        (encodeList erB ((x.columns i).states.toList.map ListOperation.setView)).length at hs
    change ((x.columns i).states[a.val] h).bits.length≤(erB (ListOperation.setView (x.columns i).states[a.val])).length at hv
    omega
  exact (NatBinary.le_two_pow_length _).trans (Nat.pow_le_pow_right (by decide) hl)

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

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

@[fun_prop] theorem bundleData_poly : Poly bundleData := by
  unfold bundleData; apply Binary.Automatic.Poly.pair
  · apply list_map <;> fun_prop
  · exact pieces_poly
abbrev PreparedRaw := StateRaw × SparseCounts.ListOperation.Table
def attach (x : StateRaw × Data SparseCounts.ListOperation.Table) : Data PreparedRaw :=
  (x.2.1,x.2.2.map (fun G => (x.1,G)))
@[fun_prop] theorem attach_poly : Poly attach := by
  unfold attach; apply Binary.Automatic.Poly.pair
  · fun_prop
  · apply list_map <;> fun_prop

def view {n m f : ℕ} (s : SparseSignedPreparation.State n m × SparseCounts.Table f n) : PreparedRaw :=
  (SparseSignedPreparation.Program.view s.1,SparseCounts.ListOperation.view s.2)
def KernelInput.result (x : KernelInput) : Data PreparedRaw :=
  ((SparseIntegerLaw.BinarySparse.raw (kernel x.D x.q x.Δ x.P x.y x.p x.z)).1,
    (kernel x.D x.q x.Δ x.P x.y x.p x.z).states.toList.map view)
end MetricKMedian.SparsePrepared.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
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (setView)
abbrev Raw := BaseRaw × QRow
def Input.base (x : Input) : 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 Input.raw (x : Input) : Raw := (x.base,List.ofFn x.c)
abbrev Input.encode (x : Input) := enc x.raw

def outerData (x : Raw) : SparseOuterLaw.Program.Raw :=
  (x.1.2.2.2.2.1.map (fun _ => ()),(x.1.1,(x.2,x.1.2.1)))
@[fun_prop] theorem outerData_poly : Poly outerData := by
  unfold outerData; apply Binary.Automatic.Poly.pair
  · apply list_map <;> fun_prop
  · fun_prop

def kernelRows (x : Raw × Data StateRaw) : List KernelRaw := x.2.2.map (fun z => (x.1.1,z))
@[fun_prop] theorem kernelRows_poly : Poly kernelRows := by unfold kernelRows; apply list_map <;> fun_prop
end MetricKMedian.SparsePrepared.Program
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 Binary Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (setView indices)

 theorem targetsData_view {f n : ℕ} (S : Data f n) :
    targetsData (supplierView S)=List.ofFn (fun e => setView (D S.A e)) := by
  rw [show (fun e => setView (D S.A e))=(fun e => setView (SupplierStars.targets S.A (index e))) by rfl,ofFn_star (fun e => setView (SupplierStars.targets S.A e))]
  simp only [targetsData,supplierView,indices,List.length_ofFn,RoundingList.range_finRange,
    List.flatMap_def,Function.comp_def,← List.ofFn_eq_map,List.map_ofFn,
    List.getElem?_ofFn,dite_eq_left (Fin.isLt _),Option.getD_some,Fin.eta,SupplierStars.targets,
    setView,mem_filter,mem_univ,true_and,mem_singleton]
  simp only [Fin.val_inj]

 theorem flagsData_view {f n : ℕ} (S : Data f n) : flagsData (supplierView S)=List.ofFn (a (f:=f) (n:=n)) := by
  change _=List.ofFn (fun e => flagQ (index e))
  rw [ofFn_star]
  simp only [flagsData,supplierView,List.flatMap_def,List.map_ofFn,Function.comp_def,flagQ]

 theorem outsideData_view {f n : ℕ} (S : Data f n) (i : Fin f) :
    outsideData (supplierView S) i.val=decide (i∈SupplierStars.outside S.P) := by
  apply Bool.eq_iff_iff.mpr
  simp only [outsideData,supplierView,List.all_map,Function.comp_def,id_eq,List.all_eq_true,List.mem_ofFn,
    forall_exists_index,forall_apply_eq_imp_iff,setView,List.getElem?_ofFn,dite_eq_left i.isLt,
    Option.getD_some,Fin.eta,decide_eq_true_eq,SupplierStars.outside,
    mem_filter,mem_univ,true_and]
  simp

 theorem pairWeight_view {f n : ℕ} (S : Data f n) (s t : Fin n) :
    pairWeight (supplierView S) s.val t.val=∑ i∈S.A s∩S.P t,S.y i := by
  simp only [pairWeight,supplierView,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,Fin.eta,← Bool.decide_and,decide_eq_true_eq,List.sum_ofFn]
  rw [← Finset.sum_filter]
  congr 1
  ext i
  simp

 theorem weightsData_view {f n : ℕ} (S : Data f n) :
    weightsData (supplierView S)=List.ofFn (fun e => weightQ S.y S.P S.A S.c S.γ (index e)) := by
  rw [ofFn_star]
  simp only [weightsData,supplierView,indices,List.length_ofFn,RoundingList.range_finRange,
    List.flatMap_def,Function.comp_def,← List.ofFn_eq_map,List.map_ofFn,
    List.getElem?_ofFn,dite_eq_left (Fin.isLt _),Option.getD_some,Fin.eta]
  change (List.ofFn (fun i => if outsideData (supplierView S) i.val then S.y i else 0) ++
     ((List.ofFn (fun s => List.ofFn (fun t => pairWeight (supplierView S) s.val t.val))).flatten ++
       List.ofFn (fun t => S.γ*S.c t)))=_
  simp only [outsideData_view,pairWeight_view,decide_eq_true_eq,weightQ]
end MetricKMedian.Preparation.RationalSuppliers.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_SupplierPreparationProgram
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 Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (setView indices)
open SparseIntegerLaw.BinarySparse
variable {τ : ℝ} (qR : FixedBatch.RationalParameters τ)
abbrev Input.raw (x : Input) := supplierView x.S
abbrev Input.encode (x : Input) := enc x.raw

def qData (x : SupplierRaw) : QRow := (weightsData x).map (fun w => w/qR.g)
@[fun_prop] theorem qData_poly : Poly (qData qR) := by unfold qData; apply list_map <;> fun_prop
 theorem qData_view (x : Input) : qData qR x.raw=List.ofFn (q x.S.y x.S.P x.S.A x.S.c x.S.γ qR.g) := by
  unfold qData Input.raw
  rw [weightsData_view,List.map_ofFn]
  rfl

def Input.prepared (x : Input) : SparsePrepared.Program.Input :=
  ⟨x.n,size x.f x.n,x.f,D x.S.A,a,q x.S.y x.S.P x.S.A x.S.c x.S.γ qR.g,
    x.S.P,x.S.y,x.S.p,qR.Δ,x.S.hy,x.S.hp,a_bounds,
    q_nonneg _ _ _ _ _ _ x.S.hy x.S.hc0 x.S.hγ.le (FixedParameters.positive qR).le⟩
def prepareData (x : SupplierRaw) : SparsePrepared.Program.Raw :=
  ((targetsData x,(qData qR x,(x.2.1,(x.1,(x.2.2.2.1,qR.Δ))))),flagsData x)
@[fun_prop] theorem prepareData_poly : Poly (prepareData qR) := by unfold prepareData; fun_prop
 theorem prepareData_view (x : Input) : prepareData qR x.raw=(x.prepared qR).raw := by
  unfold prepareData
  rw [qData_view]
  change ((targetsData (supplierView x.S),_),flagsData (supplierView x.S))=_
  rw [targetsData_view,flagsData_view]
  rfl
noncomputable def preparedInputProgram : PolyProgram Input.encode SparsePrepared.Program.Input.encode (Input.prepared qR) :=
  (prepareData_poly qR).program.recode Input.raw (fun _ => rfl) (fun x => congrArg enc (prepareData_view qR x))

abbrev PreparedRaw := SparsePrepared.Program.PreparedRaw

def countsData (x : SupplierRaw × PreparedRaw) : List ℕ :=
  ((indices x.1.1).map (fun i => ⌊(qData qR x.1)[i]?.getD 0⌋₊+
    if 0 < x.2.1.1[i]?.getD 0 then 1 else 0)) ++ x.2.2.flatten
@[fun_prop] theorem countsData_poly : Poly (countsData qR) := by
  unfold countsData
  apply append_poly
  · apply list_map <;> fun_prop
  · exact comp (⟨listFlatten (enc : ℕ → List Bool) 0⟩ : Poly (List.flatten : List (List ℕ) → List ℕ)) (by fun_prop)

theorem countsData_view (x : Input) (z : SparseSignedPreparation.State x.n (size x.f x.n) × SparseCounts.Table x.f x.n) :
    countsData qR (x.raw,SparsePrepared.Program.view z)=List.ofFn (counts x.S.y x.S.P x.S.A x.S.c x.S.γ qR.g z) := by
  change _=List.ofFn (fun e => Sum.elim _ _ (physicalIndex e))
  rw [ofFn_physical]
  simp only [countsData,Input.raw,supplierView,indices,List.length_ofFn,RoundingList.range_finRange,
    ← List.ofFn_eq_map,List.map_ofFn,Function.comp_def,SparsePrepared.Program.view,
    SparseSignedPreparation.Program.view,SparseCounts.ListOperation.view]
  congr 1
  congr 1
  funext i
  have hq := qData_view qR x
  change (⌊(qData qR x.raw)[i.val]?.getD 0⌋₊+if 0<(z.1.1.toList)[i.val]?.getD 0 then 1 else 0)=_
  rw [hq]
  simp only [SparseOuterLaw.outsideCount,SparseGridRounding.base,index_inl,List.getElem?_ofFn,
    dite_eq_left (show i.val < size x.f x.n from lt_of_lt_of_le i.isLt (Nat.le_add_right _ _)),
    Option.getD_some,Vector.getElem?_toList,Vector.getElem?_eq_getElem (show i.val < size x.f x.n from lt_of_lt_of_le i.isLt (Nat.le_add_right _ _)),
    RationalWeightedStep.point]
  rfl

def tablesData (x : SupplierRaw × List PreparedRaw) : List (List ℕ) := x.2.map (fun z => countsData qR (x.1,z))
@[fun_prop] theorem tablesData_poly : Poly (tablesData qR) := by unfold tablesData; apply list_map <;> fun_prop
end MetricKMedian.Preparation.RationalSuppliers.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_SupplierScanProgram
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 Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
variable {τ : ℝ} (qR : FixedBatch.RationalParameters τ)
abbrev ScanRaw := SupplierRaw × ((List (List ℚ) × List (List ℚ)) × ℚ)
def ScanInput.raw (x : ScanInput) : ScanRaw := (supplierView x.S,((List.ofFn (fun i => List.ofFn (x.df i)),List.ofFn (fun c => List.ofFn (x.dc c))),x.budget))
def originals (x : SupplierRaw) : List ℕ := indices x.1 ++ x.2.2.2.1.flatMap (fun _ => indices x.1)
end MetricKMedian.Preparation.RationalSuppliers.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_RationalSortProgram
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.RationalSortProgram
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly

 theorem insertData_sorted (xs : List ℚ) (hx : xs.SortedLT) (a : ℚ) : (insertData (xs,a)).SortedLT := by
  rw [List.sortedLT_iff_pairwise]
  rw [insertData,List.pairwise_append,List.pairwise_cons]
  refine ⟨hx.pairwise.filter _,⟨?_,hx.pairwise.filter _⟩,?_⟩
  · intro b hb
    exact of_decide_eq_true (List.mem_filter.mp hb).2
  · intro b hb c hc
    have hb' : b<a := of_decide_eq_true (List.mem_filter.mp hb).2
    rcases List.mem_cons.mp hc with rfl | hc
    · exact hb'
    · exact hb'.trans (of_decide_eq_true (List.mem_filter.mp hc).2)
 theorem insertData_mem (xs : List ℚ) (a q : ℚ) : q∈insertData (xs,a) ↔ q=a ∨ q∈xs := by
  simp only [insertData,List.mem_append,List.mem_filter,List.mem_cons,decide_eq_true_eq]
  constructor
  · tauto
  · rintro (rfl | hq)
    · tauto
    · rcases lt_trichotomy q a with h | h | h <;> tauto
 theorem insertData_sort (Q : Finset ℚ) (a : ℚ) : insertData (Q.sort,a) = (insert a Q).sort := by
  apply List.SortedLT.eq_of_mem_iff
  · exact insertData_sorted Q.sort Q.sortedLT_sort a
  · exact (insert a Q).sortedLT_sort
  · intro q
    simp only [insertData_mem,mem_sort,mem_insert]
 theorem fold_sort (xs : List ℚ) (Q : Finset ℚ) :
     xs.foldl (fun s a => insertData (s,a)) Q.sort=(xs.toFinset ∪ Q).sort := by
  induction xs generalizing Q with
  | nil => simp
  | cons a xs ih =>
    rw [List.foldl_cons,insertData_sort,ih]
    congr 1
    ext q
    simp only [List.toFinset_cons,mem_union,mem_insert]
    tauto
 theorem sort_eq (xs : List ℚ) : sort xs=xs.toFinset.sort := by
  have h := fold_sort xs ∅
  simpa only [sort,Finset.sort_empty,union_empty] using h
end MetricKMedian.RationalSortProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_UnitRepresentativeProgram
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.RationalUnitInput.Program
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
open MetricKMedian.MaskProgram
def view {f j : ℕ} (U : RationalUnitInput f j) : Raw :=
  ((List.ofFn U.y,List.ofFn (fun c => setView (U.F c))),
    (List.ofFn (fun c => List.ofFn (U.dc c)),(List.ofFn (fun c => List.ofFn (U.dd c)),List.ofFn (fun a => List.ofFn (U.df a)))))
abbrev Input.raw (x : Input) := view x.U
abbrev Input.encode (x : Input) := enc x.raw

 theorem ranks_view {n : ℕ} (s : Finset (Fin n)) :
    ranks (setView s)=List.ofFn (fun i : Fin s.card => (s.orderEmbOfFin rfl i).val) := by
  have h : ((List.finRange n).filter (fun i => decide (i∈s))).map Fin.val =
      List.ofFn (fun i : Fin s.card => (s.orderEmbOfFin rfl i).val) := by
    rw [EncodingLists.filter_range,Finset.filter_mem_eq_inter,Finset.univ_inter,
      ← EncodingLists.sorted_enum,List.map_ofFn]
    rfl
  rw [← h]
  simp only [ranks,indices,setView,List.length_ofFn,RoundingList.range_finRange,List.filter_map]
  congr 1
  apply List.filter_congr
  intro i hi
  simp only [Function.comp_def,MetricKMedian.MaskProgram.get,List.getElem?_ofFn,dite_eq_left i.isLt,Option.getD_some,Fin.eta]

end MetricKMedian.Preparation.RationalUnitInput.Program
end

end OAI
end