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

import Mathlib
import Definitions.Def_MetricKMedian
import Definitions.Def_OAIQ037K061
import Definitions.Def_OAIQ037K062
import Definitions.Def_OAIQ037K063

section
-- module Solutions.OAIQ037_KM.KMedian_Process_BatchOrdinalCodes
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.RationalBatchData.Ordinal
open Finset FixedBatch
open SparseGraph.ListOperation (Row Table setView indices)
variable {I : Type} [LinearOrder I] {n : ℕ}
variable (r : Fin n ≃o I) (D : Actions I I) (H : Finset I)

 theorem valid_code (e : HeavyAction D H) : ActionList.valid (view r D H) (code r D H e)=true := by
  have hp := parent_code r D H e
  cases e with
  | inl e =>
    change ActionList.valid (view r D H) (r.symm e.val).val=true
    simp only [ActionList.valid,view,sets_eq,List.length_ofFn,ite_eq_left (r.symm e.val).isLt,
      List.getElem?_ofFn,dite_eq_left (r.symm e.val).isLt,Option.getD_some,Fin.eta,
      OrderIso.apply_symm_apply,Bool.not_eq_true_eq_eq_false,decide_eq_false_iff_not]
    exact e.property
  | inr e =>
    have hc : ¬n+(r.symm e.val.1).val*n+(r.symm e.val.2).val<n := by omega
    change ActionList.valid (view r D H) (n+(r.symm e.val.1).val*n+(r.symm e.val.2).val)=true
    simp only [ActionList.valid,view,sets_eq,List.length_ofFn,ite_eq_right hc]
    rw [show ActionList.parent n (n+(r.symm e.val.1).val*n+(r.symm e.val.2).val)=(r.symm e.val.1).val from hp,
      show ActionList.child n (n+(r.symm e.val.1).val*n+(r.symm e.val.2).val)=(r.symm e.val.2).val from child_code r D H e]
    simp only [List.getElem?_ofFn,dite_eq_left (r.symm e.val.1).isLt,dite_eq_left (r.symm e.val.2).isLt,
      Option.getD_some,Fin.eta,OrderIso.apply_symm_apply,decide_eq_true e.property.1,decide_eq_true e.property.2,Bool.and_self]
 theorem mem_codes (c : ℕ) : c∈ActionList.codes (view r D H) ↔ ∃ e, code r D H e=c := by
  simp only [ActionList.codes,indices,units_length,List.mem_filter,List.mem_range]
  constructor
  · rintro ⟨hc,hv⟩
    by_cases hl : c<n
    · simp only [ActionList.valid,view,sets_eq,List.length_ofFn,ite_eq_left hl,List.getElem?_ofFn,dite_eq_left hl,
        Option.getD_some,Bool.not_eq_true_eq_eq_false,decide_eq_false_iff_not] at hv
      refine ⟨.inl ⟨r ⟨c,hl⟩,hv⟩,?_⟩
      simp only [code,OrderIso.symm_apply_apply]
    · have hn : 0<n := by nlinarith
      have hq : (c-n)/n<n := (Nat.div_lt_iff_lt_mul hn).mpr (by omega)
      have hr : (c-n)%n<n := Nat.mod_lt _ hn
      simp only [ActionList.valid,view,sets_eq,List.length_ofFn,ActionList.parent,ite_eq_right hl,ActionList.child,
        List.getElem?_ofFn,dite_eq_left hq,dite_eq_left hr,Option.getD_some,Bool.and_eq_true,decide_eq_true_eq] at hv
      refine ⟨.inr ⟨(r ⟨(c-n)/n,hq⟩,r ⟨(c-n)%n,hr⟩),hv⟩,?_⟩
      simp only [code,OrderIso.symm_apply_apply]
      have hh := Nat.mod_add_div (c-n) n
      rw [Nat.mul_comm] at hh
      have hs := Nat.sub_add_cancel (Nat.le_of_not_gt hl)
      omega
  · rintro ⟨e,rfl⟩; exact ⟨code_lt r D H e,valid_code r D H e⟩
 theorem codes_eq [Fintype I] : ActionList.codes (view r D H)=List.ofFn (fun i => code r D H (enumeration D H i)) := by
  apply List.SortedLT.eq_of_mem_iff
  · exact ((List.sortedLT_range _).pairwise.filter _).sortedLT
  · exact (enumeration_strictMono r D H).sortedLT_ofFn
  · intro c
    rw [mem_codes,List.mem_ofFn]
    constructor
    · rintro ⟨e,rfl⟩; exact ⟨(enumeration D H).symm e,by rw [Equiv.apply_symm_apply]⟩
    · rintro ⟨i,rfl⟩; exact ⟨enumeration D H i,rfl⟩
