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

import Mathlib
import Definitions.Def_OAIQ037K056
import Definitions.Def_OAIQ037K057
import Definitions.Def_OAIQ037K058

section
-- module Solutions.OAIQ037_KM.KMedian_Process_RoundingStateCompiler
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
open SparseIntegerLaw.BinarySparse

theorem branch_raw (s : Bool) (x : State s) :
    (x.raw.1,(branchLawData (x.raw.2.1,x.raw.2.2.map (fun p => probability s (x.raw.1,p))),
      x.raw.2.2.flatMap (fun p => [endpoint s false (x.raw.1,p),endpoint s true (x.raw.1,p)])))=
       x.branch.raw := by
  cases s
  · change (List.ofFn x.β,_)=(List.ofFn x.β,vectorData
      (x.μ.branch (RationalWeightedStep.probability x.β)
        (RationalWeightedStep.probability_unit x.β (x.positive rfl)) (RationalWeightedStep.endpoint x.β)))
    apply congrArg (fun d => (List.ofFn x.β,d))
    exact vectorData_branch x.μ _ _ _ (RoundingList.probability (List.ofFn x.β))
      (fun p => RoundingList.endpoint (List.ofFn x.β) p false)
      (fun p => RoundingList.endpoint (List.ofFn x.β) p true)
      (RoundingList.probability_list x.β)
      (fun p => RoundingList.endpoint_list x.β p 0) (fun p => RoundingList.endpoint_list x.β p 1)
  · change (List.ofFn x.β,_)=(List.ofFn x.β,vectorData
      (x.μ.branch (RationalSignedStep.probability x.β)
        (RationalSignedStep.probability_unit x.β) (RationalSignedStep.endpoint x.β)))
    apply congrArg (fun d => (List.ofFn x.β,d))
    exact vectorData_branch x.μ _ _ _ (RoundingList.Signed.probability (List.ofFn x.β))
      (fun p => RoundingList.Signed.endpoint (List.ofFn x.β) p false)
      (fun p => RoundingList.Signed.endpoint (List.ofFn x.β) p true)
      (RoundingList.Signed.probability_list x.β)
      (fun p => RoundingList.Signed.endpoint_list x.β p 0) (fun p => RoundingList.Signed.endpoint_list x.β p 1)

noncomputable def branchProgram (s : Bool) : PolyProgram State.encode State.encode (@State.branch s) :=
  (branchRawProgram s).recode State.raw State.encode_raw (fun x => by
    rw [branch_raw,State.encode_raw])

noncomputable def compressionInputProgram (s : Bool) :
    PolyProgram State.encode IntegerLaw.BinaryCompression.RationalInput.encode (@State.compressionInput s) := by
  let β := fst erow (ed erow)
  let law := (snd erow (ed erow)).comp (fst el (encodeList erow))
  let states := (snd erow (ed erow)).comp (snd el (encodeList erow))
  let dims := β.comp RoundingList.dimensions_poly.program
  let feats := states.comp (RoundingList.features_poly.program.listMap [])
  let work := dims.fanout (law.fanout feats)
  exact work.recode State.raw State.encode_raw (fun x => by
    change IntegerLaw.BinaryCompression.eqd
      (RoundingList.dimensions (List.ofFn x.β),
       ((x.μ.law.denominator,List.ofFn x.μ.law.numerator),
        (x.μ.states.toList.map Vector.toList).map RoundingList.features))=_
    simp only [RoundingList.dimensions_list,states_list,List.map_ofFn,Function.comp_def,RoundingList.features_list]
    rfl)

end MetricKMedian.RoundingProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_RoundingRunProgram
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 Polynomial
open SparseIntegerLaw.BinarySparse

noncomputable def startProgram (s : Bool) : PolyProgram Input.encode State.encode (@Input.start s) := by
  let β := fst erow erow
  let p := snd erow erow
  let law := constant (encodePair erow erow) el ((1:ℤ),[(1:ℤ)])
  let ps := (p.fanout (constant (encodePair erow erow) (encodeList erow) [])).comp (listCons erow)
  let work := β.fanout (law.fanout ps)
  exact work.recode Input.raw (fun _ => rfl) (fun x => by
    change encodePair erow (ed erow) (List.ofFn x.β,((1,[1]),[x.p.toList]))=_
    rw [← State.encode_raw]
    rfl)

