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

import Mathlib
import Definitions.Def_MetricKMedian
import Definitions.Def_OAIQ037K042
import Definitions.Def_OAIQ037K057
import Definitions.Def_OAIQ037K058
import Definitions.Def_OAIQ037K059

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 : ℕ}

 theorem step_pair (β : Fin n → ℚ) (hβ : ∀ i, 0 < β i)
    (μ : SparseIntegerLaw (Vector ℚ n)) (i j : Fin n) (hij : i ≠ j) :
    (step β hβ μ).moment (fun p => point p i*point p j) ≤
      μ.moment (fun p => point p i*point p j) := by
  have hh := μ.step_moment features (probability β) (probability_unit β hβ)
    (endpoint β) (finSumFinEquiv (Sum.inr (finProdFinEquiv (i,j))))
  simp only [features_pair] at hh
  exact hh.trans_le (μ.moment_mono _ _ (fun k => endpoint_pair β hβ _ i j hij))

 theorem run_pair (β : Fin n → ℚ) (hβ : ∀ i, 0 < β i)
    (p : Vector ℚ n) (t : ℕ) (i j : Fin n) (hij : i ≠ j) :
    (run β hβ p t).moment (fun q => point q i*point q j) ≤ point p i*point p j := by
  induction t with
  | zero => exact (SparseIntegerLaw.dirac_moment _ _).le
  | succ t ih => exact (step_pair β hβ _ i j hij).trans ih

end MetricKMedian.SparseWeightedPartial
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseGraphFeatures
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.SparseGraph
open Finset
variable {n m : ℕ}

theorem step_single (μ : SparseIntegerLaw (Graph n m)) (ν : SparseIntegerLaw (Finset (Fin n)))
    (i j : Fin m) (h : Fin n) :
    (step μ ν i).moment (fun G => edge G h j)=
      if j=i then ν.moment (fun S => if h∈S then 1 else 0) else μ.moment (fun G => edge G h j) := by
  have hh := (μ.prodCompress_spec ν (fun G S => next G S i) features).2.2
    (finSumFinEquiv (Sum.inl (finProdFinEquiv (h,j))))
  simp only [features_single] at hh
  refine hh.trans ?_
  by_cases hji : j=i
  · simp only [edge_next,ite_eq_left hji]
    exact μ.moment_const _
  · simp only [edge_next,ite_eq_right hji]
    simp only [SparseIntegerLaw.moment_const]

theorem step_pair (μ : SparseIntegerLaw (Graph n m)) (ν : SparseIntegerLaw (Finset (Fin n)))
    (i j k : Fin m) (h l : Fin n) (hjk : j≠k) :
    (step μ ν i).moment (fun G => edge G h j*edge G l k)=
      if j=i then ν.moment (fun S => if h∈S then 1 else 0)*μ.moment (fun G => edge G l k)
      else if k=i then μ.moment (fun G => edge G h j)*ν.moment (fun S => if l∈S then 1 else 0)
      else μ.moment (fun G => edge G h j*edge G l k) := by
  have hh := (μ.prodCompress_spec ν (fun G S => next G S i) features).2.2
    (finSumFinEquiv (Sum.inr (finProdFinEquiv (finProdFinEquiv (h,j),finProdFinEquiv (l,k)))))
  simp only [features_pair] at hh
  refine hh.trans ?_
  by_cases hji : j=i
  · have hki : k≠i := fun hk => hjk (hji.trans hk.symm)
    simp only [edge_next,ite_eq_left hji,ite_eq_right hki,
      SparseIntegerLaw.moment_mul_right,SparseIntegerLaw.moment_mul]
  · by_cases hki : k=i
    · simp only [edge_next,ite_eq_right hji,ite_eq_left hki,
        SparseIntegerLaw.moment_mul,SparseIntegerLaw.moment_mul_right]
    · simp only [edge_next,ite_eq_right hji,ite_eq_right hki,SparseIntegerLaw.moment_const]

