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

import Mathlib
import Definitions.Def_MetricKMedian
import Definitions.Def_OAIQ037K056
import Definitions.Def_OAIQ037K057
import Definitions.Def_OAIQ037K058
import Definitions.Def_OAIQ037K059

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseBernoulliSupport
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.SparseBernoulli
open Finset
variable {n d : ℕ}

theorem single_moment (p : Fin n → ℚ) (hp : ∀ i, 0 ≤ p i ∧ p i ≤ 1)
    (i : Fin n) : (run (d := 2) p hp n).moment (fun q => flag q i)=p i := by
  simpa only [prod_singleton] using subset_moment p hp {i} (by simp : ({i} : Finset (Fin n)).card ≤ 2)

end MetricKMedian.SparseBernoulli
end
end

end OAI
end

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

def kernel (u : Fin n → ℚ) (p : Vector ℚ n)
    (hp : ∀ i, 0 ≤ point p i ∧ point p i ≤ 1)
    (a : Fin (SparseSignedPartial.run u p n).length) : SparseIntegerLaw (Vector ℚ n) :=
  RationalSignedTerminal.terminal u (SparseSignedPartial.run u p n).states[a.val]
    (SparseSignedPartial.run_invariants u p hp n a).1

def round (u : Fin n → ℚ) (p : Vector ℚ n)
    (hp : ∀ i, 0 ≤ point p i ∧ point p i ≤ 1) : SparseIntegerLaw (Vector ℚ n) :=
  (SparseSignedPartial.run u p n).bindCompress (kernel u p hp) features

end MetricKMedian.SparseSignedRounding
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_SplitListProgram
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.RationalSplitting.Program
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
open MetricKMedian.MaskProgram
@[fun_prop] theorem cutsData_poly : Poly cutsData := by
  unfold cutsData
  apply comp RationalSortProgram.sort_poly
  apply list_filter
  · fun_prop
  · have h : Poly (fun x : Raw × ℕ => x.1.2.map (fun r => r[x.2]?.getD 0)) := by apply list_map <;> fun_prop
    have g : Poly (fun x : Raw × ℕ => x.1.1[x.2]?.getD (0:ℚ)) := by fun_prop
    exact Poly.comp list_cons (pair g h)

def piecesData (x : Raw) : List (ℕ × ℚ) :=
  (indices x.1).flatMap (fun i => (cutsData (x,i)).map (fun q => (i,q)))
@[fun_prop] theorem piecesData_poly : Poly piecesData := by
  unfold piecesData
  apply list_flatMap
  · apply list_map <;> fun_prop
  · fun_prop

def originalData (x : Raw) : List ℕ := (piecesData x).map Prod.fst
@[fun_prop] theorem originalData_poly : Poly originalData := by unfold originalData; apply list_map <;> fun_prop

def previousData (x : List ℚ × ℚ) : ℚ := maximum (0::x.1.filter (fun q => decide (q<x.2)))
@[fun_prop] theorem previousData_poly : Poly previousData := by
  unfold previousData
  have h : Poly (fun x : List ℚ × ℚ => x.1.filter (fun q => decide (q<x.2))) := by apply list_filter <;> fun_prop
  have h2 : Poly (fun x : List ℚ × ℚ => (0:ℚ)::x.1.filter (fun q => decide (q<x.2))) :=
    Poly.comp (f:=fun t : ℚ × List ℚ => t.1::t.2) (list_cons (α:=ℚ)) (pair (const (α:=List ℚ × ℚ) (0:ℚ)) h)
  exact Poly.comp maximum_poly h2

def weightsData (x : Raw) : List ℚ := (piecesData x).map (fun a => a.2-previousData (cutsData (x,a.1),a.2))
@[fun_prop] theorem weightsData_poly : Poly weightsData := by unfold weightsData; apply list_map <;> fun_prop

