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

import Mathlib
import Definitions.Def_MetricKMedian
import Definitions.Def_OAIQ037K037
import Definitions.Def_OAIQ037K038
import Definitions.Def_OAIQ037K039
import Definitions.Def_OAIQ037K040

section
-- module Solutions.OAIQ037_KM.KMedian_Compression_RationalKernelHeightSupport
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.Gaussian
open Finset

theorem rational_input_kernel_bounds (r n L : ℕ) (A : Fin r → Fin n → ℚ)
    (hn : r < n) (hnum : ∀ i j, |(A i j).num| ≤ (2:ℤ)^L)
    (hden : ∀ i j, ((A i j).den:ℤ) ≤ (2:ℤ)^L) :
    let z := kernel r n A
    ∀ j, |(z j).num| ≤ (2:ℤ)^(2*r*(r+L*(n+1))) ∧
      ((z j).den:ℤ) ≤ (2:ℤ)^(2*r*(r+L*(n+1))) := by
  dsimp only
  let V : Fin r → Fin n → ℤ := fun i => RationalScaling.numerator (A i)
  let D : Fin r → ℚ := fun i => RationalScaling.denominator (A i)
  have hD : ∀ i, D i ≠ 0 := by
    intro i
    apply ne_of_gt
    dsimp only [D]
    exact_mod_cast RationalScaling.denominator_pos (A i)
  have hV : ∀ i j, (V i j:ℚ)=A i j*D i := fun i j =>
    RationalScaling.numerator_cast (A i) j
  have hVb : ∀ i j, |V i j| ≤ (2:ℤ)^(L*(n+1)) := by
    intro i j
    simpa only [Fintype.card_fin] using
      RationalScaling.numerator_bound (A i) L (hnum i) (hden i) j
  have hki : ∀ z : Fin n → ℚ,
      (∀ i, ∑ j, (V i j:ℚ)*z j=0) ↔ (∀ i, ∑ j, A i j*z j=0) := by
    intro z
    simp only [hV]
    exact row_scaling_kernel_iff A D hD z
  obtain ⟨⟨w,hw⟩,hc⟩ := kernel_circuit r n A hn
  have hk := (kernel_spec r n A hn).2
  have hcV : IsCircuit (fun i j => (V i j:ℚ)) (kernel r n A) := by
    intro v hv hkV
    exact hc v hv ((hki v).mp hkV)
  obtain ⟨U,hUw,hU,hz⟩ := circuit_integer_ratio V _ (L*(n+1)) hVb
    ((hki _).mpr hk) hcV w hw
  intro j
  rw [hz j]
  exact ratio_num_den_bound (U j) (U w) hUw _ (hU j) (hU w)

end MetricKMedian.Gaussian
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Compression_GaussianResidualHeight
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.Gaussian
open Finset

 theorem rational_circuit_ratio (r n L : ℕ) (A : Fin r → Fin n → ℚ)
    (hnum : ∀ i j, |(A i j).num| ≤ (2:ℤ)^L)
    (hden : ∀ i j, ((A i j).den:ℤ) ≤ (2:ℤ)^L)
    (z : Fin n → ℚ) (hc : IsCircuit A z) (hk : ∀ i, ∑ j, A i j*z j=0)
    (w : Fin n) (hw : z w=1) :
    ∃ U : Fin n → ℤ, U w ≠ 0 ∧
      (∀ j, |U j| ≤ (2:ℤ)^(2*r*(r+L*(n+1)))) ∧
      ∀ j, z j=(U j:ℚ)/(U w:ℚ) := by
  let V : Fin r → Fin n → ℤ := fun i => RationalScaling.numerator (A i)
  let D : Fin r → ℚ := fun i => RationalScaling.denominator (A i)
  have hD : ∀ i, D i ≠ 0 := by
    intro i
    apply ne_of_gt
    dsimp only [D]
    exact_mod_cast RationalScaling.denominator_pos (A i)
  have hV : ∀ i j, (V i j:ℚ)=A i j*D i := fun i j => RationalScaling.numerator_cast (A i) j
  have hVb : ∀ i j, |V i j| ≤ (2:ℤ)^(L*(n+1)) := by
    intro i j
    simpa only [Fintype.card_fin] using RationalScaling.numerator_bound (A i) L (hnum i) (hden i) j
  have hki : ∀ v : Fin n → ℚ,
      (∀ i, ∑ j, (V i j:ℚ)*v j=0) ↔ (∀ i, ∑ j, A i j*v j=0) := by
    intro v
    simp only [hV]
    exact row_scaling_kernel_iff A D hD v
  have hcV : IsCircuit (fun i j => (V i j:ℚ)) z := by
    intro v hv hkv
    exact hc v hv ((hki v).mp hkv)
  exact circuit_integer_ratio V z (L*(n+1)) hVb ((hki z).mpr hk) hcV w hw

