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

import Mathlib
import Definitions.Def_MetricKMedian
import Definitions.Def_OAIQ037K075
import Definitions.Def_OAIQ037K076

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseOuterMoments
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.SparseOuterLaw
open Finset
open SparseGridRounding (base)
open SparseSignedPreparation (State)
variable {n m : ℕ}

theorem activation_variance (D : Fin m → Finset (Fin n)) (c q : Fin m → ℚ)
    (hc : ∀ e, 0 ≤ c e ∧ c e ≤ 1) (hq : ∀ e, 0 ≤ q e) (e : Fin m) (i : Fin n) :
    (law D c q hc hq).realIndex.variance
      (fun a => (activation D q (law D c q hc hq).states[a.val] e i:ℝ)) ≤
      ((if i∈D e then q e else 0:ℚ):ℝ) := by
  apply FiniteLaw.adjacent_variance _ _
    (m := ((if i∈D e then (base q e:ℚ) else 0:ℚ):ℝ)) ?_ ?_
    (activation_real_mean D c q hc hq e i)
  · split_ifs <;> positivity
  · intro a _
    rcases activation_adjacent D c q hc hq a e i with hh | hh
    · exact Or.inl (by exact_mod_cast hh)
    · exact Or.inr (by exact_mod_cast hh)

theorem deficit_variance (D : Fin m → Finset (Fin n)) (c q : Fin m → ℚ) (g : ℚ)
    (hc : ∀ e, 0 ≤ c e ∧ c e ≤ 1) (hq : ∀ e, 0 ≤ q e) (i : Fin n) :
    (law D c q hc hq).realIndex.variance (fun a => (deficit D q g (law D c q hc hq).states[a.val] i:ℝ)) ≤
      (g:ℝ)^2*(targetMean D q i:ℝ) := by
  have hh := FiniteLaw.variance_sum_le (law D c q hc hq).realIndex
    (fun e a => (activation D q (law D c q hc hq).states[a.val] e i:ℝ))
    (fun e => ((if i∈D e then q e else 0:ℚ):ℝ))
    (fun e => ((if i∈D e then q e else 0:ℚ):ℝ))
    (fun e => activation_real_mean D c q hc hq e i)
    (fun e => activation_variance D c q hc hq e i)
    (fun e f hef => activation_real_pair D c q hc hq e f hef i i)
  simp only [deficit,Rat.cast_mul,Rat.cast_sum,FiniteLaw.variance_mul,targetMean]
  exact mul_le_mul_of_nonneg_left hh (sq_nonneg _)

theorem clipping_budget (D : Fin m → Finset (Fin n)) (c q : Fin m → ℚ) (g : ℚ)
    (hc : ∀ e, 0 ≤ c e ∧ c e ≤ 1) (hq : ∀ e, 0 ≤ q e)
    (δ : Fin n → ℝ) {γ : ℝ} (hg : 0 ≤ g) (hγ : 0 < γ) (hδ : ∀ i, 0 ≤ δ i)
    (hmean : ∀ i, (g:ℝ)*(targetMean D q i:ℝ)=(1+γ)*δ i)
    (hsmall : ∀ i, (1+γ)*δ i ≤ 1/4) :
    1-4*(g:ℝ)*(1+γ)/γ ≤ (law D c q hc hq).realIndex.prob (fun a =>
      (∑ i, ((deficit D q g (law D c q hc hq).states[a.val] i:ℝ)-
        min (deficit D q g (law D c q hc hq).states[a.val] i:ℝ) (1/2))) ≤ γ*∑ i,δ i) := by
  classical
  apply FiniteLaw.clipping_budget _ _ δ (by exact_mod_cast hg) hγ hδ
  · intro i
    rw [deficit_mean,hmean]
    exact hsmall i
  · intro i
    have hh := deficit_variance D c q g hc hq i
    have he : (g:ℝ)^2*(targetMean D q i:ℝ)=(g:ℝ)*(1+γ)*δ i := by
      rw [pow_two,mul_assoc,hmean]
      ring
    exact hh.trans_eq he

end MetricKMedian.SparseOuterLaw
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparsePreparedProbability
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.SparsePrepared
open Finset SparseOuterLaw
open SparseSignedPreparation (State)
variable {n m : ℕ}