end MetricKMedian.RoundingProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_CardinalRoundProgram
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.SparseCardinalRounding.Program
open Binary Binary.PolyProgram Function SparseIntegerLaw.BinarySparse
def result (x : Input) : Data (List Bool) :=
  SparseGraph.Program.columnRaw ((round (Vector.ofFn x.p)).map selected)

end MetricKMedian.SparseCardinalRounding.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_TaperGraphProgram
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.TaperGraphProgram
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseIntegerLaw.BinarySparse
abbrev Input.encode (x : Input) := enc x.raw

end MetricKMedian.TaperGraphProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_CopyGraphProgram
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.RationalPhysicalKernel.CopyGraphProgram
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly Finset
open SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Row Table setView)
open CopyList

abbrev Input.encode (x : Input) := enc x.raw

 theorem prepare_input (x : Input) : prepare x.raw=x.taper.raw := by
  dsimp only [TaperGraphProgram.Input.raw,Input.taper]
  simp only [prepare,Input.raw,active_view,List.map_ofFn,Function.comp_def,rank_owner,
    List.getElem?_ofFn,dite_eq_left (Fin.isLt _),Option.getD_some,Fin.eta,
    mem_map_equiv,Equiv.symm_symm,own,mem_filter,mem_univ,true_and]
  simp only [Fin.ext_iff]
noncomputable def taperProgram : PolyProgram Input.encode TaperGraphProgram.Input.encode Input.taper :=
  prepare_poly.program.recode Input.raw (fun _ => rfl) (fun x => congrArg enc (prepare_input x))

 attribute [local instance] OAI.MetricKMedian.RationalPhysicalKernel.CopyGraphProgram.instLinearOrderSubtypeCopyFinMemFinset
theorem reindexed_lift {f Δ : ℕ} (A : Finset (CopyState.Copy (F:=Fin f) Δ))
    (G : Fin A.card → Finset (Fin A.card)) :
    RationalBatchData.Ordinal.graphView (ordinal A) (SparseEnumeratedGraph.lift (enumeration A) G)=
      SparseGraph.ListOperation.view G := by
  simp only [RationalBatchData.Ordinal.graphView,RationalBatchData.Ordinal.sets_eq,
    SparseGraph.ListOperation.view]
  apply congrArg List.ofFn
  funext i
  apply congrArg List.ofFn
  funext h
  apply Bool.eq_iff_iff.mpr
  simp only [decide_eq_true_eq]
  rw [SparseEnumeratedGraph.mem_lift]
  change (enumeration A).symm (enumeration A h)∈G ((enumeration A).symm (enumeration A i)) ↔ _
  rw [Equiv.symm_apply_apply,Equiv.symm_apply_apply]

 local instance instLinearOrderCopyFin_r3772a2_1 {f Δ : ℕ} : LinearOrder (CopyState.Copy (F:=Fin f) Δ) := copyOrder
theorem result_eq (x : Input) : x.taper.qInput.result=x.result := by
  unfold Input.result Input.law graphLaw SparseEnumeratedGraph.law
  simp only [SparseIntegerLaw.map,Vector.toList_map,List.map_map,Function.comp_def,reindexed_lift]
  unfold SparseGraph.Program.QInput.result
  rw [taper_q]
  rfl

end MetricKMedian.RationalPhysicalKernel.CopyGraphProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_MaximumProgram
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.MaskProgram
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView)
 theorem radius_view {n : ℕ} (d : Fin n → ℚ) (U : Finset (Fin n)) (hU : U.Nonempty) :
    radius (List.ofFn d,setView U)=(U.image d).max' (hU.image _) :=
  maximum_eq_finset _ _ _ (selectedValues_mem d U)