namespace ResidualCertificate
variable {R N r n : ℕ} {A : Fin R → Fin N → ℚ} {B : Fin r → Fin n → ℚ}

 theorem entry_height (P : ResidualCertificate A B) (L : ℕ)
    (hnum : ∀ i j, |(A i j).num| ≤ (2:ℤ)^L)
    (hden : ∀ i j, ((A i j).den:ℤ) ≤ (2:ℤ)^L) (i : Fin r) (j : Fin n) :
    |(B i j).num| ≤ (2:ℤ)^(residualHeight R N L) ∧
      ((B i j).den:ℤ) ≤ (2:ℤ)^(residualHeight R N L) := by
  obtain ⟨U,hUw,hU,hz⟩ := rational_circuit_ratio P.pivotCols.card R L
    (fun c t => A t (P.pivotCols.orderEmbOfFin rfl c))
    (fun c t => hnum t _) (fun c t => hden t _)
    (P.coefficient i) (P.circuit i)
    (fun c => P.annihilates i _ (P.pivotCols.orderEmbOfFin_mem rfl c)) (P.row i) (P.normalized i)
  have hc : P.pivotCols.card ≤ N := (card_le_card (subset_univ P.pivotCols)).trans_eq (card_fin N)
  have hpow : 2*P.pivotCols.card*(P.pivotCols.card+L*(R+1)) ≤ 2*N*(N+L*(R+1)) :=
    Nat.mul_le_mul (Nat.mul_le_mul_left 2 hc) (Nat.add_le_add_right hc _)
  have hUb : ∀ t, |U t| ≤ (2:ℤ)^(2*N*(N+L*(R+1))) := fun t =>
    (hU t).trans (pow_le_pow_right₀ (by norm_num) hpow)
  rw [P.represents]
  exact combination_height R (2*N*(N+L*(R+1))) L (fun t => A t (P.col j))
    (P.coefficient i) U (P.row i) hUw hUb hz (fun t => hnum t _) (fun t => hden t _)

end ResidualCertificate
end MetricKMedian.Gaussian
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Compression_GaussianStates
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.Gaussian
open Finset

 theorem kernelStates_entry_height (R N L : ℕ) (A : RatMatrix R N)
    (hnum : ∀ i j, |(values A i j).num| ≤ (2:ℤ)^L)
    (hden : ∀ i j, ((values A i j).den:ℤ) ≤ (2:ℤ)^L)
    (B : MatrixState) (hB : B ∈ kernelStates R N A) (i : Fin B.rows) (j : Fin B.cols) :
    |(values B.data i j).num| ≤ (2:ℤ)^(residualHeight R N L) ∧
      ((values B.data i j).den:ℤ) ≤ (2:ℤ)^(residualHeight R N L) := by
  obtain ⟨P⟩ := kernelStates_certificate (values A) R N A (ResidualCertificate.initial _) B hB
  exact P.entry_height L hnum hden i j

 theorem kernelStates_return_height (R N L : ℕ) (A : RatMatrix R N) (hRN : R<N)
    (hnum : ∀ i j, |(values A i j).num| ≤ (2:ℤ)^L)
    (hden : ∀ i j, ((values A i j).den:ℤ) ≤ (2:ℤ)^L)
    (B : MatrixState) (hB : B ∈ kernelStates R N A) (j : Fin B.cols) :
    |((kernelVector B.rows B.cols B.data)[j.val]).num| ≤ (2:ℤ)^(returnHeight R N L) ∧
      (((kernelVector B.rows B.cols B.data)[j.val]).den:ℤ) ≤ (2:ℤ)^(returnHeight R N L) := by
  obtain ⟨P⟩ := kernelStates_certificate (values A) R N A (ResidualCertificate.initial _) B hB
  have hrow : B.rows ≤ R := by
    simpa only [Fintype.card_fin] using Fintype.card_le_of_injective P.row P.row_injective
  have hcol : B.cols ≤ N := by
    simpa only [Fintype.card_fin] using Fintype.card_le_of_injective P.col P.col_injective
  have hentry := kernelStates_entry_height R N L A hnum hden B hB
  have hb := rational_input_kernel_bounds B.rows B.cols (residualHeight R N L) (values B.data)
    (kernelStates_underdetermined R N A hRN B hB) (fun i j => (hentry i j).1) (fun i j => (hentry i j).2) j
  have hp : 2*B.rows*(B.rows+residualHeight R N L*(B.cols+1)) ≤ returnHeight R N L := by
    exact Nat.mul_le_mul (Nat.mul_le_mul_left 2 hrow)
      (Nat.add_le_add hrow (Nat.mul_le_mul_left _ (Nat.add_le_add_right hcol 1)))
  have he := congrFun (kernelVector_eq B.rows B.cols B.data) j
  rw [he]
  exact ⟨hb.1.trans (pow_le_pow_right₀ (by norm_num) hp),hb.2.trans (pow_le_pow_right₀ (by norm_num) hp)⟩

