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

import Mathlib
import Definitions.Def_MetricKMedian
import Definitions.Def_OAIQ037K030
import Definitions.Def_OAIQ037K000
import Definitions.Def_OAIQ037K001
import Definitions.Def_OAIQ037K003
import Definitions.Def_OAIQ037K006
import Definitions.Def_OAIQ037K008
import Definitions.Def_OAIQ037K009
import Definitions.Def_OAIQ037K010
import Definitions.Def_OAIQ037K018
import Definitions.Def_OAIQ037K019
import Definitions.Def_OAIQ037K021
import Definitions.Def_OAIQ037K022
import Definitions.Def_OAIQ037K023
import Definitions.Def_OAIQ037K034
import Definitions.Def_OAIQ037K035

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_CoupledGeometry
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.Preparation
open Finset SupplierStars
attribute [instance] CoupledLaw.finite
variable {I T : Type} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T]

def physicalCount {P A : T → Finset I} {y : I → ℝ} {p c : T → ℝ} {g γ B : ℝ} {Δ : ℕ}
    (L : CoupledLaw (targets A) flag (weight y P A c γ) P y p c g γ B Δ)
    (z : L.Ω × (T → Finset I)) : Physical I T → ℕ :=
  Sum.elim (fun i => L.O z.1 (.inl i)) (L.C z.1 z.2)

noncomputable def physicalOpen {P A : T → Finset I} {y : I → ℝ} {p c : T → ℝ} {g γ B : ℝ} {Δ : ℕ}
    (L : CoupledLaw (targets A) flag (weight y P A c γ) P y p c g γ B Δ)
    (z : L.Ω × (T → Finset I)) (a : Physical I T) : ℝ := g*(physicalCount L z a:ℝ)

end MetricKMedian.Preparation
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_PhysicalOldMass
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.Preparation
open Finset SupplierStars
attribute [instance] CoupledLaw.finite
variable {I T : Type} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T]

noncomputable def oldAssignment {P A : T → Finset I} {y : I → ℝ} {p c : T → ℝ} {g γ B : ℝ} {Δ : ℕ}
    (L : CoupledLaw (targets A) flag (weight y P A c γ) P y p c g γ B Δ)
    (F : Finset I) (z : L.Ω × (T → Finset I)) : Physical I T → ℝ :=
  Sum.elim (fun i => if i ∈ F ∩ outside P then L.N z.1 (.inl i) else 0)
    (fun ti => if ti.2 ∈ F then g*(L.C z.1 z.2 ti:ℝ) else 0)

end MetricKMedian.Preparation
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_RationalTaperCandidates
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.Taper
open Finset
variable {I : Type*} [Fintype I]