theorem opening_probability (D : Fin m → Finset (Fin n)) (c q : Fin m → ℚ) (Δ : ℕ)
    (hc : ∀ e,0 ≤ c e ∧ c e ≤ 1) (hq : ∀ e,0 ≤ q e) (g : ℚ)
    (δ : Fin n → ℝ) {γ B : ℝ} (hg : 0 < g) (hγ : 0 < γ)
    (heven : Even Δ) (hunit : g*(Δ:ℚ)=1) (hδ : ∀ j,0 ≤ δ j)
    (hmean : ∀ j,(g:ℝ)*(targetMean D q j:ℝ)=(1+γ)*δ j)
    (hsmall : ∀ j,(1+γ)*δ j ≤ 1/4)
    (hplan : (g:ℝ)*(((n:ℚ)*(Δ:ℚ)+(∑ e,SparseSignedPreparation.signed D c e*q e):ℚ):ℝ)=
      B-γ*∑ j,δ j) :
    1-4*(g:ℝ)*(1+γ)/γ ≤ (SparseOuterLaw.law D c q hc hq).realIndex.prob (fun a =>
      (g:ℝ)*(opening D c q Δ (SparseOuterLaw.law D c q hc hq).states[a.val]:ℝ) ≤ B+3*(g:ℝ)) := by
  classical
  apply (SparseOuterLaw.clipping_budget D c q g hc hq δ hg.le hγ hδ hmean hsmall).trans
  apply FiniteLaw.prob_mono
  intro a ha
  have hh0 := opening_le D c q Δ hc hq a
  have hh : (opening D c q Δ (SparseOuterLaw.law D c q hc hq).states[a.val]:ℝ) ≤
      (((n:ℚ)*(Δ:ℚ)+(∑ e,SparseSignedPreparation.signed D c e*q e):ℚ):ℝ)+3+
      ∑ j,(discarded D q Δ (SparseOuterLaw.law D c q hc hq).states[a.val] j:ℝ) := by
    exact_mod_cast hh0
  have hhg := mul_le_mul_of_nonneg_left hh (show (0:ℝ) ≤ g by exact_mod_cast hg.le)
  have hdiscard : (g:ℝ)*(∑ j,(discarded D q Δ (SparseOuterLaw.law D c q hc hq).states[a.val] j:ℝ))=
      ∑ j,((deficit D q g (SparseOuterLaw.law D c q hc hq).states[a.val] j:ℝ)-
        min (deficit D q g (SparseOuterLaw.law D c q hc hq).states[a.val] j:ℝ) (1/2)) := by
    rw [mul_sum]
    exact sum_congr rfl (fun j _ => discarded_mass D q Δ _ j hg heven hunit)
  rw [mul_add,mul_add,hplan,hdiscard] at hhg
  linarith only [hhg,ha]

theorem total_deviation (D : Fin m → Finset (Fin n)) (c q : Fin m → ℚ) (Δ : ℕ)
    (hc : ∀ e,0 ≤ c e ∧ c e ≤ 1) (hq : ∀ e,0 ≤ q e) (g : ℚ)
    (p δ : Fin n → ℝ) {γ : ℝ} (hg : 0 < g) (hγ : 0 ≤ γ)
    (heven : Even Δ) (hunit : g*(Δ:ℚ)=1) (hδ : ∀ j,0 ≤ δ j)
    (hδhalf : ∀ j,δ j ≤ 1/2) (hp : ∀ j,p j+δ j=1)
    (hmean : ∀ j,(g:ℝ)*(targetMean D q j:ℝ)=(1+γ)*δ j) (j : Fin n) :
    (SparseOuterLaw.law D c q hc hq).realIndex.expect (fun a =>
      |(g:ℝ)*(total D q Δ (SparseOuterLaw.law D c q hc hq).states[a.val] j:ℝ)-p j|) ≤
      γ*δ j+Real.sqrt ((g:ℝ)*(1+γ)*δ j) := by
  have hvar := SparseOuterLaw.deficit_variance D c q g hc hq j
  have he : (g:ℝ)^2*(targetMean D q j:ℝ)=(g:ℝ)*(1+γ)*δ j := by
    rw [pow_two,mul_assoc,hmean]
    ring
  rw [he] at hvar
  have hh := FiniteLaw.rescaling_noise (SparseOuterLaw.law D c q hc hq).realIndex
    (fun a => (deficit D q g (SparseOuterLaw.law D c q hc hq).states[a.val] j:ℝ))
    (hδ j) (hδhalf j) hγ (show (0:ℝ) ≤ g by exact_mod_cast hg.le)
    ((SparseOuterLaw.deficit_mean D c q g hc hq j).trans (hmean j)) hvar
  apply le_trans (le_of_eq ?_) hh
  apply FiniteLaw.expect_congr_support
  intro a _
  rw [total_deficit_identity D q Δ _ j hg heven hunit]
  congr 1
  linarith only [hp j]

