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

import Mathlib
import Definitions.Def_MetricKMedian
import Definitions.Def_OAIQ037K072
import Definitions.Def_OAIQ037K073
import Definitions.Def_OAIQ037K074

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseOuterLaw
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.SparseOuterLaw
open Finset
open RationalWeightedStep (point)
open SparseGridRounding (base fraction)
open SparseSignedPreparation (State)
variable {n m : ℕ}

theorem activation_mean (D : Fin m → Finset (Fin n)) (c q : Fin m → ℚ)
    (hc : ∀ e, 0 ≤ c e ∧ c e ≤ 1) (hq : ∀ e, 0 ≤ q e) (e : Fin m) (i : Fin n) :
    (law D c q hc hq).moment (fun z => activation D q z e i)=if i∈D e then q e else 0 := by
  unfold activation
  rw [SparseIntegerLaw.moment_add,SparseIntegerLaw.moment_const,SparseSignedPreparation.target]
  by_cases hi : i∈D e
  · simp only [ite_eq_left hi,fraction_identity]
  · simp only [ite_eq_right hi,add_zero]

theorem activation_pair (D : Fin m → Finset (Fin n)) (c q : Fin m → ℚ)
    (hc : ∀ e, 0 ≤ c e ∧ c e ≤ 1) (hq : ∀ e, 0 ≤ q e) (e f : Fin m) (hef : e≠f) (i j : Fin n) :
    (law D c q hc hq).moment (fun z => activation D q z e i*activation D q z f j) ≤
      (if i∈D e then q e else 0)*(if j∈D f then q f else 0) := by
  have hh := SparseIntegerLaw.moment_affine_pair_le (law D c q hc hq)
    (fun z => if i∈z.2.1 e then 1 else 0) (fun z => if j∈z.2.1 f then 1 else 0)
    (if i∈D e then (base q e:ℚ) else 0) (if j∈D f then (base q f:ℚ) else 0)
    (if i∈D e then point (fraction q) e else 0) (if j∈D f then point (fraction q) f else 0)
    (SparseSignedPreparation.target _ _ _ _ _ e i) (SparseSignedPreparation.target _ _ _ _ _ f j)
    (SparseSignedPreparation.target_pair _ _ _ _ _ e f hef i j)
  change (law D c q hc hq).moment (fun z => activation D q z e i*activation D q z f j) ≤ _ at hh
  by_cases hi : i∈D e <;> by_cases hj : j∈D f
  all_goals simpa only [hi,hj,ite_true,ite_false,fraction_identity,zero_add] using hh

end MetricKMedian.SparseOuterLaw
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseOuterReal
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.SparseOuterLaw
open Finset
open RationalWeightedStep (point)
open SparseGridRounding (base fraction)
open SparseSignedPreparation (State)
variable {n m : ℕ}

theorem outsideCount_le_at (D : Fin m → Finset (Fin n)) (c q : Fin m → ℚ)
    (hc : ∀ e, 0 ≤ c e ∧ c e ≤ 1) (hq : ∀ e, 0 ≤ q e) (L : ℕ)
    (a : Fin (law D c q hc hq).length) (e : Fin m) (hL : q e ≤ L) :
    outsideCount q (law D c q hc hq).states[a.val] e ≤ L := by
  have hb : base q e ≤ L := by exact_mod_cast (Nat.floor_le (hq e)).trans hL
  by_cases hi : 0 < point (law D c q hc hq).states[a.val].1 e
  · have hl : base q e < L := by
      by_contra hn
      have heq : base q e = L := le_antisymm hb (le_of_not_gt hn)
      have hz : point (fraction q) e = 0 := by
        simp only [fraction, point, Vector.getElem_ofFn]
        have hh := Nat.floor_le (hq e)
        change (base q e : ℚ) ≤ q e at hh
        rw [heq] at hh ⊢
        linarith only [hh, hL]
      have hf := point_fixed D c q hc hq e hz a
      rw [hf] at hi
      exact (lt_irrefl 0) hi
    simpa only [outsideCount, ite_eq_left hi] using Nat.add_one_le_iff.mpr hl
  · simpa only [outsideCount, ite_eq_right hi, Nat.add_zero] using hb

end MetricKMedian.SparseOuterLaw
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseOuterMoments
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.SparseOuterLaw
open Finset
open SparseGridRounding (base)
open SparseSignedPreparation (State)
variable {n m : ℕ}