end MetricKMedian.Gaussian
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Compression_GaussianInputBounds
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.Gaussian.ListOperation
open Binary Finset Polynomial

 theorem input_audit (I : Input) :
    Audit I.encode.length I.encode.length (residualHeight I.encode.length I.encode.length I.encode.length)
      (returnHeight I.encode.length I.encode.length I.encode.length) I.rows I.cols I.data := by
  let L := I.encode.length
  obtain ⟨hr,hn,hh⟩ := input_bounds I
  intro B hB
  obtain ⟨P⟩ := kernelStates_certificate (values I.data) I.rows I.cols I.data (ResidualCertificate.initial _) B hB
  have hrB : B.rows ≤ I.rows := by
    simpa only [Fintype.card_fin] using Fintype.card_le_of_injective P.row P.row_injective
  have hnB : B.cols ≤ I.cols := by
    simpa only [Fintype.card_fin] using Fintype.card_le_of_injective P.col P.col_injective
  refine ⟨hrB.trans hr,hnB.trans hn,?_,?_⟩
  · intro i j
    have hb := kernelStates_entry_height I.rows I.cols L I.data (fun i j => (hh i j).1) (fun i j => (hh i j).2) B hB i j
    exact HasHeight.mono hb (residualHeight_mono hr hn le_rfl)
  · intro j
    have hb := kernelStates_return_height I.rows I.cols L I.data I.underdetermined
      (fun i j => (hh i j).1) (fun i j => (hh i j).2) B hB j
    exact HasHeight.mono hb (returnHeight_mono hr hn le_rfl)

end MetricKMedian.Gaussian.ListOperation
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Geometry_RationalUnitScan
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.RationalUnitInput
open Finset
variable {f j : ℕ} {X : Type} [PseudoMetricSpace X]
variable (U : RationalUnitInput f j) (R : U.Realization X) {η τ : ℝ} (p : RationalAllParameters η τ)

def suppliers : RationalSuppliers.Data f (U.representatives p.M).card :=
  RationalBundles.suppliers (fun t => U.F (U.ridx p.M t)) U.y
    (fun t => R.c (U.ridx p.M t)) R.i
    (fun t u => U.dd (U.ridx p.M t) (U.ridx p.M u))
    (fun t a => U.dc (U.ridx p.M t) a) (fun t => U.V (U.ridx p.M t)) p.M p.δ p.γ
    (fun t u => R.hdd (U.ridx p.M t) (U.ridx p.M u))
    (fun t a => R.hdc (U.ridx p.M t) a) U.hy p.hM p.hδ (by linarith only [p.hδ1])
    p.hθ p.hγ p.hγ1 (fun t => U.hu (U.ridx p.M t)) (fun _ => rfl)
    (U.representative_separation p.M p.hM.le)

