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

import Mathlib
import Definitions.Def_OAIQ037K048
import Definitions.Def_OAIQ037K049

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_SequentialParserProgram
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.InputParser
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly Polynomial
section Generic
variable {α : Type} [Coding α] [Inhabited α] (read : List Bool → α × List Bool)
variable (P : PolyProgram enc enc read) (hrest : ∀ xs, (read xs).2.length≤xs.length)
noncomputable def parseBound : Polynomial ℕ := X+X*(2*P.sizeBound+1)
end Generic
end MetricKMedian.InputParser
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Compression_ComputedCompressionStep
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 compressionStep_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 ν := compressionStep μ v L hv hsize
    ν.denominator ≤ μ.denominator*(2:ℤ)^((2*(d+1)*(d+1+L))*(n+1)) ∧
      ν.support ⊆ μ.support ∧ ν.support.card < μ.support.card ∧
      ∀ j, (∑ i, ν.rational.weight i*(v i j:ℚ))=∑ i, μ.rational.weight i*(v i j:ℚ) := by
  let z := computedAffineKernel μ v
  have hz := computedAffineKernel_spec μ v L hv hsize
  have hP := positiveSet_nonempty z hz.2.1 hz.1
  let p := computedPivot μ z hP
  have hp := computedPivot_spec μ z hP
  have he := eliminateAt_preserves μ (fun i j => (v i j:ℚ)) z p hp.1 hp.2
    hz.2.1 hz.2.2.1 hz.2.2.2.1
  change (eliminateAt μ z p hp.1 hp.2 hz.2.1).denominator ≤ _ ∧ _
  refine ⟨?_,he.2.2.2.1.trans (erase_subset _ _),?_,he.2.2.2.2⟩
  · change μ.denominator*z p ≤ _
    exact mul_le_mul_of_nonneg_left ((le_abs_self _).trans (hz.2.2.2.2 p)) μ.denominator_pos.le
  · change (eliminateAt μ z p hp.1 hp.2 hz.2.1).support.card < μ.support.card
    have hh := card_le_card he.2.2.2.1
    rw [card_erase_of_mem ((μ.mem_support p).mpr he.2.1)] at hh
    omega

end MetricKMedian.IntegerLaw

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Compression_ComputedCompression
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 compressSteps_spec {n d : ℕ} (v : Fin n → Fin d → ℤ) (L : ℕ)
    (hv : ∀ i j, |v i j| ≤ (2:ℤ)^L) (t : ℕ) (μ : IntegerLaw (Fin n))
    (hμ : μ.support.card ≤ t+(d+1)) :
    let ν := compressSteps v L hv t μ
    ν.denominator ≤ μ.denominator*(2:ℤ)^(((2*(d+1)*(d+1+L))*(n+1))*t) ∧
      ν.support ⊆ μ.support ∧ ν.support.card ≤ d+1 ∧
      ∀ j, (∑ i, ν.rational.weight i*(v i j:ℚ))=∑ i, μ.rational.weight i*(v i j:ℚ) := by
  induction t generalizing μ with
  | zero =>
    dsimp only [compressSteps]
    refine ⟨?_,Subset.rfl,by omega,fun _ => rfl⟩
    simp only [Nat.mul_zero,pow_zero,mul_one,le_refl]
  | succ t ih =>
    dsimp only
    by_cases h : d+1 < μ.support.card
    · rw [compressSteps,dite_eq_left h]
      let ν := compressionStep μ v L hv h
      have hs := compressionStep_spec μ v L hv h
      have hν : ν.support.card ≤ t+(d+1) := by
        dsimp only [ν]
        have hh := hs.2.2.1
        omega
      have hi := ih ν hν
      refine ⟨?_,hi.2.1.trans hs.2.1,hi.2.2.1,fun j => (hi.2.2.2 j).trans (hs.2.2.2 j)⟩
      let Z := ((2*(d+1)*(d+1+L))*(n+1))
      calc
        _ ≤ ν.denominator*(2:ℤ)^(Z*t) := hi.1
        _ ≤ (μ.denominator*(2:ℤ)^Z)*(2:ℤ)^(Z*t) :=
          mul_le_mul_of_nonneg_right hs.1 (by positivity)
        _ = μ.denominator*(2:ℤ)^(Z*(t+1)) := by
          rw [mul_assoc,← pow_add]
          congr 2
          ring
    · rw [compressSteps,dite_eq_right h]
      refine ⟨?_,Subset.rfl,by omega,fun _ => rfl⟩
      exact le_mul_of_one_le_right μ.denominator_pos.le (one_le_pow₀ (by norm_num))

theorem computedCompress_spec {n d : ℕ} (μ : IntegerLaw (Fin n))
    (v : Fin n → Fin d → ℤ) (L : ℕ) (hv : ∀ i j, |v i j| ≤ (2:ℤ)^L) :
    let ν := computedCompress μ v L hv
    ν.denominator ≤ μ.denominator*(2:ℤ)^(((2*(d+1)*(d+1+L))*(n+1))*n) ∧
      ν.support ⊆ μ.support ∧ ν.support.card ≤ d+1 ∧
      ∀ j, (∑ i, ν.rational.weight i*(v i j:ℚ))=∑ i, μ.rational.weight i*(v i j:ℚ) := by
  apply compressSteps_spec
  exact (card_le_univ _).trans ((Fintype.card_fin n).trans_le (Nat.le_add_right _ _))

