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

import Mathlib
import Definitions.Def_OAIQ037K036
import Definitions.Def_OAIQ037K000
import Definitions.Def_OAIQ037K002
import Definitions.Def_OAIQ037K004
import Definitions.Def_OAIQ037K006
import Definitions.Def_OAIQ037K008
import Definitions.Def_OAIQ037K010
import Definitions.Def_OAIQ037K013
import Definitions.Def_OAIQ037K014
import Definitions.Def_OAIQ037K016
import Definitions.Def_OAIQ037K017
import Definitions.Def_OAIQ037K019
import Definitions.Def_OAIQ037K021
import Definitions.Def_OAIQ037K027
import Definitions.Def_OAIQ037K028
import Definitions.Def_OAIQ037K029
import Definitions.Def_OAIQ037K030
import Definitions.Def_OAIQ037K038
import Definitions.Def_OAIQ037K039
import Definitions.Def_OAIQ037K040
import Definitions.Def_OAIQ037K041

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_LPBinaryInput
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.LPBinary
open Binary Polynomial Finset

namespace Input

 theorem bounds (I : Input) : I.n ≤ I.encode.length ∧ I.m ≤ I.encode.length ∧ I.k ≤ I.encode.length ∧
    ∀ j i, HasHeight (I.distance j i) I.encode.length := by
  let L := I.encode.length
  have henc : L=2*(ers I.rows).length+1+I.k.bits.length := by
    simp only [L,raw,encodePair_length]
  have hm := EncodedList.length_le er I.rows
  change I.rows.length ≤ (ers I.rows).length at hm
  simp only [rows,List.length_ofFn] at hm
  change I.m ≤ (ers I.rows).length at hm
  have hrow (j : Fin I.m) : (er (List.ofFn (I.distance j))).length  ≤  (ers I.rows).length :=
    EncodedList.member_length er I.rows _ (List.mem_ofFn.mpr ⟨j,rfl⟩)
  have hn := EncodedList.length_le Ratio.encode (List.ofFn (I.distance ⟨0,I.mpos⟩))
  change (List.ofFn (I.distance ⟨0,I.mpos⟩)).length ≤ (er (List.ofFn (I.distance ⟨0,I.mpos⟩))).length at hn
  simp only [List.length_ofFn] at hn
  have hnL : I.n ≤ L := by have hh := hrow ⟨0,I.mpos⟩; omega
  refine ⟨hnL,by omega,I.kle.trans hnL,?_⟩
  intro j i
  have hh := EncodedList.member_length Ratio.encode (List.ofFn (I.distance j)) _ (List.mem_ofFn.mpr ⟨i,rfl⟩)
  change (Ratio.encode (I.distance j i)).length ≤ (er (List.ofFn (I.distance j))).length at hh
  have hrow := hrow j
  exact (Ratio.height_length _).mono (by omega)

