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

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

section
-- module Solutions.OAIQ037_KM.KMedian_Compression_CompressionListStep
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.IntegerLaw.BinaryCompression
open Binary Binary.PolyProgram Function Finset

noncomputable def largeProgram : PolyProgram Input.encode encodeBool (fun I => decide I.large) := by
  let nums := lawProgram.comp (snd Signed.encode er)
  let nonz := (((identity Signed.encode).fanout (constant Signed.encode Signed.encode 0)).comp intEQ).comp boolNot
  let size := (nums.comp (nonz.listFilter 0)).comp (listLength Signed.encode 0)
  let dim := ((dimProgram.comp (listLength Gaussian.ListOperation.eu ())).fanout (constant Input.encode Nat.bits 1)).comp natAdd
  exact ((dim.fanout size).comp natLT).congr _ (fun I => by
    simp only [Function.comp_apply,Input.large,Input.lawData,List.length_replicate]
    congr 1
    congr 1
    change ((List.ofFn I.μ.numerator).filter (fun z => !decide (z=0))).length=I.μ.support.card
    have he : (List.ofFn I.μ.numerator).filter (fun z => !decide (z=0))=
        List.ofFn (fun j : Fin I.μ.support.card => I.μ.numerator ((I.μ.support.orderIsoOfFin rfl) j).val) := by
      simp only [← decide_not]
      rw [List.ofFn_eq_map,List.filter_map]
      exact EncodingLists.map_filter_enum _ (fun i => I.μ.numerator i≠0)
    rw [he,List.length_ofFn])