end MetricKMedian.Preparation.RationalUnitInput
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_ApproximationListProgram
attribute [-instance] _root_.OAI.MetricKMedian.TruncatedLP.instDecidableValid
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.LPBinary
open Binary Binary.PolyProgram Function Finset
namespace Repair
def raw (r : ℕ) (I : Input) : Output := finish I.rows (result r I) (rawPenalty r I.raw) (TruncatedLP.loss r I.k)

theorem raw_eq (r : ℕ) (hr : 0 < r) (I : Input) (hd : ∀ j i, 0 ≤ I.distance j i) :
    raw r I=encodeData (TruncatedLP.approximation I.distance r I.k hr I.kpos hd) := by
  let H := TruncatedLP.penalty r I.k
  let y := ProjectedSubgradient.point (TruncatedLP.optimize I.distance r I.k H hr I.kpos (TruncatedLP.penalty_pos r I.k hr))
  have hy : ProjectedSubgradient.feasible (I.k:ℚ) y := (TruncatedLP.optimize_spec I.distance r I.k H hr I.kpos
    (TruncatedLP.penalty_pos r I.k hr) hd (ProjectedSubgradient.point (ProjectedSubgradient.initial (I.k:ℚ)))
    (ProjectedSubgradient.initial_feasible _ (by positivity))).1
  have hm : 1 ≤ ∑ i, y i := by rw [hy.2]; exact_mod_cast I.kpos
  unfold raw finish
  rw [result_eq r hr]
  change (opening (List.ofFn y) (TruncatedLP.loss r I.k),
    assignments I.rows (nearestRows (Truncated.matrix I.rows H) (List.ofFn y)))=_
  rw [opening_ofFn]
  have hn : nearestRows (Truncated.matrix I.rows H) (List.ofFn y)=
      List.ofFn (fun j => List.ofFn (ProjectedSubgradient.point (Preparation.computedNearest y (TruncatedLP.truncated I.distance H j) hy.1 hm))) := by
    simp only [Input.rows,Truncated.matrix_ofFn,nearestRows,List.map_ofFn,Function.comp_def,Nearest.filling_ofFn _ _ hy.1 hm]
  rw [hn]
  unfold Input.rows
  rw [assignments_ofFn]
  simp only [encodeData,TruncatedLP.approximation,Vector.getElem_ofFn,ProjectedSubgradient.point_ofFn]
  rfl

end Repair
end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_FractionalSelectProgram
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.LPBinary
open Binary Binary.PolyProgram Function Finset
namespace Scale

def candidate (r : ℕ) (I : Input) (B : ℚ) : Repair.Output :=
  if 0 < B then Repair.raw r (I.scale B) else I.zeroOutput

theorem candidate_eq (r : ℕ) (hr : 0 < r) (I : Input) (hd : ∀ j i, 0 ≤ I.distance j i) (B : ℚ) :
    candidate r I B=Repair.encodeData (TruncatedLP.scaledCandidate I.distance r I.k hr I.kpos hd B) := by
  unfold candidate TruncatedLP.scaledCandidate
  by_cases hB : 0 < B
  · rw [ite_eq_left hB,dite_eq_left hB]
    exact Repair.raw_eq r hr (I.scale B) (fun j i => div_nonneg (hd j i) hB.le)
  · rw [ite_eq_right hB,dite_eq_right hB]
    have hz : ProjectedSubgradient.point (Vector.replicate I.n (0:ℚ)) = (fun _ => 0) := by
      funext i
      exact Vector.getElem_replicate _
    simp only [Repair.encodeData,Input.zeroOutput,Vector.getElem_replicate,hz,List.ofFn_const]

def feasible (r : ℕ) (I : Input) : Row := (guesses I.rows).filter (fun B => Repair.valid (candidate r I B) I.k)
def selectedScale (r : ℕ) (I : Input) : ℚ := argmin (feasible r I) (fun B => Repair.value (candidate r I B) I.rows)
def selected (r : ℕ) (I : Input) : Repair.Output := candidate r I (selectedScale r I)

end Scale
end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_ZeroCostBranch
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
open Finset
namespace Instance

