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

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

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

theorem opening_le (D : Fin m → Finset (Fin n)) (c q : Fin m → ℚ) (Δ : ℕ)
    (hc : ∀ e,0 ≤ c e ∧ c e ≤ 1) (hq : ∀ e,0 ≤ q e)
    (a : Fin (SparseOuterLaw.law D c q hc hq).length) :
    opening D c q Δ (SparseOuterLaw.law D c q hc hq).states[a.val] ≤
      (n:ℚ)*(Δ:ℚ)+(∑ e,SparseSignedPreparation.signed D c e*q e)+3+
       ∑ j,discarded D q Δ (SparseOuterLaw.law D c q hc hq).states[a.val] j := by
  rw [raw_identity]
  have hh := (SparseOuterLaw.budget D c q hc hq a).2.2.2.2.2
  linarith only [hh]

end MetricKMedian.SparsePrepared
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Reduction_DeletionProgram
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)
open Completion.Rational.BestProgram (card card_view)
open Enumeration

def eligibleData (x : (Raw × ℚ) × Row) : Row :=
  (indices x.2).map (fun i => get x.2 i && decide (costData (x.1.1,erase (i,x.2))-costData (x.1.1,x.2)≤x.1.2))
@[fun_prop] theorem eligibleData_poly : Poly eligibleData := by unfold eligibleData; apply list_map <;> fun_prop
 theorem eligibleData_view (I : Instance) (B : ℚ) (U : Finset (Fin I.n)) :
    eligibleData ((view I,B),setView U)=setView (rationalEligible I B U) := by
  simp only [eligibleData,indices,setView,List.length_ofFn,RoundingList.range_finRange,← List.ofFn_eq_map,List.map_ofFn]
  apply congrArg List.ofFn
  funext i
  change (get (setView U) i.val && decide (costData (view I,erase (i.val,setView U))-costData (view I,setView U)≤B))=decide _
  rw [get_view,erase_view,costData_view,costData_view]
  simp only [rationalEligible,mem_filter,Bool.decide_and]
def deleteData (x : (Raw × ℚ) × Row) : Row :=
  if x.1.1.2.1 < card x.2 then
    let E := eligibleData x
    if E.any id then erase (InstanceProgram.first E,x.2) else x.2
  else x.2
@[fun_prop] theorem deleteData_poly : Poly deleteData := by unfold deleteData; fun_prop
 theorem deleteData_view (I : Instance) (B : ℚ) (U : Finset (Fin I.n)) :
    deleteData ((view I,B),setView U)=setView (rationalDeleteStep I B U) := by
  unfold deleteData rationalDeleteStep
  change (if I.k < card (setView U) then _ else _)=_
  rw [card_view]
  by_cases hk : I.k < U.card
  · simp only [ite_eq_left hk]
    rw [eligibleData_view,Completion.Rational.PackingProgram.any_view]
    by_cases he : (rationalEligible I B U).Nonempty
    · simp only [decide_eq_true he,ite_true,dite_eq_left he,InstanceProgram.first_view _ he,erase_view]
    · simp only [decide_eq_false he,Bool.false_eq_true,ite_false,dite_eq_right he]
  · simp only [ite_eq_right hk]

def historyData : ℕ → (Raw × ℚ) × Row → Row
  | 0,x => x.2
  | c+1,x => deleteData (x.1,historyData c x)
@[fun_prop] theorem historyData_poly (c : ℕ) : Poly (historyData c) := by
  induction c with
  | zero => exact snd
  | succ c ih => change Poly (fun x => deleteData (x.1,historyData c x)); fun_prop
 theorem historyData_view (I : Instance) (B : ℚ) (U : Finset (Fin I.n)) (c : ℕ) :
    historyData c ((view I,B),setView U)=setView (rationalHistory I B U c) := by
  induction c with
  | zero => rfl
  | succ c ih => simp only [historyData,rationalHistory,ih,deleteData_view]

def valuesData (c : ℕ) (x : Raw × Row) : List ℚ :=
  (choicesRaw c x.2).flatMap (fun D => (Preparation.RationalUnitInput.Program.ranks x.2).map (fun i =>
    costData (x.1,erase (i,diff (x.2,D)))-costData (x.1,diff (x.2,D))))
@[fun_prop] theorem valuesData_poly (c : ℕ) : Poly (valuesData c) := by unfold valuesData; apply list_flatMap; apply list_map <;> fun_prop; fun_prop
 theorem valuesData_view (I : Instance) (T : Finset (Fin I.n)) (c : ℕ) :
    valuesData c (view I,setView T)=values I T c := by
  simp only [valuesData,choicesRaw_choices,List.flatMap_map,Preparation.RationalUnitInput.Program.ranks_view,List.map_ofFn,
    Function.comp_def,diff_view,erase_view,costData_view,values]

