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

import Mathlib
import Definitions.Def_OAIQ037K036
import Definitions.Def_OAIQ037K037

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
noncomputable def valueProgram : PolyProgram (encodeList encodeBool) Nat.bits Word.value := unpackProgram.comp PolyProgram.toBits
end BooleanLists
end MetricKMedian.Binary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_BinaryIterations
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 Iteration
open PolyProgram
variable {α : Type}

noncomputable def program {ea : α → List Bool} {f : α → α}
    (P : PolyProgram ea ea f) (a0 : α) :
    PolyProgram (enc ea) (encodeLoop (enc ea) (encodeList ea)) (body f) := by
  let n := fst Nat.bits (encodePair ea (encodeList ea))
  let st := snd Nat.bits (encodePair ea (encodeList ea))
  let a := st.comp (fst ea (encodeList ea))
  let bs := st.comp (snd ea (encodeList ea))
  let test := n.comp natZero
  let dec := (n.fanout (constant (enc ea) Nat.bits 1)).comp natSub
  let next := dec.fanout ((a.comp P).fanout ((a.fanout bs).comp (listCons ea)))
  let go := next.comp (injectRight (enc ea) (encodeList ea))
  let stop := (bs.comp (listReverse ea a0)).comp (injectLeft (enc ea) (encodeList ea))
  exact (ite test go stop).congr _ (fun s => by simp only [Function.comp_apply,body,decide_eq_true_eq])

end Iteration

namespace PolyProgram
variable {α β : Type} {ea : α → List Bool} {eb : β → List Bool}
variable {f : α → α} {start : β → α} {count : β → ℕ}

noncomputable def iteratesFrom (P : PolyProgram ea ea f) (initial : PolyProgram eb ea start)
    (steps : PolyProgram eb Nat.bits count) (a0 : α) (N A : Polynomial ℕ)
    (hn : ∀ b, count b≤N.eval (eb b).length)
    (ha : ∀ b i, i ≤ count b → (ea (f^[i] (start b))).length≤A.eval (eb b).length) :
    PolyProgram eb (encodeList ea) (fun b => Iteration.iterates f (start b) (count b)) := by
  let init := steps.fanout (initial.fanout (constant eb (encodeList ea) []))
  exact init.loopFrom (Iteration.program P a0) _ (N+1) (2*(N+1)+1+2*A+1+N*(2*A+1)) (fun b => by
    refine ⟨count b+1,by simp only [eval_add,eval_one]; have hh := hn b; omega,?_⟩
    have hr := Iteration.run ea f (N.eval (eb b).length) (A.eval (eb b).length) (count b) (start b) []
      (by simpa using hn b) (ha b) (by simp)
    simpa only [List.reverse_nil,List.nil_append,Iteration.enc,Iteration.bound,eval_add,eval_mul,eval_ofNat,eval_one] using hr)
end PolyProgram
end MetricKMedian.Binary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_BinaryListSelection
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
variable {α : Type} {ea : α → List Bool}
noncomputable def listChoose {p : α × α → Bool} (P : PolyProgram (encodePair ea ea) encodeBool p) (a0 : α) :
    PolyProgram (encodePair (encodeList ea) ea) ea
      (fun x : List α × α => x.1.foldl (fun b a => if p (b,a) then a else b) x.2) := by
  let step : PolyProgram (encodePair ea ea) ea (fun x => if p x then x.2 else x.1) :=
    (ite P (fst ea ea) (snd ea ea)).congr _ (fun _ => rfl)
  exact step.listFold a0 X (fun as b pre suf he => by
    rcases ListAlgorithms.foldChoice p pre b with h|h
    · rw [h]
      simp only [eval_X,encodePair_length]; omega
    · have hp : (encodeList ea pre).length ≤ (encodeList ea as).length := by
        rw [he,EncodedList.append,List.length_append]; omega
      have hh := (EncodedList.member_length ea pre _ h).trans hp
      simp only [eval_X,encodePair_length]; omega)
end PolyProgram
end MetricKMedian.Binary
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}

noncomputable def program {ea : α → List Bool} {f : α → α}
    (P : PolyProgram ea ea f) : PolyProgram (enc ea) (encodeLoop (enc ea) ea) (body f) := by
  open PolyProgram in
  let n := fst Nat.bits ea
  let a := snd Nat.bits ea
  let dec := (n.fanout (constant (enc ea) Nat.bits 1)).comp natSub
  let go := (dec.fanout (a.comp P)).comp (injectRight (enc ea) ea)
  let stop := a.comp (injectLeft (enc ea) ea)
  exact (ite (n.comp natZero) go stop).congr _ (fun _ => by simp only [Function.comp_apply,body,decide_eq_true_eq])

end Repeat