theorem activation_real_mean (D : Fin m → Finset (Fin n)) (c q : Fin m → ℚ)
    (hc : ∀ e, 0 ≤ c e ∧ c e ≤ 1) (hq : ∀ e, 0 ≤ q e) (e : Fin m) (i : Fin n) :
    (law D c q hc hq).realIndex.expect (fun a => (activation D q (law D c q hc hq).states[a.val] e i:ℝ))=
      ((if i∈D e then q e else 0:ℚ):ℝ) := by
  exact ((law D c q hc hq).realIndex_expect (fun z => activation D q z e i)).trans
    (congrArg (fun x : ℚ => (x:ℝ)) (activation_mean D c q hc hq e i))

theorem activation_real_pair (D : Fin m → Finset (Fin n)) (c q : Fin m → ℚ)
    (hc : ∀ e, 0 ≤ c e ∧ c e ≤ 1) (hq : ∀ e, 0 ≤ q e) (e f : Fin m) (hef : e≠f) (i j : Fin n) :
    (law D c q hc hq).realIndex.expect (fun a =>
      (activation D q (law D c q hc hq).states[a.val] e i:ℝ)*
        (activation D q (law D c q hc hq).states[a.val] f j:ℝ)) ≤
      ((if i∈D e then q e else 0:ℚ):ℝ)*((if j∈D f then q f else 0:ℚ):ℝ) := by
  have hh := activation_pair D c q hc hq e f hef i j
  have he := SparseIntegerLaw.realIndex_expect (law D c q hc hq)
    (fun z => activation D q z e i*activation D q z f j)
  simp only [Rat.cast_mul] at he
  rw [he]
  exact_mod_cast hh

theorem deficit_mean (D : Fin m → Finset (Fin n)) (c q : Fin m → ℚ) (g : ℚ)
    (hc : ∀ e, 0 ≤ c e ∧ c e ≤ 1) (hq : ∀ e, 0 ≤ q e) (i : Fin n) :
    (law D c q hc hq).realIndex.expect (fun a => (deficit D q g (law D c q hc hq).states[a.val] i:ℝ))=
      (g:ℝ)*(targetMean D q i:ℝ) := by
  simp only [deficit,Rat.cast_mul,Rat.cast_sum,FiniteLaw.expect_mul,FiniteLaw.expect_sum,
    activation_real_mean,targetMean]

end MetricKMedian.SparseOuterLaw
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)
noncomputable def program : PolyProgram Input.encode (ed SparseGraph.ListOperation.er) Input.result := by
  let p : PolyProgram Input.encode RoundingProgram.Input.encode Input.weighted :=
    prepare_poly.program.recode Input.raw (fun _ => rfl) (fun x => congrArg enc (prepare_input x))
  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 SparseGraph.ListOperation.er)
      (fun x : Data (List ℚ) => (x.1,x.2.map SparseCardinalRounding.Program.selectedRow)) := by
    apply Poly.program
    apply pair
    · fun_prop
    · apply list_map <;> fun_prop
  exact (p.comp RoundingProgram.WeightedRound.program |>.comp get |>.comp post).congr _ (fun x => by
    simp only [Function.comp_def,Input.result,law,SparseGraph.Program.columnRaw,SparseIntegerLaw.map,RoundingProgram.vectorData,
      Vector.toList_map,List.map_map,SparseCardinalRounding.Program.selectedRow_eq]
    rfl)
end MetricKMedian.SparseTargetSubset.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_StarActivationProgram
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.SparseStarActivation.Program
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Row Table setView indices)
noncomputable def graphProgram : PolyProgram Input.encode SparseGraph.Program.Input.encode Input.graph := by
  let n : PolyProgram Input.encode enc (fun x : Input => x.raw.1) :=
    (fst enc enc).recode Input.raw (fun _ => rfl) (fun _ => rfl)
  let columns := columnsProgram.comp (SparseTargetSubset.Program.program.listMap dummy)
  exact (n.fanout columns).recode id (fun _ => rfl) (fun x => by
    change SparseGraph.Program.ei (x.raw.1,x.columns.map SparseTargetSubset.Program.Input.result)=_
    simp only [Input.columns,List.map_ofFn,Function.comp_def]
    rfl)

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

