Definitions bundle OAIQ037K019 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
import Definitions.Def_OAIQ037K006

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 Ω]

omit [DecidableEq Ω] in
theorem denominator_bound (q : Ω → ℚ) (L : ℕ)
    (hq : ∀ i, ((q i).den:ℤ) ≤ 2^L) :
    denominator q ≤ (2:ℤ)^(L*Fintype.card Ω) := by
  calc
    _ ≤ ∏ _i : Ω, (2:ℤ)^L := prod_le_prod (fun index _ => by positivity) (fun index _ => hq index)
    _ = _ := by simp only [prod_const,card_univ,← pow_mul]

end MetricKMedian.RationalScaling

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 Rows := Binary.IntegerList.Rows

end MetricKMedian.IntegerLaw.ListOperation
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Compression_ComputedElimination
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 eliminateAt_preserves {n d : ℕ} (μ : IntegerLaw (Fin n))
    (v : Fin n → Fin d → ℚ) (z : Fin n → ℤ) (p : Fin n)
    (hp : 0 < z p) (hmin : ∀ i, 0 < z i → ratio μ z p ≤ ratio μ z i)
    (hzsum : ∑ i, z i=0) (hzmoment : ∀ j, ∑ i, (z i:ℚ)*v i j=0)
    (hzsupport : ∀ i, μ.numerator i=0 → z i=0) :
    let ν := eliminateAt μ z p hp hmin hzsum
    ν.numerator p=0 ∧ μ.numerator p ≠ 0 ∧
      (∀ i, μ.numerator i=0 → ν.numerator i=0) ∧
      ν.support ⊆ μ.support.erase p ∧
      ∀ j, (∑ i, ν.rational.weight i*v i j)=∑ i, μ.rational.weight i*v i j := by
  dsimp only
  have hz : (eliminateAt μ z p hp hmin hzsum).numerator p=0 := by
    rw [eliminateAt_numerator,sub_self]
  have hn : μ.numerator p ≠ 0 := by intro hp0; exact hp.ne' (hzsupport p hp0)
  have hs : ∀ i, μ.numerator i=0 → (eliminateAt μ z p hp hmin hzsum).numerator i=0 := by
    intro i hi
    rw [eliminateAt_numerator,hi,hzsupport i hi]
    ring
  refine ⟨hz,hn,hs,?_,?_⟩
  · intro i hi
    have hni := (mem_support _ i).mp hi
    apply mem_erase.mpr
    refine ⟨?_,(μ.mem_support i).mpr ?_⟩
    · intro he; subst i; exact hni hz
    · intro he; exact hni (hs i he)
  · intro j
    have hD : (μ.denominator:ℚ) ≠ 0 := by exact_mod_cast μ.denominator_pos.ne'
    have hpQ : (z p:ℚ) ≠ 0 := by exact_mod_cast hp.ne'
    change (∑ i, (((eliminateAt μ z p hp hmin hzsum).numerator i:ℚ)/
        ((μ.denominator*z p:ℤ):ℚ))*v i j)=_
    simp only [eliminateAt_numerator,Int.cast_mul,Int.cast_sub]
    have heq : ∀ i, (((μ.numerator i:ℚ)*(z p:ℚ)-(μ.numerator p:ℚ)*(z i:ℚ))/
        ((μ.denominator:ℚ)*(z p:ℚ)))*v i j=
        ((μ.numerator i:ℚ)*v i j)/(μ.denominator:ℚ)-
        ((μ.numerator p:ℚ)/(μ.denominator:ℚ)/(z p:ℚ))*((z i:ℚ)*v i j) := by
      intro i
      field_simp
    simp only [heq,sum_sub_distrib,← mul_sum,hzmoment,mul_zero,sub_zero]
    apply sum_congr rfl
    intro i _
    dsimp only [rational]
    ring

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
abbrev Rows := Binary.IntegerList.Rows

