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

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

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseWeightedPartial
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.SparseWeightedPartial
open Finset RationalWeightedStep
variable {n : ℕ}

 theorem step_mean (β : Fin n → ℚ) (hβ : ∀ i, 0 < β i)
    (μ : SparseIntegerLaw (Vector ℚ n)) (i : Fin n) :
    (step β hβ μ).moment (fun p => point p i)=μ.moment (fun p => point p i) := by
  have hh := μ.step_moment features (probability β) (probability_unit β hβ)
    (endpoint β) (finSumFinEquiv (Sum.inl i))
  simp only [features_single] at hh
  exact hh.trans (μ.moment_congr _ _ (fun a => endpoint_mean β hβ _ i))

 theorem run_mean (β : Fin n → ℚ) (hβ : ∀ i, 0 < β i)
    (p : Vector ℚ n) (t : ℕ) (i : Fin n) :
    (run β hβ p t).moment (fun q => point q i)=point p i := by
  induction t with
  | zero => exact SparseIntegerLaw.dirac_moment _ _
  | succ t ih => rw [run,step_mean,ih]

end MetricKMedian.SparseWeightedPartial
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseCardinalRounding
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.SparseCardinalRounding
open Finset RationalWeightedStep
variable {n : ℕ}

theorem round_mean (p : Vector ℚ n) (i : Fin n) :
    (round p).moment (fun q => point q i)=point p i :=
  SparseWeightedPartial.run_mean _ _ p n i

