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

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

noncomputable def K (p z : ℝ) (b : Bool → ℝ) (s : Bool) (r : ℝ) : ℝ :=
  C p s - k p s - b s * r + (8 / 5) * z

noncomputable def centered (p m a z : ℝ) (b : Bool → ℝ)
    (s : Bool) (D q Z : ℝ) : ℝ :=
  (m * D + b s * (D + 1)) * q +
    D * (C p s * psi p q + a * (1 - q) - C p s) -
    ((2 / 5) * D + 8 / 5) * z - C p s + k p s -
    (k p s - (C p s * psi p q - (1 - q))) * Z

end MetricKMedian.FiniteComparison

namespace MetricKMedian.FiniteComparison

noncomputable def rowValue {I : Type*} [Fintype I] (π Z q : I → ℝ)
    (p m a z : ℝ) (b : Bool → ℝ) (s : Bool) (D R : ℝ) : ℝ :=
  C p s * (1 - average π q) * R +
    (m * D + b s * (D + 1)) * average π q - C p s * (D + 1) -
    average π (fun t => (1 - q t) * max (Z t - a * D) 0) -
    ((2 / 5) * D + 8 / 5) * z

end MetricKMedian.FiniteComparison


end
end

end OAI
end

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

noncomputable def uprime (p m z : ℝ) (b : Bool → ℝ) (s : Bool) (D r : ℝ) : ℝ :=
  ((m * D + b s * (D + 1)) * r - ((2 / 5) * D + 8 / 5) * z) / (C p s * r)

end MetricKMedian.FiniteComparison


end
end

end OAI
end

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

open Analytic

noncomputable def actualB (x w : ℝ) (s : Bool) : ℝ :=
  (2-ScalarTransfer.bit s)*P x*(x+w)

end MetricKMedian.FiniteComparison

end
end

end OAI
end

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

namespace OAI

namespace MetricKMedian.Compression
open Finset Matrix
variable {R C : Type} [Fintype R] [Fintype C] [DecidableEq C]

theorem gram_cramer_bound (A : Matrix R C ℤ) (w : R → ℤ) (M : ℤ) (hM : 0 ≤ M)
    (hA : ∀ r c, |A r c| ≤ M) (hw : ∀ r, |w r| ≤ M) (c : C) :
    |((A.transpose*A).cramer (A.transpose*ᵥw)) c| ≤ (Nat.factorial (Fintype.card C):ℤ)*
      ((Fintype.card R:ℤ)*M^2)^(Fintype.card C) := by
  rw [Matrix.cramer_apply]
  have hentry : ∀ i j, |((A.transpose*A).updateCol c (A.transpose*ᵥw)) i j| ≤
      (Fintype.card R:ℤ)*M^2 := by
    intro i j
    by_cases hj : j=c
    · subst j
      simpa using gram_rhs_bound A w M hM hA hw i
    · simpa [Matrix.updateCol_apply,hj] using gram_entry_bound A M hM hA i j
  simpa only [AbsoluteValue.abs_apply,nsmul_eq_mul] using
    (Matrix.det_le (abv := AbsoluteValue.abs) hentry)

end MetricKMedian.Compression

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Compression_AffineListOperations
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.ListOperation
open Binary Gaussian
open Finset
abbrev Row := Binary.IntegerList.Row

end MetricKMedian.IntegerLaw.ListOperation
end

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
abbrev LawData := ListPivot.LawData

end MetricKMedian.IntegerLaw.BinaryCompression
end

end OAI
end

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

namespace OAI

namespace MetricKMedian

namespace FiniteLaw
variable {Ω : Type*} [Fintype Ω]
noncomputable def prob (μ : FiniteLaw Ω) (E : Ω → Prop) [DecidablePred E] : ℝ :=
  μ.expect (fun ω => if E ω then 1 else 0)