end Input

 theorem penalty_bound (I : Input) (r : ℕ) : TruncatedLP.penalty r I.k  ≤  4*r*(I.encode.length+1) := by
  unfold TruncatedLP.penalty
  gcongr
  exact I.bounds.2.2.1
 theorem grad_bound (I : Input) (r : ℕ) :
    TruncatedLP.gradSize (n:=I.n) (m:=I.m) (TruncatedLP.penalty r I.k)  ≤  gradientBound r I.encode.length := by
  unfold TruncatedLP.gradSize gradientBound
  gcongr
  · exact I.bounds.1
  · exact I.bounds.2.1
  · exact penalty_bound I r
 theorem steps_bound (I : Input) (r : ℕ) :
    TruncatedLP.steps (n:=I.n) (m:=I.m) r I.k (TruncatedLP.penalty r I.k)  ≤  stepsBound r I.encode.length := by
  unfold TruncatedLP.steps stepsBound
  gcongr
  · exact grad_bound I r
  · exact I.bounds.2.2.1

 theorem iterate_height (I : Input) (r : ℕ) (hr : 0 < r) (t : ℕ)
    (ht : t ≤ TruncatedLP.steps (n:=I.n) (m:=I.m) r I.k (TruncatedLP.penalty r I.k)) (i : Fin I.n) :
    HasHeight (ProjectedSubgradient.point (I.vector r t) i) (heightBound r I.encode.length) := by
  let L := I.encode.length
  let q := fun p : Fin I.m × Fin I.n => I.distance p.1 p.2
  let R := RationalScaling.denominator q
  have hR : 0 < R := RationalScaling.denominator_pos q
  have hd : ∀ j i, RationalGrid.At R (I.distance j i) := by
    intro j i
    refine ⟨RationalScaling.numerator q (j,i),?_⟩
    rw [RationalScaling.numerator_cast,mul_div_cancel_right₀]
    exact_mod_cast hR.ne'
  have hRbound : R ≤ (2:ℤ)^(L*(L*L)) := by
    have hh := RationalScaling.denominator_bound q L (fun p => (I.bounds.2.2.2 p.1 p.2).2)
    simp only [Fintype.card_prod,Fintype.card_fin] at hh
    apply hh.trans
    apply pow_le_pow_right₀ (by norm_num)
    gcongr
    · exact I.bounds.2.1
    · exact I.bounds.1
  have hbn : TruncatedLP.rateDen (n:=I.n) (m:=I.m) r (TruncatedLP.penalty r I.k)*(I.n:ℤ) ≤ baseBound r L := by
    unfold TruncatedLP.rateDen
    have hg := grad_bound I r
    have hn := I.bounds.1
    dsimp only [baseBound]
    exact_mod_cast Nat.mul_le_mul (Nat.mul_le_mul_left (2*r) hg) hn
  have hnat : (baseBound r L:ℤ) ≤ (2:ℤ)^(baseBound r L) := by exact_mod_cast (Nat.lt_two_pow_self (n:=baseBound r L)).le
  have hbase : TruncatedLP.rateDen (n:=I.n) (m:=I.m) r (TruncatedLP.penalty r I.k)*R*(I.n:ℤ) ≤ (2:ℤ)^(exponentBound r L) := by
    calc
      _ = (TruncatedLP.rateDen (n:=I.n) (m:=I.m) r (TruncatedLP.penalty r I.k)*(I.n:ℤ))*R := by ring
      _  ≤  (2:ℤ)^(baseBound r L)*(2:ℤ)^(L*(L*L)) := mul_le_mul (hbn.trans hnat) hRbound hR.le (by positivity)
      _ = (2:ℤ)^(baseBound r L+L*(L*L)) := (pow_add ..).symm
      _  ≤  _ := pow_le_pow_right₀ (by norm_num) (by unfold exponentBound; omega)
  have hk : (I.k:ℤ) ≤ (2:ℤ)^(exponentBound r L) := by
    have hkL : (I.k:ℤ) ≤ L := by exact_mod_cast I.bounds.2.2.1
    have hL : (L:ℤ) ≤ (2:ℤ)^L := by exact_mod_cast (Nat.lt_two_pow_self (n:=L)).le
    exact (hkL.trans hL).trans (pow_le_pow_right₀ (by norm_num) (by unfold exponentBound; omega))
  have hh := TruncatedLP.trajectory_height I.distance r I.k (TruncatedLP.penalty r I.k) hr I.kpos
    (TruncatedLP.penalty_pos r I.k hr) R hR hd (exponentBound r L) hbase hk t i
  apply hh.mono
  unfold heightBound
  exact Nat.mul_le_mul_left _ (Nat.succ_le_succ (ht.trans (steps_bound I r)))

 theorem iterate_size (I : Input) (r : ℕ) (hr : 0 < r) (t : ℕ)
    (ht : t ≤ TruncatedLP.steps (n:=I.n) (m:=I.m) r I.k (TruncatedLP.penalty r I.k)) :
    (er (I.iterate r t)).length  ≤  I.encode.length*(2*(3*heightBound r I.encode.length+10)+1) := by
  have hh := EncodedList.length_bound Ratio.encode (I.iterate r t) (3*heightBound r I.encode.length+10) (by
    intro q hq
    obtain ⟨i,rfl⟩ := List.mem_ofFn.mp hq
    exact Ratio.length_height (iterate_height I r hr t ht i))
  simp only [Input.iterate,List.length_ofFn] at hh
  exact hh.trans (Nat.mul_le_mul_right _ I.bounds.1)

end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_LPBinaryStart
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.LPBinary
open Binary Binary.PolyProgram Function

namespace Program
noncomputable def rawPenaltyProgram (r : ℕ) : PolyProgram ei Nat.bits (rawPenalty r) := by
  let k := snd ers Nat.bits
  let p := (k.fanout (constant ei Nat.bits 1)).comp natAdd
  exact ((constant ei Nat.bits (4*r)).fanout p |>.comp natMul).congr _ (fun _ => rfl)
end Program

end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseRealExpectation
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}

noncomputable def expectation (μ : SparseIntegerLaw α) (f : α → ℝ) : ℝ :=
  μ.realIndex.expect (fun i => f μ.states[i.val])

end MetricKMedian.SparseIntegerLaw

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_affine_pair (μ : SparseIntegerLaw α) (f g : α → ℚ) (a b : ℚ) :
    μ.moment (fun x => (a+f x)*(b+g x))=
      a*b+a*μ.moment g+b*μ.moment f+μ.moment (fun x => f x*g x) := by
  calc
    _ = μ.moment (fun x => a*b+a*g x+b*f x+f x*g x) :=
      μ.moment_congr _ _ (fun _ => by ring)
    _ = _ := by rw [moment_add,moment_add,moment_add,moment_const,moment_mul,moment_mul]

theorem moment_affine_pair_le (μ : SparseIntegerLaw α) (f g : α → ℚ) (a b x y : ℚ)
    (hf : μ.moment f=x) (hg : μ.moment g=y)
    (hpair : μ.moment (fun t => f t*g t) ≤ x*y) :
    μ.moment (fun t => (a+f t)*(b+g t)) ≤ (a+x)*(b+y) := by
  rw [moment_affine_pair,hf,hg]
  nlinarith only [hpair]

end MetricKMedian.SparseIntegerLaw
end
end

end OAI
end

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