end MetricKMedian.IntegerLaw.BinaryCompression
end

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 B (P : ℚ) (d : I → ℚ) (t : ℚ) : ℚ := ∑ i, bCoef P (d i) t

end MetricKMedian.Taper
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_RationalTaper
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 rationalMass (g P : ℚ) (d : I → ℚ) (r : ℚ) : ℚ :=
  ∑ i, g*rationalMarginal P (d i) r

end MetricKMedian.Taper
end
end

end OAI
end

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

variable {I : Type*} [Fintype I] [DecidableEq I]
open MarginalRounding

omit [Fintype I] in
theorem move_left (p : I → ℝ) {i j : I} (hij : i ≠ j) (r t : ℝ) :
    move p i j r t i=p i+t := by simp only [move, sign, ite_true, ite_eq_right hij, sub_zero, mul_one]
omit [Fintype I] in
theorem move_right (p : I → ℝ) {i j : I} (hij : i ≠ j) (r t : ℝ) :
    move p i j r t j=p j-r*t := by simp only [move, sign, ite_eq_right hij.symm, ite_true, zero_sub]; ring
omit [Fintype I] in
theorem move_other (p : I → ℝ) {i j k : I} (hki : k ≠ i) (hkj : k ≠ j) (r t : ℝ) :
    move p i j r t k=p k := by simp only [move, sign, ite_eq_right hki, ite_eq_right hkj, sub_self, mul_zero, add_zero]

omit [Fintype I] in
theorem move_bounds {p : I → ℝ} (hp : ∀ k, 0 ≤ p k) (hp1 : ∀ k, p k ≤ 1)
    {i j : I} (hij : i ≠ j) {r t : ℝ} (hr : 0 < r)
    (ht0 : -down p i j r ≤ t) (ht1 : t ≤ up p i j r) :
    (∀ k, 0 ≤ move p i j r t k) ∧ (∀ k, move p i j r t k ≤ 1) := by
  have hl1 := min_le_left (p i) ((1-p j)/r)
  have hl2 := (le_div_iff₀ hr).mp (min_le_right (p i) ((1-p j)/r))
  have hu1 := min_le_left (1-p i) (p j/r)
  have hu2 := (le_div_iff₀ hr).mp (min_le_right (1-p i) (p j/r))
  have htl := mul_le_mul_of_nonneg_left ht0 hr.le
  have htu := mul_le_mul_of_nonneg_left ht1 hr.le
  change -min (p i) ((1-p j)/r) ≤ t at ht0
  change t ≤ min (1-p i) (p j/r) at ht1
  change r * -min (p i) ((1-p j)/r) ≤ r*t at htl
  change r*t ≤ r*min (1-p i) (p j/r) at htu
  constructor <;> intro k <;> by_cases hki : k=i
  · subst k; rw [move_left p hij]; linarith only [ht0, hl1]
  · by_cases hkj : k=j
    · subst k; rw [move_right p hij]; nlinarith only [htu, hu2]
    · rw [move_other p hki hkj]; exact hp k
  · subst k; rw [move_left p hij]; linarith only [ht1, hu1]
  · by_cases hkj : k=j
    · subst k; rw [move_right p hij]; nlinarith only [htl, hl2]
    · rw [move_other p hki hkj]; exact hp1 k

theorem fractional_subset {p : I → ℝ} {i j : I}
    (hi : i ∈ fractional p) (hj : j ∈ fractional p) (r t : ℝ) :
    fractional (move p i j r t) ⊆ fractional p := by
  intro k hk
  by_cases hki : k=i
  · simpa only [hki] using hi
  by_cases hkj : k=j
  · simpa only [hkj] using hj
  simpa only [mem_fractional, move_other p hki hkj] using hk

end MetricKMedian.WeightedRounding
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 : ℕ}

def edge (G : Graph n m) (h : Fin n) (i : Fin m) : ℚ := if h ∈ G i then 1 else 0