def assignedData (x : Raw) : Table := x.2.map (fun row => (piecesData x).map (fun a => decide (a.2 ≤ row[a.1]?.getD 0)))
@[fun_prop] theorem assignedData_poly : Poly assignedData := by
  unfold assignedData
  apply list_map
  · apply list_map <;> fun_prop
  · fun_prop
end MetricKMedian.Preparation.RationalSplitting.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_FractionalInputProgram
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.Program
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
open MetricKMedian.MaskProgram
@[fun_prop] theorem assignmentData_poly : Poly assignmentData := by
  have h : Poly (fun z : Raw => (z.1,z.2.1)) := by fun_prop
  exact ⟨(h.program.comp (LPBinary.Nearest.fillingProgram.listMapWith [] [])).congr _ (fun _ => rfl)⟩

def splitData (z : Raw) : RationalSplitting.Program.Raw := (z.1,assignmentData z)
@[fun_prop] theorem splitData_poly : Poly splitData := by unfold splitData; fun_prop

def unitData (z : Raw) : RationalUnitInput.Program.Raw :=
  ((RationalSplitting.Program.weightsData (splitData z),RationalSplitting.Program.assignedData (splitData z)),
    (z.2.1.map (fun d => pullback (d,RationalSplitting.Program.originalData (splitData z))),
      (z.2.2.1,pullbackMatrix (z.2.2.2,RationalSplitting.Program.originalData (splitData z)))))
@[fun_prop] theorem unitData_poly : Poly unitData := by
  unfold unitData
  have h : Poly (fun z : Raw => z.2.1.map (fun d => pullback (d,RationalSplitting.Program.originalData (splitData z)))) := by
    apply list_map <;> fun_prop
  fun_prop

end MetricKMedian.Preparation.FractionalRefinement.Program
end

end OAI
end

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

namespace OAI


                                           
section
namespace MetricKMedian.Preparation.RationalUnitInput.Program
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
open MetricKMedian.MaskProgram

@[fun_prop] theorem pickRows_poly {α : Type} [Coding α] [Inhabited α] : Poly (pickRows (α:=α)) := by
  unfold pickRows; apply list_map <;> fun_prop

def geometryData (x : Raw × Row) : RationalBundles.Program.Raw :=
  ((pullbackMatrix (x.1.2.2.1,ranks x.2),pickRows (x.1.2.1,ranks x.2)),
    (pickRows (x.1.1.2,ranks x.2),x.1.1.1))
@[fun_prop] theorem geometryData_poly : Poly geometryData := by unfold geometryData; fun_prop

def suppliersData (δ γ : ℚ) (x : RationalBundles.Program.Raw) : RationalSuppliers.Program.SupplierRaw :=
  (x.2.2,(RationalBundles.Program.bundlesData δ x,(RationalBundles.Program.missingData δ x,
    (RationalBundles.Program.massData (x.2.2,RationalBundles.Program.bundlesData δ x),
      (RationalBundles.Program.massData (x.2.2,RationalBundles.Program.missingData δ x),γ)))))
@[fun_prop] theorem suppliersData_poly (δ γ : ℚ) : Poly (suppliersData δ γ) := by unfold suppliersData; fun_prop
end MetricKMedian.Preparation.RationalUnitInput.Program
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 Raw := (Row × Row) × (ℕ × Matrix)
def view (I : Instance) : Raw :=
  ((setView I.clients,setView I.facilities),(I.k,List.ofFn (fun i => List.ofFn (I.distance i))))