def endpointsData (c : ℕ) (x : Raw × Row) : Table :=
  (0::valuesData c x).map (fun B => historyData c ((x.1,B),x.2))
@[fun_prop] theorem endpointsData_poly (c : ℕ) : Poly (endpointsData c) := by
  unfold endpointsData
  apply list_map
  · fun_prop
  · have h := comp (list_cons (α := ℚ)) (pair (const 0 : Poly (fun _ : Raw × Row => (0:ℚ))) (valuesData_poly c))
    exact h
 theorem endpointsData_view (I : Instance) (T : Finset (Fin I.n)) (c : ℕ) :
    endpointsData c (view I,setView T)=(endpoints I T c).map setView := by
  simp only [endpointsData,valuesData_view,endpoints,List.map_map,Function.comp_def,historyData_view]
end MetricKMedian.Reduction.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_BranchProgram
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 Preparation Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView)
open InstanceProgram (Raw view)
open Completion.Rational.BestProgram (card card_view)
open Enumeration
variable (r : ℕ) (hr : 0 < r) {η τ : ℝ} (p : RationalAllParameters η τ) (c a b : ℕ) (δ : ℚ)
def branchOut (B : Branch) : List (Finset (Fin B.original.n)) :=
  if h : B.allowed then outcomes B.original B.facilities ((B.restricted h).computedPseudo r hr p c) δ c b else []
def allList (I : Instance) : List (Finset (Fin I.n)) :=
  (branches I I.facilities a).flatMap (fun F => branchOut r hr p c b δ ⟨I,F⟩)
end MetricKMedian.Reduction.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_FinalSelectionProgram
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 Preparation Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView)
open InstanceProgram (Raw view)
open Completion.Rational.BestProgram (card card_view)
def feasibleData (x : Raw × Row) : Bool := InstanceProgram.subsetRaw (x.2,x.1.1.2) && x.2.any id && decide (card x.2≤x.1.2.1)
@[fun_prop] theorem feasibleData_poly : Poly feasibleData := by unfold feasibleData; fun_prop
 theorem feasibleData_view (I : Instance) (S : Finset (Fin I.n)) : feasibleData (view I,setView S)=feasible I S := by
  simp only [feasibleData,view,InstanceProgram.subsetRaw_view,Completion.Rational.PackingProgram.any_view,card_view,feasible,Bool.decide_and,Bool.and_assoc]
def annotateData (x : Raw × Table) : List SparseSelect.TaggedProgram.Tag :=
  x.2.map (fun S => (feasibleData (x.1,S),(costData (x.1,S),S)))
@[fun_prop] theorem annotateData_poly : Poly annotateData := by unfold annotateData; apply list_map <;> fun_prop
def selectRaw (x : Raw × Table) : Table := SparseSelect.TaggedProgram.raw (annotateData x)
@[fun_prop] theorem selectRaw_poly : Poly selectRaw := by unfold selectRaw; fun_prop
 theorem selectRaw_view (I : Instance) (L : List (Finset (Fin I.n))) :
    selectRaw (view I,L.map setView)=((SparseSelect.best (feasible I) (rationalCost I) L).map setView).toList := by
  let ann := fun S : Finset (Fin I.n) => (feasible I S,(rationalCost I S,setView S))
  have ha : annotateData (view I,L.map setView)=L.map ann := by
    simp only [annotateData,List.map_map,Function.comp_def,feasibleData_view,costData_view]; rfl
  unfold selectRaw
  rw [ha,SparseSelect.TaggedProgram.raw_best]
  rw [← SparseSelect.best_map (feasible I) (rationalCost I) Prod.fst (fun a => a.2.1) ann (fun _ => rfl) (fun _ => rfl)]
  simp only [Option.map_map]; rfl
def selectData (x : Raw × Table) : Row := InstanceProgram.fallbackData (x.1,selectRaw x)
@[fun_prop] theorem selectData_poly : Poly selectData := by unfold selectData; fun_prop
end MetricKMedian.Reduction.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Reduction_OrdinaryListProgram
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 Preparation Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView)
open InstanceProgram (Raw view)
variable (r : ℕ) (hr : 0 < r) {η τ : ℝ} (p : RationalAllParameters η τ) (c a b : ℕ) (δ : ℚ)
def ordinarySet (I : Instance) : Finset (Fin I.n) :=
  if I.zeroTest then I.zeroOutput else selectList I (allList r hr p c a b δ I)
def algorithm (I : Instance) : List Bool := setView (ordinarySet r hr p c a b δ I)
end MetricKMedian.Reduction.Program
end

end OAI
end