noncomputable def productiveProgram : PolyProgram (fun I : {I : Input // I.large} => I.val.encode) el
    (fun I => (I.val.step).lawData) := by
  let a := dimProgram.fanout ((lawProgram.comp (snd Signed.encode er)).fanout featuresProgram)
  let A : PolyProgram (fun I : {I : Input // I.large} => I.val.encode) ListOperation.Input.encode
      (fun I => I.val.affine I.property) :=
    a.recode (fun I : {I : Input // I.large} => I.val) (fun _ => rfl) (fun _ => rfl)
  let K := A.comp ListOperation.affineKernelProgram
  let M := lawProgram.recode (fun I : {I : Input // I.large} => I.val) (fun _ => rfl) (fun _ => rfl)
  exact ((M.fanout K).comp ListPivot.updateProgram).congr _ (fun I => by
    unfold Input.step Input.lawData Input.nextLaw
    rw [dite_eq_left I.property]
    obtain ⟨L,hL⟩ := exists_feature_bound I.val.v
    have hz := computedAffineKernel_spec I.val.μ I.val.v L hL I.property
    exact ListPivot.update_ofFn I.val.μ _ (positiveSet_nonempty _ hz.2.1 hz.1) hz.2.1)

noncomputable def nextLawProgram : PolyProgram Input.encode el (fun I => (I.step).lawData) := by
  let safe := checkedProgram Input.large largeProgram ⟨dummy,dummy_large⟩
  let work := safe.comp productiveProgram
  exact (ite largeProgram lawProgram work).congr _ (fun I => by
    by_cases h : I.large
    · simp only [Function.comp_apply, h,decide_true,ite_true,checked,dite_eq_left]
    · simp only [Function.comp_apply, h,decide_false,Bool.false_eq_true,ite_false]
      simp [Input.step,Input.lawData,Input.nextLaw,h])

noncomputable def stepProgram : PolyProgram Input.encode Input.encode Input.step :=
  ((dimProgram.fanout (nextLawProgram.fanout featuresProgram))).recode id (fun _ => rfl) (fun _ => rfl)

end MetricKMedian.IntegerLaw.BinaryCompression
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Compression_CompressionBounds
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.IntegerLaw.BinaryCompression
open Binary Binary.PolyProgram Function Finset Polynomial

theorem lawStep_denominator {n d : ℕ} (μ : IntegerLaw (Fin n)) (v : Fin n → Fin d → ℤ)
    (L : ℕ) (hv : ∀ i j, |v i j|≤(2:ℤ)^L) :
    (lawStep v μ).denominator ≤ μ.denominator*(2:ℤ)^((2*(d+1)*(d+1+L))*(n+1)) := by
  unfold lawStep
  split_ifs with h
  · rw [compressionStepAuto_eq μ v L hv h]
    exact (compressionStep_spec μ v L hv h).1
  · exact le_mul_of_one_le_right μ.denominator_pos.le (one_le_pow₀ (by norm_num))

theorem iterate_denominator {n d : ℕ} (μ : IntegerLaw (Fin n)) (v : Fin n → Fin d → ℤ)
    (L : ℕ) (hv : ∀ i j, |v i j|≤(2:ℤ)^L) (hμ : μ.denominator≤(2:ℤ)^L) (t : ℕ) :
    ((lawStep v)^[t] μ).denominator ≤ (2:ℤ)^(L+((2*(d+1)*(d+1+L))*(n+1))*t) := by
  induction t with
  | zero => simpa using hμ
  | succ t ih =>
      rw [Function.iterate_succ_apply']
      apply (lawStep_denominator _ v L hv).trans
      apply (mul_le_mul_of_nonneg_right ih (by positivity)).trans
      rw [← pow_add]
      have he : L+((2*(d+1)*(d+1+L))*(n+1))*t+((2*(d+1)*(d+1+L))*(n+1))=
          L+((2*(d+1)*(d+1+L))*(n+1))*(t+1) := by ring
      rw [he]

theorem state_size (I : Input) (t : ℕ) (ht : t≤I.n) :
    (Input.encode (Input.step^[t] I)).length≤ statePolynomial.eval I.encode.length := by
  let L := I.encode.length
  let ν := (lawStep I.v)^[t] I.μ
  obtain ⟨hn,hd,hμ,hv⟩ := input_bounds I
  have hν : ν.denominator≤(2:ℤ)^(height L) := by
    apply (iterate_denominator I.μ I.v L hv hμ t).trans
    apply pow_le_pow_right₀ (by norm_num)
    dsimp only [height]
    gcongr
    exact ht.trans hn
  have hden : (Signed.encode ν.denominator).length≤height L+4 :=
    Signed.length_height (by rwa [abs_of_pos ν.denominator_pos])
  have hnum : (er (List.ofFn ν.numerator)).length ≤ L*(2*(height L+4)+1) := by
    apply (EncodedList.length_bound Signed.encode (List.ofFn ν.numerator) (height L+4) ?_).trans
    · simpa only [List.length_ofFn] using Nat.mul_le_mul_right (2*(height L+4)+1) hn
    · intro z hz
      obtain ⟨i,rfl⟩ := List.mem_ofFn.mp hz
      apply Signed.length_height
      rw [abs_of_nonneg (ν.numerator_nonneg i)]
      exact (ν.numerator_le i).trans hν
  have hfeat : (em I.features).length≤L := by
    simp only [L,Input.raw,encodePair_length]
    omega
  rw [input_iterate,Input.encode_length,statePolynomial_eval]
  exact size_arithmetic L I.d (Signed.encode ν.denominator).length
    (er (List.ofFn ν.numerator)).length (em I.features).length (height L) hd hden hnum hfeat

end MetricKMedian.IntegerLaw.BinaryCompression
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Compression_CompressionBinaryProgram
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.IntegerLaw.BinaryCompression
open Binary Binary.PolyProgram Function Polynomial

noncomputable def iterateProgram : PolyProgram Input.encode Input.encode
    (fun I => Input.step^[I.n] I) :=
  stepProgram.repeatFrom (identity Input.encode) countProgram X statePolynomial
    (fun I => by simpa using (input_bounds I).1) (fun I i hi => state_size I i hi)

noncomputable def compressProgram : PolyProgram Input.encode el Input.compressed :=
  (iterateProgram.comp lawProgram).congr _ (fun I => by
    simp only [Function.comp_apply,input_iterate,Input.lawData,Input.compressed,compressSteps_eq_iterate])

noncomputable def rationalCompressProgram : PolyProgram RationalInput.encode el RationalInput.compressed :=
  (integerInputProgram.comp compressProgram).congr _ (fun _ => rfl)

end MetricKMedian.IntegerLaw.BinaryCompression
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_RoundingUniformStep
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI


                                           
section
namespace MetricKMedian.RoundingList
open Binary Binary.Automatic Binary.Automatic.Poly

theorem dimensions_list {n : ℕ} (β : Fin n → ℚ) :
    dimensions (List.ofFn β)=List.replicate (n+n*n) () := by
  simp only [dimensions,indices,square,List.length_ofFn]
  simp

theorem features_list {n : ℕ} (p : Vector ℚ n) :
    features p.toList=List.ofFn (SparseWeightedPartial.features p) := by
  have hp : p.toList=List.ofFn (RationalWeightedStep.point p) := by
    apply List.ext_getElem <;> intros <;> simp [RationalWeightedStep.point]
  simp only [features,hp,List.flatMap_def,List.map_ofFn,Function.comp_def,ofFn_product]
  rw [List.ofFn_add]
  congr 1
  · congr 1; funext i
    have hi : (Fin.castAdd (n*n) i : Fin (n+n*n))=finSumFinEquiv (Sum.inl i) := by rfl
    change _=SparseWeightedPartial.features p (Fin.castAdd (n*n) i)
    rw [hi,SparseWeightedPartial.features_single]
  · congr 1; funext i
    have hi : (Fin.natAdd n i : Fin (n+n*n))=finSumFinEquiv (Sum.inr i) := by
      apply Fin.ext; simp [finSumFinEquiv]
    rw [hi]
    simp only [SparseWeightedPartial.features,Equiv.symm_apply_apply,Sum.elim_inr]

end MetricKMedian.RoundingList

namespace MetricKMedian.RoundingProgram
open Binary Binary.PolyProgram Function
open SparseIntegerLaw.BinarySparse

def probability (s : Bool) : Row × Row → ℚ :=
  if s then fun x => RoundingList.Signed.probability x.1 x.2 else fun x => RoundingList.probability x.1 x.2
def endpoint (s b : Bool) : Row × Row → Row :=
  if s then fun x => RoundingList.Signed.endpoint x.1 x.2 b else fun x => RoundingList.endpoint x.1 x.2 b

noncomputable def probabilityProgram (s : Bool) : PolyProgram (encodePair erow erow) Ratio.encode (probability s) := by
  cases s
  · exact RoundingList.probability_poly.program
  · exact RoundingList.Signed.probability_poly.program
noncomputable def endpointProgram (s b : Bool) : PolyProgram (encodePair erow erow) erow (endpoint s b) := by
  cases s
  · exact (RoundingList.endpoint_poly b).program
  · exact (RoundingList.Signed.endpoint_poly b).program

noncomputable def branchRawProgram (s : Bool) :
    PolyProgram (encodePair erow (ed erow)) (encodePair erow (ed erow)) (fun x =>
      (x.1,(branchLawData (x.2.1,x.2.2.map (fun p => probability s (x.1,p))),
        x.2.2.flatMap (fun p => [endpoint s false (x.1,p),endpoint s true (x.1,p)])))) := 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 probs := (β.fanout states).comp ((probabilityProgram s).listMapWith [] 0)
  let laws := (law.fanout probs).comp branchLawProgram
  let endpoints := ((endpointProgram s false).fanout (endpointProgram s true)).comp pairList
  let ps := (β.fanout states).comp (endpoints.listFlatMapWith [] [])
  exact (β.fanout (laws.fanout ps)).congr _ (fun _ => rfl)

end MetricKMedian.RoundingProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseProduct
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.SparseIntegerLaw
open Finset
variable {α β γ : Type}

theorem prodCompress_spec {d : ℕ} (μ : SparseIntegerLaw α) (ν : SparseIntegerLaw β)
    (f : α → β → γ) (v : γ → Fin d → ℚ) :
    let ρ := μ.prodCompress ν f v
    ρ.length ≤ d+1 ∧
    (∀ a : Fin ρ.length, ∃ b : Fin μ.length, ∃ c : Fin ν.length,
      ρ.states[a.val]=f μ.states[b.val] ν.states[c.val]) ∧
    ∀ j, ρ.moment (fun t => v t j)=μ.moment (fun a => ν.moment (fun b => v (f a b) j)) := by
  have h := (μ.prod ν f).compressAuto_correct v
  refine ⟨h.1,?_,fun j => (h.2.2 j).trans (prod_moment μ ν f _)⟩
  intro a
  obtain ⟨b,hb⟩ := h.2.1 a
  refine ⟨((finProdFinEquiv (m := μ.length) (n := ν.length)).symm b).1,((finProdFinEquiv (m := μ.length) (n := ν.length)).symm b).2,?_⟩
  exact hb.trans (by
    simp only [prod,Vector.getElem_ofFn]
    congr 3)

end MetricKMedian.SparseIntegerLaw
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Geometry_GraphListOperations
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.ListOperation
open Binary Binary.Automatic Binary.Automatic.Poly

 theorem edges_view {n m : ℕ} (G : Graph 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,
    decide_eq_true_eq]
  rw [RoundingList.ofFn_product]
  rfl

 theorem featureList_view {n m : ℕ} (G : Graph 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]

 theorem dimensions_eq {n m : ℕ} (cs : Fin m → SparseIntegerLaw.BinarySparse.Data Row) :
    dimensions (List.replicate n (),List.ofFn cs)=List.replicate (n*m+(n*m)*(n*m)) () := by
  have h : (List.replicate n ()).flatMap (fun _ => (List.ofFn cs).map (fun _ => (0:ℚ)))=
      List.ofFn (fun _ : Fin (n*m) => (0:ℚ)) := by
    simp only [List.map_const',List.length_ofFn,List.flatMap_replicate,List.ofFn_const]
    simp [List.flatten_replicate_replicate]
  simp only [dimensions,h,RoundingList.dimensions_list]
end MetricKMedian.SparseGraph.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

def vectorData {n : ℕ} (μ : SparseIntegerLaw (Vector ℚ n)) : Data Row :=
  ((μ.law.denominator,List.ofFn μ.law.numerator),μ.states.toList.map Vector.toList)

theorem vectorData_branch {n : ℕ} (μ : SparseIntegerLaw (Vector ℚ n))
    (p : Vector ℚ n → ℚ) (hp : ∀ q, 0≤p q ∧ p q≤1) (next : Vector ℚ n → Fin 2 → Vector ℚ n)
    (P : Row → ℚ) (E0 E1 : Row → Row)
    (hP : ∀ q, P q.toList=p q) (hE0 : ∀ q, E0 q.toList=(next q 0).toList)
    (hE1 : ∀ q, E1 q.toList=(next q 1).toList) :
    (branchLawData ((vectorData μ).1,(vectorData μ).2.map P),
      (vectorData μ).2.flatMap (fun q => [E0 q,E1 q]))=vectorData (μ.branch p hp next) := by
  simp only [vectorData,states_list,List.map_ofFn,Function.comp_def,hP]
  rw [branchLaw_ofFn μ.law _ (fun i => hp μ.states[i.val])]
  congr 1
  simp only [SparseIntegerLaw.branch,Vector.getElem_ofFn,List.flatMap_def,List.map_ofFn,Function.comp_def,hE0,hE1]
  exact (two_expand (fun i b => (next μ.states[i.val] b).toList)).symm

end MetricKMedian.RoundingProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_DependentSparseProgram
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.SparseIntegerLaw.DependentProgram
open Binary Binary.PolyProgram Function BinarySparse
variable {C A : Type} (T : C → Type)

variable {T} (ec : C → List Bool) (ea : A → List Bool) (view : ∀ c, T c → A)

noncomputable def compressProgram (a0 : A) (d : C → ℕ) (v : ∀ c, T c → Fin (d c) → ℚ)
    (F : C × A → List ℚ) (hF : ∀ c a, F (c,view c a)=List.ofFn (v c a))
    (D : PolyProgram ec IntegerLaw.BinaryCompression.es (fun c => List.replicate (d c) ()))
    (V : PolyProgram (encodePair ec ea) IntegerLaw.BinaryCompression.eqr F) :
    PolyProgram (Bundle.encode ec ea view) (Bundle.encode ec ea view) (Bundle.compress d v) := by
  let law := (compressionInputProgram ec ea view a0 d v F hF D V).comp IntegerLaw.BinaryCompression.rationalCompressProgram
  let trimmed := (law.fanout (statesProgram ec ea view)).comp (trimDataProgram ea a0)
  let work := (contextProgram ec ea view).fanout trimmed
  exact work.recode id (fun _ => rfl) (fun x => by
    change encodePair ec (ed ea) (x.ctx,
      trimData (((x.law.law.compressAuto (fun i => v x.ctx x.law.states[i.val])).denominator,
       List.ofFn (x.law.law.compressAuto (fun i => v x.ctx x.law.states[i.val])).numerator),
         x.law.states.toList.map (view x.ctx)))=_
    rw [show trimData _= _ from trim_view view x.ctx
      (⟨x.law.length,x.law.states,x.law.law.compressAuto (fun i => v x.ctx x.law.states[i.val])⟩ : SparseIntegerLaw (T x.ctx))]
    rfl)

end MetricKMedian.SparseIntegerLaw.DependentProgram
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

def rowProbability (x : Context × Row) : ℚ := x.1.raw.1[x.1.t]?.getD 0
def rowEndpoint (b : Bool) (x : Context × Row) : Row := ListOperation.endpoint x.1.t b x.2
noncomputable def endpointProgram (b : Bool) : PolyProgram (encodePair Context.encode er) er (rowEndpoint b) :=
  (((fst Context.encode er).comp ((snd qr Nat.bits).recode Context.raw (fun _ => rfl) (fun _ => rfl))).fanout
     (snd Context.encode er)).comp (ListOperation.endpoint_poly b).program

end MetricKMedian.SparseBernoulli.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_PhysicalBatchList
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.ListOperation
open Binary Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table er et indices)

 theorem conflictFree_view {n : ℕ} (C : Fin n → Finset (Fin n)) (ω : Fin n → Bool) (e : Fin n) :
    conflictFree (List.ofFn (fun a => SparseGraph.ListOperation.setView (C a)),List.ofFn ω) e.val=true ↔
      ∀ f∈C e, ω f=false := by
  simp only [conflictFree,indices,List.length_ofFn,RoundingList.range_finRange,List.map_map,
    Function.comp_def,List.all_map,List.all_eq_true,List.mem_finRange,forall_const,
    SparseGraph.ListOperation.setView,List.getElem?_ofFn,dite_eq_left (Fin.isLt _),Option.getD_some,
    Fin.eta,id_eq,Bool.or_eq_true,Bool.not_eq_true_eq_eq_false,decide_eq_false_iff_not]
  constructor
  · intro h f hf
    exact (h f).resolve_left (not_not.mpr hf)
  · intro h f
    by_cases hf : f∈C e
    · exact Or.inr (h f hf)
    · exact Or.inl hf

 theorem select_view {n : ℕ} (Z : Finset (Fin n)) (C : Fin n → Finset (Fin n))
    (p : ℚ) (q : Fin n → ℚ) (ω : Fin n → Bool) (bal : Bool) :
    select bal (((SparseGraph.ListOperation.setView Z,List.ofFn (fun a => SparseGraph.ListOperation.setView (C a))),
      (p,List.ofFn q)),List.ofFn ω)=SparseGraph.ListOperation.setView
      (if bal then balanced Z C ω else unbalanced Z ω) := by
  apply List.ext_getElem
  · simp only [select,indices,List.length_ofFn,List.length_map,List.length_range,
      SparseGraph.ListOperation.setView]
  · intro i hi hi'
    have hin : i<n := by simpa only [SparseGraph.ListOperation.setView,List.length_ofFn] using hi'
    simp only [select,indices,List.length_ofFn,List.getElem_map,List.getElem_range,
      List.getElem_ofFn,SparseGraph.ListOperation.setView,List.getElem?_ofFn,dite_eq_left hin,Option.getD_some]
    apply Bool.eq_iff_iff.mpr
    cases bal
    · simp only [Bool.false_eq_true,ite_false,unbalanced,Finset.mem_filter,Finset.mem_univ,true_and,
        Bool.and_eq_true,Bool.not_eq_true_eq_eq_false,decide_eq_false_iff_not,decide_eq_true_eq]
    · simp only [ite_true,balanced,Finset.mem_inter,Finset.mem_filter,Finset.mem_univ,true_and,
        Bool.and_eq_true,decide_eq_true_eq]
      rw [show conflictFree (List.ofFn (fun a => List.ofFn (fun h => decide (h∈C a))),List.ofFn ω) i=true ↔
        ∀ f∈C ⟨i,hin⟩, ω f=false from conflictFree_view C ω ⟨i,hin⟩]
end MetricKMedian.SparsePhysicalBatch.ListOperation
end

end OAI
end

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

 theorem overlap_view {n : ℕ} (A B : Finset (Fin n)) :
    overlap (setView A) (setView B)=true ↔ (A∩B).Nonempty := by
  simp only [overlap,indices,setView,List.length_ofFn,RoundingList.range_finRange,List.map_map,
    Function.comp_def,List.any_map,List.any_eq_true,List.mem_finRange,true_and,
    List.getElem?_ofFn,dite_eq_left (Fin.isLt _),Option.getD_some,Fin.eta,id_eq,Bool.and_eq_true,
    decide_eq_true_eq,Finset.Nonempty,mem_inter]

end MetricKMedian.RationalBatchData.ActionArrays

end

end OAI
end

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

 theorem amount_view {n : ℕ} (m : Fin n → ℚ) : amount (List.ofFn m)=RationalBatchData.amount m := by
  simp only [amount,List.map_ofFn,List.sum_ofFn,Function.comp_def,RationalBatchData.amount]
end MetricKMedian.RationalBatchData.GraphData
end

end OAI
end

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 parent_code (e : HeavyAction D H) :
    ActionList.parent n (code r D H e)=(r.symm (heavyParent D H e)).val := by
  cases e with
  | inl e => simp only [ActionList.parent,code,Fin.isLt,ite_true,heavyParent]
  | inr e =>
    have hn : 0<n := Nat.zero_lt_of_lt (r.symm e.val.1).isLt
    have hi := (r.symm e.val.2).isLt
    have hc : ¬n+(r.symm e.val.1).val*n+(r.symm e.val.2).val<n := by omega
    change ActionList.parent n (n+(r.symm e.val.1).val*n+(r.symm e.val.2).val)=(r.symm e.val.1).val
    rw [ActionList.parent,ite_eq_right hc,Nat.add_assoc,Nat.add_sub_cancel_left,Nat.mul_comm _ n,
      Nat.mul_add_div hn,Nat.div_eq_of_lt hi,Nat.add_zero]
 theorem child_code (e : {p : I × I // p.1∈H ∧ p.2∈D.erase p.1}) :
    ActionList.child n (code r D H (.inr e))=(r.symm e.val.2).val := by
  simp only [ActionList.child,code]
  rw [Nat.add_assoc,Nat.add_sub_cancel_left,Nat.add_mod,Nat.mul_mod_left,Nat.zero_add,Nat.mod_mod,Nat.mod_eq_of_lt (r.symm e.val.2).isLt]
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)

 omit [Fintype I] in
 theorem bias_code (m : I → ℚ) (p φ : ℚ) (e : HeavyAction D H) :
    ActionArrays.bias (((p,φ),List.ofFn (fun i => m (r i))),n) (code r D H e)=
      RationalBatchData.bias m p φ (heavyParent D H e) := by
  simp only [ActionArrays.bias,parent_code,List.getElem?_ofFn,dite_eq_left (Fin.isLt _),Option.getD_some,
    Fin.eta,OrderIso.apply_symm_apply,RationalBatchData.bias]

end MetricKMedian.RationalBatchData.Ordinal
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseMixProgram
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.SparseIntegerLaw.BinarySparse
open Binary Binary.Automatic Binary.Automatic.Poly
variable {α A : Type}

 theorem mixData_raw (μ ν : SparseIntegerLaw α) (view : α → A) :
    mixData (((raw μ).1,μ.states.toList.map view),((raw ν).1,ν.states.toList.map view))=
      ((raw (μ.mix ν)).1,(μ.mix ν).states.toList.map view) := by
  have h := bindData_raw (fair) (fun a => if a.val=0 then μ else ν) view
  simpa [mixData,mix,raw,fair,List.ofFn_succ] using h

end MetricKMedian.SparseIntegerLaw.BinarySparse
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)

def Input.raw (x : Input) : ListOperation.Raw :=
  ((SparseGraph.ListOperation.setView x.Z,List.ofFn fun e => SparseGraph.ListOperation.setView (x.C e)),
    (x.p,List.ofFn x.q))
abbrev Input.encode (x : Input) := Binary.Automatic.enc x.raw

def Input.partData (bal : Bool) (x : Input) : Data Row :=
  (((x.part bal).law.denominator,List.ofFn (x.part bal).law.numerator),
    (x.part bal).states.toList.map SparseGraph.ListOperation.setView)
def Input.result (x : Input) : Data Row :=
  (((law x.Z x.C x.p x.q x.hp x.hq).law.denominator,List.ofFn (law x.Z x.C x.p x.q x.hp x.hq).law.numerator),
    (law x.Z x.C x.p x.q x.hp x.hq).states.toList.map SparseGraph.ListOperation.setView)

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}

def Input.result (x : Input I) : Data Row :=
  (((x.law).law.denominator,List.ofFn (x.law).law.numerator),
    x.law.states.toList.map (fun Z => setView (Z.map x.enumActions.symm.toEmbedding)))

 theorem result_eq (x : Input I) : x.batch.result=x.result := by
  unfold Input.result Input.law proposal SparseEnumeratedBatch.law
  simp only [SparseIntegerLaw.map,Vector.toList_map,List.map_map,Function.comp_def]
  change x.batch.result=(((SparsePhysicalBatch.law x.batch.Z x.batch.C x.batch.p x.batch.q x.batch.hp x.batch.hq).law.denominator,
    List.ofFn (SparsePhysicalBatch.law x.batch.Z x.batch.C x.batch.p x.batch.q x.batch.hp x.batch.hq).law.numerator),_)
  unfold SparsePhysicalBatch.Program.Input.result
  congr 1
  apply List.map_congr_left
  intro Z hZ
  clear hZ
  dsimp only [Input.batch] at Z ⊢
  congr 1
  ext i
  simp only [mem_map_equiv,Equiv.symm_symm,Equiv.symm_apply_apply]

end MetricKMedian.RationalBatchData.ProposalProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_TaperListProgram
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 upper_list {n : ℕ} (d : Fin n → ℚ) : upper (List.ofFn d)=Taper.upper d := by
  simp only [upper,Taper.upper,List.map_ofFn,List.sum_ofFn,one_div,Function.comp_def]
end MetricKMedian.Taper.ListOperation
end

end OAI
end

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

theorem run_length (ν : Fin m → SparseIntegerLaw (Finset (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.SparseGraph
end
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
 theorem selectedRow_eq {n : ℕ} (q : Vector ℚ n) :
    selectedRow q.toList=SparseGraph.ListOperation.setView (selected q) := by
  apply List.ext_getElem
  · simp only [selectedRow,List.length_map,Vector.length_toList,SparseGraph.ListOperation.setView,List.length_ofFn]
  · intro i hi hi'
    have hin : i<n := by simpa only [SparseGraph.ListOperation.setView,List.length_ofFn] using hi'
    simp only [selectedRow,List.getElem_map,Vector.getElem_toList,SparseGraph.ListOperation.setView,
      List.getElem_ofFn,selected,Finset.mem_filter,Finset.mem_univ,true_and,RationalWeightedStep.point]

end MetricKMedian.SparseCardinalRounding.Program
end

end OAI
end