end MetricKMedian.SparseGraph
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 round_invariants (p : Vector ℚ n)
    (hp : ∀ i, 0 ≤ point p i ∧ point p i ≤ 1) (K : ℕ)
    (hs : (∑ i, point p i)=(K:ℚ)) :
    ∀ a : Fin (round p).length,
      (∀ i, point (round p).states[a.val] i=0 ∨ point (round p).states[a.val] i=1) ∧
      (∑ i, point (round p).states[a.val] i)=(K:ℚ) := by
  intro a
  obtain ⟨h0,h1,h2⟩ := SparseWeightedPartial.run_invariants (fun _ => 1)
    (fun _ => by norm_num) p hp n a
  simp only [one_mul] at h1
  have hsum : (∑ i, point (round p).states[a.val] i)=(K:ℚ) := h1.trans hs
  exact ⟨integral_of_small_fractional _ h0 K hsum (by simpa only [round, Nat.sub_self, max_eq_right (Nat.zero_le 1)] using h2),hsum⟩

theorem round_pair (p : Vector ℚ n) (i j : Fin n) (hij : i ≠ j) :
    (round p).moment (fun q => point q i*point q j) ≤ point p i*point p j :=
  SparseWeightedPartial.run_pair _ _ p n i j hij

end MetricKMedian.SparseCardinalRounding
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseGraphRun
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.SparseGraph
open Finset
variable {n m : ℕ}

theorem run_single (ν : Fin m → SparseIntegerLaw (Finset (Fin n)))
    (q : Fin n → Fin m → ℚ)
    (hq : ∀ h i, (ν i).moment (fun S => if h∈S then 1 else 0)=q h i)
    (t : ℕ) (ht : t ≤ m) (h : Fin n) (i : Fin m) :
    (run ν t).moment (fun G => edge G h i)=target q t h i := by
  induction t with
  | zero => simp [run,SparseIntegerLaw.dirac_moment,edge,target]
  | succ t ih =>
    have htm : t < m := by omega
    rw [run,dite_eq_left htm,step_single]
    by_cases hi : i=⟨t,htm⟩
    · subst i
      rw [ite_eq_left rfl,hq,target_succ_eq]
    · rw [ite_eq_right hi,ih (by omega),target_succ_ne q t htm h i hi]

theorem run_pair (ν : Fin m → SparseIntegerLaw (Finset (Fin n)))
    (q : Fin n → Fin m → ℚ)
    (hq : ∀ h i, (ν i).moment (fun S => if h∈S then 1 else 0)=q h i)
    (t : ℕ) (ht : t ≤ m) (h l : Fin n) (i j : Fin m) (hij : i≠j) :
    (run ν t).moment (fun G => edge G h i*edge G l j)=target q t h i*target q t l j := by
  induction t with
  | zero => simp [run,SparseIntegerLaw.dirac_moment,edge,target]
  | succ t ih =>
    have htm : t < m := by omega
    rw [run,dite_eq_left htm,step_pair _ _ _ _ _ _ _ hij]
    by_cases hi : i=⟨t,htm⟩
    · have hj : j≠⟨t,htm⟩ := fun he => hij (hi.trans he.symm)
      rw [ite_eq_left hi,hq,run_single ν q hq t (by omega),
        target_succ_ne q t htm l j hj]
      subst i
      rw [target_succ_eq]
    · rw [ite_eq_right hi]
      by_cases hj : j=⟨t,htm⟩
      · rw [ite_eq_left hj,hq,run_single ν q hq t (by omega),target_succ_ne q t htm h i hi]
        subst j
        rw [target_succ_eq]
      · rw [ite_eq_right hj,ih (by omega),target_succ_ne q t htm h i hi,
          target_succ_ne q t htm l j hj]

end MetricKMedian.SparseGraph
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_BoundedEnumerationProgram
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.Enumeration
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
@[fun_prop] theorem words_poly {α : Type} [Coding α] [Inhabited α] (c : ℕ) : Poly (@words α c) := by
  induction c with
  | zero => exact const [[]]
  | succ c ih =>
    change Poly (fun xs : List α => []::xs.flatMap (fun a => (words c xs).map (List.cons a)))
    have h : Poly (fun xs : List α => xs.flatMap (fun a => (words c xs).map (List.cons a))) := by
      apply list_flatMap
      · apply list_map
        · exact comp list_cons (pair (comp snd fst) snd)
        · exact comp ih fst
      · fun_prop
    have hh := comp (list_cons (α := List α)) (pair (const ([] : List α) : Poly (fun _ : List α => ([] : List α))) h)
    exact hh