def edgeCode (G : Graph n m) (a : Fin (n*m)) : ℚ :=
  edge G (finProdFinEquiv.symm a).1 (finProdFinEquiv.symm a).2

def features (G : Graph n m) (a : Fin (n*m+(n*m)*(n*m))) : ℚ :=
  Sum.elim (edgeCode G) (fun ij : Fin ((n*m)*(n*m)) =>
    edgeCode G (finProdFinEquiv.symm ij).1*edgeCode G (finProdFinEquiv.symm ij).2)
    (finSumFinEquiv.symm a)

@[simp] theorem features_single (G : Graph n m) (h : Fin n) (i : Fin m) :
    features G (finSumFinEquiv (Sum.inl (finProdFinEquiv (h,i))))=edge G h i := by
  simp only [features,edgeCode,Equiv.symm_apply_apply,Sum.elim_inl]

@[simp] theorem features_pair (G : Graph n m) (h k : Fin n) (i j : Fin m) :
    features G (finSumFinEquiv (Sum.inr (finProdFinEquiv
      (finProdFinEquiv (h,i),finProdFinEquiv (k,j)))))=edge G h i*edge G k j := by
  simp only [features,edgeCode,Equiv.symm_apply_apply,Sum.elim_inr]

def next (G : Graph n m) (S : Finset (Fin n)) (i : Fin m) : Graph n m :=
  Function.update G i S

@[simp] theorem edge_next (G : Graph n m) (S : Finset (Fin n)) (h : Fin n) (i j : Fin m) :
    edge (next G S i) h j=if j=i then (if h∈S then 1 else 0) else edge G h j := by
  by_cases hji : j=i <;> simp [edge,next,hji]

end MetricKMedian.SparseGraph
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseEnumeratedGraph
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.SparseEnumeratedGraph
open Finset
variable {I : Type} [DecidableEq I] {n : ℕ}

def lift (enum : Fin n ≃ I) (G : SparseGraph.Graph n n) : I → Finset I :=
  fun i => (G (enum.symm i)).map enum.toEmbedding

omit [DecidableEq I] in
@[simp] theorem mem_lift (enum : Fin n ≃ I) (G : SparseGraph.Graph n n) (h i : I) :
    h∈lift enum G i ↔ enum.symm h∈G (enum.symm i) := by
  simp only [lift,mem_map,Equiv.toEmbedding_apply]
  constructor
  · rintro ⟨a,ha,he⟩
    simpa only [← he,Equiv.symm_apply_apply] using ha
  · intro ha
    exact ⟨enum.symm h,ha,enum.apply_symm_apply h⟩

end MetricKMedian.SparseEnumeratedGraph
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseHistories
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.SparseHistories
open Finset
variable {α : Type}

def extend (h : History α) (a : α) : History α := (a,h.1::h.2)

end MetricKMedian.SparseHistories
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_RationalSignedStep
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.RationalSignedStep
open Finset RationalWeightedStep
variable {n : ℕ}