abbrev encode (I : Instance) := enc (view I)
def dcData (x : Raw) : Matrix := (pickRows (x.2.2,ranks x.1.1)).map (fun d => pullback (d,ranks x.1.2))
@[fun_prop] theorem dcData_poly : Poly dcData := by unfold dcData; apply list_map <;> fun_prop
def ddData (x : Raw) : Matrix := pullbackMatrix (x.2.2,ranks x.1.1)
def dfData (x : Raw) : Matrix := pullbackMatrix (x.2.2,ranks x.1.2)
@[fun_prop] theorem ddData_poly : Poly ddData := by unfold ddData; fun_prop
@[fun_prop] theorem dfData_poly : Poly dfData := by unfold dfData; fun_prop
def lpData (x : Raw) : Matrix × ℕ := (dcData x,x.2.1)
@[fun_prop] theorem lpData_poly : Poly lpData := by unfold lpData; fun_prop
def fractionalData (x : Raw × LPBinary.Repair.Output) : FractionalRefinement.Program.Raw :=
  (x.2.1,(dcData x.1,(ddData x.1,dfData x.1)))
@[fun_prop] theorem fractionalData_poly : Poly fractionalData := by unfold fractionalData; fun_prop
end MetricKMedian.InstanceProgram
end

end OAI
end

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

namespace OAI


                                             
section
namespace MetricKMedian.InputParser
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
open InstanceProgram (Raw view)
@[fun_prop] theorem take_comp {α β : Type} [Coding α] [Coding β] [Inhabited β]
    {f : α → ℕ} {g : α → List β} (hf : Poly f) (hg : Poly g) : Poly (fun x => (g x).take (f x)) :=
  comp list_take (pair hg hf)
@[fun_prop] theorem drop_comp {α β : Type} [Coding α] [Coding β] [Inhabited β]
    {f : α → ℕ} {g : α → List β} (hf : Poly f) (hg : Poly g) : Poly (fun x => (g x).drop (f x)) :=
  comp list_drop (pair hg hf)