theorem nonzero_optimum (I : Instance) (h : ¬I.zeroTest) : 0 < optimum I :=
  lt_of_le_of_ne I.optimum_nonneg (fun he => h (I.zeroTest_iff.mpr he.symm))

theorem initialPhase_spec (I : Instance) (r : ℕ) (hr : 0 < r) :
    if h : I.zeroTest then
      I.zeroOutput ⊆ I.facilities ∧ I.zeroOutput.Nonempty ∧ I.zeroOutput.card ≤ I.k ∧
        cost I I.zeroOutput=0
    else
      let out := I.computedFractional r hr (I.nonzero_clients h)
      out.Valid I.k ∧ (out.value I.indexedDistance:ℝ) ≤
        (1+3/(r:ℝ))*optimum I := by
  split_ifs with h
  · exact I.zeroOutput_spec h
  · obtain ⟨S,hSF,hS,hSk,he⟩ := I.optimum_attained
    have hc : 0 < rationalCost I S := by
      have hh := I.nonzero_optimum h
      rw [← he,← I.cast_rationalCost S] at hh
      exact_mod_cast hh
    obtain ⟨hv,hc⟩ := I.computedFractional_spec r hr (I.nonzero_clients h) S hSF hS hSk hc
    refine ⟨hv,?_⟩
    have hh : ((I.computedFractional r hr (I.nonzero_clients h)).value I.indexedDistance:ℝ) ≤
        (1+3/(r:ℝ))*(rationalCost I S:ℝ) := by
      have hh := (Rat.cast_le (K:=ℝ)).mpr hc
      push_cast at hh
      exact hh
    rwa [I.cast_rationalCost,he] at hh

end Instance
end MetricKMedian
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_PivotListProgram
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.ListPivot
open Binary Binary.PolyProgram Function Finset

theorem update_ofFn {n : ℕ} (μ : IntegerLaw (Fin n)) (z : Fin n → ℤ)
    (h : (positiveSet z).Nonempty) (hzsum : ∑ i, z i=0) :
    update (μ.denominator,List.ofFn μ.numerator) (List.ofFn z)=
      let ν := eliminateAt μ z (computedPivot μ z h) (computedPivot_spec μ z h).1 (computedPivot_spec μ z h).2 hzsum
      (ν.denominator,List.ofFn ν.numerator) := by
  simp only [update,Gaussian.ListOperation.zip_ofFn,pivot_ofFn μ z h,Gaussian.ListOperation.get_ofFn,List.map_ofFn,
    Function.comp_def,eliminateAt,Vector.getElem_ofFn]

end MetricKMedian.IntegerLaw.ListPivot
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseListTrim
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.PolyProgram Function Finset
abbrev er := IntegerLaw.ListPivot.er
variable {α : Type}
abbrev encode (ea : α → List Bool) (μ : SparseIntegerLaw α) := ed ea (raw μ)

theorem activeEntries_raw (μ : SparseIntegerLaw α) : activeEntries (raw μ)=
    List.ofFn (fun j : Fin μ.law.support.card => let i := μ.law.support.orderEmbOfFin rfl j;
      (μ.law.numerator i,μ.states[i.val])) := by
  rw [activeEntries,raw,states_list,Gaussian.ListOperation.zip_ofFn,List.ofFn_eq_map,List.filter_map]
  exact EncodingLists.map_filter_enum _ (fun i => μ.law.numerator i≠0)

theorem trimData_raw (μ : SparseIntegerLaw α) : trimData (raw μ)=raw μ.trim := by
  unfold trimData
  rw [activeEntries_raw]
  simp only [raw,trim,Vector.toList_ofFn,List.map_ofFn,Function.comp_def,IntegerLaw.trim_denominator]
  congr 2
  exact congrArg List.ofFn (funext (IntegerLaw.trim_numerator μ.law)).symm

end MetricKMedian.SparseIntegerLaw.BinarySparse
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.SparseIntegerLaw
open Binary
variable {α : Type} {d : ℕ}