end MetricKMedian.MaskProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_NearestMaskProgram
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.RationalNearest.MaskProgram
open Finset Binary Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
open MetricKMedian.MaskProgram

 theorem erase_view {n : ℕ} (U : Finset (Fin n)) (a : Fin n) : erase (a.val,setView U)=setView (U.erase a) := by
  simp only [erase,indices,setView,List.length_ofFn,RoundingList.range_finRange,← List.ofFn_eq_map,List.map_ofFn]
  apply congrArg List.ofFn
  funext i
  simp only [Function.comp_def,MetricKMedian.MaskProgram.get,List.getElem?_ofFn,dite_eq_left i.isLt,Option.getD_some,Fin.eta,mem_erase,
    Bool.decide_and]
  simp only [ne_eq,Fin.val_inj]
  exact Bool.and_comm _ _
 theorem insert_view {n : ℕ} (U : Finset (Fin n)) (a : Fin n) : insert (a.val,setView U)=setView (Insert.insert a U) := by
  simp only [insert,indices,setView,List.length_ofFn,RoundingList.range_finRange,← List.ofFn_eq_map,List.map_ofFn]
  apply congrArg List.ofFn
  funext i
  simp only [Function.comp_def,MetricKMedian.MaskProgram.get,List.getElem?_ofFn,dite_eq_left i.isLt,Option.getD_some,Fin.eta,mem_insert,Fin.ext_iff,
    Bool.decide_or]
  exact Bool.or_comm _ _

 theorem raw_view {n : ℕ} (d : Fin n → ℚ) (U : Finset (Fin n)) (k : ℕ) :
    raw k (List.ofFn d,setView U)=setView (takeNearest d k U) := by
  induction k generalizing U with
  | zero => simp only [raw,takeNearest,setView,List.map_ofFn,Function.comp_def,notMem_empty,decide_false]
  | succ k ih =>
    unfold raw takeNearest
    rw [Completion.Rational.PackingProgram.any_view]
    by_cases h : U.Nonempty
    · simp only [decide_eq_true h,ite_true,dite_eq_left h]
      rw [MetricKMedian.MaskProgram.nearest_view d U h]
      have he : Preparation.firstNearest U d h=least U d h := rfl
      rw [he,erase_view,ih,insert_view]
    · simp only [decide_eq_false h,Bool.false_eq_true,ite_false,dite_eq_right h,setView,List.map_ofFn,
        Function.comp_def,notMem_empty,decide_false]
end MetricKMedian.Preparation.RationalNearest.MaskProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_CopyNearestProgram
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.FixedBatch.RationalParameters.CopyNearestProgram
open Finset Binary Binary.Automatic Binary.Automatic.Poly
open RationalPhysicalKernel RationalPhysicalKernel.CopyList
open SparseGraph.ListOperation (Row Table setView indices)
variable {τ : ℝ} (q : RationalParameters τ)
 theorem distances_view {f Δ : ℕ} (d : Fin f → ℚ) (A : Finset (CopyState.Copy (F:=Fin f) Δ)) :
    distances Δ (List.ofFn d,view A)=List.ofFn (fun k : Fin (f*Δ) => d (finProdFinEquiv.symm k).1) := by
  simp only [distances,indices,view,setView,List.length_ofFn,RoundingList.range_finRange,← List.ofFn_eq_map,List.map_ofFn]
  apply congrArg List.ofFn
  funext k
  have hk : k.val/Δ=(finProdFinEquiv.symm k).1.val := by
    simpa only [rank,Equiv.apply_symm_apply] using CopyGraphProgram.rank_owner (finProdFinEquiv.symm k)
  simp only [Function.comp_def,hk,List.getElem?_ofFn,dite_eq_left (Fin.isLt _),Option.getD_some,Fin.eta]

@[fun_prop] theorem nearestRaw_poly (Δ : ℕ) : Poly (nearestRaw Δ) := by unfold nearestRaw; fun_prop
 attribute [local instance] OAI.MetricKMedian.FixedBatch.RationalParameters.CopyNearestProgram.instLinearOrderCopyFin