def squareUnits (xs : Row) : List Unit := xs.flatMap (fun _ => xs.map (fun _ => ()))
@[fun_prop] theorem squareUnits_poly : Poly squareUnits := by unfold squareUnits; apply list_flatMap; apply list_map <;> fun_prop; fun_prop
 theorem squareUnits_length (xs : Row) : (squareUnits xs).length=xs.length*xs.length := by
  simp only [squareUnits,List.length_flatMap,List.length_map]
  rw [List.map_const',List.sum_replicate]
  simp only [smul_eq_mul]
def reshape (x : Row × List ℚ) : InstanceProgram.Matrix :=
  (indices x.1).map (fun i => (indices x.1).map (fun j => x.2[i*x.1.length+j]?.getD 0))
@[fun_prop] theorem reshape_poly : Poly reshape := by unfold reshape; apply list_map; apply list_map <;> fun_prop; fun_prop
 theorem reshape_flatten {n : ℕ} (S : Finset (Fin n)) (d : Fin n → Fin n → ℚ) :
    reshape (setView S,(List.ofFn (fun i => List.ofFn (d i))).flatten)=List.ofFn (fun i => List.ofFn (d i)) := by
  rw [flatten_ofFn]
  simp only [reshape,indices,setView,List.length_ofFn,RoundingList.range_finRange,← List.ofFn_eq_map,List.map_ofFn,Function.comp_def]
  apply congrArg List.ofFn
  funext i
  apply congrArg List.ofFn
  funext j
  have hij : i.val*n+j.val<n*n := by
    calc
      i.val*n+j.val < i.val*n+n := Nat.add_lt_add_left j.isLt _
      _ = (i.val+1)*n := by simp only [Nat.add_mul,Nat.one_mul]
      _ ≤ n*n := Nat.mul_le_mul_right n i.isLt
  simp only [List.getElem?_ofFn,dite_eq_left hij,Option.getD_some]
  have he : (⟨i.val*n+j.val, hij⟩ : Fin (n*n)) = finProdFinEquiv (i,j) := by
    apply Fin.ext; change _=j.val+n*i.val; ac_rfl
  rw [he]
  exact congrArg (fun p : Fin n × Fin n => d p.1 p.2) (finProdFinEquiv.symm_apply_apply (i,j))
def matrix (x : Row × List Bool) : InstanceProgram.Matrix :=
  reshape (x.1,(parse ratRead (squareUnits x.1,x.2)).1)
noncomputable def matrixProgram : PolyProgram enc enc matrix := by
  have hp : Poly (parse ratRead) := ⟨parseProgram ratRead ratRead_poly.program ratRead_rest_length⟩
  have h : Poly matrix := by unfold matrix; fun_prop
  exact h.program
 theorem matrix_encoded {n : ℕ} (S : Finset (Fin n)) (d : Fin n → Fin n → ℚ) (xs : List Bool) :
    matrix (setView S,((List.ofFn (fun i => List.ofFn (d i))).flatten.map encodeRat).flatten++xs)=
      List.ofFn (fun i => List.ofFn (d i)) := by
  unfold matrix
  have hu : squareUnits (setView S)=List.replicate (List.ofFn (fun i => List.ofFn (d i))).flatten.length () := by
    apply List.eq_replicate_iff.mpr
    refine ⟨?_,fun _ _ => rfl⟩
    rw [squareUnits_length,flatten_ofFn]
    simp only [setView,List.length_ofFn]
  rw [hu,parse_encoded ratRead encodeRat ratRead_append]
  exact reshape_flatten S d
abbrev Header := (Row × Row) × ℕ
def header (xs : List Bool) : Header × List Bool :=
  let a := natRead xs
  let b := natRead a.2
  (((b.2.take a.1,(b.2.drop a.1).take a.1),b.1),b.2.drop (a.1+a.1))
@[fun_prop] theorem header_poly : Poly header := by unfold header; fun_prop
 theorem header_encoded (I : Instance) : header (encodeInstance I)=
    (((setView I.clients,setView I.facilities),I.k),
      (List.ofFn (fun i => (List.ofFn (fun j => encodeRat (I.distance i j))).flatten)).flatten) := by
  unfold header encodeInstance
  simp only [List.append_assoc,natRead_append]
  have hc : (setView I.clients).length=I.n := by simp only [setView,List.length_ofFn]
  have hf : (setView I.facilities).length=I.n := by simp only [setView,List.length_ofFn]
  change (((((setView I.clients)++(setView I.facilities++_)).take I.n,
    (((setView I.clients)++(setView I.facilities++_)).drop I.n).take I.n),I.k),
    ((setView I.clients)++(setView I.facilities++_)).drop (I.n+I.n))=_
  have htC (xs : Row) : (setView I.clients++xs).take I.n=setView I.clients := by simpa only [hc] using List.take_left (l₁ := setView I.clients) (l₂ := xs)
  have hdC (xs : Row) : (setView I.clients++xs).drop I.n=xs := by simpa only [hc] using List.drop_left (l₁ := setView I.clients) (l₂ := xs)
  have htF (xs : Row) : (setView I.facilities++xs).take I.n=setView I.facilities := by simpa only [hf] using List.take_left (l₁ := setView I.facilities) (l₂ := xs)
  have hdF (xs : Row) : (setView I.facilities++xs).drop I.n=xs := by simpa only [hf] using List.drop_left (l₁ := setView I.facilities) (l₂ := xs)
  simp only [htC,hdC,htF,← List.drop_drop,hdF]

def raw (xs : List Bool) : Raw :=
  let h := header xs
  (h.1.1,(h.1.2,matrix (h.1.1.1,h.2)))
noncomputable def rawProgram : PolyProgram enc enc raw := by
  have hm : Poly matrix := ⟨matrixProgram⟩
  exact (by unfold raw; fun_prop : Poly raw).program
 theorem raw_encoded (I : Instance) : raw (encodeInstance I)=view I := by
  unfold raw
  rw [header_encoded]
  have he : (List.ofFn (fun i => (List.ofFn (fun j => encodeRat (I.distance i j))).flatten)).flatten=
      ((List.ofFn (fun i => List.ofFn (I.distance i))).flatten.map encodeRat).flatten := by
    simp only [List.map_flatten,List.map_ofFn,Function.comp_def]
    rw [List.flatten_flatten]
    simp only [List.map_ofFn,Function.comp_def]
  rw [he]
  dsimp only
  have hm := matrix_encoded I.clients I.distance []
  simp only [List.append_nil] at hm
  rw [hm]
  rfl
noncomputable def instanceProgram : PolyProgram encodeInstance InstanceProgram.encode (id : Instance → Instance) :=
  (BooleanLists.packProgram.comp rawProgram).recode encodeInstance (fun _ => rfl) (fun I => congrArg enc (raw_encoded I))
end MetricKMedian.InputParser
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Probability_BernoulliRunHeight
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
open Binary
variable {n d : ℕ}

theorem denominator_height (p : Fin n → ℚ) (hp : ∀ i, 0 ≤ p i ∧ p i ≤ 1)
    (L : ℕ) (hL : ∀ i, HasHeight (p i) L) (t : ℕ) :
    (run (d:=d) p hp t).law.denominator ≤ (2:ℤ)^(stepHeight n d L*t) := by
  induction t with
  | zero => simp [run,SparseIntegerLaw.dirac]
  | succ t ih =>
    rw [run]
    split_ifs with ht
    · rw [dite_eq_left ht]
      have h := SparseIntegerLaw.step_denominator_height (run (d:=d) p hp t) (features (d:=d))
        (fun _ => p ⟨t,ht⟩) (fun _ => hp ⟨t,ht⟩) (fun q b => endpoint q ⟨t,ht⟩ b)
        ((n+1)^d+1) L 0 (run_length p hp t) (fun _ => hL _) (fun _ _ _ => features_height _ _)
      apply h.trans
      calc
        _ ≤ (2:ℤ)^(stepHeight n d L*t)*(2:ℤ)^(stepHeight n d L) :=
          mul_le_mul_of_nonneg_right ih (by positivity)
        _ = _ := by rw [← pow_add,Nat.mul_succ]
    · rw [dite_eq_right ht]
      exact ih.trans (pow_le_pow_right₀ (by norm_num) (Nat.mul_le_mul_left _ (Nat.le_succ t)))

end MetricKMedian.SparseBernoulli
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
 theorem endpoint_view (c : Context) (q : T c) (b : Fin 2) :
    rowEndpoint (decide (b=0)) (c,view c q)=view c (endpoint c q b) := by
  apply List.ext_getElem
  · simp only [rowEndpoint,ListOperation.endpoint,List.length_map,List.length_range,view,List.length_ofFn]
  · intro i hi hi'
    have hin : i < c.input.n := by simpa only [view,List.length_ofFn] using hi'
    simp only [rowEndpoint,ListOperation.endpoint,view,List.getElem_map,List.getElem_range,
      List.getElem_ofFn,List.getElem?_ofFn,dite_eq_left hin,Option.getD_some,endpoint]

noncomputable def probabilityProgram : PolyProgram (encodePair Context.encode er) Ratio.encode rowProbability := by
  let raw : PolyProgram (encodePair (encodePair qr Nat.bits) er) Ratio.encode
      (fun x : (List ℚ × ℕ) × Row => x.1.1[x.1.2]?.getD 0) := by
    exact Binary.Automatic.Poly.program (by fun_prop)
  exact raw.recode (fun x => (x.1.raw,x.2)) (fun _ => rfl) (fun _ => rfl)

noncomputable def compressProgram (d : ℕ) : PolyProgram State.encode State.encode
    (Bundle.compress (fun c : Context => (c.input.n+1)^d) (fun _ => features (d:=d))) :=
  SparseIntegerLaw.DependentProgram.compressProgram Context.encode er view [] (fun c => (c.input.n+1)^d) (fun _ => features (d:=d))
    (fun x => ListOperation.featureList d x.2) (fun _ q => ListOperation.featureList_ofFn q)
    (dimensionsProgram d) (featuresProgram d)

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

 theorem state_size (x : Input) (d t : ℕ) (ht : t ≤ x.n) :
    (State.encode (x.state d t)).length ≤ (sizePolynomial d).eval x.encode.length := by
  let L := x.encode.length
  obtain ⟨hn,hp⟩ := input_bounds x
  have htL : t ≤ L := ht.trans hn
  have hc : (Context.encode ⟨x,t⟩).length ≤ 3*L+2 := by
    have hbits : t.bits.length ≤ t+1 := NatBinary.length_le_height (Nat.lt_two_pow_self.le)
    change (encodePair qr Nat.bits (List.ofFn x.p,t)).length ≤ _
    rw [encodePair_length]
    change 2*L+1+t.bits.length ≤ _
    omega
  have hN : (x.state d t).law.length ≤ supportBound d L := by
    apply (run_length x.p x.feasible t).trans
    unfold supportBound
    gcongr
  have hH : SparseBernoulli.stepHeight x.n d L*t ≤ heightBound d L := by
    unfold heightBound SparseBernoulli.stepHeight SparseIntegerLaw.stepHeight
    gcongr
  have hD : (x.state d t).law.law.denominator ≤ (2:ℤ)^(heightBound d L) :=
    (denominator_height x.p x.feasible L hp t).trans (pow_le_pow_right₀ (by norm_num) hH)
  have hs (q : Fin x.n → Bool) : (er (List.ofFn q)).length ≤ 3*L := by
    have hh := EncodedList.length_bound encodeBool (List.ofFn q) 1 (fun _ _ => by rfl)
    simp only [List.length_ofFn] at hh
    exact hh.trans (by omega)
  have hb := SparseIntegerLaw.encode_length_bound (fun q : Fin x.n → Bool => er (List.ofFn q))
    (run (d:=d) x.p x.feasible t) (supportBound d L) (heightBound d L) (3*L) hN hD (fun _ => hs _)
  have he : State.encode (x.state d t)=encodePair Context.encode
      (SparseIntegerLaw.BinarySparse.encode (fun q : Fin x.n → Bool => er (List.ofFn q)))
        (⟨x,t⟩,run (d:=d) x.p x.feasible t) := by
    simp only [State.encode,Bundle.encode,Bundle.raw,Input.state,Context.encode,
      SparseIntegerLaw.BinarySparse.encode,SparseIntegerLaw.BinarySparse.raw,ed,encodePair,RoundingProgram.encodeList_map]
  rw [sizePolynomial_eval,he,encodePair_length]
  unfold sizeBound
  dsimp only at ⊢
  simp only [L] at hc hb ⊢
  omega

end MetricKMedian.SparseBernoulli.Program
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 overlap_sets (A B : Finset I) :
    ActionArrays.overlap (sets r A) (sets r B)=true ↔ (A∩B).Nonempty := by
  rw [sets,sets,ActionArrays.overlap_view,← map_inter]
  exact Finset.map_nonempty
 theorem transpose_graph (G : I → Finset I) :
    GraphData.transpose (graphView r G)=List.ofFn (fun h => sets r ((graph G).erase (r h))) := by
  simp only [GraphData.transpose,graphView,indices,List.length_ofFn,RoundingList.range_finRange,
    Function.comp_def,← List.ofFn_eq_map,List.map_ofFn,sets_eq,List.getElem?_ofFn,
    dite_eq_left (Fin.isLt _),Option.getD_some,Fin.eta,graph,mem_filter,mem_univ,true_and]
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 extras_list {n : ℕ} (d : Fin n → ℚ) (own : Finset (Fin n)) (Δ : ℕ) :
    extras ((List.ofFn d,List.ofFn fun i => decide (i∈own)),Δ)=
      (((zeroSources d\own).sort).take (Δ-own.card)).map Fin.val := by
  have hf : (RoundingList.indices (List.ofFn d)).filter
      (fun i => decide ((List.ofFn d)[i]?.getD 0=0) && !((List.ofFn fun k => decide (k∈own))[i]?.getD false))=
      ((zeroSources d\own).sort).map Fin.val := by
    simp only [RoundingList.indices,List.length_ofFn,RoundingList.range_finRange,List.filter_map,Function.comp_def,
      List.getElem?_ofFn,dite_eq_left (Fin.isLt _),Option.getD_some,Fin.eta]
    rw [show (fun i : Fin n => decide (d i=0) && !decide (i∈own))=
      (fun i : Fin n => decide (i∈zeroSources d\own)) by
      funext i; simp only [zeroSources,mem_sdiff,mem_filter,mem_univ,true_and,Bool.decide_and,decide_not]]
    rw [EncodingLists.filter_range]
    simp only [filter_univ_mem]
  simp only [extras,hf,EncodingLists.bool_card,List.map_take]
 theorem zeroRow_list {n : ℕ} (d : Fin n → ℚ) (own : Finset (Fin n)) (Δ : ℕ) :
    zeroRow ((List.ofFn d,List.ofFn fun i => decide (i∈own)),Δ)=List.ofFn (zeroMarginal d own Δ) := by
  apply List.ext_getElem
  · simp only [zeroRow,RoundingList.indices,List.length_map,List.length_range,List.length_ofFn]
  · intro k hk hk'
    have hkn : k<n := by simpa only [List.length_ofFn] using hk'
    let i : Fin n := ⟨k,hkn⟩
    simp only [zeroRow,RoundingList.indices,List.length_ofFn,List.getElem_map,List.getElem_range,
      List.getElem_ofFn,List.getElem?_ofFn,dite_eq_left hkn,Option.getD_some,extras_list]
    have he : natMember ((((zeroSources d\own).sort).take (Δ-own.card)).map Fin.val,i.val)=true ↔
        i∈(((zeroSources d\own).sort).take (Δ-own.card)).toFinset := by
      rw [natMember_true,List.mem_toFinset]
      simp only [List.mem_map,Fin.val_inj]
      simp only [exists_eq_right]
    change (if decide (i∈own) || natMember ((((zeroSources d\own).sort).take (Δ-own.card)).map Fin.val,i.val) then (1:ℚ) else 0)=zeroMarginal d own Δ i
    simp only [Bool.or_eq_true,decide_eq_true_eq,he,zeroMarginal,zeroSelection,extend,mem_union]
end MetricKMedian.Taper.ListOperation
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 pick_mem {f Δ : ℕ} (A : Finset (CopyState.Copy (F:=Fin f) Δ)) (S : Finset A) (k : ℕ) :
    k∈pick (active (_root_.OAI.MetricKMedian.RationalPhysicalKernel.CopyList.view A),sets (ordinal A) S) ↔ ∃a∈S,(rank a.val).val=k := by
  simp only [pick,active_view,RationalBatchData.Ordinal.sets_eq,Gaussian.ListOperation.zip_ofFn,
    List.mem_map,List.mem_filter,List.mem_ofFn]
  constructor
  · rintro ⟨z,⟨⟨i,rfl⟩,hi⟩,hk⟩
    exact ⟨enumeration A i,of_decide_eq_true hi,hk⟩
  · rintro ⟨a,ha,rfl⟩
    refine ⟨_,⟨⟨(enumeration A).symm a,rfl⟩,?_⟩,?_⟩
    · change decide (enumeration A ((enumeration A).symm a)∈S)=true
      rw [Equiv.apply_symm_apply]
      exact decide_eq_true ha
    · simp only [Equiv.apply_symm_apply]

 theorem next_view {f Δ : ℕ} (A : Finset (CopyState.Copy (F:=Fin f) Δ)) (E O : Finset A) :
    next ((Δ,_root_.OAI.MetricKMedian.RationalPhysicalKernel.CopyList.view A),(sets (ordinal A) E,sets (ordinal A) O))=
    _root_.OAI.MetricKMedian.RationalPhysicalKernel.CopyList.view (CopyState.next Δ A (E.image Subtype.val) (O.image (fun a => a.val.1))) := by
  unfold next
  have hl : (_root_.OAI.MetricKMedian.RationalPhysicalKernel.CopyList.view A).length=f*Δ := by simp only [_root_.OAI.MetricKMedian.RationalPhysicalKernel.CopyList.view,setView,List.length_ofFn]
  simp only [indices,hl,RoundingList.range_finRange,Function.comp_def,← List.ofFn_eq_map,List.map_ofFn]
  change List.ofFn (fun k : Fin (f*Δ) => _)=_
  conv_rhs => rw [view_eq]
  apply congrArg List.ofFn
  funext k
  let a := finProdFinEquiv.symm k
  have ha : rank a=k := finProdFinEquiv.apply_symm_apply k
  have hdiv : k.val/Δ=a.1.val := by rw [← ha,rank_owner]
  apply Bool.eq_iff_iff.mpr
  simp only [view_get,Bool.or_eq_true,
    Bool.and_eq_true,Bool.not_eq_true_eq_eq_false,Bool.eq_false_iff,decide_eq_true_eq,natMember_true,
    CopyState.next,mem_union,mem_sdiff,CopyState.mem_resets]
  simp only [ne_eq,natMember_true]
  rw [pick_mem]
  apply or_congr
  · apply and_congr Iff.rfl
    apply not_congr
    simp only [mem_image]
    constructor
    · rintro ⟨b,hb,hk⟩
      exact ⟨b,hb,finProdFinEquiv.injective ((Fin.ext hk).trans ha.symm)⟩
    · rintro ⟨b,hb,hba⟩
      refine ⟨b,hb,?_⟩
      change b.val=a at hba
      rw [hba,ha]
  · rw [List.mem_map]
    simp only [mem_image]
    constructor
    · rintro ⟨j,hj,hjk⟩
      obtain ⟨b,hb,rfl⟩ := (pick_mem A O j).mp hj
      rw [rank_owner,hdiv] at hjk
      exact ⟨b,hb,Fin.ext hjk⟩
    · rintro ⟨b,hb,hba⟩
      refine ⟨(rank b.val).val,(pick_mem A O _).mpr ⟨b,hb,rfl⟩,?_⟩
      rw [rank_owner,hdiv]
      exact congrArg Fin.val hba

end MetricKMedian.RationalPhysicalKernel.CopyNext
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)