namespace PolyProgram
variable {α β : Type} {ea : α → List Bool} {eb : β → List Bool}
variable {f : α → α} {start : β → α} {count : β → ℕ}
noncomputable def repeatFrom (P : PolyProgram ea ea f) (initial : PolyProgram eb ea start)
    (steps : PolyProgram eb Nat.bits count) (N A : Polynomial ℕ)
    (hn : ∀ b, count b≤N.eval (eb b).length)
    (ha : ∀ b i, i ≤ count b → (ea (f^[i] (start b))).length≤A.eval (eb b).length) :
    PolyProgram eb ea (fun b => f^[count b] (start b)) := by
  let init := steps.fanout initial
  exact init.loopFrom (Repeat.program P) _ (N+1) (2*(N+1)+1+A) (fun b => by
    refine ⟨count b+1,by simp only [eval_add,eval_one]; have hh := hn b; omega,?_⟩
    have hr := Repeat.run ea f (N.eval (eb b).length) (A.eval (eb b).length) (count b) (start b) (hn b) (ha b)
    simpa only [Repeat.enc,eval_add,eval_mul,eval_ofNat,eval_one] using hr)
end PolyProgram
end MetricKMedian.Binary
end

end OAI
end

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

namespace OAI

namespace MetricKMedian.Gaussian
open Finset

theorem computedIntegerKernel_spec (r n L : ℕ) (V : Fin r → Fin n → ℤ)
    (hn : r < n) (hV : ∀ i j, |V i j| ≤ (2:ℤ)^L) :
    (∃ j, computedIntegerKernel r n V j ≠ 0) ∧
      (∀ i, ∑ j, computedIntegerKernel r n V j*V i j=0) ∧
      ∀ j, |computedIntegerKernel r n V j| ≤ (2:ℤ)^((2*r*(r+L))*(n+1)) := by
  let q := kernel r n (fun i j => (V i j:ℚ))
  have he : computedIntegerKernel r n V=RationalScaling.numerator q := by
    funext j
    dsimp only [computedIntegerKernel]
    simp only [Vector.getElem_ofFn,kernelVector_eq,values_tabulate]
    rfl
  rw [he]
  have hq := kernel_spec r n (fun i j => (V i j:ℚ)) hn
  have hb := integer_input_kernel_bounds r n L V hn hV
  let D := RationalScaling.denominator q
  have hD : (D:ℚ) ≠ 0 := by exact_mod_cast (RationalScaling.denominator_pos q).ne'
  have heq : ∀ j, (RationalScaling.numerator q j:ℚ)=q j*(D:ℚ) :=
    RationalScaling.numerator_cast q
  refine ⟨?_,?_,?_⟩
  · obtain ⟨j,hj⟩ := hq.1
    refine ⟨j,?_⟩
    intro hz
    have hh := heq j
    rw [hz,Int.cast_zero] at hh
    exact (mul_ne_zero hj hD) hh.symm
  · intro i
    have hi : (∑ j, (RationalScaling.numerator q j:ℚ)*(V i j:ℚ))=0 := by
      simp only [heq]
      calc
        _ = (∑ j, (V i j:ℚ)*q j)*(D:ℚ) := by
          rw [sum_mul]; apply sum_congr rfl; intro j _; ring
        _ = 0 := by rw [hq.2 i,zero_mul]
    exact_mod_cast hi
  · intro j
    simpa only [Fintype.card_fin] using RationalScaling.numerator_bound q (2*r*(r+L))
      (fun j => (hb j).1) (fun j => (hb j).2) j

end MetricKMedian.Gaussian

end OAI
end

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

namespace OAI

namespace MetricKMedian.IntegerLaw
open Finset