end MetricKMedian.SparsePrepared
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseCoupledPreparation
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.SparsePrepared
open Finset SparseOuterLaw
open SparseSignedPreparation (State)
variable {n m f : ℕ}

theorem request_mean (D : Fin m → Finset (Fin n)) (a q : Fin m → ℚ) (Δ : ℕ)
    (ha : ∀ e, 0 ≤ a e ∧ a e ≤ 1) (hq : ∀ e, 0 ≤ q e) {g : ℝ} (hg : 0 ≤ g)
    (j : Fin n) (e : Fin m) :
    (SparseOuterLaw.law D a q ha hq).realIndex.expect (fun b =>
      g * (requests D q Δ (SparseOuterLaw.law D a q ha hq).states[b.val] j e : ℝ)) ≤
      if j ∈ D e then g * (q e : ℝ) else 0 := by
  calc
    _ ≤ (SparseOuterLaw.law D a q ha hq).realIndex.expect (fun b =>
        g * (activation D q (SparseOuterLaw.law D a q ha hq).states[b.val] e j : ℝ)) := by
      apply FiniteLaw.expect_mono
      intro b
      apply mul_le_mul_of_nonneg_left _ hg
      have h := requests_le D q Δ (SparseOuterLaw.law D a q ha hq).states[b.val] j e
      have he := activationCount_cast D q (SparseOuterLaw.law D a q ha hq).states[b.val] e j
      have hr : (requests D q Δ (SparseOuterLaw.law D a q ha hq).states[b.val] j e : ℚ) ≤
          activation D q (SparseOuterLaw.law D a q ha hq).states[b.val] e j := by
        rw [← he]
        exact_mod_cast h
      exact_mod_cast hr
    _ = _ := by
      rw [FiniteLaw.expect_mul, activation_real_mean]
      split_ifs <;> simp