theorem expect_mono (μ : FiniteLaw Ω) {f h : Ω → ℝ} (hfh : ∀ ω, f ω ≤ h ω) :
    μ.expect f ≤ μ.expect h := by
  exact Finset.sum_le_sum (fun ω _ => mul_le_mul_of_nonneg_left (hfh ω) (μ.nonneg ω))

theorem expect_nonneg (μ : FiniteLaw Ω) {f : Ω → ℝ} (hf : ∀ ω, 0 ≤ f ω) : 0 ≤ μ.expect f := by
  exact Finset.sum_nonneg (fun ω _ => mul_nonneg (μ.nonneg ω) (hf ω))

theorem expect_mul_right (μ : FiniteLaw Ω) (f : Ω → ℝ) (c : ℝ) :
    μ.expect (fun ω => f ω * c) = μ.expect f * c := by
  simp only [expect, ← mul_assoc, Finset.sum_mul]

theorem expect_sum (μ : FiniteLaw Ω) {I : Type*} (s : Finset I) (f : Ω → I → ℝ) :
    μ.expect (fun ω => ∑ i ∈ s, f ω i) = ∑ i ∈ s, μ.expect (fun ω => f ω i) := by
  simp only [expect, Finset.mul_sum]
  exact Finset.sum_comm

theorem prob_mono (μ : FiniteLaw Ω) {E F : Ω → Prop} [DecidablePred E] [DecidablePred F]
    (hEF : ∀ ω, E ω → F ω) : μ.prob E ≤ μ.prob F := by
  apply μ.expect_mono
  intro ω
  split_ifs with he hf hf <;> try norm_num
  exact False.elim (hf (hEF ω he))

end FiniteLaw

end MetricKMedian

end OAI
end

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

namespace OAI

namespace MetricKMedian.FiniteLaw
variable {Ω Ξ : Type*} [Fintype Ω] [Fintype Ξ]

omit [Fintype Ξ] in
theorem variance_nonneg (μ : FiniteLaw Ω) (f : Ω → ℝ) : 0 ≤ μ.variance f :=
  μ.expect_nonneg (fun _ => sq_nonneg _)

omit [Fintype Ξ] in
theorem sq_expect_le_expect_sq (μ : FiniteLaw Ω) (f : Ω → ℝ) :
    (μ.expect f)^2 ≤ μ.expect (fun ω => (f ω)^2) := by
  have hv := μ.variance_nonneg f
  rw [variance_eq] at hv
  linarith only [hv]

omit [Fintype Ξ] in

theorem prob_le_expect_div (μ : FiniteLaw Ω) (f : Ω → ℝ) {t : ℝ}
    (hf : ∀ ω, 0 ≤ f ω) (ht : 0 < t) :
    μ.prob (fun ω => t ≤ f ω) ≤ μ.expect f/t := by
  classical
  apply (le_div_iff₀ ht).mpr
  unfold prob
  rw [← expect_mul_right]
  apply μ.expect_mono
  intro ω
  split_ifs with h
  · simpa only [one_mul] using h
  · simpa only [zero_mul] using hf ω

end MetricKMedian.FiniteLaw

end OAI
end

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

namespace OAI

namespace MetricKMedian.FiniteLaw

noncomputable def dirac {Ω : Type*} [Fintype Ω] [DecidableEq Ω] (ω₀ : Ω) : FiniteLaw Ω where
  weight ω := if ω=ω₀ then 1 else 0
  nonneg ω := by split_ifs <;> norm_num
  total := by simp

theorem expect_dirac {Ω : Type*} [Fintype Ω] [DecidableEq Ω] (ω₀ : Ω) (f : Ω → ℝ) :
    (dirac ω₀).expect f = f ω₀ := by simp [expect, dirac]

end MetricKMedian.FiniteLaw

end OAI
end

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

namespace OAI

namespace MetricKMedian.FiniteLaw
variable {Ω Ξ : Type*} [Fintype Ω] [Fintype Ξ]