theorem encode_length_bound (ea : α → List Bool) (μ : SparseIntegerLaw α) (N H A : ℕ)
    (hn : μ.length≤N) (hd : μ.law.denominator≤(2:ℤ)^H)
    (ha : ∀ i : Fin μ.length, (ea μ.states[i.val]).length≤A) :
    (BinarySparse.encode ea μ).length≤2*(2*(H+4)+1+N*(2*(H+4)+1))+1+N*(2*A+1) := by
  have hd' := Binary.Signed.length_height (by rwa [abs_of_pos μ.law.denominator_pos] : |μ.law.denominator|≤(2:ℤ)^H)
  have hn' : (Binary.encodeList Binary.Signed.encode (List.ofFn μ.law.numerator)).length≤N*(2*(H+4)+1) := by
    apply (Binary.EncodedList.length_bound _ _ (H+4) ?_).trans
    · simpa only [List.length_ofFn] using Nat.mul_le_mul_right (2*(H+4)+1) hn
    · intro z hz
      obtain ⟨i,rfl⟩ := List.mem_ofFn.mp hz
      exact Binary.Signed.length_height (by rw [abs_of_nonneg (μ.law.numerator_nonneg i)]; exact (μ.law.numerator_le i).trans hd)
  have hs : (Binary.encodeList ea μ.states.toList).length≤N*(2*A+1) := by
    rw [BinarySparse.states_list]
    apply (Binary.EncodedList.length_bound _ _ A ?_).trans
    · simpa only [List.length_ofFn] using Nat.mul_le_mul_right (2*A+1) hn
    · intro a hx
      obtain ⟨i,rfl⟩ := List.mem_ofFn.mp hx
      exact ha i
  simp only [BinarySparse.encode,BinarySparse.ed,BinarySparse.raw,BinarySparse.el,IntegerLaw.ListPivot.el,Binary.encodePair_length]
  change 2*(2*(Binary.Signed.encode μ.law.denominator).length+1+
    (Binary.encodeList Binary.Signed.encode (List.ofFn μ.law.numerator)).length)+1+
    (Binary.encodeList ea μ.states.toList).length≤_
  omega

end MetricKMedian.SparseIntegerLaw
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_RoundingUniformStep
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
open SparseIntegerLaw.BinarySparse

def State.encode {s : Bool} (x : State s) : List Bool :=
  encodePair erow (SparseIntegerLaw.BinarySparse.encode (fun p => erow p.toList)) (List.ofFn x.β,x.μ)

end MetricKMedian.RoundingProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_RoundingStateCompiler
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
open SparseIntegerLaw.BinarySparse

theorem trim_encode_raw {n : ℕ} (μ : SparseIntegerLaw (Vector ℚ n)) :
    trimData ((μ.law.denominator,List.ofFn μ.law.numerator),μ.states.toList.map Vector.toList)=
      (((μ.trim).law.denominator,List.ofFn (μ.trim).law.numerator),μ.trim.states.toList.map Vector.toList) := by
  change trimData ((raw μ).1,(raw μ).2.map Vector.toList)=_
  rw [trimData_map,trimData_raw]
  rfl

end MetricKMedian.RoundingProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_DependentSparseProgram
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.DependentProgram
open Binary Binary.PolyProgram Function BinarySparse
variable {C A : Type} (T : C → Type)

variable {T} (ec : C → List Bool) (ea : A → List Bool) (view : ∀ c, T c → A)

def Bundle.branch (p : ∀ c, T c → ℚ) (hp : ∀ c a, 0 ≤ p c a ∧ p c a ≤ 1)
    (next : ∀ c, T c → Fin 2 → T c) (x : Bundle T) : Bundle T :=
  ⟨x.ctx,x.law.branch (p x.ctx) (hp x.ctx) (next x.ctx)⟩