theorem nearestRaw_view {f j : ℕ} (d : Fin j → Fin f → ℚ) (A : Finset (CopyState.Copy (F:=Fin f) q.Δ)) (c : Fin j) :
    nearestRaw q.Δ (List.ofFn (d c),view A)=view (q.nearest d A c) := by
  unfold nearestRaw
  rw [distances_view,view,Preparation.RationalNearest.MaskProgram.raw_view]
  exact congrArg setView (Preparation.RationalNearest.takeNearest_map orderEquiv (fun a => d c a.1) q.Δ A)

def radiusRaw (Δ : ℕ) (x : List ℚ × Row) : ℚ :=
  MetricKMedian.MaskProgram.radius (distances Δ x,nearestRaw Δ x)
@[fun_prop] theorem radiusRaw_poly (Δ : ℕ) : Poly (radiusRaw Δ) := by unfold radiusRaw; fun_prop
 theorem radiusRaw_view {f j : ℕ} (d : Fin j → Fin f → ℚ) (A : Finset (CopyState.Copy (F:=Fin f) q.Δ))
    (hA : q.Δ≤A.card) (c : Fin j) : radiusRaw q.Δ (List.ofFn (d c),view A)=q.radius d A hA c := by
  unfold radiusRaw
  rw [distances_view,nearestRaw_view q]
  unfold view
  rw [MetricKMedian.MaskProgram.radius_view _ _ ((q.nearest_nonempty d A hA c).map)]
  have he : ((q.nearest d A c).map finProdFinEquiv.toEmbedding).image
      (fun k => d c (finProdFinEquiv.symm k).1)=(q.nearest d A c).image (fun a => d c a.1) := by
    ext r
    simp only [mem_image,mem_map]
    constructor
    · rintro ⟨b,⟨a,ha,rfl⟩,h⟩; exact ⟨a,ha,by simpa using h⟩
    · rintro ⟨a,ha,rfl⟩; exact ⟨finProdFinEquiv a,⟨a,ha,rfl⟩,by simp⟩
  simp only [he,RationalParameters.radius]
end MetricKMedian.FixedBatch.RationalParameters.CopyNearestProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_PhysicalBatchUpdateProgram
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.RationalPhysicalKernel.UpdateProgram
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly Finset FixedBatch
open SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Row Table setView)
open CopyList

abbrev Raw := (ℕ × Row) × RationalBatchData.GraphData.Raw
attribute [local instance] OAI.MetricKMedian.RationalPhysicalKernel.UpdateProgram.instLinearOrderSubtypeCopyFinMemFinset
def Input.raw (x : Input) : Raw := ((x.ctx.Δ,CopyList.view x.ctx.A),x.proposal.raw)

def finish (x : Raw × Data Row) : Data Row :=
  (x.2.1,x.2.2.map (fun Z => CopyNext.transition (x.1.1,((RationalBatchData.GraphData.prepare x.1.2).2,Z))))
@[fun_prop] theorem finish_poly : Poly finish := by
  unfold finish
  apply pair
  · fun_prop
  · apply list_map <;> fun_prop

end MetricKMedian.RationalPhysicalKernel.UpdateProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_PhysicalRoundProgram
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.RationalPhysicalKernel.RoundProgram
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly Finset
open SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Row Table)
open CopyList UpdateProgram

abbrev Raw := CopyGraphProgram.Raw × (ℚ × (ℚ × ℚ))
def ctxRaw (x : Context) : Raw := (x.toInput.raw,(x.β,(x.p,x.φ)))
abbrev ctxEncode (x : Context) := enc (ctxRaw x)

def attach (x : Raw × Data Table) : LawData × List UpdateProgram.Raw :=
  (x.2.1,x.2.2.map fun G => ((x.1.1.1.1.2,x.1.1.2),
    (((x.1.1.1.1.1.1,x.1.2.1),(x.1.1.1.1.2,x.1.2.2)),G)))
@[fun_prop] theorem attach_poly : Poly attach := by
  unfold attach
  apply pair
  · fun_prop
  · apply list_map <;> fun_prop

 local instance instLinearOrderSubtypeCopyFinMemFinset_r3772a2_1 {f Δ : ℕ} (A : Finset (CopyState.Copy (F:=Fin f) Δ)) : LinearOrder ↥A := activeOrder A