def maskWord (x : Row × List ℕ) : Row := (indices x.1).map (fun i => (x.2.map (fun a => decide (a=i))).any id)
@[fun_prop] theorem maskWord_poly : Poly maskWord := by
  unfold maskWord
  apply list_map
  · apply comp bool_any
    apply list_map <;> fun_prop
  · fun_prop
 theorem words_map {α β : Type} (f : α → β) (c : ℕ) (xs : List α) :
    words c (xs.map f)=(words c xs).map (List.map f) := by
  induction c with
  | zero => rfl
  | succ c ih => simp only [words,List.flatMap_map,List.map_cons,List.map_nil,List.map_flatMap,ih,List.map_map,Function.comp_def]

def choicesRaw (c : ℕ) (T : Row) : Table :=
  (words c (Preparation.RationalUnitInput.Program.ranks T)).map (fun ys => maskWord (T,ys))
@[fun_prop] theorem choicesRaw_poly (c : ℕ) : Poly (choicesRaw c) := by unfold choicesRaw; apply list_map <;> fun_prop
end MetricKMedian.Reduction.Enumeration
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseCountFeatures
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.SparseCounts
open Finset
variable {n m : ℕ}

theorem step_single (μ : SparseIntegerLaw (Table n m)) (ν : SparseIntegerLaw ((Fin n → ℕ)))
    (i j : Fin m) (h : Fin n) :
    (step μ ν i).moment (fun G => edge G h j)=
      if j=i then ν.moment (fun S => (S h:ℚ)) else μ.moment (fun G => edge G h j) := by
  have hh := (μ.prodCompress_spec ν (fun G S => next G S i) features).2.2
    (finSumFinEquiv (Sum.inl (finProdFinEquiv (h,j))))
  simp only [features_single] at hh
  refine hh.trans ?_
  by_cases hji : j=i
  · simp only [edge_next,ite_eq_left hji]
    exact μ.moment_const _
  · simp only [edge_next,ite_eq_right hji]
    simp only [SparseIntegerLaw.moment_const]

theorem step_pair (μ : SparseIntegerLaw (Table n m)) (ν : SparseIntegerLaw ((Fin n → ℕ)))
    (i j k : Fin m) (h l : Fin n) (hjk : j≠k) :
    (step μ ν i).moment (fun G => edge G h j*edge G l k)=
      if j=i then ν.moment (fun S => (S h:ℚ))*μ.moment (fun G => edge G l k)
      else if k=i then μ.moment (fun G => edge G h j)*ν.moment (fun S => (S l:ℚ))
      else μ.moment (fun G => edge G h j*edge G l k) := by
  have hh := (μ.prodCompress_spec ν (fun G S => next G S i) features).2.2
    (finSumFinEquiv (Sum.inr (finProdFinEquiv (finProdFinEquiv (h,j),finProdFinEquiv (l,k)))))
  simp only [features_pair] at hh
  refine hh.trans ?_
  by_cases hji : j=i
  · have hki : k≠i := fun hk => hjk (hji.trans hk.symm)
    simp only [edge_next,ite_eq_left hji,ite_eq_right hki,
      SparseIntegerLaw.moment_mul_right,SparseIntegerLaw.moment_mul]
  · by_cases hki : k=i
    · simp only [edge_next,ite_eq_right hji,ite_eq_left hki,
        SparseIntegerLaw.moment_mul,SparseIntegerLaw.moment_mul_right]
    · simp only [edge_next,ite_eq_right hji,ite_eq_right hki,SparseIntegerLaw.moment_const]

theorem step_same (μ : SparseIntegerLaw (Table n m)) (ν : SparseIntegerLaw (Fin n → ℕ))
    (i j : Fin m) (h l : Fin n) :
    (step μ ν i).moment (fun G => edge G h j*edge G l j)=
      if j=i then ν.moment (fun S => (S h:ℚ)*(S l:ℚ))
      else μ.moment (fun G => edge G h j*edge G l j) := by
  have hh := (μ.prodCompress_spec ν (fun G S => next G S i) features).2.2
    (finSumFinEquiv (Sum.inr (finProdFinEquiv (finProdFinEquiv (h,j),finProdFinEquiv (l,j)))))
  simp only [features_pair] at hh
  refine hh.trans ?_
  by_cases hji : j=i
  · simp only [edge_next,ite_eq_left hji]
    exact μ.moment_const _
  · simp only [edge_next,ite_eq_right hji,SparseIntegerLaw.moment_const]