end MetricKMedian.RationalBatchData.Ordinal
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_BatchOrdinalArrays
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.RationalBatchData.Ordinal
open Finset FixedBatch
open SparseGraph.ListOperation (Row Table setView indices)
variable {I : Type} [LinearOrder I] [Fintype I] {n : ℕ}
variable (r : Fin n ≃o I) (D : Actions I I) (H : Finset I)

 theorem bal_code (Δ : ℕ) (e : HeavyAction D H) :
    ActionArrays.bal (view r D H,Δ) (code r D H e)=true ↔ e∈balanced (heavy D H) Δ := by
  unfold ActionArrays.bal
  rw [Bool.and_eq_true,decide_eq_true_eq,decide_eq_true_eq]
  rw [show (view r D H).2.length=n from sets_length r H,erase_code,sets_card,code_light]
  change (e.isLeft=true ∧ ((heavy D H).erase e).card=Δ) ↔
    e∈((univ.filter (fun e : HeavyAction D H => e.isLeft=true)).filter (fun e => ((heavy D H).erase e).card=Δ))
  simp only [mem_filter,mem_univ,true_and]
 theorem conflict_code (Δ : ℕ) (e f : HeavyAction D H) :
    ActionArrays.conflict (view r D H,Δ) (code r D H e) (code r D H f)=true ↔ f∈conflicts (heavy D H) Δ e := by
  simp only [ActionArrays.conflict,Bool.and_eq_true,Bool.not_eq_true_eq_eq_false,decide_eq_false_iff_not,
    bal_code,erase_code,overlap_sets]
  have he : code r D H f≠code r D H e ↔ f≠e :=
    not_congr (@StrictMono.injective _ _ (actionOrder D H) _ _ (code_strictMono r D H)).eq_iff
  simp only [he]
  unfold conflicts
  split_ifs with hb <;> simp only [mem_filter,notMem_empty,iff_false] <;> tauto

 theorem data_view (m : I → ℚ) (p φ : ℚ) (Δ : ℕ) :
    ActionArrays.data ((((p,φ),List.ofFn (fun i => m (r i))),Δ),view r D H)=
    ((setView ((balanced (heavy D H) Δ).map (enumeration D H).symm.toEmbedding),
      List.ofFn (fun i => setView ((conflicts (heavy D H) Δ (enumeration D H i)).map (enumeration D H).symm.toEmbedding))),
      (p,List.ofFn (fun i => RationalBatchData.bias m p φ (heavyParent D H (enumeration D H i))))) := by
  unfold ActionArrays.data
  dsimp only
  rw [codes_eq]
  apply Prod.ext
  · apply Prod.ext
    · dsimp only
      rw [List.map_ofFn]
      apply congrArg List.ofFn
      funext i
      apply Bool.eq_iff_iff.mpr
      simp only [decide_eq_true_eq,mem_map_equiv,Equiv.symm_symm,Function.comp_def]
      exact bal_code r D H Δ (enumeration D H i)
    · dsimp only
      simp only [List.map_ofFn]
      apply congrArg List.ofFn
      funext i
      apply congrArg List.ofFn
      funext j
      apply Bool.eq_iff_iff.mpr
      simp only [decide_eq_true_eq,mem_map_equiv,Equiv.symm_symm,Function.comp_def]
      exact conflict_code r D H Δ (enumeration D H i) (enumeration D H j)
  · apply Prod.ext
    · rfl
    · dsimp only
      rw [List.map_ofFn,show (view r D H).2.length=n from sets_length r H]
      apply congrArg List.ofFn
      funext i
      exact bias_code r D H m p φ (enumeration D H i)

 theorem masses_graph (G : I → Finset I) (g : ℚ) :
    GraphData.masses (g,graphView r G)=List.ofFn (fun h => graphMass G g (r h)) := by
  simp only [GraphData.masses,transpose_graph,List.map_ofFn,Function.comp_def,sets_card]
  rfl
 theorem heavy_graph (G : I → Finset I) (g b : ℚ) :
    GraphData.heavy (b,GraphData.masses (g,graphView r G))=sets r (heavySet (graphMass G g) b) := by
  rw [masses_graph]
  simp only [GraphData.heavy,GraphData.amount_view,List.map_ofFn,Function.comp_def,sets_eq,
    heavySet,mem_filter,mem_univ,true_and]
  have ha : RationalBatchData.amount (fun h => graphMass G g (r h))=RationalBatchData.amount (graphMass G g) :=
    r.toEquiv.sum_comp (fun h => max (1-graphMass G g h) 0)
  rw [ha]
 theorem prepare_graph (G : I → Finset I) (g b p φ : ℚ) (Δ : ℕ) :
    GraphData.prepare (((g,b),(Δ,(p,φ))),graphView r G)=
      ((((p,φ),List.ofFn (fun h => graphMass G g (r h))),Δ),view r (graph G) (heavySet (graphMass G g) b)) := by
  unfold GraphData.prepare
  dsimp only
  rw [heavy_graph,masses_graph,transpose_graph]
  rfl