noncomputable def coupled
    (D : Fin m → Finset (Fin n)) (a q : Fin m → ℚ) (Δ : ℕ)
    (P : Fin n → Finset (Fin f)) (y : Fin f → ℚ) (p : Fin n → ℚ)
    (ha : ∀ e, 0 ≤ a e ∧ a e ≤ 1) (hq : ∀ e, 0 ≤ q e) (g : ℚ)
    (δ : Fin n → ℝ) (γ B : ℝ)
    (hg : 0 < g) (hγ : 0 < γ) (hγ1 : γ ≤ 1) (heven : Even Δ)
    (hunit : g * (Δ : ℚ) = 1)
    (hy : ∀ i, 0 ≤ y i) (hp : ∀ j, 0 < p j) (hm : ∀ j, ∑ i ∈ P j, y i = p j)
    (hδ : ∀ j, 0 ≤ δ j) (hδ1 : ∀ j, δ j ≤ 1/8)
    (hpunit : ∀ j, (p j : ℝ) + δ j = 1)
    (hmean : ∀ j, (g : ℝ) * (targetMean D q j : ℝ) = (1+γ) * δ j)
    (hplan : (g : ℝ) * (((n : ℚ) * (Δ : ℚ) +
      (∑ e, SparseSignedPreparation.signed D a e * q e) : ℚ) : ℝ) = B - γ * ∑ j, δ j) :
    Preparation.CoupledLaw D (fun e => (a e : ℝ)) (fun e => (g : ℝ) * (q e : ℝ))
      P (fun i => (y i : ℝ)) (fun j => (p j : ℝ)) δ (g : ℝ) γ B Δ := by
  let μ := SparseOuterLaw.law D a q ha hq
  let z := fun b : Fin μ.length => μ.states[b.val]
  have hgR : (0 : ℝ) < g := by exact_mod_cast hg
  have huR : (g : ℝ) * (Δ : ℝ) = 1 := by exact_mod_cast hunit
  refine {
    Ω := Fin μ.length
    ν := μ.realIndex
    κ := fun b => SparseRescaledInner.encodedLaw P y p (total D q Δ (z b))
    O := fun b => outsideCount q (z b)
    N := fun b => nominalMass q (g : ℝ) (z b)
    R := fun b => requests D q Δ (z b)
    K := fun b => total D q Δ (z b)
    C := fun b => SparseRescaledInner.encodedCount P y p (total D q Δ (z b))
    open_cap := ?_
    open_zero := ?_
    nominal_nonneg := fun b _ e => nominalMass_nonneg q hgR.le (z b) e
    nominal_cap := fun b _ e => nominalMass_cap D a q ha hq hgR.le b e
    nominal_mean := fun e => nominalMass_mean D a q ha hq (g : ℝ) e
    nominal_variance := fun e => nominalMass_variance D a q ha hq (g : ℝ) e
    nominal_pair := fun e h heh => nominalMass_pair D a q ha hq (g : ℝ) e h heh
    request_cap := ?_
    request_target := ?_
    request_mean := fun j e => request_mean D a q Δ ha hq hgR.le j e
    exact_total := fun b j => exact_total D q Δ (z b) j
    half := fun b j => total_half D q Δ (z b) j hgR heven huR
    total_cap := fun b j => total_le D q Δ (z b) j
    total_deviation := ?_
    pieces := fun b ξ hξ => SparseRescaledInner.encoded_pieces P y p _ Δ hy hp hm
      (total_le D q Δ (z b)) ξ hξ
    piece_mean := fun b j i => SparseRescaledInner.encoded_mean P y p _ Δ (g : ℝ) hy hp hm
      (total_le D q Δ (z b)) j i
    piece_pair := fun b u v huv => SparseRescaledInner.encoded_pair P y p _ Δ (g : ℝ) hy hp hm
      (total_le D q Δ (z b)) u v huv
    piece_variance := fun b u => SparseRescaledInner.encoded_variance P y p _ Δ (g : ℝ) hy hp hm
      (total_le D q Δ (z b)) u
    budget := ?_ }
  · intro b _ e he
    have he' : q e ≤ (Δ : ℚ) := by
      have hr : (q e : ℝ) ≤ (Δ : ℝ) := (mul_le_mul_iff_right₀ hgR).mp (he.trans_eq huR.symm)
      exact_mod_cast hr
    have hcap := outsideCount_le_at D a q ha hq Δ b e he'
    exact (mul_le_mul_of_nonneg_left (by exact_mod_cast hcap) hgR.le).trans_eq huR
  · intro b _ e he
    have hz : q e = 0 := by
      have hr : (q e : ℝ) = 0 := (mul_eq_zero.mp he).resolve_left hgR.ne'
      exact_mod_cast hr
    exact Nat.eq_zero_of_le_zero (outsideCount_le_at D a q ha hq 0 b e (by simp [hz]))
  · intro b _ j e
    exact (requests_le D q Δ (z b) j e).trans (activationCount_le D a q ha hq b e j)
  · intro b j e hj
    have h := requests_le D q Δ (z b) j e
    have hz := activationCount_support D a q ha hq b e j hj
    exact Nat.eq_zero_of_le_zero (h.trans_eq hz)
  · intro j
    exact total_deviation D a q Δ ha hq g (fun j => (p j : ℝ)) δ hg hγ.le heven hunit hδ
      (fun j => (hδ1 j).trans (by norm_num)) hpunit hmean j
  · have hsmall : ∀ j, (1+γ) * δ j ≤ 1/4 := by
      intro j
      calc
        _ ≤ 2 * δ j := mul_le_mul_of_nonneg_right (by linarith only [hγ1]) (hδ j)
        _ ≤ 1/4 := by linarith only [hδ1 j]
    have h := opening_probability D a q Δ ha hq g δ hg hγ heven hunit hδ hmean hsmall hplan
    simpa only [opening_cast] using h

end MetricKMedian.SparsePrepared
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_RationalSupplierPreparation
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.Preparation.RationalSuppliers
open Finset SupplierStars
variable {f n : ℕ}