end MetricKMedian.SparseCounts
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseCountRun
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.SparseCounts
open Finset
variable {n m : ℕ}

theorem run_single (ν : Fin m → SparseIntegerLaw ((Fin n → ℕ)))
    (q : Fin n → Fin m → ℚ)
    (hq : ∀ h i, (ν i).moment (fun S => (S h:ℚ))=q h i)
    (t : ℕ) (ht : t ≤ m) (h : Fin n) (i : Fin m) :
    (run ν t).moment (fun G => edge G h i)=target q t h i := by
  induction t with
  | zero => simp [run,SparseIntegerLaw.dirac_moment,edge,target]
  | succ t ih =>
    have htm : t < m := by omega
    rw [run,dite_eq_left htm,step_single]
    by_cases hi : i=⟨t,htm⟩
    · subst i
      rw [ite_eq_left rfl,hq,target_succ_eq]
    · rw [ite_eq_right hi,ih (by omega),target_succ_ne q t htm h i hi]

theorem run_pair (ν : Fin m → SparseIntegerLaw ((Fin n → ℕ)))
    (q : Fin n → Fin m → ℚ)
    (hq : ∀ h i, (ν i).moment (fun S => (S h:ℚ))=q h i)
    (t : ℕ) (ht : t ≤ m) (h l : Fin n) (i j : Fin m) (hij : i≠j) :
    (run ν t).moment (fun G => edge G h i*edge G l j)=target q t h i*target q t l j := by
  induction t with
  | zero => simp [run,SparseIntegerLaw.dirac_moment,edge,target]
  | succ t ih =>
    have htm : t < m := by omega
    rw [run,dite_eq_left htm,step_pair _ _ _ _ _ _ _ hij]
    by_cases hi : i=⟨t,htm⟩
    · have hj : j≠⟨t,htm⟩ := fun he => hij (hi.trans he.symm)
      rw [ite_eq_left hi,hq,run_single ν q hq t (by omega),
        target_succ_ne q t htm l j hj]
      subst i
      rw [target_succ_eq]
    · rw [ite_eq_right hi]
      by_cases hj : j=⟨t,htm⟩
      · rw [ite_eq_left hj,hq,run_single ν q hq t (by omega),target_succ_ne q t htm h i hi]
        subst j
        rw [target_succ_eq]
      · rw [ite_eq_right hj,ih (by omega),target_succ_ne q t htm h i hi,
          target_succ_ne q t htm l j hj]