theorem endpoint_feasible (β : Fin n → ℚ) 
    (p : Vector ℚ n) (hp : ∀ k, 0 ≤ point p k ∧ point p k ≤ 1) (b : Fin 2) :
    ∀ k, 0 ≤ point (endpoint β p b) k ∧ point (endpoint β p b) k ≤ 1 := by
  by_cases h : Active β p
  · let a := pair β p h
    let r := β a.val.1/β a.val.2
    have hr : 0 < r := pair_ratio_pos β p h
    have hu := up_pos p _ _ r hr a.property.1 a.property.2.1
    have hd := down_pos p _ _ r hr a.property.1 a.property.2.1
    have hpr0 : ∀ k, 0 ≤ realPoint p k := fun k => by
      dsimp only [realPoint]; exact_mod_cast (hp k).1
    have hpr1 : ∀ k, realPoint p k ≤ 1 := fun k => by
      dsimp only [realPoint]; exact_mod_cast (hp k).2
    have hrr : (0:ℝ) < r := by exact_mod_cast hr
    let t := if b=0 then up p a.val.1 a.val.2 r else -down p a.val.1 a.val.2 r
    have ht0 : -down p a.val.1 a.val.2 r ≤ t := by dsimp only [t]; split_ifs <;> linarith
    have ht1 : t ≤ up p a.val.1 a.val.2 r := by dsimp only [t]; split_ifs <;> linarith
    have ht0r : -WeightedRounding.down (realPoint p) a.val.1 a.val.2 (r:ℝ) ≤ (t:ℝ) := by
      rw [← real_down,← Rat.cast_neg]; exact_mod_cast ht0
    have ht1r : (t:ℝ) ≤ WeightedRounding.up (realPoint p) a.val.1 a.val.2 (r:ℝ) := by
      rw [← real_up]; exact_mod_cast ht1
    have hh := WeightedRounding.move_bounds hpr0 hpr1 a.property.2.2.1 hrr ht0r ht1r
    rw [← real_move] at hh
    simp only [realPoint] at hh
    intro k
    simp only [endpoint,dite_eq_left h]
    exact ⟨by exact_mod_cast hh.1 k,by exact_mod_cast hh.2 k⟩
  · simpa only [endpoint,dite_eq_right h] using hp

end MetricKMedian.RationalSignedStep
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_CopyListEncoding
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.RationalPhysicalKernel.CopyList
open Finset Binary Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row indices)
variable {f Δ : ℕ}
local instance instLinearOrderCopyFin_rad9b99_1 : LinearOrder (CopyState.Copy (F:=Fin f) Δ) := copyOrder
abbrev activeOrder (A : Finset (CopyState.Copy (F:=Fin f) Δ)) : LinearOrder ↥A :=
  @Subtype.instLinearOrder _ (copyOrder (F:=Fin f) (Δ:=Δ)) (·∈A)

 def ordinal (A : Finset (CopyState.Copy (F:=Fin f) Δ)) :=
  @Fintype.orderIsoFinOfCardEq A (activeOrder A) _ _ (Fintype.card_coe A)

end MetricKMedian.RationalPhysicalKernel.CopyList
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Probability_BernoulliStepProgram
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.SparseBernoulli.Program
open Binary Binary.PolyProgram Function
structure Context where
  input : Input
  t : ℕ

end MetricKMedian.SparseBernoulli.Program
end

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.RationalSignedStep
open RationalWeightedStep RationalGrid
variable {n : ℕ}

theorem endpoint_grid (β : Fin n → ℚ) 
    (D : ℤ) (hb : ∀ i, At D (β i)) (p : Vector ℚ n)
    (hp : ∀ i, At D (β i*point p i)) (b : Fin 2) :
    ∀ i, At D (β i*point (endpoint β p b) i) := by
  by_cases h : Active β p
  · let a := pair β p h
    let i := a.val.1
    let j := a.val.2
    let r := β i/β j
    let t := if b=0 then up p i j r else -down p i j r
    let q := move p i j r t
    have hij : i≠j := a.property.2.2.1
    have hr : r≠0 := (pair_ratio_pos β p h).ne'
    have he : endpoint β p b=q := by rw [endpoint,dite_eq_left h]
    have hw : β i*point q i+β j*point q j=β i*point p i+β j*point p j :=
      move_pair_weighted β p i j hij (pair_right_ne β p h) t
    have hint : (point q i=0 ∨ point q i=1) ∨ (point q j=0 ∨ point q j=1) := by
      by_cases hb0 : b=0
      · have hh := up_integral p i j hij r hr
        simpa only [q,t,hb0,ite_true] using hh.imp (fun hi => Or.inr hi) (fun hj => Or.inl hj)
      · have hh := down_integral p i j hij r hr
        simpa only [q,t,hb0,ite_false] using hh.imp (fun hi => Or.inl hi) (fun hj => Or.inr hj)
    have hpi : At D (β i*point q i) ∧ At D (β j*point q j) := by
      rcases hint with hi | hj
      · have hai : At D (β i*point q i) := by
          rcases hi with hi | hi
          · rw [hi,mul_zero]; exact RationalGrid.zero _
          · rw [hi,mul_one]; exact hb i
        refine ⟨hai,?_⟩
        have hh := RationalGrid.sub (RationalGrid.add (hp i) (hp j)) hai
        convert hh using 1
        all_goals try with_reducible_and_instances rfl
        linarith
      · have haj : At D (β j*point q j) := by
          rcases hj with hj | hj
          · rw [hj,mul_zero]; exact RationalGrid.zero _
          · rw [hj,mul_one]; exact hb j
        refine ⟨?_,haj⟩
        have hh := RationalGrid.sub (RationalGrid.add (hp i) (hp j)) haj
        convert hh using 1
        all_goals try with_reducible_and_instances rfl
        linarith
    intro k
    rw [he]
    by_cases hki : k=i
    · subst k; exact hpi.1
    by_cases hkj : k=j
    · subst k; exact hpi.2
    simpa only [q,point_move_rest _ _ _ _ hki hkj] using hp k
  · simpa only [endpoint,dite_eq_right h] using hp