noncomputable def coupled (y : Fin f → ℚ) (P A : Fin n → Finset (Fin f))
    (p c : Fin n → ℚ) (γ g : ℚ) (Δ : ℕ)
    (hy : ∀ i, 0 ≤ y i) (hp : ∀ t, 0 < p t)
    (hP : Pairwise (fun s t => Disjoint (P s) (P t)))
    (hm : ∀ t, ∑ i ∈ P t, y i=p t) (hc : ∀ t, ∑ i ∈ A t, y i=c t)
    (hc0 : ∀ t, 0 ≤ c t) (hc1 : ∀ t, c t ≤ 1/8) (hunit : ∀ t, p t+c t=1)
    (hγ : 0 < γ) (hγ1 : γ ≤ 1) (hg : 0 < g) (heven : Even Δ) (hgrid : g*(Δ:ℚ)=1) :
    CoupledLaw (targets A) flag
      (weight (fun i => (y i : ℝ)) P A (fun t => (c t : ℝ)) γ)
      P (fun i => (y i : ℝ)) (fun t => (p t : ℝ)) (fun t => (c t : ℝ))
      g γ (∑ i, (y i : ℝ)) Δ := by
  have hcR : ∀ t, ∑ i ∈ A t, (y i : ℝ)=(c t : ℝ) := by
    intro t
    exact_mod_cast hc t
  have huR : ∀ t, (p t : ℝ)+(c t : ℝ)=1 := by
    intro t
    exact_mod_cast hunit t
  have hmR : ∀ t, ∑ i ∈ P t, (y i : ℝ)=(p t : ℝ) := by
    intro t
    exact_mod_cast hm t
  have mean : ∀ t, (g : ℝ)*(SparseOuterLaw.targetMean (D A) (q y P A c γ g) t : ℝ) =
      (1+(γ:ℝ))*(c t : ℝ) := by
    intro t
    simp only [SparseOuterLaw.targetMean, Rat.cast_sum, mul_sum]
    calc
      _ = ∑ e, if t ∈ targets A (index e) then
          weight (fun i => (y i : ℝ)) P A (fun t => (c t : ℝ)) γ (index e) else 0 := by
        apply sum_congr rfl
        intro e _
        change (g:ℝ) * ((if t ∈ targets A (index e) then q y P A c γ g e else 0 : ℚ):ℝ) = _
        split_ifs <;> simp only [scaled_q y P A c γ g hg.ne', Rat.cast_zero, mul_zero]
      _ = _ := by
        rw [(index (f:=f) (n:=n)).sum_comp (fun e => if t ∈ targets A e then
          weight (fun i => (y i : ℝ)) P A (fun t => (c t : ℝ)) γ e else 0)]
        exact targeted_weight _ _ _ _ _ hP hcR t
  have planned : (g : ℝ) * (((n:ℚ)*(Δ:ℚ) +
      (∑ e, SparseSignedPreparation.signed (D A) a e * q y P A c γ g e) : ℚ) : ℝ) =
      (∑ i, (y i : ℝ)) - (γ:ℝ)*∑ t, (c t : ℝ) := by
    have hgR : (g:ℝ)*(Δ:ℝ)=1 := by exact_mod_cast hgrid
    simp only [Rat.cast_add, Rat.cast_mul, Rat.cast_natCast, Rat.cast_sum, mul_add, mul_sum]
    have hf : (g:ℝ)*((n:ℝ)*(Δ:ℝ))=(n:ℝ) := by nlinarith only [hgR]
    rw [hf]
    have he : (∑ e, (g:ℝ) * ((SparseSignedPreparation.signed (D A) a e : ℝ) *
        (q y P A c γ g e : ℝ))) = ∑ e,
        (flag (index e) - ((targets A (index e)).card : ℝ)) *
        weight (fun i => (y i : ℝ)) P A (fun t => (c t : ℝ)) γ (index e) := by
      apply sum_congr rfl
      intro e _
      rw [mul_left_comm, scaled_q y P A c γ g hg.ne']
      simp only [SparseSignedPreparation.signed, Rat.cast_sub, Rat.cast_natCast, D, a,
        Function.comp_apply, flag_cast]
    rw [he, (index (f:=f) (n:=n)).sum_comp (fun e =>
      (flag e - ((targets A e).card : ℝ)) *
        weight (fun i => (y i : ℝ)) P A (fun t => (c t : ℝ)) γ e)]
    simpa only [Fintype.card_fin, mul_sum] using raw_identity (fun i => (y i : ℝ)) P A
      (fun t => (c t : ℝ)) (γ:ℝ) hP hcR (fun t => by rw [hmR]; exact huR t)
  let L := SparsePrepared.coupled (D A) a (q y P A c γ g) Δ P y p a_bounds
    (q_nonneg y P A c γ g hy hc0 hγ.le hg.le) g (fun t => (c t : ℝ)) γ
    (∑ i, (y i : ℝ)) hg (by exact_mod_cast hγ) (by exact_mod_cast hγ1) heven hgrid
    hy hp hm (fun t => by exact_mod_cast hc0 t) (fun t => by
      have hh : (c t : ℝ) ≤ ((1/8:ℚ):ℝ) := Rat.cast_le.mpr (hc1 t)
      norm_num at hh ⊢
      exact hh)
    huR mean planned
  have L' : CoupledLaw (targets A ∘ index) (flag ∘ index)
      (weight (fun i => (y i : ℝ)) P A (fun t => (c t : ℝ)) γ ∘ index)
      P (fun i => (y i : ℝ)) (fun t => (p t : ℝ)) (fun t => (c t : ℝ))
      g γ (∑ i, (y i : ℝ)) Δ := by
    exact L.castWeights (funext (fun e => flag_cast (index e)))
      (funext (fun e => scaled_q y P A c γ g hg.ne' e))
  exact L'.reindexStars index

end MetricKMedian.Preparation.RationalSuppliers
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_RationalSupplierScan
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.Preparation.RationalSuppliers
open Finset SupplierStars

namespace Data
variable {f n j : ℕ} {τ : ℝ} (D : Data f n) (qR : FixedBatch.RationalParameters τ)

noncomputable def coupled (heven : Even qR.Δ) := RationalSuppliers.coupled D.y D.P D.A D.p D.c D.γ qR.g qR.Δ
  D.hy D.hp D.hP D.hm D.hc D.hc0 D.hc1 D.hunit D.hγ D.hγ1 (FixedParameters.positive qR) heven (FixedParameters.grid qR)

end Data
end MetricKMedian.Preparation.RationalSuppliers
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Reduction_LocalCompletionProgram
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.Program
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
open InstanceProgram (Raw view)
open MetricKMedian.MaskProgram
open Preparation.RationalNearest.MaskProgram (erase erase_view insert insert_view)
open Enumeration

@[fun_prop] theorem radiiData_poly : Poly radiiData := by unfold radiiData; apply list_map <;> fun_prop

abbrev LocalRaw := (Raw × (Row × Row)) × (List ℚ × ℚ)
def candidatesData (x : LocalRaw × ℕ) : Row :=
  (indices x.1.1.2.1).map (fun a => get x.1.1.2.1 a &&
    decide (getDist (x.1.1.1,(x.2,a))≤x.1.2.2*(x.1.2.1[x.2]?.getD 0)))
@[fun_prop] theorem candidatesData_poly : Poly candidatesData := by unfold candidatesData; apply list_map <;> fun_prop

def weightData (x : LocalRaw × (ℕ × ℕ)) : ℚ :=
  ((indices x.1.1.1.1.1).map (fun j => if get x.1.1.1.1.1 j &&
    decide (3*getDist (x.1.1.1,(j,x.2.1))≤x.1.2.1[x.2.1]?.getD 0) then
      nearestData (x.1.1.1.2.2[j]?.getD [],insert (x.2.2,x.1.1.2.2)) else 0)).sum
@[fun_prop] theorem weightData_poly : Poly weightData := by unfold weightData; apply comp rat_sum; apply list_map <;> fun_prop

def pickData (x : List ℚ × Row) : Row :=
  if x.2.any id then InstanceProgram.singletonRaw (x.2,MetricKMedian.MaskProgram.nearest x) else x.2.map (fun _ => false)
@[fun_prop] theorem pickData_poly : Poly pickData := by unfold pickData; fun_prop

def localData (x : LocalRaw × ℕ) : Row :=
  pickData ((indices x.1.1.2.1).map (fun a => weightData (x.1,(x.2,a))),candidatesData x)
@[fun_prop] theorem localData_poly : Poly localData := by unfold localData; apply comp pickData_poly; apply pair; apply list_map <;> fun_prop; fun_prop

def unionData (x : Row × Table) : Row := (indices x.1).map (fun i => (x.2.map (fun S => get S i)).any id)
@[fun_prop] theorem unionData_poly : Poly unionData := by unfold unionData; apply list_map; apply comp bool_any; apply list_map <;> fun_prop; fun_prop

def completionData (x : LocalRaw × Row) : Row := union (x.1.1.2.2,unionData (x.2,
  (Preparation.RationalUnitInput.Program.ranks x.2).map (fun t => localData (x.1,t))))
@[fun_prop] theorem completionData_poly : Poly completionData := by
  unfold completionData
  have hm : Poly (fun x : LocalRaw × Row => (Preparation.RationalUnitInput.Program.ranks x.2).map (fun t => localData (x.1,t))) := by apply list_map <;> fun_prop
  fun_prop
end MetricKMedian.Reduction.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Reduction_ReductionOutcomesProgram
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.Program
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
open InstanceProgram (Raw view)
open Enumeration
def completionsData (δ : ℚ) (b : ℕ) (x : Raw × (Row × Row)) : Table :=
  (choicesRaw b x.2.2).flatMap (fun H => (choicesRaw b x.2.1).map (fun B =>
    completionData (((x.1,(x.2.1,B)),(radiiData (x.1,x.2.2),δ)),diff (x.2.2,H))))
@[fun_prop] theorem completionsData_poly (δ : ℚ) (b : ℕ) : Poly (completionsData δ b) := by
  unfold completionsData; apply list_flatMap; apply list_map <;> fun_prop; fun_prop
def outcomesData (δ : ℚ) (c b : ℕ) (x : Raw × (Row × Row)) : Table :=
  x.2.2::(endpointsData c (x.1,x.2.2)).flatMap (fun U => U::completionsData δ b (x.1,(x.2.1,U)))
@[fun_prop] theorem outcomesData_poly (δ : ℚ) (c b : ℕ) : Poly (outcomesData δ c b) := by
  unfold outcomesData
  have h : Poly (fun x : (Raw × (Row × Row)) × Row => x.2::completionsData δ b (x.1.1,(x.1.2.1,x.2))) := by
    have hh := comp (list_cons (α := Row)) (pair (snd : Poly (fun x : (Raw × (Row × Row)) × Row =>x.2))
      (show Poly (fun x : (Raw × (Row × Row)) × Row => completionsData δ b (x.1.1,(x.1.2.1,x.2))) from by fun_prop))
    exact hh
  have hh : Poly (fun x : Raw × (Row × Row) => (endpointsData c (x.1,x.2.2)).flatMap (fun U => U::completionsData δ b (x.1,(x.2.1,U)))) := by
    apply list_flatMap <;> fun_prop
  have hhh := comp (list_cons (α := Row)) (pair (show Poly (fun x : Raw × (Row × Row) => x.2.2) from by fun_prop) hh)
  exact hhh
end MetricKMedian.Reduction.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_BranchProgram
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.Program
open Finset Preparation Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView)
open InstanceProgram (Raw view)
open Completion.Rational.BestProgram (card card_view)
open Enumeration
namespace Branch
def view (B : Branch) : Raw × Row := (InstanceProgram.view B.original,setView B.facilities)
def encode (B : Branch) : List Bool := enc B.view
noncomputable def allowedProgram : PolyProgram encode encodeBool (fun B => decide B.allowed) :=
  (by fun_prop : Poly (fun x : Raw × Row => decide (x.1.2.1 ≤ card x.2))).program.recode view (fun _ => rfl) (fun B => by
    apply congrArg encodeBool
    simp only [view,InstanceProgram.view,card_view,allowed]
    rfl)
def restrictedData (x : Raw × Row) : Raw := ((x.1.1.1,x.2),x.1.2)
@[fun_prop] theorem restrictedData_poly : Poly restrictedData := by unfold restrictedData; fun_prop
end Branch
end MetricKMedian.Reduction.Program
end

end OAI
end