theorem attach_input (x : Context) : attach ((ctxRaw x),x.toInput.result)=
    (x.toInput.result.1, (ctxInputs x).map UpdateProgram.Input.raw) := by
  simp only [attach,ctxRaw,CopyGraphProgram.Input.result,ctxInputs,
    List.map_map,Function.comp_def]
  rfl

def ctxResult (x : Context) : Data Row :=
  (((ctxLaw x).law.denominator,List.ofFn (ctxLaw x).law.numerator),(ctxLaw x).states.toList.map CopyList.view)

end MetricKMedian.RationalPhysicalKernel.RoundProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_PhysicalHistoriesProgram
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.RationalPhysicalKernel.HistoryProgram
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly Finset
open SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Row Table)
open CopyList UpdateProgram
abbrev view (x : Context) (z : Hist x) := CopyList.view z.1.1
def result (P : ℕ → ℚ) (T : ℕ) (x : Context) : Data Row := table (law P T x) (view x)

def nextRaw (P : ℚ) (x : RoundProgram.Raw × Row) : RoundProgram.Raw :=
  (((((x.1.1.1.1.1.1,P),x.1.1.1.1.2),x.1.1.1.2),x.2),x.1.2)
@[fun_prop] theorem nextRaw_poly (P : ℚ) : Poly (nextRaw P) := by unfold nextRaw; fun_prop

def attach (P : ℚ) (x : RoundProgram.Raw × Data Row) : LawData × List RoundProgram.Raw :=
  (x.2.1,x.2.2.map (fun A => nextRaw P (x.1,A)))
@[fun_prop] theorem attach_poly (P : ℚ) : Poly (attach P) := by
  unfold attach
  apply pair
  · fun_prop
  · apply list_map <;> fun_prop

 theorem attach_result (P : ℕ → ℚ) (T : ℕ) (hP : 0<P T) (x : Context) :
    attach (P T) (RoundProgram.ctxRaw x,result P T x)=
      ((result P T x).1,(inputs P T hP x).map RoundProgram.ctxRaw) := by
  simp only [attach,result,table,inputs,List.map_map,Function.comp_def]
  rfl

 theorem conditional (P : ℕ → ℚ) (T : ℕ) (hP : 0<P T) (x : Context) (z : Hist x) :
    RoundProgram.ctxResult (nextCtx x (P T) hP z.1.1)=
      table (SparseHistories.branch (step x.d x.g x.β x.p x.φ (P T) x.hp x.hφ x.hupper) z) (view x) := by
  change table (RoundProgram.ctxLaw (nextCtx x (P T) hP z.1.1)) CopyList.view=_
  have hs := RoundProgram.law_step (nextCtx x (P T) hP z.1.1) z.1 rfl
  rw [hs,table_map]
  unfold SparseHistories.branch
  rw [table_map]
  rfl

end MetricKMedian.RationalPhysicalKernel.HistoryProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_HistorySelectionProgram
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.FixedBatch.RationalParameters.SelectionProgram
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Row Table setView)
open RationalPhysicalKernel
variable {τ : ℝ} (q : RationalParameters τ)
def Input.raw (x : Input q) : Raw := (List.ofFn (fun i => List.ofFn (x.d₀ i)),x.toInput.raw)
abbrev Input.encode (x : Input q) := enc x.raw

def ctxRaw (x : Raw) : RoundProgram.Raw := (((((q.g,1),q.Δ),x.1),x.2.2.2.2),(q.β,(q.probabilityQ,q.φ)))
@[fun_prop] theorem ctxRaw_poly : Poly (ctxRaw q) := by unfold ctxRaw; fun_prop

def Input.items (x : Input q) : List (Completion.Rational.Program.Input q.Δ) :=
  (q.tree x.d₀ x.A).states.toList.map (fun z => {x.toInput with A:=z.1.1})
def attach (x : Raw × Data Row) : List Completion.Rational.Program.Raw :=
  x.2.2.map (fun A => (x.1.2.1,(x.1.2.2.1,(x.1.2.2.2.1,A))))