theorem endpoint_zero_weight (β : Fin n → ℚ) (p : Vector ℚ n) (b : Fin 2)
    (k : Fin n) (hk : β k=0) : point (endpoint β p b) k=point p k := by
  by_cases h : Active β p
  · let a := pair β p h
    have hi : k≠a.val.1 := by
      intro he
      have hm := a.property.2.2.2
      rw [← he,hk,zero_mul] at hm
      exact lt_irrefl _ hm
    have hj : k≠a.val.2 := by
      intro he
      have hm := a.property.2.2.2
      rw [← he,hk,mul_zero] at hm
      exact lt_irrefl _ hm
    rw [endpoint,dite_eq_left h]
    exact point_move_rest _ _ _ _ hi hj _ _
  · rw [endpoint,dite_eq_right h]

end MetricKMedian.RationalSignedStep

end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_RoundingCoordinateHeight
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.RationalGrid
open Binary

theorem unit_height {D : ℤ} {q : ℚ} {H : ℕ} (hD : D≠0) (hDb : |D|≤(2:ℤ)^H)
    (hq : At D q) (hu : |q|≤1) : HasHeight q H := by
  obtain ⟨A,ha⟩ := hq
  have hDc : (D:ℚ)≠0 := by exact_mod_cast hD
  have he : (A:ℚ)=q*(D:ℚ) := ((eq_div_iff hDc).mp ha).symm
  have hA : |A|≤(2:ℤ)^H := by
    have hh : |(A:ℚ)|≤|(D:ℚ)| := by
      rw [he,abs_mul]
      simpa only [one_mul] using mul_le_mul_of_nonneg_right hu (abs_nonneg (D:ℚ))
    exact (by exact_mod_cast hh : |A|≤|D|).trans hDb
  rw [ha]
  exact Gaussian.ratio_num_den_bound A D hD _ hA hDb

end MetricKMedian.RationalGrid

namespace MetricKMedian.RoundingHeight
open RationalGrid RationalWeightedStep Binary
variable {n : ℕ}

def denominator (β : Fin n → ℚ) (p : Vector ℚ n) : ℤ :=
  RationalScaling.denominator β * RationalScaling.denominator (point p)

end MetricKMedian.RoundingHeight
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseIterationHeight
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.RationalWeightedStep
open Binary
variable {n : ℕ}

theorem up_height (p : Vector ℚ n) (i j : Fin n) (r : ℚ) (A B : ℕ)
    (hp : ∀ i, HasHeight (point p i) A) (hr : HasHeight r B) :
    HasHeight (up p i j r) (A+B+1) := by
  exact ((HasHeight.one 0 |>.sub (hp i)).mono (by omega)).min ((hp j |>.div hr).mono (by omega))