end MetricKMedian.SparseCardinalRounding
end
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_columns (ν : Fin m → SparseIntegerLaw (Finset (Fin n)))
    (P : Fin m → Finset (Fin n) → Prop)
    (hP : ∀ i, ∀ a : Fin (ν i).length, P i (ν i).states[a.val]) (t : ℕ) (ht : t ≤ m) :
    ∀ a : Fin (run ν t).length, ∀ i, i.val<t → P i ((run ν t).states[a.val] i) := by
  induction t with
  | zero => intro a i hi; omega
  | succ t ih =>
    have htm : t < m := by omega
    have he : run ν (t+1)=step (run ν t) (ν ⟨t,htm⟩) ⟨t,htm⟩ := by
      rw [run,dite_eq_left htm]
    let inv : SparseIntegerLaw (Graph n m) → Prop := fun μ =>
      ∀ a : Fin μ.length, ∀ i, i.val<t+1 → P i (μ.states[a.val] i)
    change inv (run ν (t+1))
    rw [he]
    intro a i hi
    obtain ⟨j,k,hjk⟩ := ((run ν t).prodCompress_spec (ν ⟨t,htm⟩)
      (fun G S => next G S ⟨t,htm⟩) features).2.1 a
    change (step (run ν t) (ν ⟨t,htm⟩) ⟨t,htm⟩).states[a.val]=_ at hjk
    rw [hjk]
    by_cases hi' : i=⟨t,htm⟩
    · subst i
      simpa only [next,Function.update_self] using hP ⟨t,htm⟩ k
    · have hiv : i.val≠t := fun h => hi' (Fin.ext h)
      simpa only [next,Function.update_of_ne hi'] using ih (by omega) j i (by omega)

end MetricKMedian.SparseGraph
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_RepresentativeProgram
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.RationalRepresentatives.Program
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly Polynomial
open SparseGraph.ListOperation (Row Table setView indices)
open MaskProgram

def Input.raw (x : Input) : Raw := ((List.ofFn x.R,(List.ofFn (fun i => List.ofFn (x.d i)),x.M)),setView x.U)
def Input.encode (x : Input) : List Bool := enc x.raw
def State.raw (s : State) : Raw × (Row × Row) := (s.input.raw,(setView s.cut.1,setView s.cut.2))
def State.encode (s : State) : List Bool := enc s.raw

 theorem stepRaw_state (s : State) : stepRaw s.raw=(s.step).raw := by
  unfold stepRaw State.raw State.step advance
  rw [any_view]
  by_cases h : s.cut.1.Nonempty
  · simp only [decide_eq_true h,ite_true,dite_eq_left h,Input.raw,nearest_view s.input.R s.cut.1 h]
    apply Prod.ext
    · rfl
    apply Prod.ext
    · simp only [indices,setView,List.length_ofFn,RoundingList.range_finRange,Function.comp_def,← List.ofFn_eq_map,List.map_ofFn]
      apply congrArg List.ofFn
      funext i
      simp only [MaskProgram.get,List.getElem?_ofFn,dite_eq_left i.isLt,Option.getD_some,Fin.eta,
        dite_eq_left (Preparation.firstNearest _ _ h).isLt,mem_filter,Bool.decide_and]
    · simp only [indices,setView,List.length_ofFn,RoundingList.range_finRange,Function.comp_def,← List.ofFn_eq_map,List.map_ofFn]
      apply congrArg List.ofFn
      funext i
      simp only [MaskProgram.get,List.getElem?_ofFn,dite_eq_left i.isLt,Option.getD_some,Fin.eta,mem_insert,Bool.decide_or]
      rw [Bool.or_comm]
      congr 1
      simp only [Fin.ext_iff]
  · simp only [decide_eq_false h,Bool.false_eq_true,ite_false,dite_eq_right h]

noncomputable def stepProgram : PolyProgram State.encode State.encode State.step :=
  stepRaw_poly.program.recode State.raw (fun _ => rfl) (fun s => congrArg enc (stepRaw_state s))

noncomputable def startProgram : PolyProgram Input.encode State.encode Input.start := by
  have hp : Poly (fun x : Raw => (x,(x.2,x.2.map (fun _ => false)))) := by
    apply pair
    · fun_prop
    · apply pair
      · fun_prop
      · apply list_map <;> fun_prop
  exact hp.program.recode Input.raw (fun _ => rfl) (fun x => by
    change enc (x.raw,(setView x.U,(setView x.U).map (fun _ => false)))=enc (x.raw,(setView x.U,setView ∅))
    simp only [setView,List.map_ofFn,notMem_empty,decide_false,Function.comp_def]
    rfl)
noncomputable def countProgram : PolyProgram Input.encode Nat.bits Input.n := by
  have hp : Poly (fun x : Raw => x.2.length) := by fun_prop
  exact hp.program.recode Input.raw (fun _ => rfl) (fun x => by simp only [Input.raw,setView,List.length_ofFn]; rfl)
 theorem input_bound (x : Input) : x.n≤x.encode.length := by
  have hh := EncodedList.length_le encodeBool (setView x.U)
  simp only [setView,List.length_ofFn] at hh
  have he : x.encode.length=2*(enc (x.raw.1)).length+1+(enc x.raw.2).length := encodePair_length _ _ _
  change x.n≤(enc (setView x.U)).length at hh
  change x.encode.length=2*(enc x.raw.1).length+1+(enc (setView x.U)).length at he
  omega
 theorem mask_length {n : ℕ} (U : Finset (Fin n)) : (enc (setView U)).length≤3*n := Completion.Rational.PackingProgram.mask_length U
 theorem state_size (x : Input) (t : ℕ) : (State.encode (x.state t)).length≤11*x.encode.length+2 := by
  have h1 := mask_length ((advance x)^[t] (x.U,∅)).1
  have h2 := mask_length ((advance x)^[t] (x.U,∅)).2
  have hn := input_bound x
  change (encodePair Input.encode (encodePair (encodeList encodeBool) (encodeList encodeBool))
    (x,(setView ((advance x)^[t] (x.U,∅)).1,setView ((advance x)^[t] (x.U,∅)).2))).length≤_
  rw [encodePair_length,encodePair_length]
  dsimp only at ⊢
  change (encodeList encodeBool _).length≤3*x.n at h1 h2
  omega

noncomputable def program : PolyProgram Input.encode (encodeList encodeBool)
    (fun x => setView (select x.d x.R x.M x.n x.U)) := by
  let run := stepProgram.repeatFrom startProgram countProgram X (11*X+2)
    (fun x => by simpa using input_bound x)
    (fun x t _ => by rw [state_iterate]; simpa using state_size x t)
  let out : PolyProgram State.encode (encodeList encodeBool) (fun s => setView s.cut.2) :=
    ((snd enc (encodePair (encodeList encodeBool) (encodeList encodeBool))).comp
      (snd (encodeList encodeBool) (encodeList encodeBool))).recode State.raw (fun _ => rfl) (fun _ => rfl)
  exact (run.comp out).congr _ (fun x => by
    dsimp only [Function.comp_def]
    rw [state_iterate]
    change setView (((advance x)^[x.n] (x.U,∅)).2)=_
    rw [advance_result,empty_union])
end MetricKMedian.Preparation.RationalRepresentatives.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_BundleGeometryProgram
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.RationalBundles.Program
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
open MetricKMedian.MaskProgram
def view {f n : ℕ} (d : Fin n → Fin n → ℚ) (di : Fin n → Fin f → ℚ)
    (F : Fin n → Finset (Fin f)) (y : Fin f → ℚ) : Raw :=
  ((List.ofFn (fun i => List.ofFn (d i)),List.ofFn (fun i => List.ofFn (di i))),
    (List.ofFn (fun i => setView (F i)),List.ofFn y))
 theorem neighborMask_view {n : ℕ} (ds : Fin n → ℚ) (t : Fin n) :
    neighborMask (List.ofFn ds,t.val)=setView (univ.erase t) := by
  simp only [neighborMask,indices,List.length_ofFn,RoundingList.range_finRange,← List.ofFn_eq_map,
    List.map_ofFn,Function.comp_def,setView,mem_erase,mem_univ,and_true]
  simp only [ne_eq,Fin.val_inj]
 theorem nextData_view {n : ℕ} (d : Fin n → Fin n → ℚ) (t : Fin n) :
     nextData (List.ofFn (d t),t.val)=(next d t).val := by
  unfold nextData
  rw [neighborMask_view,Completion.Rational.PackingProgram.any_view]
  simp only [decide_eq_true_eq]
  unfold next
  split_ifs with h
  · rw [MetricKMedian.MaskProgram.nearest_view]
  · rfl

 theorem bundleData_view {f n : ℕ} (d : Fin n → Fin n → ℚ) (di : Fin n → Fin f → ℚ)
    (F : Fin n → Finset (Fin f)) (y : Fin f → ℚ) (δ : ℚ) (t : Fin n) :
    bundleData δ (view d di F y,t.val)=setView (bundle d di F δ t) := by
  simp only [bundleData,view,List.getElem?_ofFn,dite_eq_left t.isLt,Option.getD_some,Fin.eta,nextData_view]
  by_cases h : next d t=t
  · simp only [h,ite_true,bundle]
  · have hn : (next d t).val≠t.val := fun hh => h (Fin.ext hh)
    simp only [hn,ite_false,bundle,h,indices,List.length_ofFn,RoundingList.range_finRange,
      ← List.ofFn_eq_map,List.map_ofFn,Function.comp_def,MetricKMedian.MaskProgram.get,List.getElem?_ofFn,
      dite_eq_left (Fin.isLt _),Option.getD_some,Fin.eta,setView,mem_filter,Bool.decide_and]

 theorem bundlesData_view {f n : ℕ} (d : Fin n → Fin n → ℚ) (di : Fin n → Fin f → ℚ)
    (F : Fin n → Finset (Fin f)) (y : Fin f → ℚ) (δ : ℚ) :
    bundlesData δ (view d di F y)=List.ofFn (fun t => setView (bundle d di F δ t)) := by
  unfold bundlesData
  simp only [view,indices,List.length_ofFn,RoundingList.range_finRange,← List.ofFn_eq_map,List.map_ofFn,Function.comp_def]
  change List.ofFn (fun t : Fin n => bundleData δ (view d di F y,t.val))=_
  simp only [bundleData_view]

 theorem missingData_view {f n : ℕ} (d : Fin n → Fin n → ℚ) (di : Fin n → Fin f → ℚ)
    (F : Fin n → Finset (Fin f)) (y : Fin f → ℚ) (δ : ℚ) :
    missingData δ (view d di F y)=List.ofFn (fun t => setView (missing d di F δ t)) := by
  unfold missingData
  simp only [view,indices,List.length_ofFn,RoundingList.range_finRange,← List.ofFn_eq_map,List.map_ofFn,Function.comp_def]
  change List.ofFn (fun t : Fin n => List.ofFn (fun a : Fin f => MetricKMedian.MaskProgram.get ((List.ofFn (fun t => setView (F t)))[t.val]?.getD []) a.val && !MetricKMedian.MaskProgram.get (bundleData δ (view d di F y,t.val)) a.val))=_
  simp only [bundleData_view,MetricKMedian.MaskProgram.get,setView,List.getElem?_ofFn,dite_eq_left (Fin.isLt _),Option.getD_some,
    Fin.eta,missing,mem_sdiff,Bool.decide_and,decide_not]

 theorem massData_view {f n : ℕ} (y : Fin f → ℚ) (P : Fin n → Finset (Fin f)) :
    massData (List.ofFn y,List.ofFn (fun t => setView (P t)))=List.ofFn (mass y P) := by
  simp only [massData,List.map_ofFn,Function.comp_def,indices,List.length_ofFn,RoundingList.range_finRange,
    ← List.ofFn_eq_map,List.map_ofFn,MetricKMedian.MaskProgram.get,setView,List.getElem?_ofFn,dite_eq_left (Fin.isLt _),
    Option.getD_some,Fin.eta,decide_eq_true_eq,List.sum_ofFn,← Finset.sum_filter]
  simp only [Finset.filter_mem_eq_inter,Finset.univ_inter]
  rfl
end MetricKMedian.Preparation.RationalBundles.Program
end

end OAI
end

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

namespace OAI

section
section
namespace MetricKMedian.SparseSignedPartial
open Finset RationalSignedStep
open RationalWeightedStep (point fractional)
open SparseWeightedPartial (features features_single features_pair)
variable {n : ℕ}

 theorem step_mean (β : Fin n → ℚ) 
    (μ : SparseIntegerLaw (Vector ℚ n)) (i : Fin n) :
    (step β μ).moment (fun p => point p i)=μ.moment (fun p => point p i) := by
  have hh := μ.step_moment features (probability β) (probability_unit β)
    (endpoint β) (finSumFinEquiv (Sum.inl i))
  simp only [features_single] at hh
  exact hh.trans (μ.moment_congr _ _ (fun a => endpoint_mean β _ i))

end MetricKMedian.SparseSignedPartial
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseWeightedRounding
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.SparseWeightedRounding
open Finset RationalWeightedStep SparseWeightedPartial
variable {n : ℕ}

theorem round_mean (β : Fin n → ℚ) (hβ : ∀ i, 0 < β i)
    (p : Vector ℚ n) (i : Fin n) :
    (round β hβ p).moment (fun q => point q i)=point p i := by
  have hh := (run β hβ p n).step_moment features RationalLastFraction.probability
    RationalLastFraction.probability_unit RationalLastFraction.endpoint
    (finSumFinEquiv (Sum.inl i))
  simp only [features_single] at hh
  exact hh.trans (((run β hβ p n).moment_congr _ _
    (fun a => RationalLastFraction.endpoint_mean _ i)).trans (run_mean β hβ p n i))

theorem round_invariants (β : Fin n → ℚ) (hβ : ∀ i, 0 < β i)
    (p : Vector ℚ n) (hp : ∀ i, 0 ≤ point p i ∧ point p i ≤ 1)
    {M : ℚ} (hM : 0 ≤ M) (hβM : ∀ i, β i ≤ M) :
    ∀ a : Fin (round β hβ p).length,
      let q := (round β hβ p).states[a.val]
      (∀ i, point q i=0 ∨ point q i=1) ∧
      |(∑ i, β i*point q i)-(∑ i, β i*point p i)| ≤ M := by
  apply (run β hβ p n).step_property features RationalLastFraction.probability
    RationalLastFraction.probability_unit RationalLastFraction.endpoint
    (fun q => (∀ i, point q i=0 ∨ point q i=1) ∧
      |(∑ i, β i*point q i)-(∑ i, β i*point p i)| ≤ M)
  intro a b
  obtain ⟨ha,hb,hc⟩ := run_invariants β hβ p hp n a
  have hc' : (fractional (run β hβ p n).states[a.val]).card ≤ 1 := by simpa using hc
  refine ⟨RationalLastFraction.endpoint_integral _ ha hc' b,?_⟩
  have hh := RationalLastFraction.endpoint_noise (run β hβ p n).states[a.val] β
    (fun k => (hβ k).le) hβM hM b
  rwa [hb] at hh

end MetricKMedian.SparseWeightedRounding
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_LastFractionProgram
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.WeightedRound
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly SparseIntegerLaw.BinarySparse

 theorem lastRaw_state (x : RoundingProgram.State false) : lastRaw x.raw=(State.last x).raw := by
  change (List.ofFn x.β,_)=(List.ofFn x.β,vectorData _)
  apply congrArg (fun d => (List.ofFn x.β,d))
  exact vectorData_branch x.μ _ RationalLastFraction.probability_unit _ RoundingList.Last.probability
    (RoundingList.Last.endpoint false) (RoundingList.Last.endpoint true)
    RoundingList.Last.probability_list (fun p => RoundingList.Last.endpoint_list p 0)
    (fun p => RoundingList.Last.endpoint_list p 1)
noncomputable def lastProgram : PolyProgram RoundingProgram.State.encode RoundingProgram.State.encode State.last :=
  lastRaw_poly.program.recode RoundingProgram.State.raw RoundingProgram.State.encode_raw (fun x => by
    rw [lastRaw_state]
    exact RoundingProgram.State.encode_raw _)

end MetricKMedian.RoundingProgram.WeightedRound
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseTargetSubset
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.SparseTargetSubset
open Finset RationalWeightedStep
variable {n : ℕ}

theorem integral (D : Finset (Fin n)) {q : ℚ} (hq : 0 ≤ q ∧ q ≤ 1)
    (a : Fin (vectors D q).length) : ∀ i, point (vectors D q).states[a.val] i=0 ∨
      point (vectors D q).states[a.val] i=1 :=
  (SparseWeightedRounding.round_invariants (fun _ => 1) (fun _ => by norm_num)
    (initial D q) (initial_unit D hq) (show (0:ℚ) ≤ 1 by norm_num) (fun _ => le_rfl) a).1

theorem mean (D : Finset (Fin n)) {q : ℚ} (hq : 0 ≤ q ∧ q ≤ 1) (i : Fin n) :
    (law D q).moment (fun S => if i∈S then 1 else 0)=if i∈D then q else 0 := by
  rw [law,SparseIntegerLaw.map_moment]
  calc
    _ = (vectors D q).moment (fun p => point p i) :=
      SparseIntegerLaw.moment_congr _ _ _ (fun a =>
        SparseCardinalRounding.selected_indicator _ (integral D hq a) i)
    _ = point (initial D q) i := SparseWeightedRounding.round_mean _ _ _ _
    _ = _ := point_initial D q i

theorem subset (D : Finset (Fin n)) {q : ℚ} (hq : 0 ≤ q ∧ q ≤ 1)
    (a : Fin (law D q).length) : (law D q).states[a.val] ⊆ D := by
  intro i hi
  by_contra hn
  exact (law D q).zero_indicator (fun S => i∈S)
    (by rw [mean D hq i,ite_eq_right hn]) a (positive D q a) hi

theorem fixed (D : Finset (Fin n)) {q : ℚ} (hq : 0 ≤ q ∧ q ≤ 1)
    (a : Fin (law D q).length) :
    (q=0 → (law D q).states[a.val]=∅) ∧ (q=1 → (law D q).states[a.val]=D) := by
  constructor
  · intro hq0
    apply eq_empty_iff_forall_notMem.mpr
    intro i
    exact (law D q).zero_indicator (fun S => i∈S)
      (by rw [mean D hq i,hq0]; split_ifs <;> rfl) a (positive D q a)
  · intro hq1
    apply Subset.antisymm (subset D hq a)
    intro i hi
    exact (law D q).one_indicator (fun S => i∈S)
      (by rw [mean D hq i,ite_eq_left hi,hq1]) a (positive D q a)

theorem count_error (D : Finset (Fin n)) {q : ℚ} (hq : 0 ≤ q ∧ q ≤ 1)
    (a : Fin (law D q).length) :
    |(((law D q).states[a.val]).card:ℚ)-(D.card:ℚ)*q| ≤ 1 := by
  have hh := (SparseWeightedRounding.round_invariants (fun _ => 1) (fun _ => by norm_num)
    (initial D q) (initial_unit D hq) (show (0:ℚ) ≤ 1 by norm_num) (fun _ => le_rfl) a).2
  simp only [one_mul] at hh
  have hsum : (∑ i, point (initial D q) i)=(D.card:ℚ)*q := by
    simp only [point_initial,sum_ite_mem,univ_inter,sum_const,nsmul_eq_mul]
  have hcard : (((law D q).states[a.val]).card:ℚ)=
      ∑ i, point (vectors D q).states[a.val] i := by
    have he := SparseIntegerLaw.map_states (vectors D q) SparseCardinalRounding.selected a
    change (law D q).states[a.val]=_ at he
    rw [he]
    calc
      _ = ∑ i, if i∈SparseCardinalRounding.selected (vectors D q).states[a.val] then (1:ℚ) else 0 := by simp
      _ = _ := sum_congr rfl (fun i _ =>
        SparseCardinalRounding.selected_indicator _ (integral D hq a) i)
  rw [hcard]
  rwa [hsum] at hh

end MetricKMedian.SparseTargetSubset
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_TargetSubsetProgram
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.SparseTargetSubset.Program
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Row Table setView)
 theorem prepare_input (x : Input) : prepare x.raw=x.weighted.raw := by
  simp only [prepare,Input.raw,setView,List.map_ofFn,Function.comp_def,Input.weighted,RoundingProgram.Input.raw,
    initial,Vector.toList_ofFn,decide_eq_true_eq]