theorem maximal_root_in_candidates (g P : ℚ) (d : I → ℚ)
    (hg : 0 < (g:ℝ)) (hP : 0 < (P:ℝ)) (hP1 : (P:ℝ) ≤ 1/2)
    (hd : ∀ i, 0 ≤ d i) (hcol : colocatedMass g (fun i => (d i:ℝ)) < 1)
    (r : ℝ) (hr : 0 < r) (hroot : mass g P (fun i => (d i:ℝ)) r=1)
    (hmax : ∀ u, 1 ≤ mass g P (fun i => (d i:ℝ)) u → u ≤ r) :
    ∃ q ∈ candidates g P d, (q:ℝ)=r := by
  classical
  by_cases heq : ∃ q ∈ breakpoints P d, (q:ℝ)=r
  · obtain ⟨q,hq,he⟩ := heq
    exact ⟨q,mem_union_left _ hq,he⟩
  have hnot : ∀ q ∈ breakpoints P d, (q:ℝ) ≠ r := by simpa only [not_exists,not_and] using heq
  have hU : r < (upper d:ℝ) := by
    by_contra hn
    have hh := mass_antitone (d := fun i => (d i:ℝ)) hg.le hP (fun i => by exact_mod_cast hd i) (le_of_not_gt hn)
    rw [hroot,mass_upper g P d hP (by linarith) hd] at hh
    linarith
  obtain ⟨a,ha,b,hb,har,hrb,hgap⟩ := rational_bracket (breakpoints P d) r 0 (upper d)
    (mem_insert_self _ _) (mem_insert_of_mem (mem_insert_self _ _)) (by simpa only [Rat.cast_zero] using hr) hU hnot
  have hab : a < b := by exact_mod_cast har.trans hrb
  let t : ℚ := (a+b)/2
  have ht : a < t ∧ t < b := by dsimp only [t]; constructor <;> linarith
  have hPq : P < 1 := by exact_mod_cast (show (P:ℝ) < 1 by linarith)
  have hcuts := cuts_in_interval hd hPq a b t hgap ht r ⟨har,hrb⟩
  have haff := mass_affine (g := g) hP hcuts.1 hcuts.2
  rw [hroot] at haff
  have hB : B P d t ≠ 0 := by
    intro hz
    let u := (r+(b:ℝ))/2
    have hur : r < u := by dsimp only [u]; linarith
    have hu : (a:ℝ) < u ∧ u < (b:ℝ) := by dsimp only [u]; constructor <;> linarith
    have hcu := cuts_in_interval hd hPq a b t hgap ht u hu
    have hfu := mass_affine (g := g) hP hcu.1 hcu.2
    rw [hz,Rat.cast_zero,mul_zero,sub_zero] at hfu haff
    have hmass : mass g P (fun i => (d i:ℝ)) u=1 := hfu.trans haff.symm
    exact not_le_of_gt hur (hmax u hmass.ge)
  refine ⟨(A P d t-1/g)/B P d t,mem_union_right _ (mem_image.mpr ⟨(a,b),mem_product.mpr ⟨ha,hb⟩,rfl⟩),?_⟩
  have hBR : (B P d t:ℝ) ≠ 0 := by exact_mod_cast hB
  have hgR := hg.ne'
  push_cast
  apply (div_eq_iff hBR).mpr
  have hdiv : (A P d t:ℝ)-r*(B P d t:ℝ)=1/(g:ℝ) := (eq_div_iff hgR).mpr (by nlinarith [haff])
  linarith

end MetricKMedian.Taper
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_RationalTaper
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.Taper
open Finset
variable {I : Type*} [Fintype I]

theorem inverseRadius_spec (g P : ℚ) (d : I → ℚ)
    (hg : 0 < (g:ℝ)) (hP : 0 < (P:ℝ)) (hP1 : (P:ℝ) ≤ 1/2)
    (hd : ∀ i, 0 ≤ d i) (htotal : 1 ≤ ∑ _i : I, (g:ℝ))
    (hcol : colocatedMass g (fun i => (d i:ℝ)) < 1) :
    0 < inverseRadius g P d ∧ rationalMass g P d (inverseRadius g P d)=1 ∧
      ∀ u : ℝ, 1 ≤ mass g P (fun i => (d i:ℝ)) u → u ≤ (inverseRadius g P d:ℝ) := by
  obtain ⟨r,hr,he,hmax⟩ := exists_minimal_radius (fun i => (d i:ℝ)) hg hP hP1
    (fun i => by exact_mod_cast hd i) htotal hcol
  obtain ⟨q,hq,hqr⟩ := maximal_root_in_candidates g P d hg hP hP1 hd hcol r hr he hmax
  have hqpos : 0 < q := by exact_mod_cast (hqr ▸ hr)
  have hqe : rationalMass g P d q=1 := by
    have hh : (rationalMass g P d q:ℝ)=1 := by rw [cast_rationalMass,hqr,he]
    exact_mod_cast hh
  have hmem : q ∈ rootCandidates g P d := mem_filter.mpr ⟨hq,hqpos,hqe⟩
  have hne : (rootCandidates g P d).Nonempty := ⟨q,hmem⟩
  have hm : inverseRadius g P d ∈ rootCandidates g P d := by
    unfold inverseRadius
    rw [dite_eq_left hne]
    exact max'_mem _ hne
  obtain ⟨_,hpos,hroot⟩ := mem_filter.mp hm
  refine ⟨hpos,hroot,?_⟩
  have hle : q ≤ inverseRadius g P d := by
    unfold inverseRadius
    rw [dite_eq_left hne]
    exact le_max' _ _ hmem
  have hleR : r ≤ (inverseRadius g P d:ℝ) := by rw [← hqr]; exact_mod_cast hle
  intro u hu
  exact (hmax u hu).trans hleR