omit [Fintype Ξ] in
 theorem prob_compl (μ : FiniteLaw Ω) (E : Ω → Prop) [DecidablePred E] :
    μ.prob (fun ω => ¬E ω)=1-μ.prob E := by
  have hp : ∀ ω, (if ¬E ω then (1:ℝ) else 0)=1-(if E ω then 1 else 0) := by
    intro ω; split_ifs <;> simp_all
  simp only [prob, hp, expect_sub, expect_const]

end MetricKMedian.FiniteLaw

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_PreparationMoments
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.FiniteLaw
open Finset
variable {Ω I : Type*} [Fintype Ω] [Fintype I]

omit [Fintype I] in
 theorem expect_abs_centered_le_sqrt (μ : FiniteLaw Ω) (X : Ω → ℝ) :
    μ.expect (fun ω => |X ω-μ.expect X|) ≤ Real.sqrt (μ.variance X) := by
  have hs := μ.sq_expect_le_expect_sq (fun ω => |X ω-μ.expect X|)
  simp only [sq_abs] at hs
  exact (Real.le_sqrt (μ.expect_nonneg (fun _ => abs_nonneg _)) (μ.variance_nonneg X)).mpr hs

end MetricKMedian.FiniteLaw
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Probability_Conditioning
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.FiniteLaw
open Finset
variable {Ω : Type*} [Fintype Ω]

noncomputable def condition (μ : FiniteLaw Ω) (P : Ω → Prop) [DecidablePred P]
    (hP : 0 < μ.prob P) : FiniteLaw Ω where
  weight := fun ω => if P ω then μ.weight ω/μ.prob P else 0
  nonneg := fun ω => by split_ifs; exact div_nonneg (μ.nonneg ω) hP.le; exact le_rfl
  total := by
    have he : ∀ ω, (if P ω then μ.weight ω/μ.prob P else 0)=
        (μ.weight ω*(if P ω then 1 else 0))/μ.prob P := by
      intro ω; split_ifs <;> simp
    simp only [he, ← sum_div]
    change μ.prob P/μ.prob P=1
    exact div_self hP.ne'

end MetricKMedian.FiniteLaw
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Probability_FiniteClipping
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.FiniteLaw
open Finset
variable {Ω I : Type*} [Fintype Ω] [Fintype I]

omit [Fintype I] in
 theorem nonneg_expect_zero_support (μ : FiniteLaw Ω) (X : Ω → ℝ)
    (hX : ∀ ω, 0 ≤ X ω) (hmean : μ.expect X=0) :
    ∀ ω, 0 < μ.weight ω → X ω=0 := by
  intro ω hω
  have hh := single_le_sum (s := univ) (f := fun ξ => μ.weight ξ*X ξ)
    (fun ξ _ => mul_nonneg (μ.nonneg ξ) (hX ξ)) (mem_univ ω)
  change μ.weight ω*X ω ≤ μ.expect X at hh
  rw [hmean] at hh
  exact le_antisymm (by nlinarith only [hh, hω]) (hX ω)

omit [Fintype I] in
 theorem expected_half_clip (μ : FiniteLaw Ω) (Z : Ω → ℝ)
    {v : ℝ} (hmean : μ.expect Z ≤ 1/4) (hvar : μ.variance Z ≤ v) :
    μ.expect (fun ω => Z ω-min (Z ω) (1/2)) ≤ 4*v := by
  have he := μ.expect_mono (fun ω => half_clip_point (z := Z ω) hmean)
  rw [expect_mul] at he
  exact he.trans (mul_le_mul_of_nonneg_left hvar (by norm_num))