theorem computedAffineKernel_spec {n d : ℕ} (μ : IntegerLaw (Fin n))
    (v : Fin n → Fin d → ℤ) (L : ℕ) (hv : ∀ i j, |v i j| ≤ (2:ℤ)^L)
    (hsize : d+1 < μ.support.card) :
    let z := computedAffineKernel μ v
    (∃ i, z i ≠ 0) ∧ (∑ i, z i=0) ∧
      (∀ j, ∑ i, (z i:ℚ)*(v i j:ℚ)=0) ∧
      (∀ i, μ.numerator i=0 → z i=0) ∧
      ∀ i, |z i| ≤ (2:ℤ)^((2*(d+1)*(d+1+L))*(n+1)) := by
  dsimp only
  let V := activeMatrix μ v
  let zi := Gaussian.computedIntegerKernel (d+1) μ.support.card V
  have hVb : ∀ j i, |V j i| ≤ (2:ℤ)^L := by
    intro j i
    refine Fin.cases ?_ (fun j => ?_) j
    · simpa only [V,activeMatrix,Fin.cases_zero,abs_one] using
        (one_le_pow₀ (by norm_num : (1:ℤ) ≤ 2) : (1:ℤ) ≤ 2^L)
    · simpa only [V,activeMatrix,Fin.cases_succ] using hv ((μ.support.orderIsoOfFin rfl) i).val j
  have hzi := Gaussian.computedIntegerKernel_spec (d+1) μ.support.card L V hsize hVb
  have he : computedAffineKernel μ v=Compression.extendVector μ.support zi := by
    funext i
    simp only [computedAffineKernel,Vector.getElem_ofFn]
    rfl
  rw [he]
  refine ⟨?_,?_,?_,?_,?_⟩
  · obtain ⟨i,hi⟩ := hzi.1
    exact ⟨((μ.support.orderIsoOfFin rfl) i).val,by rwa [Compression.extendVector_at]⟩
  · have hh := hzi.2.1 0
    simp only [V,activeMatrix,Fin.cases_zero,mul_one] at hh
    simpa only [mul_one] using
      (Compression.extendVector_sum μ.support zi (fun _ => 1)).trans (by simpa only [mul_one] using hh)
  · intro j
    have hh := hzi.2.1 j.succ
    simp only [V,activeMatrix,Fin.cases_succ] at hh
    have ht := (Compression.extendVector_sum μ.support zi (fun i => v i j)).trans hh
    exact_mod_cast ht
  · intro i hi
    apply Compression.extendVector_zero
    simpa only [mem_support,not_not] using hi
  · intro i
    have heN : μ.support.card ≤ n := (card_le_univ _).trans_eq (Fintype.card_fin n)
    apply Compression.extendVector_bound _ _ _ (by positivity) _ i
    intro j
    exact (hzi.2.2 j).trans (pow_le_pow_right₀ (by norm_num)
      (Nat.mul_le_mul_left _ (Nat.add_le_add_right heN 1)))

end MetricKMedian.IntegerLaw

end OAI
end

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

namespace OAI

namespace MetricKMedian.IntegerLaw
open Finset

def compressionStepAuto {n d : ℕ} (μ : IntegerLaw (Fin n))
    (v : Fin n → Fin d → ℤ) (hsize : d+1 < μ.support.card) : IntegerLaw (Fin n) :=
  let z := computedAffineKernel μ v
  have hz : (∃ i, z i ≠ 0) ∧ (∑ i, z i=0) := by
    obtain ⟨L,hL⟩ := exists_feature_bound v
    have h := computedAffineKernel_spec μ v L hL hsize
    exact ⟨h.1,h.2.1⟩
  have hP := positiveSet_nonempty z hz.2 hz.1
  let p := computedPivot μ z hP
  have hp := computedPivot_spec μ z hP
  eliminateAt μ z p hp.1 hp.2 hz.2

def compressStepsAuto {n d : ℕ} (v : Fin n → Fin d → ℤ) :
    ℕ → IntegerLaw (Fin n) → IntegerLaw (Fin n)
  | 0,μ => μ
  | t+1,μ => if h : d+1 < μ.support.card then
      compressStepsAuto v t (compressionStepAuto μ v h) else μ

def compressAuto {n d : ℕ} (μ : IntegerLaw (Fin n)) (v : Fin n → Fin d → ℚ) :
    IntegerLaw (Fin n) :=
  compressStepsAuto (RationalLaw.scaledFeatures v) n μ

end MetricKMedian.IntegerLaw

end OAI
end

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

def compressAuto {d : ℕ} (μ : SparseIntegerLaw α) (v : α → Fin d → ℚ) :
    SparseIntegerLaw α :=
  let ν : SparseIntegerLaw α := ⟨μ.length,μ.states,
    μ.law.compressAuto (fun i => v μ.states[i.val])⟩
  ν.trim

def step {d : ℕ} (v : α → Fin d → ℚ) (μ : SparseIntegerLaw α)
    (p : α → ℚ) (hp : ∀ a, 0 ≤ p a ∧ p a ≤ 1) (next : α → Fin 2 → α) :
    SparseIntegerLaw α := (μ.branch p hp next).compressAuto v

end MetricKMedian.SparseIntegerLaw

end OAI
end

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

 def step (β : Fin n → ℚ) (hβ : ∀ i, 0 < β i)
    (μ : SparseIntegerLaw (Vector ℚ n)) : SparseIntegerLaw (Vector ℚ n) :=
  μ.step features (probability β) (probability_unit β hβ) (endpoint β)

 def run (β : Fin n → ℚ) (hβ : ∀ i, 0 < β i) (p : Vector ℚ n) :
    ℕ → SparseIntegerLaw (Vector ℚ n)
  | 0 => .dirac p
  | t+1 => step β hβ (run β hβ p t)

end MetricKMedian.SparseWeightedPartial
end
end

end OAI
end

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

namespace OAI

namespace MetricKMedian.SparseBernoulli
open Finset
variable {n d : ℕ}

