Definitions bundle OAIQ037K018 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
import Definitions.Def_OAIQ037K005

section
-- module Solutions.OAIQ037_KM.KMedian_Compression_GaussianKernel
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 lift_kernel {r n : ℕ} (A : Fin (r+1) → Fin (n+1) → ℚ) (p : Fin (n+1))
    (hp : A 0 p ≠ 0) (z : Fin n → ℚ)
    (hz : ∀ i, ∑ j, residual A p i j*z j=0) :
    ∀ i, ∑ j, A i j*lift A p z j=0 := by
  intro i
  refine Fin.cases ?_ (fun i => ?_) i
  · rw [Fin.sum_univ_succAbove _ p]
    simp only [lift,Fin.insertNth_apply_same,Fin.insertNth_apply_succAbove,mul_neg]
    have hs : A 0 p*(∑ j, A 0 (p.succAbove j)/A 0 p*z j)=
        ∑ j, A 0 (p.succAbove j)*z j := by
      rw [mul_sum]
      apply sum_congr rfl
      intro j _
      field_simp
    rw [hs,neg_add_cancel]
  · rw [Fin.sum_univ_succAbove _ p]
    simp only [lift,Fin.insertNth_apply_same,Fin.insertNth_apply_succAbove]
    have hh := hz i
    simp only [residual,sub_mul,sum_sub_distrib] at hh
    have he : (∑ j, A 0 (p.succAbove j)/A 0 p*A i.succ p*z j)=
        A i.succ p*(∑ j, A 0 (p.succAbove j)/A 0 p*z j) := by
      rw [mul_sum]
      apply sum_congr rfl
      intro j _
      ring
    rw [he] at hh
    linarith

def kernel : (r n : ℕ) → (Fin r → Fin n → ℚ) → Fin n → ℚ
  | 0, _, _ => fun j => if j.val=0 then 1 else 0
  | _+1, 0, _ => Fin.elim0
  | r+1, n+1, A =>
    if h : (univ.filter (fun j => A 0 j ≠ 0)).Nonempty then
      let p := (univ.filter (fun j => A 0 j ≠ 0)).min' h
      lift A p (kernel r n (residual A p))
    else kernel r (n+1) (fun i j => A i.succ j)