theorem clipping_budget (μ : FiniteLaw Ω) (Z : I → Ω → ℝ) (c : I → ℝ)
    {g γ : ℝ} (hg : 0 ≤ g) (hγ : 0 < γ)
    (hc : ∀ i, 0 ≤ c i)
    (hmean : ∀ i, μ.expect (Z i) ≤ 1/4)
    (hvar : ∀ i, μ.variance (Z i) ≤ g*(1+γ)*c i) :
    1-4*g*(1+γ)/γ ≤ μ.prob (fun ω =>
      (∑ i, (Z i ω-min (Z i ω) (1/2))) ≤ γ*∑ i, c i) := by
  classical
  let W : Ω → ℝ := fun ω => ∑ i, (Z i ω-min (Z i ω) (1/2))
  have hW : ∀ ω, 0 ≤ W ω := by
    intro ω
    exact sum_nonneg (fun i _ => sub_nonneg.mpr (min_le_left _ _))
  have hE : μ.expect W ≤ 4*g*(1+γ)*∑ i, c i := by
    change μ.expect (fun ω => ∑ i, (Z i ω-min (Z i ω) (1/2))) ≤ _
    rw [expect_sum, mul_sum]
    exact sum_le_sum (fun i _ => (expected_half_clip μ (Z i) (hmean i) (hvar i)).trans_eq (by ring))
  have hC : 0 ≤ ∑ i, c i := sum_nonneg (fun i _ => hc i)
  have hρ : 0 ≤ 4*g*(1+γ)/γ := by positivity
  have hfail : μ.prob (fun ω => γ*∑ i, c i < W ω) ≤ 4*g*(1+γ)/γ := by
    rcases hC.eq_or_lt with hz | hz
    · have hzero : μ.expect W=0 := le_antisymm (by simpa only [← hz, mul_zero] using hE)
        (μ.expect_nonneg hW)
      have hs := μ.nonneg_expect_zero_support W hW hzero
      have he0 : μ.prob (fun ω => γ*∑ i, c i < W ω)=0 := by
        change μ.expect (fun ω => if γ*∑ i, c i < W ω then 1 else 0)=0
        calc
          _ = μ.expect (fun _ => 0) := μ.expect_congr_support (fun ω hω => by
            rw [hs ω hω, ← hz, mul_zero, ite_eq_right (lt_irrefl 0)])
          _ = 0 := μ.expect_const _
      rw [he0]
      exact hρ
    · have he := μ.prob_le_expect_div W hW (mul_pos hγ hz)
      have hp := μ.prob_mono (E := fun ω => γ*∑ i, c i < W ω)
        (F := fun ω => γ*∑ i, c i ≤ W ω) (fun _ h => h.le)
      calc
        _ ≤ μ.expect W/(γ*∑ i, c i) := hp.trans he
        _ ≤ (4*g*(1+γ)*∑ i, c i)/(γ*∑ i, c i) := div_le_div_of_nonneg_right hE (by positivity)
        _ = _ := by field_simp
  have hcomp := μ.prob_compl (fun ω => γ*∑ i, c i < W ω)
  simp only [not_lt] at hcomp
  change 1-4*g*(1+γ)/γ ≤ μ.prob (fun ω => W ω ≤ γ*∑ i, c i)
  rw [hcomp]
  linarith only [hfail]

end MetricKMedian.FiniteLaw
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Probability_FiniteJoint
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.FiniteLaw
variable {Ω Ξ : Type*} [Fintype Ω] [Fintype Ξ]

noncomputable def joint (μ : FiniteLaw Ω) (κ : Ω → FiniteLaw Ξ) : FiniteLaw (Ω × Ξ) where
  weight z := μ.weight z.1*(κ z.1).weight z.2
  nonneg z := mul_nonneg (μ.nonneg z.1) ((κ z.1).nonneg z.2)
  total := by
    rw [Fintype.sum_prod_type]
    simp only [← Finset.mul_sum, total, mul_one]

end MetricKMedian.FiniteLaw
end
end

end OAI
end

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

namespace OAI

namespace MetricKMedian.FiniteLaw

variable {Ω Ξ : Type*} [Fintype Ω] [Fintype Ξ]