noncomputable def boundProgram : PolyProgram Input.encode State.encode boundState := by
  let part :=  runProgram true
  let law := part.comp ((snd erow (ed erow)).comp (fst el (encodeList erow)) |>.recode (@State.raw true) State.encode_raw (fun _ => rfl))
  let kernels := partialInputsProgram.comp (Terminal.program.listMap emptyInput)
  let bound := (law.fanout kernels).comp SparseIntegerLaw.BinarySparse.bindData_poly.program
  let β := (fst erow erow).recode (@Input.raw true) (fun _ => rfl) (fun _ => rfl)
  exact (β.fanout bound).recode id (fun _ => rfl) (fun x => by
    rw [← State.encode_raw]
    change encodePair erow (ed erow) (List.ofFn x.β,
      bindData (((SparseSignedPartial.run x.β x.p x.n).law.denominator,
        List.ofFn (SparseSignedPartial.run x.β x.p x.n).law.numerator),
        (partialInputs x).map Terminal.result))=_
    simp only [partialInputs,List.map_ofFn,Function.comp_def]
    change encodePair erow (ed erow) (List.ofFn x.β,
      bindData ((raw (SparseSignedPartial.run x.β x.p x.n)).1,
        List.ofFn (fun i => ((raw (SparseSignedRounding.kernel x.β x.p x.feasible i)).1,
          (SparseSignedRounding.kernel x.β x.p x.feasible i).states.toList.map Vector.toList))))=_
    rw [bindData_raw]
    rfl)

noncomputable def program : PolyProgram Input.encode State.encode result :=
  (boundProgram.comp (compressProgram true)).congr _ (fun _ => rfl)

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 kernelProgram : PolyProgram KernelInput.encode (enc : Data StateRaw → List Bool) KernelInput.result := by
  let p : PolyProgram KernelInput.encode enc (fun x : KernelInput => x.p.toList) :=
    ((snd enc enc).comp (snd enc enc)).recode KernelInput.raw (fun _ => rfl) (fun _ => rfl)
  exact (p.fanout ((starInputProgram.comp SparseStarActivation.Program.program).fanout bernoulliProgram
    |>.comp prodData_poly.program) |>.comp attach_poly.program).congr _ kernel_raw