def Bundle.compressionInput (d : C → ℕ) (v : ∀ c, T c → Fin (d c) → ℚ) (x : Bundle T) :
    IntegerLaw.BinaryCompression.RationalInput :=
  ⟨x.law.length,d x.ctx,x.law.law,fun i => v x.ctx x.law.states[i.val]⟩

 theorem trim_view (c : C) (μ : SparseIntegerLaw (T c)) :
    trimData ((μ.law.denominator,List.ofFn μ.law.numerator),μ.states.toList.map (view c))=
      (((μ.trim).law.denominator,List.ofFn (μ.trim).law.numerator),μ.trim.states.toList.map (view c)) := by
  change trimData ((raw μ).1,(raw μ).2.map (view c))=_
  rw [RoundingProgram.trimData_map,trimData_raw]
  rfl

 theorem raw_branch (p : ∀ c, T c → ℚ) (hp : ∀ c a, 0 ≤ p c a ∧ p c a ≤ 1)
    (next : ∀ c, T c → Fin 2 → T c)
    (P : C × A → ℚ) (E0 E1 : C × A → A)
    (hP : ∀ c a, P (c,view c a)=p c a)
    (hE0 : ∀ c a, E0 (c,view c a)=view c (next c a 0))
    (hE1 : ∀ c a, E1 (c,view c a)=view c (next c a 1)) (x : Bundle T) :
    (x.ctx,(branchLawData ((x.raw view).2.1,(x.raw view).2.2.map (fun a => P (x.ctx,a))),
      (x.raw view).2.2.flatMap (fun a => [E0 (x.ctx,a),E1 (x.ctx,a)])))=
       (x.branch p hp next).raw view := by
  simp only [Bundle.raw,Bundle.branch,states_list,List.map_ofFn,Function.comp_def,hP]
  rw [branchLaw_ofFn x.law.law _ (fun i => hp x.ctx x.law.states[i.val])]
  congr 2
  simp only [SparseIntegerLaw.branch,Vector.getElem_ofFn,List.flatMap_def,List.map_ofFn,
    Function.comp_def,hE0,hE1]
  exact (two_expand (fun i b => view x.ctx (next x.ctx x.law.states[i.val] b))).symm

end MetricKMedian.SparseIntegerLaw.DependentProgram
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
open SparseIntegerLaw.DependentProgram

def State.increment (x : State) : State := ⟨⟨x.ctx.input,x.ctx.t+1⟩,x.law⟩

end MetricKMedian.SparseBernoulli.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Probability_BernoulliRunProgram
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 Polynomial
open SparseIntegerLaw.DependentProgram
open SparseIntegerLaw.BinarySparse (el ed)

def Input.start (x : Input) : State := ⟨⟨x,0⟩,.dirac (fun _ => false)⟩

 theorem input_bounds (x : Input) : x.n ≤ x.encode.length ∧ ∀ i, HasHeight (x.p i) x.encode.length := by
  refine ⟨?_,?_⟩
  · simpa only [List.length_ofFn] using (EncodedList.length_le Ratio.encode (List.ofFn x.p))
  · intro i
    exact (Ratio.height_length _).mono (EncodedList.member_length _ _ _ (List.mem_ofFn.mpr ⟨i,rfl⟩))

end MetricKMedian.SparseBernoulli.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_GraphStepProgram
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.SparseGraph.Program
open Binary Binary.PolyProgram Function
open SparseIntegerLaw.DependentProgram SparseIntegerLaw.BinarySparse
open ListOperation (Row Table er )
structure Context where
  input : Input
  t : ℕ
abbrev T (c : Context) := Graph c.input.n c.input.m
abbrev State := Bundle T

def column (c : Context) : SparseIntegerLaw (Finset (Fin c.input.n)) :=
  if h : c.t < c.input.m then c.input.columns ⟨c.t,h⟩ else .dirac ∅
def update (c : Context) (G : T c) (S : Finset (Fin c.input.n)) : T c :=
  fun i => if i.val=c.t then S else G i

def State.product (x : State) : State := ⟨x.ctx,x.law.prod (column x.ctx) (update x.ctx)⟩

def State.increment (x : State) : State := ⟨⟨x.ctx.input,x.ctx.t+1⟩,x.law⟩
end MetricKMedian.SparseGraph.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_GraphRunProgram
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.SparseGraph.Program
open Binary Binary.PolyProgram Function Polynomial
open SparseIntegerLaw.DependentProgram SparseIntegerLaw.BinarySparse
open ListOperation (Row Table )
def Input.start (x : Input) : State := ⟨⟨x,0⟩,.dirac (fun _ => ∅)⟩

end MetricKMedian.SparseGraph.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_GraphLawProgram
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.SparseGraph.Program
open Binary Binary.PolyProgram Function SparseIntegerLaw.BinarySparse
open SparseIntegerLaw.DependentProgram