theorem expect_bind (μ : FiniteLaw Ω) (κ : Ω → FiniteLaw Ξ) (f : Ξ → ℝ) :
    (μ.bind κ).expect f = μ.expect (fun ω => (κ ω).expect f) := by
  simp only [bind, expect, Finset.sum_mul, mul_assoc, Finset.mul_sum]
  exact Finset.sum_comm

theorem property_bind (μ : FiniteLaw Ω) (κ : Ω → FiniteLaw Ξ) (R : Ξ → Prop)
    (hR : ∀ ω, 0 < μ.weight ω → ∀ ξ, 0 < (κ ω).weight ξ → R ξ) :
    ∀ ξ, 0 < (μ.bind κ).weight ξ → R ξ := by
  intro ξ hξ
  by_contra hn
  have hpoint : ∀ ω, μ.weight ω*(κ ω).weight ξ=0 := by
    intro ω
    by_cases hω : 0 < μ.weight ω
    · have hk : (κ ω).weight ξ=0 := by
        apply le_antisymm _ ((κ ω).nonneg ξ)
        by_contra hneg
        exact hn (hR ω hω ξ (lt_of_not_ge hneg))
      rw [hk, mul_zero]
    · rw [le_antisymm (le_of_not_gt hω) (μ.nonneg ω), zero_mul]
  have hz : (μ.bind κ).weight ξ=0 := Finset.sum_eq_zero (fun ω _ => hpoint ω)
  rw [hz] at hξ
  exact lt_irrefl _ hξ

noncomputable def map [DecidableEq Ξ] (μ : FiniteLaw Ω) (f : Ω → Ξ) : FiniteLaw Ξ :=
  μ.bind (fun ω => dirac (f ω))

theorem expect_map [DecidableEq Ξ] (μ : FiniteLaw Ω) (f : Ω → Ξ) (g : Ξ → ℝ) :
    (μ.map f).expect g=μ.expect (fun ω => g (f ω)) := by
  rw [map, expect_bind]
  simp_rw [expect_dirac]

theorem property_map [DecidableEq Ξ] (μ : FiniteLaw Ω) (f : Ω → Ξ) (R : Ξ → Prop)
    (hR : ∀ ω, 0 < μ.weight ω → R (f ω)) :
    ∀ ξ, 0 < (μ.map f).weight ξ → R ξ := by
  apply property_bind
  intro ω hω ξ hξ
  by_cases heq : ξ=f ω
  · rw [heq]; exact hR ω hω
  · simp only [dirac, ite_eq_right heq] at hξ
    exact False.elim (lt_irrefl _ hξ)

end MetricKMedian.FiniteLaw

end OAI
end

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

open Analytic

variable {I : Type*}

noncomputable def savingsFraction (g : ℝ) : ℝ :=
  min 1 (2 * P 1 * g / (1 + 1 / g))

end MetricKMedian.PhysicalPotential
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_CopyState
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.CopyState
open Finset PhysicalPotential
variable {F : Type*} [DecidableEq F]
variable (Δ : ℕ)

variable [Fintype F]

def next (A erased : Finset (Copy (F := F) Δ)) (O : Finset F) := (A \ erased) ∪ resets Δ O

end MetricKMedian.CopyState
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_CopyRound
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.CopyState
open Finset FixedBatch
variable {F : Type*} [DecidableEq F] [Fintype F] (Δ : ℕ)

variable {Δ}

noncomputable def roundErased (A : Finset (Copy (F := F) Δ)) (G : A → Finset A)
    (H : Finset A) (Z : Finset (HeavyAction (graphActions G) H)) : Finset (Copy (F := F) Δ) :=
  (Z.biUnion (heavyActions (graphActions G) H).erase).image Subtype.val

noncomputable def roundOpened (A : Finset (Copy (F := F) Δ)) (G : A → Finset A)
    (H : Finset A) (Z : Finset (HeavyAction (graphActions G) H)) : Finset F :=
  (selectedSources G H Z).image (fun i => i.val.1)

end MetricKMedian.CopyState
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_CopyTransport
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.CopyState
open Finset PhysicalPotential
variable {F : Type*} [DecidableEq F] {Δ : ℕ}