theorem kernel_spec (r n : ℕ) (A : Fin r → Fin n → ℚ) (hn : r < n) :
    (∃ j, kernel r n A j ≠ 0) ∧ (∀ i, ∑ j, A i j*kernel r n A j=0) := by
  induction r generalizing n with
  | zero =>
    have hn0 : 0 < n := hn
    refine ⟨⟨⟨0,hn0⟩,?_⟩,fun i => Fin.elim0 i⟩
    simp only [kernel,ite_true,ne_eq,one_ne_zero,not_false_eq_true]
  | succ r ih =>
    cases n with
    | zero => omega
    | succ n =>
      by_cases hh : (univ.filter (fun j => A 0 j ≠ 0)).Nonempty
      · let p := (univ.filter (fun j => A 0 j ≠ 0)).min' hh
        have hp : A 0 p ≠ 0 := (mem_filter.mp (min'_mem _ hh)).2
        have hi := ih n (residual A p) (by omega)
        change (∃ j, (if h : (univ.filter (fun j => A 0 j ≠ 0)).Nonempty then
            lift A ((univ.filter (fun j => A 0 j ≠ 0)).min' h)
              (kernel r n (residual A ((univ.filter (fun j => A 0 j ≠ 0)).min' h)))
            else kernel r (n+1) (fun i j => A i.succ j)) j ≠ 0) ∧ _
        simp only [kernel,dite_eq_left hh]
        exact ⟨lift_nonzero A p _ hi.1,lift_kernel A p hp _ hi.2⟩
      · have hzero : ∀ j, A 0 j=0 := by
          intro j
          by_contra hj
          exact hh ⟨j,mem_filter.mpr ⟨mem_univ _,hj⟩⟩
        have hi := ih (n+1) (fun i j => A i.succ j) (by omega)
        have he : kernel (r+1) (n+1) A=kernel r (n+1) (fun i j => A i.succ j) := by
          rw [kernel,dite_eq_right hh]
        rw [he]
        refine ⟨hi.1,?_⟩
        intro i
        refine Fin.cases ?_ (fun i => hi.2 i) i
        simp only [hzero,zero_mul,sum_const_zero]

end MetricKMedian.Gaussian

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Compression_GaussianCircuit
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 lift_eq_of_kernel {r n : ℕ} (A : Fin (r+1) → Fin (n+1) → ℚ)
    (p : Fin (n+1)) (hp : A 0 p ≠ 0) (v : Fin (n+1) → ℚ)
    (h0 : ∑ j, A 0 j*v j=0) :
    v=lift A p (fun j => v (p.succAbove j)) := by
  have he : v p= -(∑ j, A 0 (p.succAbove j)/A 0 p*v (p.succAbove j)) := by
    rw [Fin.sum_univ_succAbove _ p] at h0
    have hs : A 0 p*(∑ j, A 0 (p.succAbove j)/A 0 p*v (p.succAbove j))=
        ∑ j, A 0 (p.succAbove j)*v (p.succAbove j) := by
      rw [mul_sum]
      apply sum_congr rfl
      intro j _
      field_simp
    apply (mul_left_cancel₀ hp)
    rw [mul_neg,hs]
    linarith
  funext j
  by_cases hj : j=p
  · subst j
    simpa only [lift,Fin.insertNth_apply_same] using he
  · obtain ⟨k,rfl⟩ := Fin.exists_succAbove_eq hj
    simp only [lift,Fin.insertNth_apply_succAbove]

theorem residual_kernel {r n : ℕ} (A : Fin (r+1) → Fin (n+1) → ℚ)
    (p : Fin (n+1)) (hp : A 0 p ≠ 0) (v : Fin (n+1) → ℚ)
    (hv : ∀ i, ∑ j, A i j*v j=0) :
    ∀ i, ∑ j, residual A p i j*v (p.succAbove j)=0 := by
  have he := lift_eq_of_kernel A p hp v (hv 0)
  intro i
  have hi := hv i.succ
  rw [Fin.sum_univ_succAbove _ p] at hi
  have hep := congrFun he p
  simp only [lift,Fin.insertNth_apply_same] at hep
  rw [hep] at hi
  simp only [residual,sub_mul,sum_sub_distrib]
  have hs : (∑ j, A 0 (p.succAbove j)/A 0 p*A i.succ p*v (p.succAbove j))=
      A i.succ p*(∑ j, A 0 (p.succAbove j)/A 0 p*v (p.succAbove j)) := by
    rw [mul_sum]
    apply sum_congr rfl
    intro j _
    ring
  rw [hs]
  linarith

theorem lift_smul {r n : ℕ} (A : Fin (r+1) → Fin (n+1) → ℚ)
    (p : Fin (n+1)) (z : Fin n → ℚ) (t : ℚ) :
    lift A p (fun j => t*z j)=fun j => t*lift A p z j := by
  funext j
  by_cases hj : j=p
  · subst j
    simp only [lift,Fin.insertNth_apply_same]
    rw [mul_neg, mul_sum]
    congr 1
    apply sum_congr rfl
    intro i _
    ring
  · obtain ⟨k,rfl⟩ := Fin.exists_succAbove_eq hj
    simp only [lift,Fin.insertNth_apply_succAbove]

theorem lift_circuit {r n : ℕ} (A : Fin (r+1) → Fin (n+1) → ℚ)
    (p : Fin (n+1)) (hp : A 0 p ≠ 0) (z : Fin n → ℚ)
    (hz : IsCircuit (residual A p) z) : IsCircuit A (lift A p z) := by
  intro v hs hv
  have hsub : ∀ j, z j=0 → v (p.succAbove j)=0 := by
    intro j hj
    apply hs
    simpa only [lift,Fin.insertNth_apply_succAbove] using hj
  obtain ⟨t,ht⟩ := hz (fun j => v (p.succAbove j)) hsub (residual_kernel A p hp v hv)
  refine ⟨t,?_⟩
  have he := lift_eq_of_kernel A p hp v (hv 0)
  rw [show (fun j => v (p.succAbove j))=(fun j => t*z j) from funext ht,lift_smul] at he
  exact congrFun he

theorem kernel_circuit (r n : ℕ) (A : Fin r → Fin n → ℚ) (hn : r < n) :
    (∃ j, kernel r n A j=1) ∧ IsCircuit A (kernel r n A) := by
  induction r generalizing n with
  | zero =>
    let j0 : Fin n := ⟨0,hn⟩
    refine ⟨⟨j0,by simp only [kernel,j0,ite_true]⟩,?_⟩
    intro v hs _
    refine ⟨v j0,?_⟩
    intro j
    by_cases hj : j.val=0
    · have he : j=j0 := Fin.ext hj
      subst j
      simp only [kernel,j0,ite_true,mul_one]
    · have hh := hs j (by simp only [kernel,ite_eq_right hj])
      simp only [kernel,ite_eq_right hj,mul_zero,hh]
  | succ r ih =>
    cases n with
    | zero => omega
    | succ n =>
      by_cases hh : (univ.filter (fun j => A 0 j ≠ 0)).Nonempty
      · let p := (univ.filter (fun j => A 0 j ≠ 0)).min' hh
        have hp : A 0 p ≠ 0 := (mem_filter.mp (min'_mem _ hh)).2
        obtain ⟨⟨j,hj⟩,hc⟩ := ih n (residual A p) (by omega)
        have he : kernel (r+1) (n+1) A=lift A p (kernel r n (residual A p)) := by
          rw [kernel,dite_eq_left hh]
        rw [he]
        refine ⟨⟨p.succAbove j,?_⟩,lift_circuit A p hp _ hc⟩
        simpa only [lift,Fin.insertNth_apply_succAbove] using hj
      · have hi := ih (n+1) (fun i j => A i.succ j) (by omega)
        have he : kernel (r+1) (n+1) A=kernel r (n+1) (fun i j => A i.succ j) := by
          rw [kernel,dite_eq_right hh]
        rw [he]
        refine ⟨hi.1,?_⟩
        intro v hs hv
        exact hi.2 v hs (fun i => hv i.succ)

end MetricKMedian.Gaussian

end OAI
end

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

def kernelVector : (r n : ℕ) → RatMatrix r n → Vector ℚ n
  | 0, _, _ => Vector.ofFn (fun j => if j.val=0 then 1 else 0)
  | _+1, 0, _ => Vector.ofFn Fin.elim0
  | r+1, n+1, A =>
    let a := values A
    if h : (univ.filter (fun j => a 0 j ≠ 0)).Nonempty then
      let p := (univ.filter (fun j => a 0 j ≠ 0)).min' h
      let B := tabulate (residual a p)
      let z := kernelVector r n B
      Vector.ofFn (lift a p (fun j => z[j.val]))
    else kernelVector r (n+1) (tabulate (fun i j => a i.succ j))

theorem kernelVector_eq (r n : ℕ) (A : RatMatrix r n) :
    (fun j : Fin n => (kernelVector r n A)[j.val])=kernel r n (values A) := by
  induction r generalizing n with
  | zero => funext j; simp only [kernelVector,kernel,Vector.getElem_ofFn]
  | succ r ih =>
    cases n with
    | zero => exact funext (fun j => Fin.elim0 j)
    | succ n =>
      by_cases h : (univ.filter (fun j => values A 0 j ≠ 0)).Nonempty
      · rw [kernelVector,kernel,dite_eq_left h,dite_eq_left h]
        have hh := ih n (tabulate (residual (values A) ((univ.filter (fun j => values A 0 j ≠ 0)).min' h)))
        simp only [values_tabulate] at hh
        funext j
        simp only [Vector.getElem_ofFn]
        rw [hh]
      · rw [kernelVector,kernel,dite_eq_right h,dite_eq_right h]
        have hh := ih (n+1) (tabulate (fun i j => values A i.succ j))
        simpa only [values_tabulate] using hh

end MetricKMedian.Gaussian

end OAI
end

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

namespace OAI

namespace MetricKMedian.RationalScaling
open Finset
variable {Ω : Type} [Fintype Ω] [DecidableEq Ω]

theorem numerator_bound (q : Ω → ℚ) (L : ℕ)
    (hqnum : ∀ i, |(q i).num| ≤ (2:ℤ)^L)
    (hqden : ∀ i, ((q i).den:ℤ) ≤ (2:ℤ)^L) (i : Ω) :
    |numerator q i| ≤ (2:ℤ)^(L*(Fintype.card Ω+1)) := by
  have hprod0 : 0 ≤ ∏ j ∈ univ.erase i, ((q j).den:ℤ) :=
    prod_nonneg (fun _ _ => by positivity)
  have hp : (∏ j ∈ univ.erase i, ((q j).den:ℤ)) ≤ (2:ℤ)^(L*Fintype.card Ω) := by
    calc
      _ ≤ ∏ _j ∈ univ.erase i, (2:ℤ)^L :=
        prod_le_prod (fun _ _ => by positivity) (fun index _ => hqden index)
      _ = (2:ℤ)^(L*(univ.erase i).card) := by rw [prod_const,pow_mul]
      _ ≤ _ := pow_le_pow_right₀ (by norm_num) (Nat.mul_le_mul_left L (card_erase_le.trans_eq (card_univ)))
  rw [numerator,abs_mul,abs_of_nonneg hprod0]
  calc
    _ ≤ (2:ℤ)^L * (2:ℤ)^(L*Fintype.card Ω) :=
      mul_le_mul (hqnum i) hp hprod0 (by positivity)
    _ = _ := by rw [← pow_add]; congr 1; ring

end MetricKMedian.RationalScaling

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

def computedIntegerKernel (r n : ℕ) (V : Fin r → Fin n → ℤ) : Fin n → ℤ :=
  let A := tabulate (fun i j => (V i j:ℚ))
  let q := kernelVector r n A
  let b := Vector.ofFn (RationalScaling.numerator (fun j => q[j.val]))
  fun j => b[j.val]

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

def computedAffineKernel {n d : ℕ} (μ : IntegerLaw (Fin n))
    (v : Fin n → Fin d → ℤ) : Fin n → ℤ :=
  let zi := Gaussian.computedIntegerKernel (d+1) μ.support.card (activeMatrix μ v)
  let z := Vector.ofFn (Compression.extendVector μ.support zi)
  fun i => z[i.val]

end MetricKMedian.IntegerLaw

end OAI
end

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

namespace OAI

namespace MetricKMedian.RationalLaw
open Finset

def scaledFeatures {n d : ℕ} (v : Fin n → Fin d → ℚ) : Fin n → Fin d → ℤ :=
  let M := Vector.ofFn (fun i => Vector.ofFn (fun j => RationalScaling.numerator (fun i => v i j) i))
  fun i j => M[i.val][j.val]

@[simp] theorem scaledFeatures_eq {n d : ℕ} (v : Fin n → Fin d → ℚ)
    (i : Fin n) (j : Fin d) :
    scaledFeatures v i j=RationalScaling.numerator (fun i => v i j) i := by
  simp only [scaledFeatures,Vector.getElem_ofFn]

end MetricKMedian.RationalLaw

end OAI
end

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

namespace OAI

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

def branchNumerator (p : Fin n → ℚ) (i : Fin n) (b : Fin 2) : ℤ :=
  if b=0 then RationalScaling.numerator p i
    else RationalScaling.denominator p-RationalScaling.numerator p i

end MetricKMedian.IntegerBranching

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_RationalTaperAffine
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.Taper
open Finset

variable {I : Type*} [Fintype I]

def A (P : ℚ) (d : I → ℚ) (t : ℚ) : ℚ := ∑ i, aCoef P (d i) t

end MetricKMedian.Taper
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_RationalPhysicalKernel
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.RationalPhysicalKernel
open Finset
variable {F : Type} [LinearOrder F] [Fintype F] {Δ : ℕ}

local instance instLinearOrderCopy : LinearOrder (CopyState.Copy (F := F) Δ) := copyOrder

def own (A : Finset (CopyState.Copy (F := F) Δ)) (i : A) : Finset A :=
  univ.filter (fun h => h.val.1=i.val.1)

def enumeration (A : Finset (CopyState.Copy (F := F) Δ)) : Fin A.card ≃ A :=
  (Fintype.orderIsoFinOfCardEq A (Fintype.card_coe A)).toEquiv

end MetricKMedian.RationalPhysicalKernel
end
end

end OAI
end