end MetricKMedian.RationalBatchData.Ordinal
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_TaperAllProgram
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.Taper.ListOperation
open Binary Binary.Automatic Binary.Automatic.Poly Finset
 theorem sourceRow_list {n : ℕ} (g P : ℚ) (d : Fin n → ℚ) (own : Finset (Fin n)) (Δ : ℕ) :
    sourceRow ((((g,P),List.ofFn d),List.ofFn fun i => decide (i∈own)),Δ)=List.ofFn (sourceMarginals g P d own Δ) := by
  simp only [sourceRow,colocated_list,sourceMarginals]
  split_ifs
  · exact zeroRow_list d own Δ
  · simp only [List.map_ofFn,radius_list,Function.comp_def]
end MetricKMedian.Taper.ListOperation
end

end OAI
end

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

noncomputable def compressProgram (s : Bool) : PolyProgram State.encode State.encode (@State.compress s) := by
  let law := (compressionInputProgram s).comp IntegerLaw.BinaryCompression.rationalCompressProgram
  let trimmed := (law.fanout (statesProgram s)).comp (trimDataProgram erow [])
  let work := (weightsProgram s).fanout trimmed
  exact work.recode id (fun _ => rfl) (fun x => by
    change encodePair erow (ed erow) (List.ofFn x.β,
      trimData (((x.μ.law.compressAuto (fun i => SparseWeightedPartial.features x.μ.states[i.val])).denominator,
       List.ofFn (x.μ.law.compressAuto (fun i => SparseWeightedPartial.features x.μ.states[i.val])).numerator),
         x.μ.states.toList.map Vector.toList))=_
    rw [show trimData _= _ from trim_encode_raw
      (⟨x.μ.length,x.μ.states,x.μ.law.compressAuto (fun i => SparseWeightedPartial.features x.μ.states[i.val])⟩ : SparseIntegerLaw (Vector ℚ x.n))]
    exact State.encode_raw x.compress)

noncomputable def stepProgram (s : Bool) : PolyProgram State.encode State.encode (@State.step s) :=
  (branchProgram s).comp (compressProgram s)

end MetricKMedian.RoundingProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Probability_BernoulliStepProgram
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.SparseBernoulli.Program
open Binary Binary.PolyProgram Function
open SparseIntegerLaw.DependentProgram

noncomputable def branchProgram : PolyProgram State.encode State.encode (Bundle.branch probability probability_unit endpoint) :=
  SparseIntegerLaw.DependentProgram.branchProgram Context.encode er view [] probability probability_unit endpoint
    rowProbability (rowEndpoint true) (rowEndpoint false) probability_view
    (fun c q => endpoint_view c q 0) (fun c q => endpoint_view c q 1)
    probabilityProgram (endpointProgram true) (endpointProgram false)