@[simp] theorem mem_localSet (A S : Finset (Copy (F := F) Δ)) (i : A) :
    i ∈ localSet A S ↔ i.val ∈ S := by simp [localSet]

end MetricKMedian.CopyState
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_PhysicalRound
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.CopyState
open Finset PhysicalPotential FixedBatch
variable {F : Type*} [DecidableEq F] [Fintype F] {Δ : ℕ}

noncomputable def forcedGroups (A : Finset (Copy (F := F) Δ)) (H : Finset A) : Finset F :=
  H.image (fun i => i.val.1)

noncomputable def forcedAlive (A S : Finset (Copy (F := F) Δ)) (H : Finset A) : Finset A :=
  (localSet A S).filter (fun i => i.val.1 ∈ forcedGroups A H)

noncomputable def roundAlive (A S : Finset (Copy (F := F) Δ)) (G : A → Finset A)
    (H : Finset A) (Z : Finset (HeavyAction (graphActions G) H)) (x g : ℝ) (d : F → ℝ) :
    Finset (Copy (F := F) Δ) :=
  (nextAliveAt (heavyActions (graphActions G) H) (Analytic.coefficient x (mass g S))
    (fun i => d i.val.1) (localSet A S \ forcedAlive A S H) Z).image Subtype.val

end MetricKMedian.CopyState
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_PhysicalState
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.CopyState
open Finset PhysicalPotential FixedBatch Analytic
variable {F J X : Type*} [Fintype F] [DecidableEq F] [Fintype J] [DecidableEq J]
variable [PseudoMetricSpace X] {Δ : ℕ}

abbrev State (F J : Type*) (Δ : ℕ) := Finset (Copy (F := F) Δ) × (J → Finset (Copy (F := F) Δ))

noncomputable def advance (s : State F J Δ) (G : s.1 → Finset s.1) (H : Finset s.1)
    (Z : Finset (HeavyAction (graphActions G) H)) (x g : ℝ)
    (d : J → F → ℝ) : State F J Δ :=
  (next Δ s.1 (roundErased s.1 G H Z) (roundOpened s.1 G H Z),
    fun j => roundAlive s.1 (s.2 j) G H Z x g (d j))

end MetricKMedian.CopyState
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_StateInvariants
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.CopyState
open Finset PhysicalPotential FixedBatch
variable {F J X : Type*} [Fintype F] [DecidableEq F] [Fintype J] [DecidableEq J]
variable [PseudoMetricSpace X] {Δ : ℕ}

def Valid (g : ℝ) (location : F → X) (client : J → X) (R : J → ℝ)
    (S₀ : J → Finset (Copy (F := F) Δ)) (s : State F J Δ) : Prop :=
  1 ≤ mass g s.1 ∧
    (∀ j, s.2 j ⊆ s.1) ∧ (∀ j, s.2 j ⊆ S₀ j) ∧
    ∀ j, (¬∃ f ∈ integral Δ s.1, dist (client j) (location f) ≤ 5*R j) → S₀ j ⊆ s.1

end MetricKMedian.CopyState
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_CopyNearestProgram
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.FixedBatch.RationalParameters.CopyNearestProgram
open Finset Binary Binary.Automatic Binary.Automatic.Poly
open RationalPhysicalKernel RationalPhysicalKernel.CopyList
open SparseGraph.ListOperation (Row indices)
variable {τ : ℝ}
local instance instLinearOrderCopyFin {f Δ : ℕ} : LinearOrder (CopyState.Copy (F:=Fin f) Δ) := copyOrder

end MetricKMedian.FixedBatch.RationalParameters.CopyNearestProgram
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}

def weights (x : LawData) : List ℚ := x.2.map (fun z : ℤ => (z:ℚ)/(x.1:ℚ))

end MetricKMedian.SparseIntegerLaw.BinarySparse
end

end OAI
end