noncomputable def CoupledLaw.reindexStars (e : E ≃ E')
    {D : E' → Finset T} {a w : E' → ℝ} {P : T → Finset I}
    {y : I → ℝ} {p c : T → ℝ} {g γ B : ℝ} {Δ : ℕ}
    (L : CoupledLaw (D ∘ e) (a ∘ e) (w ∘ e) P y p c g γ B Δ) :
    CoupledLaw D a w P y p c g γ B Δ where
  Ω := L.Ω
  ν := L.ν
  κ := L.κ
  O := fun z i => L.O z (e.symm i)
  N := fun z i => L.N z (e.symm i)
  R := fun z t i => L.R z t (e.symm i)
  K := L.K
  C := L.C
  open_cap := by simpa only [Function.comp_apply, e.apply_symm_apply] using
    fun z hz i => L.open_cap z hz (e.symm i)
  open_zero := by simpa only [Function.comp_apply, e.apply_symm_apply] using
    fun z hz i => L.open_zero z hz (e.symm i)
  nominal_nonneg := fun z hz i => L.nominal_nonneg z hz (e.symm i)
  nominal_cap := fun z hz i => L.nominal_cap z hz (e.symm i)
  nominal_mean := by simpa only [Function.comp_apply, e.apply_symm_apply] using
    fun i => L.nominal_mean (e.symm i)
  nominal_variance := by simpa only [Function.comp_apply, e.apply_symm_apply] using
    fun i => L.nominal_variance (e.symm i)
  nominal_pair := by
    intro i j hij
    simpa only [Function.comp_apply, e.apply_symm_apply] using
      L.nominal_pair (e.symm i) (e.symm j) (e.symm.injective.ne hij)
  request_cap := fun z hz t i => L.request_cap z hz t (e.symm i)
  request_target := by simpa only [Function.comp_apply, e.apply_symm_apply] using
    fun z t i => L.request_target z t (e.symm i)
  request_mean := by simpa only [Function.comp_apply, e.apply_symm_apply] using
    fun t i => L.request_mean t (e.symm i)
  exact_total := by
    intro z t
    rw [e.symm.sum_comp]
    exact L.exact_total z t
  half := L.half
  total_cap := L.total_cap
  total_deviation := L.total_deviation
  pieces := L.pieces
  piece_mean := L.piece_mean
  piece_pair := L.piece_pair
  piece_variance := L.piece_variance
  budget := by
    have he : ∀ z, (∑ i, a i * (g * (L.O z (e.symm i) : ℝ))) =
        ∑ j, a (e j) * (g * (L.O z j : ℝ)) := by
      intro z
      rw [← e.sum_comp]
      simp only [e.symm_apply_apply]
    simpa only [he, Function.comp_apply] using L.budget

end MetricKMedian.Preparation
end

end OAI
end

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

noncomputable def CoupledLaw.castWeights {D : E → Finset T} {a a' w w' : E → ℝ}
    {P : T → Finset I} {y : I → ℝ} {p c : T → ℝ} {g γ B : ℝ} {Δ : ℕ}
    (L : CoupledLaw D a w P y p c g γ B Δ) (ha : a=a') (hw : w=w') :
    CoupledLaw D a' w' P y p c g γ B Δ where
  Ω := L.Ω
  ν := L.ν
  κ := L.κ
  O := L.O
  N := L.N
  R := L.R
  K := L.K
  C := L.C
  open_cap := by rw [← hw]; exact L.open_cap
  open_zero := by rw [← hw]; exact L.open_zero
  nominal_nonneg := L.nominal_nonneg
  nominal_cap := L.nominal_cap
  nominal_mean := by rw [← hw]; exact L.nominal_mean
  nominal_variance := by rw [← hw]; exact L.nominal_variance
  nominal_pair := by rw [← hw]; exact L.nominal_pair
  request_cap := L.request_cap
  request_target := L.request_target
  request_mean := by rw [← hw]; exact L.request_mean
  exact_total := L.exact_total
  half := L.half
  total_cap := L.total_cap
  total_deviation := L.total_deviation
  pieces := L.pieces
  piece_mean := L.piece_mean
  piece_pair := L.piece_pair
  piece_variance := L.piece_variance
  budget := by rw [← ha]; exact L.budget

end MetricKMedian.Preparation
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_FractionalInputProgram
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.Program
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
open MetricKMedian.MaskProgram

def Input.unit (z : Input) : RationalUnitInput.Program.Input :=
  ⟨count z.a z.k z.ha z.hj z.dc,z.j,unitInput z.a z.k z.ha z.hj z.dc z.dd z.df z.hdc z.hdd z.hds⟩
end MetricKMedian.Preparation.FractionalRefinement.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_LastFractionProgram
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.WeightedRound
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly SparseIntegerLaw.BinarySparse

def State.last (x : RoundingProgram.State false) : RoundingProgram.State false :=
  ⟨x.n,x.β,x.positive,x.μ.branch RationalLastFraction.probability RationalLastFraction.probability_unit RationalLastFraction.endpoint⟩
end MetricKMedian.RoundingProgram.WeightedRound
end

end OAI
end