noncomputable def stepProgram (d : ℕ) : PolyProgram State.encode State.encode (State.step d) :=
  ((PolyProgram.ite activeProgram (identity State.encode) (branchProgram.comp (compressProgram d))).comp incrementProgram).congr _
    (fun x => by simp only [State.step,Function.comp_def,decide_eq_true_eq,id_eq])

end MetricKMedian.SparseBernoulli.Program
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 runProgram (s : Bool) : PolyProgram Input.encode State.encode (fun x : Input s => x.run x.n) :=
  ((stepProgram s).repeatFrom (startProgram s) (countProgram s) X statePolynomial
    (fun x => by simpa using (input_bounds x).1) (fun x i hi => by
      rw [input_iterate]; exact run_size x i hi)).congr _ (fun x => input_iterate x _)

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

noncomputable def program : PolyProgram encodeInput (ed br) result := by
  let part := inputProgram.comp (RoundingProgram.runProgram false)
  let get : PolyProgram RoundingProgram.State.encode (ed RoundingProgram.erow)
      (fun x : RoundingProgram.State false => RoundingProgram.vectorData x.μ) :=
    (snd RoundingProgram.erow (ed RoundingProgram.erow)).recode RoundingProgram.State.raw
      RoundingProgram.State.encode_raw (fun _ => rfl)
  let post : PolyProgram (ed RoundingProgram.erow) (ed br)
      (fun x : Data (List ℚ) => (x.1,x.2.map selectedRow)) := by
    apply Binary.Automatic.Poly.program
    apply Binary.Automatic.Poly.pair
    · fun_prop
    · apply Binary.Automatic.Poly.list_map <;> fun_prop
  exact (part.comp get |>.comp post).congr _ (fun x => by
    simp only [Function.comp_def,result,RoundingProgram.vectorData,SparseGraph.Program.columnRaw,
      SparseIntegerLaw.map,Vector.toList_map,List.map_map,selectedRow_eq]
    rfl)
end MetricKMedian.SparseCardinalRounding.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_GraphLawProgram
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.SparseGraph.Program
open Binary Binary.PolyProgram Function SparseIntegerLaw.BinarySparse
open SparseIntegerLaw.DependentProgram

noncomputable def inputProgram : PolyProgram QInput.encode Input.encode QInput.input := by
  let n := (fst (encodeList (fun _ : Unit => [])) qt).recode QInput.raw (fun _ => rfl) (fun _ => rfl)
  let cols := columnsProgram.comp (SparseCardinalRounding.Program.program.listMap emptyColumn)
  exact (n.fanout cols).recode id (fun _ => rfl) (fun x => by
    change ei (x.raw.1,x.columns.map SparseCardinalRounding.Program.result)=Input.encode x.input
    simp only [QInput.columns,List.map_ofFn,Function.comp_def]
    rfl)

noncomputable def lawProgram : PolyProgram QInput.encode (ed ListOperation.et) QInput.result := by
  let get : PolyProgram State.encode (ed ListOperation.et) (fun x : State => (x.raw view).2) :=
    (snd Context.encode (ed ListOperation.et)).recode (Bundle.raw view) (fun _ => rfl) (fun _ => rfl)
  exact (inputProgram.comp runStateProgram |>.comp get).congr _ (fun _ => rfl)
end MetricKMedian.SparseGraph.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

 theorem rawQ_input (x : Input) : rawQ x.raw=x.qInput.raw := by
  simp only [rawQ,Input.raw,List.map_ofFn,Function.comp_def,Taper.ListOperation.sourceRow_list,
    SparseGraph.Program.QInput.raw,Input.qInput,List.ofFn_const]

noncomputable def qInputProgram : PolyProgram Input.encode SparseGraph.Program.QInput.encode Input.qInput :=
  rawQ_poly.program.recode Input.raw (fun _ => rfl) (fun x => congrArg enc (rawQ_input x))
noncomputable def program : PolyProgram Input.encode (ed SparseGraph.ListOperation.et)
    (fun x : Input => x.qInput.result) := qInputProgram.comp SparseGraph.Program.lawProgram
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