noncomputable def columnsProgram : PolyProgram QInput.encode (encodeList SparseBernoulli.Program.Input.encode) QInput.columns :=
  (snd (encodeList (fun _ : Unit => [])) qt).recode QInput.raw (fun _ => rfl) (fun x => by
    change qt (List.ofFn (fun i => List.ofFn (x.column i).p))=
      encodeList SparseBernoulli.Program.Input.encode (List.ofFn x.column)
    rw [show List.ofFn (fun i => List.ofFn (x.column i).p)=
      (List.ofFn x.column).map (fun c => List.ofFn c.p) by rw [List.map_ofFn]; rfl]
    exact RoundingProgram.encodeList_map qr (fun c : SparseBernoulli.Program.Input => List.ofFn c.p) _)

end MetricKMedian.SparseGraph.Program
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 Table setView)
open CopyList

 attribute [local instance] OAI.MetricKMedian.RationalPhysicalKernel.CopyGraphProgram.instLinearOrderSubtypeCopyFinMemFinset
theorem taper_q (x : Input) : x.taper.qInput.q =
    (fun h i => Taper.sourceMarginals x.g x.P (fun a : x.A => x.d (enumeration x.A i).val.1 a.val.1)
      (own x.A (enumeration x.A i)) x.Δ (enumeration x.A h)) := by
  funext h i
  let e := ordinal x.A
  have hm : ((own x.A (enumeration x.A i)).map (enumeration x.A).symm.toEmbedding).map e.toEquiv.toEmbedding =
      own x.A (enumeration x.A i) := by
    rw [ordinal_enum]
    ext a
    simp only [mem_map_equiv,Equiv.symm_symm,Equiv.apply_symm_apply]
  have hh := Taper.source_reindex e x.g x.P (fun a : x.A => x.d (enumeration x.A i).val.1 a.val.1)
    ((own x.A (enumeration x.A i)).map (enumeration x.A).symm.toEmbedding) x.Δ h
  rw [hm] at hh
  exact hh.symm

end MetricKMedian.RationalPhysicalKernel.CopyGraphProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_CountStepProgram
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.SparseCounts.Program
open Binary Binary.PolyProgram Function
open SparseIntegerLaw.DependentProgram SparseIntegerLaw.BinarySparse
open ListOperation (Row Table er et)
structure Context where
  input : Input
  t : ℕ
end MetricKMedian.SparseCounts.Program
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}

 theorem bindData_raw (μ : SparseIntegerLaw α) (κ : Fin μ.length → SparseIntegerLaw β)
    (view : β → A) :
    bindData ((raw μ).1,List.ofFn (fun i => ((raw (κ i)).1,(κ i).states.toList.map view)))=
      ((raw (μ.bindIndexed κ)).1,(μ.bindIndexed κ).states.toList.map view) := by
  unfold bindData
  rw [jointWeights_raw,IntegerList.denominator_ofFn,IntegerList.numerators_ofFn]
  let w := (μ.law.rational.sigma (fun i => (κ i).law.rational)).weight
  change ((RationalScaling.denominator (fun j => w (finSigmaFinEquiv.symm j)),
    List.ofFn (RationalScaling.numerator (fun j => w (finSigmaFinEquiv.symm j)))),_) = _
  rw [scaling_denominator_equiv finSigmaFinEquiv w]
  rw [show RationalScaling.numerator (fun j => w (finSigmaFinEquiv.symm j)) =
    (fun j => RationalScaling.numerator w (finSigmaFinEquiv.symm j)) from
      funext (scaling_numerator_equiv finSigmaFinEquiv w)]
  have hs : (List.ofFn fun i => ((raw (κ i)).1,(κ i).states.toList.map view)).flatMap Prod.snd=
      (μ.bindIndexed κ).states.toList.map view := by
    simp only [List.flatMap_def,List.map_ofFn,Function.comp_def,states_list,List.map_ofFn]
    rw [ListSigma.ofFn_sigma]
    simp only [bindIndexed,Vector.getElem_ofFn]
  rw [hs]
  rfl

end MetricKMedian.SparseIntegerLaw.BinarySparse
end

end OAI
end