noncomputable def bernInputProgram (bal : Bool) :
    PolyProgram Input.encode SparseBernoulli.Program.Input.encode (Input.bernInput bal) := by
  let raw : PolyProgram Binary.Automatic.enc SparseBernoulli.Program.qr
      (fun x : ListOperation.Raw => if bal then x.2.2.map (fun _ => x.2.1) else x.2.2) := by
    apply Binary.Automatic.Poly.program
    have hm : Binary.Automatic.Poly (fun x : ListOperation.Raw => x.2.2.map (fun _ => x.2.1)) := by
      apply Binary.Automatic.Poly.list_map <;> fun_prop
    fun_prop
  exact raw.recode Input.raw (fun _ => rfl) (fun x => by
    cases bal <;> simp only [Bool.false_eq_true,ite_false,ite_true,Input.raw,List.map_const',List.length_ofFn,
      Input.bernInput,SparseBernoulli.Program.Input.encode,List.ofFn_const,Fin.cast_eq_self])

end MetricKMedian.SparsePhysicalBatch.Program
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 subsetRaw (x : Row × Row) : Bool := (x.1.zip x.2).all (fun p => !p.1 || p.2)
@[fun_prop] theorem subsetRaw_poly : Poly subsetRaw := by
  unfold subsetRaw
  have h : Poly (fun x : Row × Row => (x.1.zip x.2).map (fun p => !p.1 || p.2)) := by apply list_map <;> fun_prop
  simpa only [List.all_map,Function.comp_def,id_eq] using (comp bool_all h)
end MetricKMedian.InstanceProgram
end

end OAI
end