theorem positive_data (g P : ℚ) (d : I → ℚ) (Δ : ℕ)
    (hg : 0 < (g:ℝ)) (hunit : (g:ℝ)*(Δ:ℝ)=1)
    (hP : 0 < (P:ℝ)) (hP1 : (P:ℝ) ≤ 1/2)
    (hd : ∀ i, 0 ≤ d i) (htotal : 1 ≤ ∑ _i : I, (g:ℝ))
    (hcol : colocatedMass g (fun i => (d i:ℝ)) < 1) :
    let r := inverseRadius g P d
    let q := fun i => rationalMarginal P (d i) r
    0 < 1/r ∧ (∀ i, 0 ≤ q i) ∧ (∀ i, q i ≤ 1) ∧
      (∑ i, g*q i=1) ∧ (∑ i, q i=Δ) ∧
      (∀ i, d i=0 → q i=1) ∧
      (∀ i, q i < 1 → (1/r)*(1-P*q i) ≤ d i) ∧
      (∀ i, 0 < q i → d i ≤ (1/r)*(1-P*q i)) ∧
      (∀ R : ℝ, 0 < R → 1 ≤ mass g P (fun i => (d i:ℝ)) (1/R) → (1/r:ℚ) ≤ R) := by
  dsimp only
  let r := inverseRadius g P d
  let q := fun i => rationalMarginal P (d i) r
  obtain ⟨hr,he,hmax⟩ := inverseRadius_spec g P d hg hP hP1 hd htotal hcol
  have hrR : (0:ℝ) < r := by exact_mod_cast hr
  have hq : ∀ i, (q i:ℝ)=marginal P (d i) r := fun i => cast_rationalMarginal P (d i) r
  have hsum : (∑ i, q i)=(Δ:ℚ) := by
    apply mul_left_cancel₀ (show g ≠ 0 by exact_mod_cast hg.ne')
    rw [mul_sum]
    change rationalMass g P d r=g*(Δ:ℚ)
    rw [he]
    exact_mod_cast hunit.symm
  refine ⟨one_div_pos.mpr hr,?_,?_,he,hsum,?_,?_,?_,?_⟩
  · intro i
    have hh := marginal_nonneg (d := (d i:ℝ)) (r := (r:ℝ)) hP
    rw [← hq] at hh
    exact_mod_cast hh
  · intro i
    have hh := marginal_le_one (P:ℝ) (d i:ℝ) (r:ℝ)
    rw [← hq] at hh
    exact_mod_cast hh
  · intro i hi
    have hh : (q i:ℝ)=1 := by
      rw [hq,hi,Rat.cast_zero]
      exact marginal_at_zero_distance hP (by linarith)
    exact_mod_cast hh
  · intro i hi
    have hiR : marginal P (d i) r < 1 := by rw [← hq]; exact_mod_cast hi
    have hh := lower_comparison hP hiR
    have hres : (1/(r:ℝ))*(1-(P:ℝ)*(q i:ℝ)) ≤ (d i:ℝ) := by
      rw [one_div_mul_eq_div]
      apply (div_le_iff₀ hrR).mpr
      rw [hq]
      nlinarith only [hh]
    exact_mod_cast hres
  · intro i hi
    have hiR : 0 < marginal P (d i) r := by rw [← hq]; exact_mod_cast hi
    have hh := upper_comparison hP hiR
    have hres : (d i:ℝ) ≤ (1/(r:ℝ))*(1-(P:ℝ)*(q i:ℝ)) := by
      rw [one_div_mul_eq_div]
      apply (le_div_iff₀ hrR).mpr
      rw [hq]
      nlinarith only [hh]
    exact_mod_cast hres
  · intro R hR hm
    have hh := (div_le_iff₀ hR).mp (hmax (1/R) hm)
    change ((1/r:ℚ):ℝ) ≤ R
    push_cast
    exact (div_le_iff₀ hrR).mpr (by nlinarith only [hh])

end MetricKMedian.Taper
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_RationalTaperData
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.Taper
open Finset
variable {I : Type*} [Fintype I] [LinearOrder I]

def rationalRadius (g P : ℚ) (d : I → ℚ) : ℚ :=
  if 1 ≤ rationalColocatedMass g d then 0 else 1/inverseRadius g P d

theorem rational_data (g P : ℚ) (d : I → ℚ) (own : Finset I) (Δ : ℕ)
    (hg : 0 < (g:ℝ)) (hunit : (g:ℝ)*(Δ:ℝ)=1)
    (hP : 0 < (P:ℝ)) (hP1 : (P:ℝ) ≤ 1/2)
    (hd : ∀ i, 0 ≤ d i) (htotal : 1 ≤ ∑ _i : I, (g:ℝ))
    (hown : ∀ i ∈ own, d i=0) (howncard : own.card ≤ Δ) :
    let N := rationalRadius g P d
    let q := sourceMarginals g P d own Δ
    0 ≤ N ∧ (∀ i, 0 ≤ q i) ∧ (∀ i, q i ≤ 1) ∧
      (∑ i, g*q i=1) ∧ (∑ i, q i=Δ) ∧ (∀ i ∈ own, q i=1) ∧
      (∀ i, q i < 1 → N*(1-P*q i) ≤ d i) ∧
      (∀ i, 0 < q i → d i ≤ N*(1-P*q i)) ∧
      (∀ R : ℝ, 0 < R → 1 ≤ mass g P (fun i => (d i:ℝ)) (1/R) → (N:ℝ) ≤ R) := by
  by_cases hc : 1 ≤ rationalColocatedMass g d
  · have hcR : 1 ≤ colocatedMass g (fun i => (d i:ℝ)) := by
      rw [← cast_rationalColocatedMass]
      exact_mod_cast hc
    obtain ⟨hq0,hq1,hs,hn,ho,hz⟩ := zero_data g d own Δ hg hunit hcR hown howncard
    dsimp only
    simp only [rationalRadius,sourceMarginals,ite_eq_left hc]
    refine ⟨le_refl _,hq0,hq1,hs,hn,ho,?_,?_,?_⟩
    · intro i _; simpa only [zero_mul] using hd i
    · intro i hi; simp only [hz i hi,zero_mul,le_refl]
    · intro R hR _; simpa only [Rat.cast_zero] using hR.le
  · have hcR : colocatedMass g (fun i => (d i:ℝ)) < 1 := by
      rw [← cast_rationalColocatedMass]
      exact_mod_cast (lt_of_not_ge hc)
    obtain ⟨hN,hq0,hq1,hs,hn,ho,hl,hu,hr⟩ := positive_data g P d Δ hg hunit hP hP1 hd htotal hcR
    dsimp only
    simp only [rationalRadius,sourceMarginals,ite_eq_right hc]
    exact ⟨hN.le,hq0,hq1,hs,hn,fun i hi => ho i (hown i hi),hl,hu,hr⟩

end MetricKMedian.Taper
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 integral_of_small_fractional (q : Vector ℚ n)
    (hq : ∀ i, 0 ≤ point q i ∧ point q i ≤ 1) (K : ℕ)
    (hs : (∑ i, point q i)=(K:ℚ)) (hf : (fractional q).card ≤ 1) :
    ∀ i, point q i=0 ∨ point q i=1 := by
  have has : MarginalRounding.fractional (realPoint q)=∅ := by
    by_contra h
    obtain ⟨i,hi⟩ := nonempty_iff_ne_empty.mpr h
    have h0 : ∀ i, 0 ≤ realPoint q i := fun i => by
      dsimp only [realPoint]; exact_mod_cast (hq i).1
    have h1 : ∀ i, realPoint q i ≤ 1 := fun i => by
      dsimp only [realPoint]; exact_mod_cast (hq i).2
    have hsum : (∑ i, realPoint q i)=(K:ℝ) := by
      dsimp only [realPoint]; exact_mod_cast hs
    obtain ⟨j,hj,hji⟩ := MarginalRounding.second_fractional h0 h1 hsum hi
    rw [real_fractional] at hi hj
    exact hji (card_le_one.mp hf j hj i hi)
  intro i
  apply RationalLastFraction.nonfractional q hq i
  rw [← real_fractional,has]
  exact notMem_empty i

end MetricKMedian.SparseCardinalRounding
end
end

end OAI
end

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 raw_counts (D : Fin m → Finset (Fin n)) (c q : Fin m → ℚ) (z : State n m) :
    SparseSignedPreparation.raw D c (base q) z=
      (∑ e,c e*(outsideCount q z e:ℚ))-(∑ j,∑ e,(activationCount D q z e j:ℚ)) := by
  rw [sum_comm]
  simp only [SparseSignedPreparation.raw,sum_sub_distrib,← Nat.cast_sum,activation_sum,
    Nat.cast_add,Nat.cast_mul,outsideCount_cast]

theorem raw_identity (D : Fin m → Finset (Fin n)) (c q : Fin m → ℚ) (Δ : ℕ)
    (z : State n m) :
    opening D c q Δ z=(n:ℚ)*(Δ:ℚ)+SparseSignedPreparation.raw D c (base q) z+
      ∑ j,discarded D q Δ z j := by
  have ht : ∀ j,(total D q Δ z j:ℚ)=(Δ:ℚ)-
      (min (∑ e,activationCount D q z e j) (Δ/2):ℕ) := by
    intro j
    exact Nat.cast_sub ((min_le_right _ _).trans (Nat.div_le_self _ _))
  simp only [opening,ht,raw_counts,discarded,sum_sub_distrib,sum_const,card_univ,Fintype.card_fin,
    nsmul_eq_mul,Nat.cast_sum]
  ring

end MetricKMedian.SparsePrepared
end
end

end OAI
end

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

theorem opening_cast (D : Fin m → Finset (Fin n)) (a q : Fin m → ℚ) (Δ : ℕ)
    (z : State n m) (g : ℝ) :
    g * (opening D a q Δ z : ℝ) =
      (∑ e, (a e : ℝ) * (g * (outsideCount q z e : ℝ))) +
      (∑ j, g * (total D q Δ z j : ℝ)) := by
  simp only [opening, Rat.cast_add, Rat.cast_sum, Rat.cast_mul, Rat.cast_natCast,
    mul_add, mul_sum]
  congr 1
  exact sum_congr rfl (fun _ _ => by ring)

end MetricKMedian.SparsePrepared
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)
def feasible (I : Instance) (S : Finset (Fin I.n)) : Bool := decide (S⊆I.facilities ∧ S.Nonempty ∧ S.card≤I.k)
def selectList (I : Instance) (L : List (Finset (Fin I.n))) : Finset (Fin I.n) :=
  (SparseSelect.best (feasible I) (rationalCost I) L).getD {I.facilities.min' I.facilities_nonempty}
end MetricKMedian.Reduction.Program
end

end OAI
end