noncomputable def kernelsProgram : PolyProgram Input.encode (encodeList KernelInput.encode) Input.kernels := by
  let r : PolyProgram Input.encode enc Input.raw := (identity enc).recode Input.raw (fun _ => rfl) (fun _ => rfl)
  let s := signedInputProgram.comp RoundingProgram.SignedRound.program
  let sr : PolyProgram RoundingProgram.State.encode enc (RoundingProgram.State.raw (s:=true)) :=
    (identity enc).recode RoundingProgram.State.raw RoundingProgram.State.encode_raw (fun _ => rfl)
  exact (r.fanout (s.comp sr) |>.comp inputRows_poly.program).recode id (fun _ => rfl) (fun x => by
    change encodeList enc (inputRows (x.raw,(RoundingProgram.SignedRound.result x.signed).raw))=_
    simp only [inputRows,RoundingProgram.State.raw,states_list,List.map_ofFn,
      Function.comp_def]
    change encodeList enc (List.ofFn (fun i => (x.ker i).raw))=encodeList KernelInput.encode x.kernels
    rw [List.ofFn_comp',encodeList_map]; rfl)

noncomputable def weightsProgram : PolyProgram Input.encode el (fun x => (SparseIntegerLaw.BinarySparse.raw x.μ).1) := by
  let weights : PolyProgram RoundingProgram.State.encode el (fun x : RoundingProgram.State true => (x.raw).2.1) :=
    ((snd enc enc).comp (fst enc enc)).recode RoundingProgram.State.raw RoundingProgram.State.encode_raw (fun _ => rfl)
  exact (signedInputProgram.comp RoundingProgram.SignedRound.program |>.comp weights).congr _ (fun _ => rfl)
noncomputable def program : PolyProgram Input.encode (enc : Data StateRaw → List Bool) Input.result :=
  (weightsProgram.fanout (kernelsProgram.comp (kernelProgram.listMap dummy)) |>.comp bindData_poly.program).congr _ bind_result

end MetricKMedian.SparseSignedPreparation.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_OuterLawProgram
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.SparseOuterLaw.Program
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Table setView)
noncomputable def program : PolyProgram Input.encode (enc : Data SparseSignedPreparation.Program.StateRaw → List Bool) Input.result :=
  (signedProgram.comp SparseSignedPreparation.Program.program).congr _ (fun _ => rfl)
end MetricKMedian.SparseOuterLaw.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_PreparedLawProgram
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.SparsePrepared.Program
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (setView)
noncomputable def kernelsProgram : PolyProgram Input.encode (encodeList KernelInput.encode) Input.kernels := by
  let r : PolyProgram Input.encode enc Input.raw := (identity enc).recode Input.raw (fun _ => rfl) (fun _ => rfl)
  exact (r.fanout (outerInputProgram.comp SparseOuterLaw.Program.program) |>.comp kernelRows_poly.program).recode id
    (fun _ => rfl) (fun x => by
      change encodeList enc (kernelRows (x.raw,SparseOuterLaw.Program.Input.result x.outer))=_
      simp only [kernelRows,SparseOuterLaw.Program.Input.result,states_list,List.map_ofFn,Function.comp_def]
      change encodeList enc (List.ofFn (fun i => (x.ker i).raw))=encodeList KernelInput.encode x.kernels
      rw [List.ofFn_comp',RoundingProgram.encodeList_map]; rfl)
noncomputable def weightsProgram : PolyProgram Input.encode el (fun x => (SparseIntegerLaw.BinarySparse.raw x.μ).1) :=
  (outerInputProgram.comp SparseOuterLaw.Program.program |>.comp (fst el (encodeList enc))).congr _ (fun _ => rfl)
noncomputable def program : PolyProgram Input.encode (enc : Data PreparedRaw → List Bool) Input.result :=
  (weightsProgram.fanout (kernelsProgram.comp (kernelProgram.listMap dummy)) |>.comp bindData_poly.program).congr _ bind_result
end MetricKMedian.SparsePrepared.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_SupplierPreparationProgram
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.RationalSuppliers.Program
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (setView indices)
open SparseIntegerLaw.BinarySparse
variable {τ : ℝ} (qR : FixedBatch.RationalParameters τ)
noncomputable def tablesProgram : PolyProgram Input.encode (enc : List (List ℕ) → List Bool)
    (fun x => (x.S.tables qR).map List.ofFn) := by
  let r : PolyProgram Input.encode enc Input.raw := (identity enc).recode Input.raw (fun _ => rfl) (fun _ => rfl)
  let states := preparedInputProgram qR |>.comp SparsePrepared.Program.program |>.comp (snd el (encodeList enc))
  exact (r.fanout states |>.comp (tablesData_poly qR).program).congr _ (fun x => by
    simp only [Function.comp_def,tablesData,SparsePrepared.Program.Input.result,List.map_map]
    change ((x.S.law qR).states.toList.map (fun z => countsData qR (x.raw,SparsePrepared.Program.view z)))=_
    simp only [countsData_view,Data.tables,List.map_map,Function.comp_def])
end MetricKMedian.Preparation.RationalSuppliers.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_SupplierScanProgram
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.RationalSuppliers.Program
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
variable {τ : ℝ} (qR : FixedBatch.RationalParameters τ)
noncomputable def scanTablesProgram : PolyProgram ScanInput.encode (enc : List (List ℕ) → List Bool)
    (fun x => (x.S.tables qR).map List.ofFn) :=
  (scanPrepProgram.comp (tablesProgram qR)).congr _ (by intro x; simp only [Function.comp_def,ScanInput.prep])
noncomputable def scanRawPairProgram : PolyProgram ScanInput.encode (enc : ScanRaw × List (List ℕ) → List Bool)
    (fun x => (x.raw,(x.S.tables qR).map List.ofFn)) :=
  ((identity enc).recode ScanInput.raw (fun _ => rfl) (fun _ => rfl)).fanout (scanTablesProgram qR)
noncomputable def scanRawProgram : PolyProgram ScanInput.encode enc
    (fun x => scanData (x.raw,(x.S.tables qR).map List.ofFn)) :=
  scanRawPairProgram qR |>.comp scanData_poly.program
noncomputable def scanInputProgram : PolyProgram ScanInput.encode FixedBatch.RationalParameters.PreparedScanProgram.Input.encode (ScanInput.scan qR) :=
  (scanRawProgram qR).recode id (fun _ => rfl) (fun x => congrArg enc (scanData_view qR x))
noncomputable def scanProgram : PolyProgram ScanInput.encode (enc : Table → List Bool)
    (fun x => ((x.S.scan qR x.df x.dc x.budget).map setView).toList) :=
  (scanInputProgram qR |>.comp (FixedBatch.RationalParameters.PreparedScanProgram.program qR)).congr _ (by
    intro x
    simp only [Function.comp_def,FixedBatch.RationalParameters.PreparedScanProgram.Input.result,ScanInput.scan,Data.scan]
    rfl)
end MetricKMedian.Preparation.RationalSuppliers.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

 theorem suppliersData_view {f j : ℕ} (U : RationalUnitInput f j) {X : Type} [PseudoMetricSpace X]
    (R : U.Realization X) {η τ : ℝ} (p : RationalAllParameters η τ) :
    suppliersData p.δ p.γ (geometryData (view U,setView (U.representatives p.M)))=
      RationalSuppliers.Program.supplierView (U.suppliers R p) := by
  rw [geometryData_view]
  unfold suppliersData
  rw [RationalBundles.Program.bundlesData_view,RationalBundles.Program.missingData_view]
  simp only [RationalBundles.Program.view,RationalBundles.Program.massData_view]
  rfl

end MetricKMedian.Preparation.RationalUnitInput.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_UnitScanProgram
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.ScanProgram
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
open Program
variable {η τ : ℝ} (p : RationalAllParameters η τ)
 theorem postData_view (x : Input) :
    postData (x.raw,suppliersData p.δ p.γ (geometryData (view x.U,setView (x.U.representatives p.M))))=(x.sup p).raw := by
  let := x.metric
  unfold postData
  rw [suppliersData_view x.U x.R p]
  rfl
noncomputable def unitProgram : PolyProgram Input.encode Program.Input.encode Input.unit :=
  (fst enc enc).recode Input.raw (fun _ => rfl) (fun _ => rfl)
noncomputable def suppliersProgram : PolyProgram Input.encode enc
    (fun x => suppliersData p.δ p.γ (geometryData (view x.U,setView (x.U.representatives p.M)))) :=
  (unitProgram.comp (Program.supplierRawProgram p)).congr _ (fun _ => rfl)
noncomputable def supplierInputProgram : PolyProgram Input.encode RationalSuppliers.Program.ScanInput.encode (Input.sup p) :=
  (((identity enc).recode Input.raw (fun _ => rfl) (fun _ => rfl) |>.fanout (suppliersProgram p)).comp postData_poly.program).recode
    id (fun _ => rfl) (fun x => congrArg enc (postData_view p x))
noncomputable def program : PolyProgram Input.encode (enc : Table → List Bool) (Input.result p) :=
  (supplierInputProgram p |>.comp (RationalSuppliers.Program.scanProgram p.round)).congr _ (by
    intro x
    simp only [Function.comp_def,Input.result,Input.sup,RationalUnitInput.scan])
end MetricKMedian.Preparation.RationalUnitInput.ScanProgram
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
attribute [local irreducible] RationalUnitInput.ScanProgram.Input.result
variable {η τ : ℝ} (p : RationalAllParameters η τ)
noncomputable def masksProgram : PolyProgram Input.encode (enc : Table → List Bool)
    (fun z => RationalUnitInput.ScanProgram.Input.result p z.unit) :=
  @PolyProgram.comp Input RationalUnitInput.ScanProgram.Input Table Input.encode
    RationalUnitInput.ScanProgram.Input.encode enc Input.unit (RationalUnitInput.ScanProgram.Input.result p)
    unitProgram (RationalUnitInput.ScanProgram.program p)
noncomputable def program : PolyProgram Input.encode (enc : Table → List Bool) (Input.result p) :=
  (PolyProgram.comp (g:=imageData)
    (((identity enc).recode Input.raw (fun _ => rfl) (fun _ => rfl) |>.comp (fst enc enc)).fanout (masksProgram p))
    imageData_poly.program).congr _ (imageData_view p)
end MetricKMedian.Preparation.FractionalRefinement.ScanProgram
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)
 theorem zeroTestData_view (I : Instance) : zeroTestData (view I)=decide I.zeroTest := by
  apply Bool.eq_iff_iff.mpr
  simp only [zeroTestData,view,subsetRaw_view,card_view,Bool.and_eq_true,decide_eq_true_eq]
  rfl
noncomputable def zeroTestProgram : PolyProgram encode encodeBool (fun I => decide I.zeroTest) :=
  zeroTestData_poly.program.recode view (fun _ => rfl) (fun I => congrArg encodeBool (zeroTestData_view I))

 theorem singletonRaw_view {n : ℕ} (S : Finset (Fin n)) (a : Fin n) : singletonRaw (setView S,a.val)=setView {a} := by
  simp only [singletonRaw,indices,setView,List.length_ofFn,RoundingList.range_finRange,← List.ofFn_eq_map,List.map_ofFn,Function.comp_def,mem_singleton,Fin.ext_iff]
 theorem singletonData_view (I : Instance) : singletonData (view I)=setView {I.facilities.min' I.facilities_nonempty} := by
  unfold singletonData view
  rw [first_view,singletonRaw_view]
 theorem zeroOutputData_view (I : Instance) : zeroOutputData (view I)=setView I.zeroOutput := by
  unfold zeroOutputData Instance.zeroOutput
  change (if (setView I.clients).any id then setView I.clients else singletonData (view I))=_
  rw [Completion.Rational.PackingProgram.any_view]
  simp only [decide_eq_true_eq]
  split_ifs
  · rfl
  · exact singletonData_view I
noncomputable def zeroOutputProgram : PolyProgram encode (enc : Row → List Bool) (fun I => setView I.zeroOutput) :=
  zeroOutputData_poly.program.recode view (fun _ => rfl) (fun I => congrArg enc (zeroOutputData_view I))
end MetricKMedian.InstanceProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_InstanceRoundProgram
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
variable (r : ℕ) (hr : 0 < r) {η τ : ℝ} (p : RationalAllParameters η τ) (C : ℕ)
attribute [local irreducible] FractionalRefinement.scan Instance.computedFractional
noncomputable def nonzeroRoundProgram : PolyProgram nzEncode (enc : Table → List Bool)
    (fun I => ((I.val.nonzeroRound I.property r hr p C).map setView).toList) :=
  ((((identity enc).recode (fun I : Nonzero => view I.val) (fun _ => rfl) (fun _ => rfl)).fanout
    ((scanInputProgram r hr C).comp (FractionalRefinement.ScanProgram.program p))).comp imageData_poly.program).congr
      _ (imageData_view r hr p C)

noncomputable def nonzeroPseudoProgram : PolyProgram nzEncode (enc : Row → List Bool)
    (fun I => setView ((I.val.nonzeroRound I.property r hr p C).getD {I.val.facilities.min' I.val.facilities_nonempty})) :=
  ((((identity enc).recode (fun I : Nonzero => view I.val) (fun _ => rfl) (fun _ => rfl)).fanout
    (nonzeroRoundProgram r hr p C)).comp fallbackData_poly.program).congr _ (by
      intro I
      simp only [Function.comp_def,fallbackData,id_eq,singletonData_view]
      cases I.val.nonzeroRound I.property r hr p C <;> rfl)
noncomputable def pseudoProgram : PolyProgram encode (enc : Row → List Bool)
    (fun I => setView (I.computedPseudo r hr p C)) :=
  (dependentIfTotal Instance.zeroTest zeroTestProgram
    (fun I h => setView ((I.nonzeroRound h r hr p C).getD {I.facilities.min' I.facilities_nonempty}))
    (fun I _ => setView I.zeroOutput) (nonzeroPseudoProgram r hr p C)
    (zeroOutputProgram.recode Subtype.val (fun _ => rfl) (fun _ => rfl))).congr _ (by
      intro I
      unfold Instance.computedPseudo
      split_ifs <;> rfl)
end MetricKMedian.InstanceProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_RestrictionProgram
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.Reduction.Enumeration
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
open InstanceProgram (Raw view)
open MetricKMedian.MaskProgram
 theorem branchesData_view (I : Instance) (F : Finset (Fin I.n)) (a : ℕ) :
    branchesData a (view I,setView F)=(branches I F a).map setView := by
  simp only [branchesData,arcpairs_view,words_map,List.map_map,Function.comp_def,branches,restrictData_view]
end MetricKMedian.Reduction.Enumeration
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Reduction_LocalCompletionProgram
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.Reduction.Program
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
open InstanceProgram (Raw view)
open MetricKMedian.MaskProgram
open Preparation.RationalNearest.MaskProgram (erase erase_view insert insert_view)
open Enumeration

def getDist (x : Raw × (ℕ × ℕ)) : ℚ := (x.1.2.2[x.2.1]?.getD [])[x.2.2]?.getD 0
@[fun_prop] theorem getDist_poly : Poly getDist := by unfold getDist; fun_prop

def radiiData (x : Raw × Row) : List ℚ := (indices x.2).map (fun t => nearestData (x.1.2.2[t]?.getD [],erase (t,x.2)))
end MetricKMedian.Reduction.Program
end

end OAI
end