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

import Mathlib
import Definitions.Def_MetricKMedian
import Definitions.Def_OAIQ037K029
import Definitions.Def_OAIQ037K030
import Definitions.Def_OAIQ037K000
import Definitions.Def_OAIQ037K001
import Definitions.Def_OAIQ037K002
import Definitions.Def_OAIQ037K005
import Definitions.Def_OAIQ037K006
import Definitions.Def_OAIQ037K017
import Definitions.Def_OAIQ037K022
import Definitions.Def_OAIQ037K033

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

namespace OAI

namespace MetricKMedian.SparseIntegerLaw
open Finset
variable {α : Type}

 theorem moment_mono (μ : SparseIntegerLaw α) (f g : α → ℚ)
    (h : ∀ i : Fin μ.length, f μ.states[i.val] ≤ g μ.states[i.val]) :
    μ.moment f ≤ μ.moment g := by
  apply sum_le_sum
  intro i _
  exact mul_le_mul_of_nonneg_left (h i) (μ.law.rational.nonneg i)

 theorem moment_const (μ : SparseIntegerLaw α) (c : ℚ) : μ.moment (fun _ => c)=c := by
  unfold moment
  rw [← sum_mul,μ.law.rational.total,one_mul]

end MetricKMedian.SparseIntegerLaw

end OAI
end

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

namespace OAI

namespace MetricKMedian.SparseIntegerLaw
open Finset
variable {α : Type}

theorem moment_add (μ : SparseIntegerLaw α) (f g : α → ℚ) :
    μ.moment (fun a => f a+g a)=μ.moment f+μ.moment g := by
  simp only [moment,mul_add,sum_add_distrib]

theorem moment_mul_right (μ : SparseIntegerLaw α) (f : α → ℚ) (c : ℚ) :
    μ.moment (fun a => f a*c)=μ.moment f*c := by
  simp only [moment,← mul_assoc,sum_mul]

end MetricKMedian.SparseIntegerLaw

end OAI
end

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

namespace OAI

namespace MetricKMedian.SparseIntegerLaw
open Finset
variable {α β : Type}

theorem bindIndexed_property (μ : SparseIntegerLaw α) (κ : Fin μ.length → SparseIntegerLaw β)
    (P : β → Prop) (hP : ∀ a, ∀ b : Fin (κ a).length, P (κ a).states[b.val]) :
    ∀ i : Fin (μ.bindIndexed κ).length, P (μ.bindIndexed κ).states[i.val] := by
  intro i
  change P ((Vector.ofFn (fun j => let z := finSigmaFinEquiv.symm j;
    (κ z.1).states[z.2.val]))[i.val])
  simp only [Vector.getElem_ofFn]
  exact hP _ _

end MetricKMedian.SparseIntegerLaw

end OAI
end

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

namespace OAI

namespace MetricKMedian.SparseIntegerLaw
variable {α β : Type}

theorem map_moment (μ : SparseIntegerLaw α) (f : α → β) (v : β → ℚ) :
    (μ.map f).moment v=μ.moment (fun a => v (f a)) := by
  unfold moment map
  simp only [Vector.getElem_map]

end MetricKMedian.SparseIntegerLaw

end OAI
end

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

theorem endpoint_mean (p : Vector ℚ n) (k : Fin n) :
    probability p*point (endpoint p 0) k+
      (1-probability p)*point (endpoint p 1) k=point p k := by
  by_cases h : (fractional p).Nonempty
  · simp only [probability,endpoint,dite_eq_left h,point,Vector.getElem_ofFn,Fin.eta]
    norm_num only [show (1:Fin 2) ≠ 0 by decide,ite_true,ite_false]
    by_cases hi : k=pick p h
    · subst k; simp only [ite_true]; ring
    · simp only [ite_eq_right hi]; ring
  · simp only [probability,endpoint,dite_eq_right h]; ring

theorem endpoint_integral (p : Vector ℚ n)
    (hp : ∀ k, 0 ≤ point p k ∧ point p k ≤ 1)
    (hsmall : (fractional p).card ≤ 1) (b : Fin 2) (k : Fin n) :
    point (endpoint p b) k=0 ∨ point (endpoint p b) k=1 := by
  by_cases h : (fractional p).Nonempty
  · simp only [endpoint,dite_eq_left h,point,Vector.getElem_ofFn,Fin.eta]
    by_cases hk : k=pick p h
    · simp only [ite_eq_left hk]; split_ifs <;> simp
    · simp only [ite_eq_right hk]
      apply nonfractional p hp k
      intro hm
      exact hk (card_le_one.mp hsmall k hm (pick p h) (pick_mem p h))
  · simp only [endpoint,dite_eq_right h]
    apply nonfractional p hp
    exact fun hm => h ⟨k,hm⟩

