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

import Mathlib
import Definitions.Def_OAIQ037K000
import Definitions.Def_OAIQ037K001
import Definitions.Def_OAIQ037K002
import Definitions.Def_OAIQ037K003

section
-- module Solutions.OAIQ037_KM.KMedian_Analysis_FiniteAverages
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.FiniteComparison

noncomputable def L (p m z : ℝ) (b : Bool → ℝ) (s : Bool) (r : ℝ) : ℝ :=
  (C p s - m - b s) * r + (2 / 5) * z
noncomputable def M (p a : ℝ) (s : Bool) (r : ℝ) : ℝ :=
  (1 - r) * a + C p s * p * r

end MetricKMedian.FiniteComparison


end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_BooleanMachine
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.Binary
open Turing StateTransition Function Finset

attribute [instance] Machine.decK Machine.finK Machine.finLabel Machine.finState

namespace Machine

instance allWorkFinite (M : Machine) (k : M.tm.K) : Fintype (M.tm.Γ k) :=
  inferInstanceAs (Fintype Bool)

end Machine

end MetricKMedian.Binary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_BooleanPolynomial
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.Binary
open Turing Polynomial

namespace PolyProgram
variable {α β γ : Type} {ea : α → List Bool} {eb : β → List Bool} {ec : γ → List Bool}
variable {f : α → β} {g : β → γ}

def stock (P : PolyProgram ea eb f) : TM2ComputableInPolyTime ea eb f where
  tm := P.machine.tm
  inputAlphabet := Equiv.refl Bool
  outputAlphabet := Equiv.refl Bool
  time := P.time
  outputsFun a := by
    have h := P.outputs a
    dsimp only [Machine.tm,Equiv.refl] at h ⊢
    simpa only [List.map_id] using h

end PolyProgram
end MetricKMedian.Binary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_BooleanFinite
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.Binary
open Function Finset

namespace PolyProgram

noncomputable def boolOr : PolyProgram (encodePair encodeBool encodeBool) encodeBool (fun x => x.1 || x.2) :=
  boolFunction _ _ _ (encodePair_injective encodeBool_injective encodeBool_injective)