theorem down_height (p : Vector ℚ n) (i j : Fin n) (r : ℚ) (A B : ℕ)
    (hp : ∀ i, HasHeight (point p i) A) (hr : HasHeight r B) :
    HasHeight (down p i j r) (A+B+1) := by
  exact ((hp i).mono (by omega)).min (((HasHeight.one 0 |>.sub (hp j)).div hr).mono (by omega))
end MetricKMedian.RationalWeightedStep

namespace MetricKMedian.RationalSignedStep
open Binary RationalWeightedStep
variable {n : ℕ}
theorem probability_height (β : Fin n → ℚ) (p : Vector ℚ n) (A B : ℕ)
    (hβ : ∀ i, HasHeight (β i) B) (hp : ∀ i, HasHeight (point p i) A) :
    HasHeight (probability β p) (3*(A+2*B+1)+1) := by
  unfold probability
  split_ifs with h
  · let a := pair β p h
    have hr := (hβ a.val.1).div (hβ a.val.2)
    have hu := up_height p a.val.1 a.val.2 _ A (B+B) hp hr
    have hd := down_height p a.val.1 a.val.2 _ A (B+B) hp hr
    convert hd.div (hu.add hd) using 1 <;> first | rfl | ring
  · exact HasHeight.zero _
end MetricKMedian.RationalSignedStep

end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_RoundingRunProgram
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.RoundingProgram
open Binary Binary.PolyProgram Function Polynomial
open SparseIntegerLaw.BinarySparse

def stateBound (L : ℕ) :=
  2*L+1+ (2*(2*(heightBound L+4)+1+supportBound L*(2*(heightBound L+4)+1))+1+
    supportBound L*(2*(L*(2*(3*coordinateBound L+10)+1))+1))

noncomputable def HPoly : Polynomial ℕ :=
  ((3*(CPoly+2*X+1)+1)*NPoly+
    (2*(X+X*X+1)*(X+X*X+1+(2*CPoly)*(2*NPoly+1)))*(2*NPoly+1)*(2*NPoly))*X

end MetricKMedian.RoundingProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_TaperGraphProgram
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.TaperGraphProgram
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseIntegerLaw.BinarySparse

def Input.raw (x : Input) : Raw :=
  (((x.g,x.P),x.Δ),List.ofFn fun i => (List.ofFn (x.d i),List.ofFn fun h => decide (h∈x.own i)))

 theorem marginal_unit (P d r : ℚ) (hP : 0<P) :
    0≤Taper.rationalMarginal P d r ∧ Taper.rationalMarginal P d r≤1 := by
  unfold Taper.rationalMarginal
  exact ⟨le_min (by norm_num) (div_nonneg (le_max_right _ _) hP.le), min_le_left _ _⟩
end MetricKMedian.TaperGraphProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_TaperReindex
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.Taper
open Finset
variable {I J : Type} [Fintype I] [Fintype J]

 theorem b_reindex (e : I ≃ J) (P t : ℚ) (d : J → ℚ) :
    B P (fun i => d (e i)) t=B P d t := e.sum_comp (fun j => bCoef P (d j) t)
 theorem mass_reindex (e : I ≃ J) (g P t : ℚ) (d : J → ℚ) :
    rationalMass g P (fun i => d (e i)) t=rationalMass g P d t :=
  e.sum_comp (fun j => g*rationalMarginal P (d j) t)
end MetricKMedian.Taper
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_CopyGraphProgram
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.RationalPhysicalKernel.CopyGraphProgram
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly Finset
open SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Row )
open CopyList

structure Input where
  f : ℕ
  Δ : ℕ
  d : Fin f → Fin f → ℚ
  g : ℚ
  P : ℚ
  positive : 0<P
  A : Finset (CopyState.Copy (F:=Fin f) Δ)