def Input.result (x : Input) := SparseGraph.Program.columnRaw (law x.D x.q)
end MetricKMedian.SparseTargetSubset.Program
end

end OAI
end

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

theorem columns (D : Fin m → Finset (Fin n)) (q : Fin m → ℚ)
    (hq : ∀ e, 0 ≤ q e ∧ q e ≤ 1) (a : Fin (law D q).length) (e : Fin m) :
    let S := (law D q).states[a.val] e
    S ⊆ D e ∧ |(S.card:ℚ)-((D e).card:ℚ)*q e| ≤ 1 ∧
      (q e=0 → S=∅) ∧ (q e=1 → S=D e) := by
  apply SparseGraph.run_columns (fun e => SparseTargetSubset.law (D e) (q e))
    (fun e S => S ⊆ D e ∧ |(S.card:ℚ)-((D e).card:ℚ)*q e| ≤ 1 ∧
      (q e=0 → S=∅) ∧ (q e=1 → S=D e))
    (fun e b => ⟨SparseTargetSubset.subset (D e) (hq e) b,
      SparseTargetSubset.count_error (D e) (hq e) b,
      SparseTargetSubset.fixed (D e) (hq e) b⟩) m (le_refl m) a e e.isLt

theorem upper_domination (D : Fin m → Finset (Fin n)) (q : Fin m → ℚ)
    (hq : ∀ e, 0 ≤ q e ∧ q e ≤ 1) (a : Fin (law D q).length) (e : Fin m) (i : Fin n) :
    (if i∈(law D q).states[a.val] e then (1:ℚ) else 0) ≤ upper (q e) := by
  by_cases he : 0 < q e
  · simp only [upper,ite_eq_left he]
    split_ifs <;> norm_num
  · have hz : q e=0 := le_antisymm (le_of_not_gt he) (hq e).1
    rw [(columns D q hq a e).2.2.1 hz]
    simp only [notMem_empty,ite_false,upper,ite_eq_right he,le_refl]