end PolyProgram
end MetricKMedian.Binary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_BooleanRecode
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.Binary.PolyProgram
variable {α β α' β' : Type} {ea : α → List Bool} {eb : β → List Bool}
variable {ea' : α' → List Bool} {eb' : β' → List Bool} {f : α → β} {f' : α' → β'}

def recode (P : PolyProgram ea eb f) (i : α' → α)
    (hi : ∀ a, ea (i a)=ea' a) (ho : ∀ a, eb (f (i a))=eb' (f' a)) :
    PolyProgram ea' eb' f' where
  machine := P.machine
  time := P.time
  outputs a := by
    have h := P.outputs (i a)
    rwa [hi,ho] at h

end MetricKMedian.Binary.PolyProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_BinaryListExtras
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.Binary
open Function Polynomial
namespace WordTransducer

def listBits : Transducer where
  Q := Unit
  initial := ()
  next _ b := ((),[true,b,false])
  finish _ := []
end WordTransducer
end MetricKMedian.Binary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_BinarySubtraction
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.Binary
open Function Polynomial

namespace Word
 theorem fullSubtract (a b c : Bool) :
    a.toNat+2*(borrowBit a b c).toNat=b.toNat+c.toNat+(sumBit a b c).toNat := by
  cases a <;> cases b <;> cases c <;> decide

end Word

end MetricKMedian.Binary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_BinaryDivision
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.Binary
open Function Polynomial

namespace DivisionLoop
abbrev eqr : ℕ × ℕ → List Bool := encodePair Nat.bits Nat.bits
abbrev edqr : ℕ × (ℕ × ℕ) → List Bool := encodePair Nat.bits eqr
abbrev enc : S → List Bool := encodePair id edqr

 theorem enc_length (s : S) :
    (enc s).length=2*s.1.length+2*s.2.1.bits.length+2*s.2.2.1.bits.length+s.2.2.2.bits.length+3 := by
  simp only [enc,edqr,eqr,encodePair_length,id_eq]
  omega

 theorem total_le_length (s : S) : potential s+s.2.1.bits.length≤(enc s).length := by
  simp only [potential,enc_length]
  omega

 theorem length_le_total (s : S) : (enc s).length≤3*(potential s+s.2.1.bits.length)+3 := by
  simp only [potential,enc_length]
  omega

 theorem run (xs : List Bool) (d q r S : ℕ) (hs : 3*(potential (xs,d,q,r)+d.bits.length)+3≤S) :
    BoundedRun enc body S (xs.length+1) (xs,d,q,r) (result (xs,d,q,r)) := by
  induction xs generalizing q r with
  | nil =>
      exact BoundedRun.stop ((length_le_total ([],d,q,r)).trans hs) rfl
  | cons b xs ih =>
      let s : DivisionLoop.S := (b::xs,d,q,r)
      have hp := next_potential s rfl
      change 3*(potential s+d.bits.length)+3≤S at hs
      have hnext : 3*(potential (next s)+d.bits.length)+3≤S := by omega
      have hr := ih (qstep b d q r) (rstep b d r) hnext
      have hh : result (xs,d,qstep b d q r,rstep b d r)=result s := rfl
      rw [hh] at hr
      exact BoundedRun.step ((length_le_total s).trans hs) rfl hr

end DivisionLoop

end MetricKMedian.Binary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_BinaryInteger
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.Binary
open Function Polynomial

namespace PolyProgram

noncomputable def boolXor : PolyProgram (encodePair encodeBool encodeBool) encodeBool (fun x => xor x.1 x.2) :=
  boolFunction _ _ _ (encodePair_injective encodeBool_injective encodeBool_injective)
end PolyProgram
end MetricKMedian.Binary
end

end OAI
end

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

namespace OAI

namespace MetricKMedian.Compression
open Finset Matrix
variable {R C : Type} [Fintype R] [Fintype C] [DecidableEq C]

theorem gram_det_bound (A : Matrix R C ℤ) (M : ℤ) (hM : 0 ≤ M)
    (hA : ∀ r c, |A r c| ≤ M) :
    |(A.transpose*A).det| ≤ (Nat.factorial (Fintype.card C):ℤ)*
      ((Fintype.card R:ℤ)*M^2)^(Fintype.card C) := by
  simpa only [AbsoluteValue.abs_apply,nsmul_eq_mul] using
    (Matrix.det_le (abv := AbsoluteValue.abs) (gram_entry_bound A M hM hA))

end MetricKMedian.Compression

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_LPListFacts
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 Finset

 theorem foldl_max_eq {α : Type} [LinearOrder α] (xs : List α) (a b : α)
    (ha : a ≤ b) (hb : b∈xs) (hx : ∀ x∈xs, x≤b) : xs.foldl max a=b :=
  le_antisymm (foldl_max_le xs a b ha hx) (member_le_foldl_max xs a b hb)

end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_BinaryAutomatic
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.Binary.Automatic
open PolyProgram Function
instance instCodingUnit : Coding Unit := ⟨fun _ => []⟩
end MetricKMedian.Binary.Automatic
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_BinaryBooleanLists
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.Binary
namespace BooleanLists
def pack : Transducer where
  Q := Unit
  initial := ()
  next := fun _ b => ((),[true,b,false])
  finish := fun _ => []
def unpack : Transducer where
  Q := Phase
  initial := .start
  next := fun q b => match q with
    | .start => (.value,[])
    | .value => (.stop,[b])
    | .stop => (.start,[])
  finish := fun _ => []
end BooleanLists
end MetricKMedian.Binary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_BinaryFloor
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.Binary.Automatic.Poly
 theorem natFloor_eq (q : ℚ) : ⌊q⌋₊=if q<0 then 0 else q.num.natAbs/q.den := by
  by_cases h : q<0
  · simp only [ite_eq_left h,Nat.floor_of_nonpos h.le]
  · rw [ite_eq_right h]
    have hn : 0≤q.num := Rat.num_nonneg.mpr (le_of_not_gt h)
    have he : ((q.num.natAbs:ℕ):ℚ)/(q.den:ℚ)=q := by
      rw [← Int.cast_natCast,Int.natCast_natAbs,abs_of_nonneg hn,Rat.num_div_den]
    calc
      ⌊q⌋₊=⌊((q.num.natAbs:ℕ):ℚ)/(q.den:ℚ)⌋₊ := congrArg Nat.floor he.symm
      _ = _ := Rat.natFloor_natCast_div_natCast _ _
end MetricKMedian.Binary.Automatic.Poly
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_BinaryRepeat
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.Binary
open Function Polynomial
namespace Repeat
variable {α : Type}
abbrev enc (ea : α → List Bool) := encodePair Nat.bits ea

theorem run (ea : α → List Bool) (f : α → α) (N A n : ℕ) (a : α)
    (hn : n≤N) (ha : ∀ i≤n, (ea (f^[i] a)).length≤A) :
    BoundedRun (enc ea) (body f) (2*(N+1)+1+A) (n+1) (n,a) (f^[n] a) := by
  induction n generalizing a with
  | zero =>
      have has : (ea a).length≤A := by simpa using ha 0 (Nat.zero_le _)
      have hsize : (enc ea (0,a)).length ≤ 2*(N+1)+1+A := by
        simp only [enc,encodePair_length,Nat.zero_bits,List.length_nil]; omega
      exact BoundedRun.stop hsize (by simp [body])
  | succ n ih =>
      have hnl : (n+1).bits.length≤N+1 := (NatBinary.length_le_height (Nat.lt_two_pow_self.le)).trans (by omega)
      have has : (ea a).length≤A := by simpa using ha 0 (Nat.zero_le _)
      have hsize : (enc ea (n+1,a)).length ≤ 2*(N+1)+1+A := by
        simp only [enc,encodePair_length]; omega
      have hh := ih (f a) (by omega) (fun i hi => by
        simpa only [Function.iterate_succ_apply] using ha (i+1) (by omega))
      simpa only [Function.iterate_succ_apply] using
        (BoundedRun.step hsize (by simp [body]) hh)
end Repeat

end MetricKMedian.Binary
end

end OAI
end

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

namespace OAI

namespace MetricKMedian.Compression
open Finset

theorem extendVector_at {n : ℕ} (s : Finset (Fin n)) (z : Fin s.card → ℤ)
    (i : Fin s.card) : extendVector s z ((s.orderIsoOfFin rfl) i).val=z i := by
  have hi := ((s.orderIsoOfFin rfl) i).property
  simp only [extendVector,dite_eq_left hi]
  congr 1
  exact (s.orderIsoOfFin rfl).symm_apply_apply i

theorem extendVector_zero {n : ℕ} (s : Finset (Fin n)) (z : Fin s.card → ℤ)
    (i : Fin n) (hi : i ∉ s) : extendVector s z i=0 := dite_eq_right hi

theorem extendVector_sum {n : ℕ} (s : Finset (Fin n)) (z : Fin s.card → ℤ)
    (g : Fin n → ℤ) :
    (∑ i, extendVector s z i*g i)=∑ j, z j*g ((s.orderIsoOfFin rfl) j).val := by
  let e := (s.orderIsoOfFin rfl).toEquiv
  calc
    _ = ∑ i ∈ s, extendVector s z i*g i := by
      symm
      apply sum_subset (subset_univ _)
      intro i _ hi
      rw [extendVector_zero s z i hi,zero_mul]
    _ = ∑ i : s, extendVector s z i.val*g i.val := by
      exact (sum_coe_sort s (fun i => extendVector s z i*g i)).symm
    _ = ∑ j, extendVector s z (e j).val*g (e j).val := (e.sum_comp _).symm
    _ = _ := by
      apply sum_congr rfl
      intro j _
      rw [show extendVector s z (e j).val=z j from extendVector_at s z j]
      rfl

theorem extendVector_bound {n : ℕ} (s : Finset (Fin n)) (z : Fin s.card → ℤ)
    (H : ℤ) (hH : 0 ≤ H) (hz : ∀ j, |z j| ≤ H) (i : Fin n) :
    |extendVector s z i| ≤ H := by
  by_cases hi : i ∈ s
  · simp only [extendVector,dite_eq_left hi]; exact hz _
  · rw [extendVector_zero s z i hi,abs_zero]; exact hH

end MetricKMedian.Compression

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_RoundingListOperations
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.RoundingList
open Binary Binary.Automatic Binary.Automatic.Poly Finset
def indices (p : Row) : List ℕ := List.range p.length
def fractional (p : Row) : List ℕ := (indices p).filter (fun i => frac (p[i]?.getD 0))
def first (p : Row) : ℕ := (indices p).findIdx (fun i => frac (p[i]?.getD 0))
def second (p : Row) : ℕ := (indices p).findIdx (fun i => frac (p[i]?.getD 0) && decide (i≠first p))
def active (p : Row) : Bool := decide (1<(fractional p).length)
def ratio (β p : Row) : ℚ := β[first p]?.getD 0 / β[second p]?.getD 0

def up (p : Row) (i j : ℕ) (r : ℚ) := min (1-p[i]?.getD 0) (p[j]?.getD 0/r)
def down (p : Row) (i j : ℕ) (r : ℚ) := min (p[i]?.getD 0) ((1-p[j]?.getD 0)/r)
def move (p : Row) (i j : ℕ) (r t : ℚ) : Row :=
  (indices p).map (fun k => p[k]?.getD 0+t*((if k=i then 1 else 0)-(if k=j then r else 0)))
def probability (β p : Row) : ℚ :=
  if active p then
    down p (first p) (second p) (ratio β p) /
      (up p (first p) (second p) (ratio β p)+down p (first p) (second p) (ratio β p))
  else 0

def endpoint (β p : Row) (b : Bool) : Row :=
  if active p then move p (first p) (second p) (ratio β p)
    (if b then -down p (first p) (second p) (ratio β p) else up p (first p) (second p) (ratio β p))
  else p

end MetricKMedian.RoundingList
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_LPMinimumSelection
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 Finset

theorem minimum_eq_finset (xs : Row) (U : Finset ℚ) (hU : U.Nonempty)
    (hm : ∀ q, q∈xs ↔ q∈U) : minimum xs=U.min' hU := by
  have hne : xs≠[] := by
    intro he
    obtain ⟨q,hq⟩ := hU
    have hx := (hm q).mpr hq
    rw [he] at hx
    cases hx
  have hd : xs.head?.getD 0∈xs := by
    cases xs with
    | nil => contradiction
    | cons a xs => exact List.mem_cons_self
  apply @foldl_max_eq ℚᵒᵈ _ xs _ _
  · exact min'_le U _ ((hm _).mp hd)
  · exact (hm _).mpr (min'_mem U hU)
  · intro q hq
    exact min'_le U q ((hm q).mp hq)

end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Geometry_GraphListOperations
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.SparseGraph.ListOperation
open Binary Binary.Automatic Binary.Automatic.Poly
abbrev Table := List Row
def setView {n : ℕ} (S : Finset (Fin n)) : Row := List.ofFn (fun h => decide (h∈S))
end MetricKMedian.SparseGraph.ListOperation
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_GreedyPackingProgram
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.Completion.Rational.PackingProgram
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly Polynomial
open SparseGraph.ListOperation (Row Table setView indices)
 theorem advance_result (x : Input) (t : ℕ) (s : Cut x) :
    ((advance x)^[t] s).2=s.2 ∪ packing t s.1 x.R x.B := by
  induction t generalizing s with
  | zero => simp only [Function.iterate_zero,Function.id_def,packing,union_empty]
  | succ t ih =>
    rw [Function.iterate_succ_apply,ih]
    by_cases h : s.1.Nonempty
    · simp only [advance,dite_eq_left h,packing]
      ext i
      simp only [mem_union,mem_insert]
      tauto
    · have he : s.1=∅ := not_nonempty_iff_eq_empty.mp h
      simp [advance,he,packing_empty]

end MetricKMedian.Completion.Rational.PackingProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseProductProgram
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.SparseIntegerLaw.BinarySparse
open Binary Binary.Automatic Binary.Automatic.Poly
variable {α β A B : Type}

def prodData (x : Data A × Data B) : Data (A × B) :=
  ((x.1.1.1*x.2.1.1, x.1.1.2.flatMap (fun z => x.2.1.2.map (fun w => z*w))),
    x.1.2.flatMap (fun a => x.2.2.map (fun b => (a,b))))

end MetricKMedian.SparseIntegerLaw.BinarySparse
end

end OAI
end