local instance instLinearOrderSubtypeCopyFinMemFinset {f Δ : ℕ} (A : Finset (CopyState.Copy (F:=Fin f) Δ)) : LinearOrder ↥A := activeOrder A

end MetricKMedian.RationalPhysicalKernel.CopyGraphProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_PhysicalBatchUpdateProgram
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.RationalPhysicalKernel.UpdateProgram
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly Finset FixedBatch
open SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Row )
open CopyList
local instance instLinearOrderSubtypeCopyFinMemFinset {f Δ : ℕ} (A : Finset (CopyState.Copy (F:=Fin f) Δ)) : LinearOrder ↥A := activeOrder A

structure Context extends CopyGraphProgram.Input where
  β : ℚ
  p : ℚ
  φ : ℚ
  hp : 0≤p
  hφ : 0≤φ
  hupper : (1+φ)*p≤1

structure Input where
  ctx : Context
  G : ctx.A → Finset ctx.A

abbrev Input.proposal (x : Input) : RationalBatchData.ProposalProgram.Input (fun c : Context => ↥c.A) where
  ctx := x.ctx
  n := x.ctx.A.card
  enum := ordinal x.ctx.A
  G := x.G
  Δ := x.ctx.Δ
  g := x.ctx.g
  b := x.ctx.β
  p := x.ctx.p
  φ := x.ctx.φ
  hp := x.ctx.hp
  hφ := x.ctx.hφ
  hupper := x.ctx.hupper

end MetricKMedian.RationalPhysicalKernel.UpdateProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_PhysicalRoundProgram
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.RationalPhysicalKernel.RoundProgram
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly Finset
open SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Row )
open CopyList UpdateProgram

def dummy : UpdateProgram.Input where
  ctx := {
    f := 0
    Δ := 0
    d := fun i => Fin.elim0 i
    g := 0
    P := 1
    positive := by norm_num
    A := ∅
    β := 0
    p := 0
    φ := 0
    hp := le_rfl
    hφ := le_rfl
    hupper := by norm_num }
  G := fun _ => ∅

end MetricKMedian.RationalPhysicalKernel.RoundProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_PhysicalHistoriesProgram
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.RationalPhysicalKernel.HistoryProgram
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly Finset
open SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Row )
open CopyList UpdateProgram

def nextCtx (x : Context) (P : ℚ) (hP : 0<P) (A : Finset (CopyState.Copy (F:=Fin x.f) x.Δ)) : Context :=
  {x with toInput := {x.toInput with P:=P,positive:=hP,A:=A}}

end MetricKMedian.RationalPhysicalKernel.HistoryProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_RoundCountsProgram
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.RoundCountsProgram
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row )
open RationalPhysicalKernel CopyList
variable {τ : ℝ}
def Input.raw (x : Input) : Raw := (List.replicate x.f (),((List.ofFn (fun i => List.ofFn (x.d₀ i)),
  List.ofFn (fun c => List.ofFn (x.d c))),List.ofFn x.n))
end MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_PreparedScanProgram
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.PreparedScanProgram
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row )
variable {τ : ℝ}
def Input.raw (x : Input) : Raw := ((List.replicate x.h (),List.ofFn (fun i => (x.orig i).val)),
  ((List.ofFn (fun i => List.ofFn (x.df i)),List.ofFn (fun c => List.ofFn (x.dc c))),
  (x.ns.map List.ofFn,x.budget)))

def Input.item (x : Input) (n : Fin x.f → ℕ) : RoundCountsProgram.Input :=
  ⟨x.f,x.j,(fun a b => x.df (x.orig a) (x.orig b)),(fun c a => x.dc c (x.orig a)),n⟩
def Input.items (x : Input) := x.ns.map x.item

end MetricKMedian.FixedBatch.RationalParameters.PreparedScanProgram
end

end OAI
end