theorem error (D : Fin m → Finset (Fin n)) (q c : Fin m → ℚ)
    (hq : ∀ e, 0 ≤ q e ∧ q e ≤ 1) (hc : ∀ e, 0 ≤ c e ∧ c e ≤ 1)
    (hsmall : (univ.filter (fun e => 0 < q e ∧ q e < 1)).card ≤ 1)
    (a : Fin (law D q).length) :
    (∑ e, (c e*(upper (q e)-q e)+((D e).card:ℚ)*q e-
      (((law D q).states[a.val] e).card:ℚ))) ≤ 2 := by
  have hq0 : ∀ e, (0:ℝ) ≤ (q e:ℝ) := fun e => by exact_mod_cast (hq e).1
  have hq1 : ∀ e, (q e:ℝ) ≤ 1 := fun e => by exact_mod_cast (hq e).2
  have hc0 : ∀ e, (0:ℝ) ≤ (c e:ℝ) := fun e => by exact_mod_cast (hc e).1
  have hc1 : ∀ e, (c e:ℝ) ≤ 1 := fun e => by exact_mod_cast (hc e).2
  have hs : (MarginalRounding.fractional (fun e => (q e:ℝ))).card ≤ 1 := by
    unfold MarginalRounding.fractional
    have he : (univ.filter (fun e => 0 < (q e:ℝ) ∧ (q e:ℝ)<1))=
        univ.filter (fun e => 0 < q e ∧ q e<1) := by
      apply filter_congr
      intro e _
      norm_cast
    rwa [he]
  have hh := Preparation.exceptional_raw_error D (fun e => (q e:ℝ)) (fun e => (c e:ℝ))
    (law D q).states[a.val] hq0 hq1 hc0 hc1 hs (fun e => ⟨by
      exact_mod_cast (columns D q hq a e).2.1,
      fun he => (columns D q hq a e).2.2.1 (by exact_mod_cast he),
      fun he => (columns D q hq a e).2.2.2 (by exact_mod_cast he)⟩)
  have hu : ∀ e, Preparation.upperBit (q e:ℝ)=(upper (q e):ℝ) := by
    intro e
    simp only [Preparation.upperBit,upper]
    norm_cast
  simp_rw [hu] at hh
  exact_mod_cast hh