@[fun_prop] theorem attach_poly : Poly attach := by unfold attach; apply list_map <;> fun_prop
 theorem attach_input (x : Input q) : attach (x.raw,HistoryProgram.result q.taperAt q.T x.ctx)=
    x.items.map Completion.Rational.Program.Input.raw := by
  simp only [attach,HistoryProgram.result,table,Input.items,List.map_map,Function.comp_def]
  rfl

def dummy : Completion.Rational.Program.Input q.Δ where
  f := 0
  j := 0
  d := fun c => Fin.elim0 c
  R := fun c => Fin.elim0 c
  A := ∅
  B := fun c => Fin.elim0 c
  hB := fun c => Fin.elim0 c

def metadata (x : Raw) : ℚ × List (List ℚ) :=
  (q.g*Completion.Rational.BestProgram.card x.2.2.2.2+q.allowance,x.2.2.1.1)
@[fun_prop] theorem metadata_poly : Poly (metadata q) := by unfold metadata; fun_prop

def Input.result (x : Input q) : Table :=
  ((q.selectCompleted x.d₀ x.d x.R x.A x.B x.hB).map setView).toList
end MetricKMedian.FixedBatch.RationalParameters.SelectionProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_GridDataProgram
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.FixedBatch.RationalParameters.GridDataProgram
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView)
open RationalPhysicalKernel CopyList CopyNearestProgram
variable {τ : ℝ} (q : RationalParameters τ)

structure Input where
  f : ℕ
  j : ℕ
  d₀ : Fin f → Fin f → ℚ
  d : Fin j → Fin f → ℚ
  A : Finset (CopyState.Copy (F:=Fin f) q.Δ)
  enough : q.Δ≤A.card
abbrev Raw := List Unit × ((List (List ℚ) × List (List ℚ)) × Row)
def Input.raw (x : Input q) : Raw := (List.replicate x.f (),((List.ofFn (fun i => List.ofFn (x.d₀ i)),
  List.ofFn (fun c => List.ofFn (x.d c))),view x.A))

def Input.selection (x : Input q) : SelectionProgram.Input q where
  f := x.f
  j := x.j
  d := x.d
  R := q.radius x.d x.A x.enough
  A := x.A
  B := q.nearest x.d x.A
  hB := q.nearest_nonempty x.d x.A x.enough
  d₀ := x.d₀

def prepare (Δ : ℕ) (x : Raw) : SelectionProgram.Raw :=
  (x.2.1.1,(x.1,((x.2.1.2,x.2.1.2.map (fun ds => radiusRaw Δ (ds,x.2.2))),
    (x.2.1.2.map (fun ds => nearestRaw Δ (ds,x.2.2)),x.2.2))))
@[fun_prop] theorem prepare_poly (Δ : ℕ) : Poly (prepare Δ) := by
  unfold prepare
  have hr : Poly (fun x : Raw => x.2.1.2.map (fun ds => radiusRaw Δ (ds,x.2.2))) := by apply list_map <;> fun_prop
  have hn : Poly (fun x : Raw => x.2.1.2.map (fun ds => nearestRaw Δ (ds,x.2.2))) := by apply list_map <;> fun_prop
  fun_prop
 theorem prepare_input (x : Input q) : prepare q.Δ x.raw=x.selection.raw := by
  simp only [prepare,Input.raw,List.map_ofFn,Function.comp_def,nearestRaw_view q,radiusRaw_view q x.d x.A x.enough]
  rfl
end MetricKMedian.FixedBatch.RationalParameters.GridDataProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_RoundCountsProgram
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.FixedBatch.RationalParameters.RoundCountsProgram
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView)
open RationalPhysicalKernel CopyList
variable {τ : ℝ} (q : RationalParameters τ)
abbrev Input.encode (x : Input) := enc x.raw

@[fun_prop] theorem cap_poly (Δ : ℕ) : Poly (cap Δ) := by unfold cap; apply comp bool_all; apply list_map <;> fun_prop
 theorem cap_input (x : Input) : cap q.Δ (List.ofFn x.n)=decide (∀ i, x.n i≤q.Δ) := by
  apply Bool.eq_iff_iff.mpr
  simp [cap]