noncomputable def program : PolyProgram Input.encode (ed SparseGraph.ListOperation.et) Input.result :=
  (taperProgram.comp TaperGraphProgram.program).congr _ result_eq

end MetricKMedian.RationalPhysicalKernel.CopyGraphProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Probability_BernoulliRunProgram
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.SparseBernoulli.Program
open Binary Binary.PolyProgram Function Polynomial
open SparseIntegerLaw.DependentProgram
open SparseIntegerLaw.BinarySparse (el ed)

noncomputable def runStateProgram (d : ℕ) : PolyProgram Input.encode State.encode (fun x => x.state d x.n) :=
  ((stepProgram d).repeatFrom startProgram countProgram X (sizePolynomial d)
    (fun x => by simpa using (input_bounds x).1)
    (fun x t ht => by rw [state_iterate]; exact state_size x d t ht)).congr _ (fun x => state_iterate x d _)

end MetricKMedian.SparseBernoulli.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_PhysicalBatchProgram
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.SparsePhysicalBatch.Program
open Binary Binary.PolyProgram Function
open SparseIntegerLaw.BinarySparse SparseIntegerLaw.DependentProgram
open SparseGraph.ListOperation (Row Table et)
local notation "br" => SparseGraph.ListOperation.er

noncomputable def bernProgram (bal : Bool) : PolyProgram Input.encode (ed br)
    (fun x : Input => (((x.bern bal).law.denominator,List.ofFn (x.bern bal).law.numerator),
      (x.bern bal).states.toList.map List.ofFn)) := by
  let get : PolyProgram SparseBernoulli.Program.State.encode (ed br)
      (fun x : SparseBernoulli.Program.State => (x.raw SparseBernoulli.Program.view).2) :=
    (snd SparseBernoulli.Program.Context.encode (ed br)).recode
      (Bundle.raw SparseBernoulli.Program.view) (fun _ => rfl) (fun _ => rfl)
  exact (bernInputProgram bal |>.comp (SparseBernoulli.Program.runStateProgram 4) |>.comp get).congr _ (fun _ => rfl)

noncomputable def partProgram (bal : Bool) : PolyProgram Input.encode (ed br) (Input.partData bal) := by
  let ctx : PolyProgram Input.encode Binary.Automatic.enc Input.raw := (identity Binary.Automatic.enc).recode Input.raw (fun _ => rfl) (fun _ => rfl)
  let post : PolyProgram (encodePair Binary.Automatic.enc (ed br)) (ed br)
      (fun x : ListOperation.Raw × Data Row => (x.2.1,x.2.2.map (fun row => ListOperation.select bal (x.1,row)))) := by
    apply Binary.Automatic.Poly.program
    apply Binary.Automatic.Poly.pair
    · fun_prop
    · apply Binary.Automatic.Poly.list_map <;> fun_prop
  exact (ctx.fanout (bernProgram bal) |>.comp post).congr _ (fun x => by
    simp only [Function.comp_def,Input.partData,Input.part,SparseIntegerLaw.map,Vector.toList_map,
      List.map_map]
    congr 1
    apply List.map_congr_left
    intro ω hω
    exact ListOperation.select_view x.Z x.C x.p x.q ω bal)

noncomputable def program : PolyProgram Input.encode (ed br) Input.result :=
  ((partProgram true).fanout (partProgram false) |>.comp mixData_poly.program).congr _ (fun x => by
    change mixData (((raw (x.part true)).1,(x.part true).states.toList.map SparseGraph.ListOperation.setView),
      ((raw (x.part false)).1,(x.part false).states.toList.map SparseGraph.ListOperation.setView))=_
    rw [mixData_raw]
    rfl)
end MetricKMedian.SparsePhysicalBatch.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_BatchProposalProgram
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.RationalBatchData.ProposalProgram
open Finset FixedBatch Binary Binary.PolyProgram
open SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Row Table setView)
variable {C : Type} (I : C → Type) [∀ c, LinearOrder (I c)] [∀ c, Fintype (I c)]

variable {I}

 theorem data_input (x : Input I) : GraphData.data x.raw=x.batch.raw := by
  unfold GraphData.data Input.raw
  rw [Ordinal.prepare_graph,Ordinal.data_view]
  rfl