theorem endpoint_noise (p : Vector ℚ n) (β : Fin n → ℚ) {M : ℚ}
    (hβ0 : ∀ k, 0 ≤ β k) (hβM : ∀ k, β k ≤ M) (hM : 0 ≤ M) (b : Fin 2) :
    |(∑ k, β k*point (endpoint p b) k)-(∑ k, β k*point p k)| ≤ M := by
  by_cases h : (fractional p).Nonempty
  · simp only [endpoint,dite_eq_left h]
    let i := pick p h
    have hi := (mem_filter.mp (pick_mem p h)).2
    rw [← sum_sub_distrib]
    have hid : (∑ k, (β k*point (Vector.ofFn
        (fun k => if k=pick p h then (if b=0 then 1 else 0) else point p k)) k-β k*point p k))=
        β i*((if b=0 then 1 else 0)-point p i) := by
      rw [sum_eq_single i]
      · simp only [point,Vector.getElem_ofFn,Fin.eta,i,ite_true]
        ring
      · intro k _ hki
        simp only [point,Vector.getElem_ofFn,Fin.eta,show k ≠ pick p h from hki,ite_false,sub_self]
      · intro hh; exact False.elim (hh (mem_univ i))
    rw [hid,abs_mul,abs_of_nonneg (hβ0 i)]
    have herr : |(if b=0 then (1:ℚ) else 0)-point p i| ≤ 1 := by
      apply abs_le.mpr
      split_ifs <;> constructor <;> dsimp only [i] <;> linarith only [hi.1,hi.2]
    exact (mul_le_mul_of_nonneg_left herr (hβ0 i)).trans (by simpa only [mul_one] using hβM i)
  · simpa only [endpoint,dite_eq_right h,sub_self,abs_zero] using hM

end MetricKMedian.RationalLastFraction
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseProduct
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.SparseIntegerLaw
open Finset
variable {α β γ : Type}

theorem prod_property (μ : SparseIntegerLaw α) (ν : SparseIntegerLaw β)
    (f : α → β → γ) (P : γ → Prop)
    (hP : ∀ a : Fin μ.length, ∀ b : Fin ν.length, P (f μ.states[a.val] ν.states[b.val])) :
    ∀ a : Fin (μ.prod ν f).length, P (μ.prod ν f).states[a.val] := by
  intro a
  change P ((Vector.ofFn (fun i => f μ.states[((finProdFinEquiv (m := μ.length) (n := ν.length)).symm i).1.val]
    ν.states[((finProdFinEquiv (m := μ.length) (n := ν.length)).symm i).2.val]))[a.val])
  simp only [Vector.getElem_ofFn]
  exact hP _ _

end MetricKMedian.SparseIntegerLaw
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseAffineMoments
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.SparseIntegerLaw
variable {α : Type}

theorem moment_sub (μ : SparseIntegerLaw α) (f g : α → ℚ) :
    μ.moment (fun a => f a-g a)=μ.moment f-μ.moment g := by
  simp only [moment,mul_sub,Finset.sum_sub_distrib]

end MetricKMedian.SparseIntegerLaw
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseNonnegativeSupport
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.SparseIntegerLaw
open Finset
variable {α : Type}

theorem zero_nonnegative (μ : SparseIntegerLaw α) (f : α → ℚ)
    (hf : ∀ i : Fin μ.length, 0 ≤ f μ.states[i.val])
    (hz : μ.moment f=0) (a : Fin μ.length)
    (ha : 0 < μ.law.rational.weight a) : f μ.states[a.val]=0 := by
  have hh := single_le_sum (s := univ)
    (f := fun i : Fin μ.length => μ.law.rational.weight i*f μ.states[i.val])
    (fun i _ => mul_nonneg (μ.law.rational.nonneg i) (hf i)) (mem_univ a)
  change _ ≤ μ.moment f at hh
  rw [hz] at hh
  have hn := hf a
  nlinarith only [hh,ha,hn]

end MetricKMedian.SparseIntegerLaw
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_RationalSupplierScan
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
open Finset SupplierStars

namespace FixedParameters
theorem grid {τ : ℝ} (qR : FixedBatch.RationalParameters τ) : qR.g*(qR.Δ:ℚ)=1 := by exact_mod_cast qR.unit
end FixedParameters

end MetricKMedian.Preparation.RationalSuppliers
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)
structure Branch where
  original : Instance
  facilities : Finset (Fin original.n)
namespace Branch
def allowed (B : Branch) : Prop := B.original.k ≤ B.facilities.card
instance instDecidablePredAllowed : DecidablePred allowed := fun B => inferInstanceAs (Decidable (B.original.k≤B.facilities.card))
def restricted (B : Branch) (h : B.allowed) : Instance := B.original.restrictFacilities B.facilities h
end Branch
end MetricKMedian.Reduction.Program
end

end OAI
end