theorem run_columns (ν : Fin m → SparseIntegerLaw ((Fin n → ℕ)))
    (P : Fin m → (Fin n → ℕ) → Prop)
    (hP : ∀ i, ∀ a : Fin (ν i).length, P i (ν i).states[a.val]) (t : ℕ) (ht : t ≤ m) :
    ∀ a : Fin (run ν t).length, ∀ i, i.val<t → P i ((run ν t).states[a.val] i) := by
  induction t with
  | zero => intro a i hi; omega
  | succ t ih =>
    have htm : t < m := by omega
    have he : run ν (t+1)=step (run ν t) (ν ⟨t,htm⟩) ⟨t,htm⟩ := by
      rw [run,dite_eq_left htm]
    let inv : SparseIntegerLaw (Table n m) → Prop := fun μ =>
      ∀ a : Fin μ.length, ∀ i, i.val<t+1 → P i (μ.states[a.val] i)
    change inv (run ν (t+1))
    rw [he]
    intro a i hi
    obtain ⟨j,k,hjk⟩ := ((run ν t).prodCompress_spec (ν ⟨t,htm⟩)
      (fun G S => next G S ⟨t,htm⟩) features).2.1 a
    change (step (run ν t) (ν ⟨t,htm⟩) ⟨t,htm⟩).states[a.val]=_ at hjk
    rw [hjk]
    by_cases hi' : i=⟨t,htm⟩
    · subst i
      simpa only [next,Function.update_self] using hP ⟨t,htm⟩ k
    · have hiv : i.val≠t := fun h => hi' (Fin.ext h)
      simpa only [next,Function.update_of_ne hi'] using ih (by omega) j i (by omega)

theorem run_same (ν : Fin m → SparseIntegerLaw (Fin n → ℕ))
    (t : ℕ) (ht : t ≤ m) (h l : Fin n) (i : Fin m) :
    (run ν t).moment (fun G => edge G h i*edge G l i)=
      if i.val<t then (ν i).moment (fun S => (S h:ℚ)*(S l:ℚ)) else 0 := by
  induction t with
  | zero => simp [run,SparseIntegerLaw.dirac_moment,edge]
  | succ t ih =>
    have htm : t < m := by omega
    rw [run,dite_eq_left htm,step_same]
    by_cases hi : i=⟨t,htm⟩
    · subst i
      simp only [Nat.lt_succ_self,ite_true]
    · rw [ite_eq_right hi,ih (by omega)]
      have hv : i.val≠t := fun he => hi (Fin.ext he)
      have hh : i.val<t+1 ↔ i.val<t := by omega
      simp only [hh]

end MetricKMedian.SparseCounts
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseBernoulliSupport
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.SparseBernoulli
open Finset
variable {n d : ℕ}

theorem pair_moment (p : Fin n → ℚ) (hp : ∀ i, 0 ≤ p i ∧ p i ≤ 1)
    (i j : Fin n) (hij : i≠j) :
    (run (d := 2) p hp n).moment (fun q => flag q i*flag q j)=p i*p j := by
  simpa only [prod_pair hij] using subset_moment p hp {i,j} (by simp [hij] : ({i,j} : Finset (Fin n)).card ≤ 2)

end MetricKMedian.SparseBernoulli
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseSignedPartial
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.SparseSignedPartial
open Finset RationalSignedStep
open RationalWeightedStep (point fractional)
open SparseWeightedPartial (features features_single features_pair)
variable {n : ℕ}

 theorem step_pair (β : Fin n → ℚ) 
    (μ : SparseIntegerLaw (Vector ℚ n)) (i j : Fin n) (hij : i ≠ j) :
    (step β μ).moment (fun p => point p i*point p j) ≤
      μ.moment (fun p => point p i*point p j) := by
  have hh := μ.step_moment features (probability β) (probability_unit β)
    (endpoint β) (finSumFinEquiv (Sum.inr (finProdFinEquiv (i,j))))
  simp only [features_pair] at hh
  exact hh.trans_le (μ.moment_mono _ _ (fun k => endpoint_pair β _ i j hij))

 theorem run_pair (β : Fin n → ℚ) 
    (p : Vector ℚ n) (t : ℕ) (i j : Fin n) (hij : i ≠ j) :
    (run β p t).moment (fun q => point q i*point q j) ≤ point p i*point p j := by
  induction t with
  | zero => exact (SparseIntegerLaw.dirac_moment _ _).le
  | succ t ih => exact (step_pair β _ i j hij).trans ih

end MetricKMedian.SparseSignedPartial
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseSignedPreparation
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.SparseSignedPreparation
open Finset
open RationalWeightedStep (point fractional)
variable {n m : ℕ}

theorem kernel_nominal_pair (D : Fin m → Finset (Fin n)) (q : Vector ℚ m)
    (hq : ∀ e, 0 ≤ point q e ∧ point q e ≤ 1) (e f : Fin m) (hef : e≠f) :
    (kernel D q hq).moment (fun z => SparseBernoulli.flag z.2.2 e*SparseBernoulli.flag z.2.2 f)=
      point q e*point q f := by
  rw [kernel,SparseIntegerLaw.prod_moment]
  simp only [SparseBernoulli.pair_moment _ _ _ _ hef,SparseIntegerLaw.moment_const]

end MetricKMedian.SparseSignedPreparation
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_RestrictionProgram
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.Enumeration
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
open MetricKMedian.MaskProgram
def choices {n : ℕ} (T : Finset (Fin n)) (c : ℕ) : List (Finset (Fin n)) :=
  (words c (List.ofFn (T.orderEmbOfFin rfl))).map List.toFinset

def branches (I : Instance) (F : Finset (Fin I.n)) (a : ℕ) : List (Finset (Fin I.n)) :=
  (words a (pairs F)).map (fun ps => witnessedRestriction I F ps.toFinset)
end MetricKMedian.Reduction.Enumeration
end

end OAI
end