noncomputable def inputProgram : PolyProgram (Input.encode (I:=I)) SparsePhysicalBatch.Program.Input.encode Input.batch :=
  GraphData.data_poly.program.recode Input.raw (fun _ => rfl) (fun x => congrArg Binary.Automatic.enc (data_input x))

noncomputable def program : PolyProgram (Input.encode (I:=I)) (ed SparseGraph.ListOperation.er) Input.result :=
  (inputProgram.comp SparsePhysicalBatch.Program.program).congr _ (fun x => result_eq x)
end MetricKMedian.RationalBatchData.ProposalProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_ActionTransitionList
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.RationalBatchData.ActionTransition
open Binary Binary.Automatic Binary.Automatic.Poly Finset FixedBatch
open SparseGraph.ListOperation (Row Table setView indices)

variable {I : Type} [LinearOrder I] [Fintype I] {n : ℕ}
variable (r : Fin n ≃o I) (D : Actions I I) (H : Finset I) (Z : Finset (HeavyAction D H))
def view : Raw := (Ordinal.view r D H,setView (Z.map (enumeration D H).symm.toEmbedding))
 theorem selected_mem (c : ℕ) : c∈selected (view r D H Z) ↔ ∃ e∈Z, Ordinal.code r D H e=c := by
  simp only [selected,view,Ordinal.codes_eq,setView,mem_map_equiv,Equiv.symm_symm,
    Gaussian.ListOperation.zip_ofFn,List.mem_map,List.mem_filter,List.mem_ofFn]
  constructor
  · rintro ⟨z,⟨⟨i,rfl⟩,he⟩,hc⟩
    exact ⟨enumeration D H i,of_decide_eq_true he,hc⟩
  · rintro ⟨e,he,rfl⟩
    refine ⟨_,⟨⟨(enumeration D H).symm e,rfl⟩,?_⟩,?_⟩ <;>
      simp only [Equiv.apply_symm_apply,decide_eq_true he]

 theorem selected_light (hD : ∀ i, D.source i=i) (i : Fin n) : i.val∈selected (view r D H Z) ↔
    r i∈(Z∩(heavy D H).ordinary).image (heavy D H).source := by
  rw [selected_mem]
  constructor
  · rintro ⟨e,he,hc⟩
    have hl := (Ordinal.code_light r D H e).mp (hc ▸ i.isLt)
    cases e with
    | inl h =>
      refine mem_image.mpr ⟨.inl h,mem_inter.mpr ⟨he,?_⟩,?_⟩
      · simp only [heavy,mem_filter,mem_univ,Sum.isLeft_inl,and_self]
      · change D.source h.val=r i
        rw [hD]
        have hh : r.symm h.val=i := Fin.ext hc
        exact (r.symm.injective (hh.trans (r.symm_apply_apply i).symm))
    | inr h => cases hl
  · rintro hi
    obtain ⟨e,he,hE⟩ := mem_image.mp hi
    rcases mem_inter.mp he with ⟨he,hord⟩
    cases e with
    | inl h =>
      refine ⟨.inl h,he,?_⟩
      change D.source h.val=r i at hE
      rw [hD] at hE
      simp only [Ordinal.code,hE,OrderIso.symm_apply_apply]
    | inr h => simp only [heavy,mem_filter,mem_univ,Sum.isLeft_inr,Bool.false_eq_true,and_false] at hord

 theorem dead_view : dead (view r D H Z)=Ordinal.sets r (Z.biUnion (heavy D H).erase) := by
  unfold dead
  rw [show (view r D H Z).1.2=Ordinal.sets r H from rfl]
  simp only [indices,RoundingList.range_finRange,
    Function.comp_def,← List.ofFn_eq_map,List.map_ofFn,Ordinal.sets_eq,List.length_ofFn]
  apply congrArg List.ofFn
  funext i
  apply Bool.eq_iff_iff.mpr
  simp only [List.any_map,Function.comp_def,id_eq,List.any_eq_true,decide_eq_true_eq,mem_biUnion]
  constructor
  · rintro ⟨c,hc,hv⟩
    obtain ⟨e,he,rfl⟩ := (selected_mem r D H Z c).mp hc
    dsimp only [view] at hv
    rw [Ordinal.erase_code,Ordinal.sets_eq] at hv
    simp only [List.getElem?_ofFn,dite_eq_left i.isLt,Option.getD_some,Fin.eta,decide_eq_true_eq] at hv
    exact ⟨e,he,hv⟩
  · rintro ⟨e,he,hi⟩
    refine ⟨Ordinal.code r D H e,(selected_mem r D H Z _).mpr ⟨e,he,rfl⟩,?_⟩
    dsimp only [view]
    rw [Ordinal.erase_code,Ordinal.sets_eq]
    simp only [List.getElem?_ofFn,dite_eq_left i.isLt,Option.getD_some,Fin.eta,decide_eq_true hi]

 theorem sources_view (hD : ∀ i, D.source i=i) : sources (view r D H Z)=Ordinal.sets r
    (H∪(Z∩(heavy D H).ordinary).image (heavy D H).source) := by
  unfold sources
  rw [show (view r D H Z).1.2=Ordinal.sets r H from rfl]
  simp only [indices,RoundingList.range_finRange,
    Function.comp_def,← List.ofFn_eq_map,List.map_ofFn,Ordinal.sets_eq,List.length_ofFn]
  apply congrArg List.ofFn
  funext i
  apply Bool.eq_iff_iff.mpr
  simp only [List.getElem?_ofFn,dite_eq_left i.isLt,Option.getD_some,Fin.eta,Bool.or_eq_true,
    decide_eq_true_eq,natMember_true,mem_union]
  exact or_congr Iff.rfl (selected_light r D H Z hD i)