end MetricKMedian.SparseStarActivation
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_SignedTerminalProgram
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 SparseIntegerLaw.BinarySparse
open Binary.Automatic Binary.Automatic.Poly
namespace Terminal

noncomputable def bernoulliInputProgram : PolyProgram Input.encode SparseBernoulli.Program.Input.encode bernoulliInput :=
  (snd erow erow).recode Input.raw (fun _ => rfl) (fun x => by
    change erow x.p.toList=erow (List.ofFn (RationalWeightedStep.point x.p))
    rw [point_toList])

end Terminal
end MetricKMedian.RoundingProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_SignedRoundProgram
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 SparseIntegerLaw.BinarySparse
namespace SignedRound

def partialInput (x : Input true) (i : Fin (SparseSignedPartial.run x.β x.p x.n).length) : Input true :=
  ⟨x.n,x.β,(SparseSignedPartial.run x.β x.p x.n).states[i.val],x.positive,
    (SparseSignedPartial.run_invariants _ _ x.feasible _ i).1⟩
def partialInputs (x : Input true) : List (Input true) := List.ofFn (partialInput x)

end SignedRound
end MetricKMedian.RoundingProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_SignedPreparationProgram
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.SparseSignedPreparation.Program
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Row Table setView)
noncomputable def signedInputProgram : PolyProgram Input.encode RoundingProgram.Input.encode Input.signed := by
  let p : PolyProgram enc enc (fun x : Raw => (beta x,x.2.2.2)) := Poly.program (by fun_prop)
  exact p.recode Input.raw (fun _ => rfl) (fun x => by
    change enc (beta x.raw,x.p.toList)=_
    rw [beta_input]; rfl)

end MetricKMedian.SparseSignedPreparation.Program
end

end OAI
end