def valid (Δ : ℕ) (x : Raw) : Bool := cap Δ x.2.2 && decide (Δ≤Completion.Rational.BestProgram.card (CopyState.CountsProgram.mask Δ x.2.2))
@[fun_prop] theorem valid_poly (Δ : ℕ) : Poly (valid Δ) := by unfold valid; fun_prop
 theorem valid_input (x : Input) (hn : ∀ i, x.n i≤q.Δ) : valid q.Δ x.raw=decide (q.Δ≤(CopyState.activeSlots x.n hn).card) := by
  unfold valid Input.raw
  dsimp only
  rw [cap_input q x,decide_eq_true hn,Bool.true_and,CopyState.CountsProgram.mask_view x.n hn,
    CopyList.view,Completion.Rational.BestProgram.card_view,card_map]

def dummy : SelectionProgram.Input q where
  f := 0
  j := 0
  d := fun c => Fin.elim0 c
  R := fun c => Fin.elim0 c
  A := ∅
  B := fun c => Fin.elim0 c
  hB := fun c => Fin.elim0 c
  d₀ := fun i => Fin.elim0 i

def Input.selection (x : Input) : SelectionProgram.Input q :=
  if hn : ∀ i, x.n i≤q.Δ then
    if hA : q.Δ≤(CopyState.activeSlots x.n hn).card then
      GridDataProgram.Input.selection q ⟨x.f,x.j,x.d₀,x.d,CopyState.activeSlots x.n hn,hA⟩
    else dummy q
  else dummy q

def prepare (x : Raw) : SelectionProgram.Raw :=
  if valid q.Δ x then GridDataProgram.prepare q.Δ (x.1,(x.2.1,CopyState.CountsProgram.mask q.Δ x.2.2))
  else (dummy q).raw
@[fun_prop] theorem prepare_poly : Poly (prepare q) := by unfold prepare; fun_prop
 theorem prepare_input (x : Input) : prepare q x.raw=(x.selection q).raw := by
  unfold prepare Input.selection
  by_cases hn : ∀ i, x.n i≤q.Δ
  · rw [dite_eq_left hn,valid_input q x hn]
    by_cases hA : q.Δ≤(CopyState.activeSlots x.n hn).card
    · rw [dite_eq_left hA,ite_eq_left (decide_eq_true hA)]
      rw [show (x.raw.1,(x.raw.2.1,CopyState.CountsProgram.mask q.Δ x.raw.2.2))=
        GridDataProgram.Input.raw q ⟨x.f,x.j,x.d₀,x.d,CopyState.activeSlots x.n hn,hA⟩ by
          unfold Input.raw GridDataProgram.Input.raw
          dsimp only
          rw [CopyState.CountsProgram.mask_view x.n hn]]
      exact GridDataProgram.prepare_input q _
    · simp only [dite_eq_right hA,decide_eq_false hA,Bool.false_eq_true,ite_false]
  · rw [dite_eq_right hn]
    have hv : valid q.Δ x.raw=false := by
      unfold valid Input.raw
      dsimp only
      rw [cap_input q x,decide_eq_false hn,Bool.false_and]
    simp only [hv,Bool.false_eq_true,ite_false]

def Input.result (x : Input) : Table := ((q.roundCounts x.d₀ x.d x.n).map setView).toList

def finish (x : Raw × Table) : Table := if valid q.Δ x.1 then x.2 else []
@[fun_prop] theorem finish_poly : Poly (finish q) := by unfold finish; fun_prop
 theorem finish_input (x : Input) : finish q (x.raw,SelectionProgram.Input.result q (x.selection q))=x.result q := by
  unfold finish Input.result RationalParameters.roundCounts
  by_cases hn : ∀ i, x.n i≤q.Δ
  · rw [dite_eq_left hn,valid_input q x hn]
    by_cases hA : q.Δ≤(CopyState.activeSlots x.n hn).card
    · simp only [dite_eq_left hA,decide_eq_true hA,ite_true,Input.selection,dite_eq_left hn]
      rfl
    · simp only [dite_eq_right hA,decide_eq_false hA,Bool.false_eq_true,ite_false,Option.map_none,Option.toList_none]
  · rw [dite_eq_right hn]
    have hv : valid q.Δ x.raw=false := by
      unfold valid Input.raw
      dsimp only
      rw [cap_input q x,decide_eq_false hn,Bool.false_and]
    simp only [hv,Bool.false_eq_true,ite_false,Option.map_none,Option.toList_none]

end MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_PreparedScanProgram
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.FixedBatch.RationalParameters.PreparedScanProgram
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView)
variable {τ : ℝ} (q : RationalParameters τ)
abbrev Input.encode (x : Input) := enc x.raw

def prepare (x : Raw) : List RoundCountsProgram.Raw := x.2.2.1.map (fun ns =>
  (x.1.2.map (fun _ => ()),((MaskProgram.pullbackMatrix (x.2.1.1,x.1.2),
    x.2.1.2.map (fun ds => MaskProgram.pullback (ds,x.1.2))),ns)))
@[fun_prop] theorem prepare_poly : Poly prepare := by
  unfold prepare
  apply list_map
  · have hd : Poly (fun x : Raw × List ℕ => x.1.2.1.2.map (fun ds => MaskProgram.pullback (ds,x.1.1.2))) := by
      apply list_map <;> fun_prop
    have hu : Poly (fun x : Raw × List ℕ => x.1.1.2.map (fun _ => ())) := by apply list_map <;> fun_prop
    fun_prop
  · fun_prop
 theorem prepare_input (x : Input) : prepare x.raw=x.items.map RoundCountsProgram.Input.raw := by
  simp only [prepare,Input.raw,List.map_ofFn,Function.comp_def,MaskProgram.pullbackMatrix_view,
    MaskProgram.pullback_view,List.map_map,Input.items]
  apply List.map_congr_left
  intro n _
  simp only [Input.item,RoundCountsProgram.Input.raw]
  congr 1
  simp

noncomputable def itemsProgram : PolyProgram Input.encode (encodeList RoundCountsProgram.Input.encode) Input.items :=
  prepare_poly.program.recode Input.raw (fun _ => rfl) (fun x => by
    change encodeList enc (prepare x.raw)=_
    rw [prepare_input,encodeList_map]
    rfl)

def Input.candidates (x : Input) := q.countCandidates x.df x.dc x.orig x.ns

def images (x : Raw × List Table) : Table := x.2.flatten.map (fun O => MaskProgram.imageRaw (x.1.1,O))
@[fun_prop] theorem images_poly : Poly images := by
  unfold images
  apply list_map
  · fun_prop
  · exact comp (⟨listFlatten (enc : Row → List Bool) []⟩ : Poly (List.flatten : List Table → Table)) (by fun_prop)
 theorem images_input (x : Input) : images (x.raw,x.items.map (RoundCountsProgram.Input.result q))=
    (x.candidates q).map setView := by
  simp only [images,Input.items,List.map_map,Function.comp_def,RoundCountsProgram.Input.result,
    Input.item,Input.raw]
  rw [List.map_flatten]
  simp only [List.map_map,Function.comp_def,← Option.toList_map,Option.map_map]
  change (x.ns.map (fun n => (((q.roundCounts (fun a b => x.df (x.orig a) (x.orig b))
    (fun c a => x.dc c (x.orig a)) n).map (fun O => MaskProgram.imageRaw
      ((List.replicate x.h (),List.ofFn (fun i => (x.orig i).val)),setView O))).toList))).flatten=_
  simp only [MaskProgram.imageRaw_view]
  simp only [Input.candidates,RationalParameters.countCandidates,
    List.flatMap_def,List.map_flatten,List.map_map]
  simp only [← Option.toList_map,Option.map_map,Function.comp_def]

def Input.result (x : Input) : Table := ((q.roundList x.df x.dc x.orig x.ns x.budget).map setView).toList
end MetricKMedian.FixedBatch.RationalParameters.PreparedScanProgram
end

end OAI
end