end MetricKMedian.RationalBatchData.ActionTransition
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_CopyNextProgram
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.CopyNext
open Binary Binary.Automatic Binary.Automatic.Poly Finset FixedBatch
open CopyList
open CopyGraphProgram (rank_owner)
open SparseGraph.ListOperation (Row Table setView indices)
open RationalBatchData.Ordinal (sets)

 attribute [local instance] OAI.MetricKMedian.RationalPhysicalKernel.CopyNext.instLinearOrderSubtypeCopyFinMemFinset
theorem transition_view {f Δ : ℕ} (A : Finset (CopyState.Copy (F:=Fin f) Δ)) (G : A → Finset A)
    (H : Finset A) (Z : Finset (HeavyAction (RationalBatchData.graph G) H)) :
    transition ((Δ,view A),RationalBatchData.ActionTransition.view (ordinal A) (RationalBatchData.graph G) H Z)=
      view (RationalBatchData.transition A G H Z) := by
  unfold transition
  dsimp only
  have hd := RationalBatchData.ActionTransition.dead_view (ordinal A) (RationalBatchData.graph G) H Z
  have hs := RationalBatchData.ActionTransition.sources_view (ordinal A) (RationalBatchData.graph G) H Z (fun _ => rfl)
  rw [hd,hs]
  exact next_view A _ _

end MetricKMedian.RationalPhysicalKernel.CopyNext
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 Input.encode (x : Input) := enc x.raw

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

 attribute [local instance] OAI.MetricKMedian.RationalPhysicalKernel.UpdateProgram.instLinearOrderSubtypeCopyFinMemFinset
theorem result_map (x : Input) : x.result=(x.proposal.result.1,
    x.proposal.law.states.toList.map (fun Z => CopyList.view (x.update Z))) := by
  unfold Input.result Input.law
  change (x.proposal.result.1,(Vector.map x.update x.proposal.law.states).toList.map CopyList.view)=_
  erw [Vector.toList_map,List.map_map]
  rfl

 theorem finish_input (x : Input) : finish (x.raw,x.proposal.result)=x.result := by
  rw [result_map]
  apply Prod.ext
  · rfl
  · change (x.proposal.law.states.toList.map (fun Z => setView (Z.map x.proposal.enumActions.symm.toEmbedding))).map
      (fun Z => CopyNext.transition (x.raw.1,((RationalBatchData.GraphData.prepare x.raw.2).2,Z))) = _
    rw [List.map_map]
    apply List.map_congr_left
    intro Z _
    change CopyNext.transition ((x.ctx.Δ,view x.ctx.A),
      ((RationalBatchData.GraphData.prepare (((x.ctx.g,x.ctx.β),(x.ctx.Δ,(x.ctx.p,x.ctx.φ))),
        RationalBatchData.Ordinal.graphView (ordinal x.ctx.A) x.G)).2,
        setView (Z.map x.proposal.enumActions.symm.toEmbedding)))=_
    rw [RationalBatchData.Ordinal.prepare_graph]
    exact CopyNext.transition_view x.ctx.A x.G _ Z