end MetricKMedian.IntegerLaw

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Compression_IntegerRationalCompression
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 compressRational_spec {n d : ℕ} (μ : IntegerLaw (Fin n))
    (v : Fin n → Fin d → ℚ) (L : ℕ)
    (hnum : ∀ i j, |(v i j).num| ≤ (2:ℤ)^L)
    (hden : ∀ i j, ((v i j).den:ℤ) ≤ (2:ℤ)^L) :
    let ν := μ.compressRational v L hnum hden
    ν.denominator ≤ μ.denominator*(2:ℤ)^(((2*(d+1)*(d+1+L*(n+1)))*(n+1))*n) ∧
      ν.support ⊆ μ.support ∧ ν.support.card ≤ d+1 ∧
      ∀ j, (∑ i, ν.rational.weight i*v i j)=∑ i, μ.rational.weight i*v i j := by
  have hh := μ.computedCompress_spec (RationalLaw.scaledFeatures v) (L*(n+1))
    (RationalLaw.scaledFeatures_bound v L hnum hden)
  refine ⟨hh.1,hh.2.1,hh.2.2.1,?_⟩
  intro j
  let D := RationalScaling.denominator (fun i => v i j)
  have hD : (D:ℚ) ≠ 0 := by
    exact_mod_cast (RationalScaling.denominator_pos (fun i => v i j)).ne'
  have hcast : ∀ i, (RationalLaw.scaledFeatures v i j:ℚ)=v i j*(D:ℚ) := by
    intro i
    rw [RationalLaw.scaledFeatures_eq]
    exact RationalScaling.numerator_cast _ i
  have hm := hh.2.2.2 j
  simp only [hcast,← mul_assoc,← sum_mul] at hm
  exact mul_right_cancel₀ hD hm

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

theorem compressAuto_spec {n d : ℕ} (μ : IntegerLaw (Fin n))
    (v : Fin n → Fin d → ℚ) (L : ℕ)
    (hnum : ∀ i j, |(v i j).num| ≤ (2:ℤ)^L)
    (hden : ∀ i j, ((v i j).den:ℤ) ≤ (2:ℤ)^L) :
    let ν := μ.compressAuto v
    ν.denominator ≤ μ.denominator*(2:ℤ)^(((2*(d+1)*(d+1+L*(n+1)))*(n+1))*n) ∧
      ν.support ⊆ μ.support ∧ ν.support.card ≤ d+1 ∧
      ∀ j, (∑ i, ν.rational.weight i*v i j)=∑ i, μ.rational.weight i*v i j := by
  rw [compressAuto_eq μ v L hnum hden]
  exact compressRational_spec μ v L hnum hden

theorem compressAuto_correct {n d : ℕ} (μ : IntegerLaw (Fin n))
    (v : Fin n → Fin d → ℚ) :
    let ν := μ.compressAuto v
    ν.support ⊆ μ.support ∧ ν.support.card ≤ d+1 ∧
      ∀ j, (∑ i, ν.rational.weight i*v i j)=∑ i, μ.rational.weight i*v i j := by
  obtain ⟨L,hnum,hden⟩ := exists_rational_feature_bound v
  exact (compressAuto_spec μ v L hnum hden).2

end MetricKMedian.IntegerLaw

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Compression_CompressionListStep
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.IntegerLaw.BinaryCompression
open Binary Binary.PolyProgram Function Finset
noncomputable def featuresProgram : PolyProgram Input.encode em Input.features :=
  ((rawProgram.comp (snd es (encodePair el em))).comp (snd el em)).congr _ (fun _ => rfl)
noncomputable def dimProgram : PolyProgram Input.encode es (fun I => List.replicate I.d ()) :=
  (rawProgram.comp (fst es (encodePair el em))).congr _ (fun _ => rfl)

end MetricKMedian.IntegerLaw.BinaryCompression
end

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}

theorem compressAuto_correct {d : ℕ} (μ : SparseIntegerLaw α) (v : α → Fin d → ℚ) :
    let ν := μ.compressAuto v
    ν.length ≤ d+1 ∧
      (∀ i : Fin ν.length, ∃ j : Fin μ.length, ν.states[i.val]=μ.states[j.val]) ∧
      ∀ j, ν.moment (fun a => v a j)=μ.moment (fun a => v a j) := by
  let ξ : SparseIntegerLaw α := ⟨μ.length,μ.states,
    μ.law.compressAuto (fun i => v μ.states[i.val])⟩
  have hh := μ.law.compressAuto_correct (fun i => v μ.states[i.val])
  refine ⟨hh.2.1,?_,?_⟩
  · intro i
    refine ⟨ξ.law.support.orderEmbOfFin rfl i,?_⟩
    change (Vector.ofFn (fun k => μ.states[(ξ.law.support.orderEmbOfFin rfl k).val]))[i.val] = _
    simp only [Vector.getElem_ofFn]
    congr 2
  · intro j
    change ξ.trim.moment (fun a => v a j)=_
    rw [trim_moment]
    exact hh.2.2 j