def run (p : Fin n → ℚ) (hp : ∀ i, 0 ≤ p i ∧ p i ≤ 1) :
    ℕ → SparseIntegerLaw (Fin n → Bool)
  | 0 => .dirac (fun _ => false)
  | t+1 => if ht : t<n then
      (run p hp t).step (features (d := d)) (fun _ => p ⟨t,ht⟩)
        (fun _ => hp ⟨t,ht⟩) (fun q b => endpoint q ⟨t,ht⟩ b)
    else run p hp t

end MetricKMedian.SparseBernoulli

end OAI
end

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

namespace OAI

namespace MetricKMedian.SparsePhysicalBatch
open Finset
variable {n : ℕ}

def law (Z : Finset (Fin n)) (C : Fin n → Finset (Fin n))
    (p : ℚ) (q : Fin n → ℚ) (hp : 0 ≤ p ∧ p ≤ 1) (hq : ∀ e, 0 ≤ q e ∧ q e ≤ 1) :
    SparseIntegerLaw (Finset (Fin n)) :=
  SparseIntegerLaw.mix
    ((SparseBernoulli.run (d := 4) (fun _ => p) (fun _ => hp) n).map (balanced Z C))
    ((SparseBernoulli.run (d := 4) q hq n).map (unbalanced Z))

end MetricKMedian.SparsePhysicalBatch

end OAI
end

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

namespace OAI

namespace MetricKMedian.SparseEnumeratedBatch
open Finset
variable {E : Type} [DecidableEq E] [Fintype E] {n : ℕ}

def law (enum : Fin n ≃ E) (Z : Finset E) (C : E → Finset E)
    (p : ℚ) (q : E → ℚ) (hp : 0 ≤ p ∧ p ≤ 1) (hq : ∀ e, 0 ≤ q e ∧ q e ≤ 1) :
    SparseIntegerLaw (Finset E) :=
  (SparsePhysicalBatch.law (Z.map enum.symm.toEmbedding)
    (fun a => (C (enum a)).map enum.symm.toEmbedding) p (fun a => q (enum a)) hp
    (fun a => hq (enum a))).map (fun A => A.map enum.toEmbedding)

end MetricKMedian.SparseEnumeratedBatch

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_RationalBatchFacts
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.RationalBatchData
open Finset FixedBatch PhysicalPotential
variable {I E : Type} [DecidableEq I] [Fintype I] [DecidableEq E] [Fintype E]

def proposal (G : I → Finset I) (Δ : ℕ) (g b p φ : ℚ)
    (hp : 0 ≤ p) (hφ : 0 ≤ φ) (hupper : (1+φ)*p ≤ 1) {n : ℕ}
    (enum : Fin n ≃ HeavyAction (graph G) (heavySet (graphMass G g) b)) :
    SparseIntegerLaw (Finset (HeavyAction (graph G) (heavySet (graphMass G g) b))) :=
  let m := graphMass G g
  let H := heavySet m b
  let D := heavy (graph G) H
  let q := fun e => bias m p φ (heavyParent (graph G) H e)
  SparseEnumeratedBatch.law enum (balanced D Δ) (conflicts D Δ) p q
    ⟨hp,(by have hh := mul_nonneg hp hφ; nlinarith only [hh,hupper])⟩
    (fun e => bias_probability m hp hφ hupper (heavyParent (graph G) H e))

end MetricKMedian.RationalBatchData
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_BatchProposalProgram
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.RationalBatchData.ProposalProgram
open Finset FixedBatch Binary Binary.PolyProgram
open SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Row Table setView)
variable {C : Type} (I : C → Type) [∀ c, LinearOrder (I c)] [∀ c, Fintype (I c)]

variable {I}

def Input.law (x : Input I) := proposal x.G x.Δ x.g x.b x.p x.φ x.hp x.hφ x.hupper x.enumActions
end MetricKMedian.RationalBatchData.ProposalProgram
end

end OAI
end

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

def events (μ : SparseIntegerLaw (I → Finset I)) (Δ : ℕ) (g β p φ : ℚ)
    (hp : 0 ≤ p) (hφ : 0 ≤ φ) (hupper : (1+φ)*p ≤ 1) : SparseIntegerLaw (Event I g β) :=
  μ.bindIndexed (fun i =>
    let G := μ.states[i.val]
    (proposal G Δ g β p φ hp hφ hupper
      (enumeration (graph G) (heavySet (graphMass G g) β))).map (fun Z => ⟨G,Z⟩))

end MetricKMedian.RationalBatchData
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 : ℕ}

def round (p : Vector ℚ n) : SparseIntegerLaw (Vector ℚ n) :=
  SparseWeightedPartial.run (fun _ => 1) (fun _ => by norm_num) p n

end MetricKMedian.SparseCardinalRounding
end
end

end OAI
end