noncomputable def proposalProgram : PolyProgram Input.encode
    RationalBatchData.ProposalProgram.Input.encode Input.proposal :=
  (snd enc enc).recode Input.raw (fun _ => rfl) (fun _ => rfl)

noncomputable def program : PolyProgram Input.encode (ed SparseGraph.ListOperation.er) Input.result := by
  let ctx : PolyProgram Input.encode enc Input.raw := (identity enc).recode Input.raw (fun _ => rfl) (fun _ => rfl)
  exact (ctx.fanout (proposalProgram.comp RationalBatchData.ProposalProgram.program) |>.comp finish_poly.program).congr _ finish_input
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

noncomputable def graphProgram : PolyProgram ctxEncode (ed SparseGraph.ListOperation.et)
    (fun x => x.toInput.result) :=
  (show PolyProgram ctxEncode CopyGraphProgram.Input.encode (fun x : Context => x.toInput) from
    (fst enc enc).recode ctxRaw (fun _ => rfl) (fun _ => rfl)).comp CopyGraphProgram.program

noncomputable def inputsProgram : PolyProgram ctxEncode
    (encodePair enc (encodeList UpdateProgram.Input.encode)) (fun x => (x.toInput.result.1,(ctxInputs x))) := by
  let ctx : PolyProgram ctxEncode enc ctxRaw := (identity enc).recode ctxRaw (fun _ => rfl) (fun _ => rfl)
  exact (ctx.fanout graphProgram |>.comp attach_poly.program).recode id (fun _ => rfl) (fun x => by
    dsimp only [Function.comp_def,id_eq]
    rw [attach_input]
    change encodePair enc (encodeList enc) _=encodePair enc (encodeList UpdateProgram.Input.encode) _
    apply congrArg (fun w => quote (enc x.toInput.result.1)++w)
    induction ctxInputs x with
    | nil => rfl
    | cons a as ih => simpa only [List.map_cons,encodeList,UpdateProgram.Input.encode] using congrArg (fun w => quote (enc a.raw)++w) ih)

end MetricKMedian.RationalPhysicalKernel.RoundProgram
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 τ)
 theorem metadata_input (x : Input q) : metadata q x.raw=(q.g*x.A.card+q.allowance,List.ofFn (fun c => List.ofFn (x.d c))) := by
  unfold metadata Input.raw Completion.Rational.Program.Input.raw
  dsimp only
  rw [CopyList.view,Completion.Rational.BestProgram.card_view,card_map]

end MetricKMedian.FixedBatch.RationalParameters.SelectionProgram
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 τ)

def metadata (x : Raw) : ℚ × List (List ℚ) := (x.2.2.2,x.2.1.2)
@[fun_prop] theorem metadata_poly : Poly metadata := by unfold metadata; fun_prop

end MetricKMedian.FixedBatch.RationalParameters.PreparedScanProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_FractionalScanProgram
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.FractionalRefinement.ScanProgram
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
open MetricKMedian.MaskProgram
abbrev Raw := Program.Raw × ℚ
end MetricKMedian.Preparation.FractionalRefinement.ScanProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_InstanceDataProgram
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.InstanceProgram
open Finset Preparation Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
open MaskProgram
open RationalUnitInput.Program (ranks pickRows)
abbrev nzEncode (I : Nonzero) := encode I.val
end MetricKMedian.InstanceProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_InstanceZeroProgram
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.InstanceProgram
open Finset Preparation Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
open MaskProgram
open Completion.Rational.BestProgram (card card_view)

def zeroTestData (x : Raw) : Bool := subsetRaw x.1 && decide (card x.1.1≤x.2.1)
end MetricKMedian.InstanceProgram
end

end OAI
end