theorem step_property {d : ℕ} (v : α → Fin d → ℚ) (μ : SparseIntegerLaw α)
    (p : α → ℚ) (hp : ∀ a, 0 ≤ p a ∧ p a ≤ 1) (next : α → Fin 2 → α)
    (P : α → Prop) (hP : ∀ i : Fin μ.length, ∀ b, P (next μ.states[i.val] b)) :
    ∀ i : Fin (step v μ p hp next).length, P (step v μ p hp next).states[i.val] := by
  intro i
  obtain ⟨j,hj⟩ := ((μ.branch p hp next).compressAuto_correct v).2.1 i
  change P ((μ.branch p hp next).compressAuto v).states[i.val]
  rw [hj]
  change P ((Vector.ofFn (fun k => next
    μ.states[(finProdFinEquiv.symm k).1.val] (finProdFinEquiv.symm k).2))[j.val])
  simp only [Vector.getElem_ofFn]
  exact hP _ _

end MetricKMedian.SparseIntegerLaw

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_SignedGridInvariant
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.SparseSignedPartial
open RationalSignedStep RationalGrid
open RationalWeightedStep (point)
variable {n : ℕ}

theorem run_grid (β : Fin n → ℚ) (p : Vector ℚ n)
    (D : ℤ) (hb : ∀ i, At D (β i)) (hp : ∀ i, At D (β i*point p i)) (t : ℕ) :
    ∀ a : Fin (run β p t).length, ∀ i, At D (β i*point (run β p t).states[a.val] i) := by
  induction t with
  | zero =>
    intro a
    have he : (run β p 0).states[a.val]=p := SparseIntegerLaw.dirac_states p a
    rw [he]
    exact hp
  | succ t ih =>
    apply (run β p t).step_property SparseWeightedPartial.features (probability β) (probability_unit β)
      (endpoint β) (fun q => ∀ i, At D (β i*point q i))
    intro a b
    exact endpoint_grid β D hb _ (ih a) b

theorem run_zero_weight (β : Fin n → ℚ) (p : Vector ℚ n) (t : ℕ) :
    ∀ a : Fin (run β p t).length, ∀ i, β i=0 → point (run β p t).states[a.val] i=point p i := by
  induction t with
  | zero =>
    intro a
    have he : (run β p 0).states[a.val]=p := SparseIntegerLaw.dirac_states p a
    rw [he]
    exact fun _ _ => rfl
  | succ t ih =>
    apply (run β p t).step_property SparseWeightedPartial.features (probability β) (probability_unit β)
      (endpoint β) (fun q => ∀ i, β i=0 → point q i=point p i)
    intro a b i hi
    exact (endpoint_zero_weight β _ b i hi).trans (ih a i hi)
end MetricKMedian.SparseSignedPartial
end

end OAI
end

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

variable {α β A : Type}

@[fun_prop] theorem weights_poly : Poly weights := by
  unfold weights
  apply list_map <;> fun_prop

@[fun_prop] theorem jointWeights_poly [Coding A] [Inhabited A] : Poly (jointWeights (A:=A)) := by
  unfold jointWeights
  apply list_flatMap
  · apply list_map <;> fun_prop
  · fun_prop

@[fun_prop] theorem bindData_poly [Coding A] [Inhabited A] : Poly (bindData (A:=A)) := by
  have hd : Poly IntegerList.denominator := ⟨IntegerList.denominatorProgram⟩
  have hn : Poly IntegerList.numerators := ⟨IntegerList.numeratorsProgram⟩
  have hs : Poly (fun x : LawData × List (Data A) => x.2.flatMap Prod.snd) := by
    apply list_flatMap <;> fun_prop
  exact pair (pair (comp hd jointWeights_poly) (comp hn jointWeights_poly)) hs

end MetricKMedian.SparseIntegerLaw.BinarySparse
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseMixProgram
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 : Type}

def mixData (x : Data A × Data A) : Data A := bindData ((2,[1,1]),[x.1,x.2])

@[fun_prop] theorem mixData_poly [Coding A] [Inhabited A] : Poly (mixData (A:=A)) := by
  unfold mixData
  fun_prop
end MetricKMedian.SparseIntegerLaw.BinarySparse
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseTable
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
variable {α β A : Type}
def table (μ : SparseIntegerLaw α) (v : α → A) : Data A := ((raw μ).1,μ.states.toList.map v)
 theorem table_map (μ : SparseIntegerLaw α) (f : α → β) (v : β → A) :
    table (μ.map f) v=table μ (v ∘ f) := by
  simp only [table,raw,map,Vector.toList_map,List.map_map]

end MetricKMedian.SparseIntegerLaw.BinarySparse
end

end OAI
end