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

import Mathlib
import Definitions.Def_MetricKMedian
import Definitions.Def_OAIQ037K063
import Definitions.Def_OAIQ037K064
import Definitions.Def_OAIQ037K066

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_BoundedEnumerationProgram
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)
 theorem maskWord_view {n : ℕ} (T : Finset (Fin n)) (ys : List (Fin n)) :
    maskWord (setView T,ys.map Fin.val)=setView ys.toFinset := by
  simp only [maskWord,indices,setView,List.length_ofFn,RoundingList.range_finRange,← List.ofFn_eq_map,List.map_ofFn]
  apply congrArg List.ofFn
  funext i
  apply Bool.eq_iff_iff.mpr
  simp only [Function.comp_def,List.map_map,List.any_eq_true,List.mem_map,id_eq,decide_eq_true_eq,List.mem_toFinset]
  constructor
  · rintro ⟨_,⟨a,ha,rfl⟩,he⟩
    exact (Fin.ext (of_decide_eq_true he)) ▸ ha
  · intro hi
    exact ⟨true,⟨i,hi,by simp⟩,rfl⟩
 theorem choicesRaw_view {n : ℕ} (T : Finset (Fin n)) (c : ℕ) : choicesRaw c (setView T)=
    ((words c (List.ofFn (T.orderEmbOfFin rfl))).map List.toFinset).map setView := by
  unfold choicesRaw
  rw [Preparation.RationalUnitInput.Program.ranks_view]
  have hr : List.ofFn (fun a => (T.orderEmbOfFin rfl a).val)=(List.ofFn (T.orderEmbOfFin rfl)).map Fin.val := by simp only [List.map_ofFn,Function.comp_def]
  rw [hr,words_map,List.map_map,List.map_map]
  apply List.map_congr_left
  intro ys _
  exact maskWord_view T ys
end MetricKMedian.Reduction.Enumeration
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 choicesRaw_choices {n : ℕ} (T : Finset (Fin n)) (c : ℕ) : choicesRaw c (setView T)=(choices T c).map setView :=
  choicesRaw_view T c

end MetricKMedian.Reduction.Enumeration
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 )
open Completion.Rational.BestProgram (card card_view)
open Enumeration

def values (I : Instance) (T : Finset (Fin I.n)) (c : ℕ) : List ℚ :=
  (choices T c).flatMap (fun D => (List.ofFn (T.orderEmbOfFin rfl)).map (fun i =>
    rationalCost I ((T\D).erase i)-rationalCost I (T\D)))

def endpoints (I : Instance) (T : Finset (Fin I.n)) (c : ℕ) : List (Finset (Fin I.n)) :=
  (0::values I T c).map (fun B => rationalHistory I B T c)
end MetricKMedian.Reduction.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Reduction_ReductionOutcomesProgram
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 Enumeration

def completions (I : Instance) (F U : Finset (Fin I.n)) (δ : ℚ) (b : ℕ) : List (Finset (Fin I.n)) :=
  (choices U b).flatMap (fun H => (choices F b).map (fun B => completionSet I F B (U\H) (rationalRadii I U) δ))

def outcomes (I : Instance) (F T : Finset (Fin I.n)) (δ : ℚ) (c b : ℕ) : List (Finset (Fin I.n)) :=
  T::(endpoints I T c).flatMap (fun U => U::completions I F U δ b)
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 branchList (I : Instance) : List Branch := (branches I I.facilities a).map (fun F => ⟨I,F⟩)
end MetricKMedian.Reduction.Program
end

end OAI
end