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

import Mathlib
import Definitions.Def_OAIQ037K043
import Definitions.Def_OAIQ037K044
import Definitions.Def_OAIQ037K045

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_BinaryListIndex
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.Binary
open Function Polynomial

namespace PolyProgram
variable {α : Type} (ea : α → List Bool) (a0 : α)
noncomputable def listEraseIdx : PolyProgram (encodePair (encodeList ea) Nat.bits)
    (encodeList ea) (fun x : List α × ℕ => x.1.take x.2++(x.1.drop x.2).tail) :=
  (((listSplitAt ea a0).comp ((listTail ea a0).second (encodeList ea))).comp (listAppend ea a0)).congr _ (fun _ => rfl)
noncomputable def listInsertAt : PolyProgram (encodePair (encodePair (encodeList ea) Nat.bits) ea)
    (encodeList ea) (fun x : (List α × ℕ) × α => x.1.1.take x.1.2++x.2::x.1.1.drop x.1.2) := by
  let sp := (fst (encodePair (encodeList ea) Nat.bits) ea).comp (listSplitAt ea a0)
  let pre := sp.comp (fst (encodeList ea) (encodeList ea))
  let suf := sp.comp (snd (encodeList ea) (encodeList ea))
  let elem := snd (encodePair (encodeList ea) Nat.bits) ea
  exact ((pre.fanout ((elem.fanout suf).comp (listCons ea))).comp (listAppend ea a0)).congr _ (fun _ => rfl)
end PolyProgram
end MetricKMedian.Binary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_BinaryListMapTotal
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.Binary.PolyProgram
variable {α β : Type} {ea : α → List Bool} {eb : β → List Bool} {f : α → β}
noncomputable def listMapTotal (P : PolyProgram ea eb f) :
    PolyProgram (encodeList ea) (encodeList eb) (List.map f) := by
  classical
  by_cases h : Nonempty α
  · exact P.listMap h.some
  · exact (constant (encodeList ea) (encodeList eb) []).congr _ (by
      intro xs
      cases xs with
      | nil => rfl
      | cons a xs => exact False.elim (h ⟨a⟩))
end MetricKMedian.Binary.PolyProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_BinaryListZip
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.Binary
open Function Polynomial
namespace PolyProgram
variable {α β γ : Type} (ea : α → List Bool) (eb : β → List Bool) (a0 : α) (b0 : β)
noncomputable def listZipWith {ec : γ → List Bool} {f : α × β → γ}
    (P : PolyProgram (encodePair ea eb) ec f) :
    PolyProgram (encodePair (encodeList ea) (encodeList eb)) (encodeList ec) (fun x : List α × List β => (x.1.zip x.2).map f) :=
  ((listZip ea eb a0 b0).comp (P.listMap (a0,b0))).congr _ (fun _ => rfl)
end PolyProgram
end MetricKMedian.Binary
end

end OAI
end

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

namespace OAI

namespace MetricKMedian.IntegerLaw
open Finset

def compressionStep {n d : ℕ} (μ : IntegerLaw (Fin n)) (v : Fin n → Fin d → ℤ)
    (L : ℕ) (hv : ∀ i j, |v i j| ≤ (2:ℤ)^L) (hsize : d+1 < μ.support.card) :
    IntegerLaw (Fin n) :=
  let z := computedAffineKernel μ v
  have hz := computedAffineKernel_spec μ v L hv hsize
  have hP := positiveSet_nonempty z hz.2.1 hz.1
  let p := computedPivot μ z hP
  have hp := computedPivot_spec μ z hP
  eliminateAt μ z p hp.1 hp.2 hz.2.1

end MetricKMedian.IntegerLaw

end OAI
end

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

namespace OAI

namespace MetricKMedian.IntegerLaw
open Finset

def compressSteps {n d : ℕ} (v : Fin n → Fin d → ℤ) (L : ℕ)
    (hv : ∀ i j, |v i j| ≤ (2:ℤ)^L) : ℕ → IntegerLaw (Fin n) → IntegerLaw (Fin n)
  | 0, μ => μ
  | t+1, μ =>
    if h : d+1 < μ.support.card then
      compressSteps v L hv t (compressionStep μ v L hv h)
    else μ

def computedCompress {n d : ℕ} (μ : IntegerLaw (Fin n)) (v : Fin n → Fin d → ℤ)
    (L : ℕ) (hv : ∀ i j, |v i j| ≤ (2:ℤ)^L) : IntegerLaw (Fin n) :=
  compressSteps v L hv n μ

end MetricKMedian.IntegerLaw

end OAI
end

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

namespace OAI

namespace MetricKMedian.IntegerLaw
open Finset

def compressRational {n d : ℕ} (μ : IntegerLaw (Fin n)) (v : Fin n → Fin d → ℚ)
    (L : ℕ) (hnum : ∀ i j, |(v i j).num| ≤ (2:ℤ)^L)
    (hden : ∀ i j, ((v i j).den:ℤ) ≤ (2:ℤ)^L) : IntegerLaw (Fin n) :=
  μ.computedCompress (RationalLaw.scaledFeatures v) (L*(n+1))
    (RationalLaw.scaledFeatures_bound v L hnum hden)

end MetricKMedian.IntegerLaw

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Geometry_BoundFreeCompression
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 compressionStepAuto_eq {n d : ℕ} (μ : IntegerLaw (Fin n))
    (v : Fin n → Fin d → ℤ) (L : ℕ) (hv : ∀ i j, |v i j| ≤ (2:ℤ)^L)
    (hsize : d+1 < μ.support.card) :
    compressionStepAuto μ v hsize=compressionStep μ v L hv hsize := rfl

theorem compressStepsAuto_eq {n d : ℕ} (v : Fin n → Fin d → ℤ)
    (L : ℕ) (hv : ∀ i j, |v i j| ≤ (2:ℤ)^L) (t : ℕ) (μ : IntegerLaw (Fin n)) :
    compressStepsAuto v t μ=compressSteps v L hv t μ := by
  induction t generalizing μ with
  | zero => rfl
  | succ t ih =>
    simp only [compressStepsAuto,compressSteps]
    split_ifs with h
    · rw [compressionStepAuto_eq μ v L hv h,ih]
    · rfl

theorem compressAuto_eq {n d : ℕ} (μ : IntegerLaw (Fin n))
    (v : Fin n → Fin d → ℚ) (L : ℕ)
    (hnum : ∀ i j, |(v i j).num| ≤ (2:ℤ)^L)
    (hden : ∀ i j, ((v i j).den:ℤ) ≤ (2:ℤ)^L) :
    μ.compressAuto v=μ.compressRational v L hnum hden :=
  compressStepsAuto_eq _ _ (RationalLaw.scaledFeatures_bound v L hnum hden) n μ

end MetricKMedian.IntegerLaw

end OAI
end

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

namespace Program
open Binary Binary.PolyProgram
noncomputable def maxFold : PolyProgram (encodePair er Ratio.encode) Ratio.encode (fun x : Row × ℚ => x.1.foldl max x.2) :=
  (listChoose ratLT 0).congr _ (fun x => by
    congr 1
    funext a b
    by_cases h : a<b
    · simp [h,max_eq_right h.le]
    · simp [h,max_eq_left (le_of_not_gt h)])
end Program
end MetricKMedian.LPBinary
end

end OAI
end

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

variable {α : Type}

namespace Program
open Binary Binary.PolyProgram
noncomputable def minFold : PolyProgram (encodePair er Ratio.encode) Ratio.encode (fun x : Row × ℚ => x.1.foldl min x.2) :=
  (listChoose ((exchange Ratio.encode Ratio.encode).comp ratLT) 0).congr _ (fun x => by
    congr 1
    funext a b
    by_cases h : b<a
    · simp [h,min_eq_right h.le]
    · simp [h,min_eq_left (le_of_not_gt h)])
noncomputable def minimumProgram : PolyProgram er Ratio.encode minimum :=
  (((identity er).fanout (listHead Ratio.encode 0)).comp minFold).congr _ (fun _ => rfl)
end Program
end MetricKMedian.LPBinary
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 ed := encodePair es (encodePair el em)

abbrev Input.encode (I : Input) := ed I.raw

def Input.nextLaw (I : Input) : IntegerLaw (Fin I.n) :=
  if h : I.large then compressionStepAuto I.μ I.v h else I.μ

def Input.step (I : Input) : Input := {I with μ := I.nextLaw}

noncomputable def rawProgram : PolyProgram Input.encode ed Input.raw :=
  (identity ed).recode Input.raw (fun _ => rfl) (fun _ => rfl)
noncomputable def lawProgram : PolyProgram Input.encode el Input.lawData :=
  ((rawProgram.comp (snd es (encodePair el em))).comp (fst el em)).congr _ (fun _ => rfl)

end MetricKMedian.IntegerLaw.BinaryCompression
end

end OAI
end

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

def lawStep {n d : ℕ} (v : Fin n → Fin d → ℤ) (μ : IntegerLaw (Fin n)) : IntegerLaw (Fin n) :=
  if h : d+1 < μ.support.card then compressionStepAuto μ v h else μ

theorem input_iterate (I : Input) (t : ℕ) :
    Input.step^[t] I=⟨I.n,I.d,(lawStep I.v)^[t] I.μ,I.v⟩ := by
  induction t with
  | zero => rfl
  | succ t ih =>
      rw [Function.iterate_succ_apply',ih,Function.iterate_succ_apply']
      rfl

theorem input_bounds (I : Input) :
    I.n≤I.encode.length ∧ I.d≤I.encode.length ∧
    I.μ.denominator≤(2:ℤ)^I.encode.length ∧ ∀ i j, |I.v i j|≤(2:ℤ)^I.encode.length := by
  let L := I.encode.length
  have hl : L=2*I.d+1+2*(ListPivot.el I.lawData).length+1+(em I.features).length := by
    simp only [L,Input.raw,encodePair_length,Gaussian.ListOperation.slots_size]
    omega
  have hn := EncodedList.length_le Signed.encode (List.ofFn I.μ.numerator)
  simp only [List.length_ofFn] at hn
  have hlaw : (ListPivot.el I.lawData).length=2*(Signed.encode I.μ.denominator).length+1+(er (List.ofFn I.μ.numerator)).length := by
    simp only [Input.lawData,ListPivot.el,encodePair_length]
  refine ⟨by change I.n≤L; change I.n≤(er (List.ofFn I.μ.numerator)).length at hn; omega,by change I.d≤L; omega,?_,?_⟩
  · have hlen : (Signed.encode I.μ.denominator).length≤L := by omega
    exact (le_abs_self _).trans ((Signed.height_length _).trans (pow_le_pow_right₀ (by norm_num) hlen))
  · intro i j
    have hrow : List.ofFn (I.v i)∈I.features := List.mem_ofFn.mpr ⟨i,rfl⟩
    have hcol : I.v i j∈List.ofFn (I.v i) := List.mem_ofFn.mpr ⟨j,rfl⟩
    have h1 := EncodedList.member_length Signed.encode (List.ofFn (I.v i)) _ hcol
    have h2 := EncodedList.member_length er I.features _ hrow
    change (Signed.encode (I.v i j)).length≤(er (List.ofFn (I.v i))).length at h1
    change (er (List.ofFn (I.v i))).length≤(em I.features).length at h2
    exact (Signed.height_length _).trans (pow_le_pow_right₀ (by norm_num) (by omega))

theorem Input.encode_length (I : Input) : I.encode.length =
    2*I.d+1+(2*(2*(Signed.encode I.μ.denominator).length+1+
      (er (List.ofFn I.μ.numerator)).length)+1+(em I.features).length) := by
  simp only [Input.encode,Input.raw,Input.lawData,ed,el,ListPivot.el,encodePair_length,
    Gaussian.ListOperation.slots_size]

theorem compressSteps_eq_iterate {n d : ℕ} (v : Fin n → Fin d → ℤ) (t : ℕ) (μ : IntegerLaw (Fin n)) :
    compressStepsAuto v t μ=(lawStep v)^[t] μ := by
  induction t generalizing μ with
  | zero => rfl
  | succ t ih =>
      rw [compressStepsAuto,Function.iterate_succ_apply]
      split_ifs with h
      · rw [show lawStep v μ=compressionStepAuto μ v h from dite_eq_left h,ih]
      · have he : lawStep v μ=μ := dite_eq_right h
        rw [he,Function.iterate_fixed he]

end MetricKMedian.IntegerLaw.BinaryCompression
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_RationalFeatureProgram
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
abbrev eqd := encodePair es (encodePair el eqm)

abbrev RationalInput.encode (I : RationalInput) := eqd I.raw

end MetricKMedian.IntegerLaw.BinaryCompression
end

end OAI
end

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

noncomputable def countProgram : PolyProgram Input.encode Nat.bits Input.n :=
  ((lawProgram.comp (snd Signed.encode er)).comp (listLength Signed.encode 0)).congr _
    (fun I => by simp only [Function.comp_apply,Input.lawData,List.length_ofFn])

def Input.compressed (I : Input) : LawData :=
  let ν := compressStepsAuto I.v I.n I.μ
  (ν.denominator,List.ofFn ν.numerator)

def RationalInput.compressed (I : RationalInput) : LawData :=
  ( (I.μ.compressAuto I.v).denominator, List.ofFn (I.μ.compressAuto I.v).numerator)

end MetricKMedian.IntegerLaw.BinaryCompression
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseProduct
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.SparseIntegerLaw
open Finset
variable {α β γ : Type}

def prodCompress {d : ℕ} (μ : SparseIntegerLaw α) (ν : SparseIntegerLaw β)
    (f : α → β → γ) (v : γ → Fin d → ℚ) : SparseIntegerLaw γ :=
  (μ.prod ν f).compressAuto v

end MetricKMedian.SparseIntegerLaw
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 step (μ : SparseIntegerLaw (Graph n m)) (ν : SparseIntegerLaw (Finset (Fin n)))
    (i : Fin m) : SparseIntegerLaw (Graph n m) :=
  μ.prodCompress ν (fun G S => next G S i) features

end MetricKMedian.SparseGraph
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseGraphRun
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 run (ν : Fin m → SparseIntegerLaw (Finset (Fin n))) : ℕ → SparseIntegerLaw (Graph n m)
  | 0 => .dirac (fun _ => ∅)
  | t+1 => if ht : t < m then step (run ν t) (ν ⟨t,ht⟩) ⟨t,ht⟩ else run ν t

end MetricKMedian.SparseGraph
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseGraphLaw
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 columns (q : Fin n → Fin m → ℚ) (i : Fin m) : SparseIntegerLaw (Finset (Fin n)) :=
  (SparseCardinalRounding.round (Vector.ofFn (fun h => q h i))).map SparseCardinalRounding.selected

def law (q : Fin n → Fin m → ℚ) : SparseIntegerLaw (Graph n m) := run (columns q) m

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 law (enum : Fin n ≃ I) (q : I → I → ℚ) : SparseIntegerLaw (I → Finset I) :=
  (SparseGraph.law (fun h i => q (enum h) (enum i))).map (lift enum)

end MetricKMedian.SparseEnumeratedGraph
end
end

end OAI
end

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

namespace OAI

section
section
namespace MetricKMedian.RationalPhysicalKernel
open Finset
variable {F : Type} [LinearOrder F] [Fintype F] {Δ : ℕ}

attribute [local instance] OAI.MetricKMedian.RationalPhysicalKernel.instLinearOrderCopy
def graphLaw (d : F → F → ℚ) (g P : ℚ) (A : Finset (CopyState.Copy (F := F) Δ)) :
    SparseIntegerLaw (A → Finset A) :=
  SparseEnumeratedGraph.law (enumeration A)
    (fun h i => Taper.sourceMarginals g P (fun a : A => d i.val.1 a.val.1) (own A i) Δ h)

def step (d : F → F → ℚ) (g β p φ P : ℚ)
    (hp : 0 ≤ p) (hφ : 0 ≤ φ) (hupper : (1+φ)*p ≤ 1)
    (s : State F Δ g β) : SparseIntegerLaw (State F Δ g β) :=
  (RationalBatchData.events (graphLaw d g P s.1) Δ g β p φ hp hφ hupper).map
    (updateEvent g β s.1)

def histories (d : F → F → ℚ) (g β p φ : ℚ) (P : ℕ → ℚ)
    (hp : 0 ≤ p) (hφ : 0 ≤ φ) (hupper : (1+φ)*p ≤ 1)
    (A : Finset (CopyState.Copy (F := F) Δ)) (T : ℕ) :
    SparseIntegerLaw (SparseHistories.History (State F Δ g β)) :=
  SparseHistories.tree (fun t => step d g β p φ (P t) hp hφ hupper) (A,none) T

end MetricKMedian.RationalPhysicalKernel
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Geometry_RationalParameterizedHistory
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
open Finset PhysicalPotential CopyState RationalPhysicalKernel Completion.Rational
variable {τ : ℝ} (q : RationalParameters τ)

variable {F X : Type} [LinearOrder F] [Fintype F] [PseudoMetricSpace X] {j : ℕ}

def tree (d₀ : F → F → ℚ) (A : Finset (Copy (F := F) q.Δ)) :=
  histories d₀ q.g q.β q.probabilityQ q.φ q.taperAt q.probabilityQ_pos.le
    (by exact_mod_cast q.φpos.le) q.probabilityQ_le A q.T

end MetricKMedian.FixedBatch.RationalParameters
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Geometry_RationalHistorySelection
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
open Finset PhysicalPotential CopyState RationalPhysicalKernel Completion.Rational
variable {τ : ℝ} (q : RationalParameters τ)
variable {F X : Type} [LinearOrder F] [Fintype F] [PseudoMetricSpace X] {j : ℕ}

def selectCompleted (d₀ : F → F → ℚ) (d : Fin j → F → ℚ) (R : Fin j → ℚ)
    (A : Finset (Copy (F := F) q.Δ)) (B : Fin j → Finset (Copy (F := F) q.Δ))
    (hB : ∀ c, (B c).Nonempty) : Option (Finset F) :=
  (SparseSelect.choose (q.tree d₀ A) (q.completedGood d R A B hB)
    (fun z => score d (completed d R B hB q.g q.β z))).map
      (completed d R B hB q.g q.β)

end MetricKMedian.FixedBatch.RationalParameters
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Geometry_RationalGridRound
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
open Finset PhysicalPotential CopyState RationalPhysicalKernel Completion.Rational
open Preparation.RationalNearest
variable {τ : ℝ} (q : RationalParameters τ)
variable {F X : Type} [LinearOrder F] [PseudoMetricSpace X] {j : ℕ}

variable [Fintype F]

def roundCounts (d₀ : F → F → ℚ) (d : Fin j → F → ℚ) (n : F → ℕ) : Option (Finset F) :=
  if hn : ∀ a, n a ≤ q.Δ then
    let A := activeSlots n hn
    if hA : q.Δ ≤ A.card then
      q.selectCompleted d₀ d (q.radius d A hA) A (q.nearest d A) (q.nearest_nonempty d A hA)
    else none
  else none

end MetricKMedian.FixedBatch.RationalParameters
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Preparation_RationalPreparedScan
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
open Finset PhysicalPotential CopyState Completion.Rational
variable {τ : ℝ} (q : RationalParameters τ)
variable {F H X : Type} [LinearOrder F] [Fintype F] [DecidableEq H]
  [PseudoMetricSpace X] {j : ℕ}

def countCandidates (d₀ : H → H → ℚ) (d : Fin j → H → ℚ) (orig : F → H)
    (ns : List (F → ℕ)) : List (Finset H) :=
  ns.flatMap (fun n => ((q.roundCounts (fun a b => d₀ (orig a) (orig b))
    (fun c a => d c (orig a)) n).map (fun O => O.image orig)).toList)

def roundList (d₀ : H → H → ℚ) (d : Fin j → H → ℚ) (orig : F → H)
    (ns : List (F → ℕ)) (B : ℚ) : Option (Finset H) :=
  SparseSelect.best (candidateGood B) (score d) (q.countCandidates d₀ d orig ns)

end MetricKMedian.FixedBatch.RationalParameters
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.compress {s : Bool} (x : State s) : State s :=
  { x with μ := x.μ.compressAuto SparseWeightedPartial.features }
def State.step {s : Bool} (x : State s) : State s := x.branch.compress

end MetricKMedian.RoundingProgram
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
abbrev State.encode := Bundle.encode Context.encode er view

end MetricKMedian.SparseBernoulli.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseSignedPartial
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.SparseSignedPartial
open Finset RationalSignedStep
open RationalWeightedStep (point fractional)
open SparseWeightedPartial (features features_single features_pair)
variable {n : ℕ}

 def step (β : Fin n → ℚ) 
    (μ : SparseIntegerLaw (Vector ℚ n)) : SparseIntegerLaw (Vector ℚ n) :=
  μ.step features (probability β) (probability_unit β) (endpoint β)

 def run (β : Fin n → ℚ) (p : Vector ℚ n) :
    ℕ → SparseIntegerLaw (Vector ℚ n)
  | 0 => .dirac p
  | t+1 => step β (run β p t)

end MetricKMedian.SparseSignedPartial
end
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 Input.run {s : Bool} (x : Input s) (t : ℕ) : State s :=
  ⟨x.n,x.β,x.positive,if hs : s=true then SparseSignedPartial.run x.β x.p t
    else SparseWeightedPartial.run x.β (x.positive (by simpa using hs)) x.p t⟩

theorem input_iterate {s : Bool} (x : Input s) (t : ℕ) :
    State.step^[t] x.start=x.run t := by
  cases s <;> induction t with
  | zero => rfl
  | succ t ih =>
    rw [Function.iterate_succ_apply',ih]
    rfl

end MetricKMedian.RoundingProgram
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 et)

def Input.state (x : Input) (t : ℕ) : State := ⟨⟨x,t⟩,run x.columns t⟩
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
def QInput.input (x : QInput) : Input := ⟨x.n,x.m,SparseGraph.columns x.q⟩
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

def Input.law (x : Input) := graphLaw x.d x.g x.P x.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 Table setView)
open CopyList

attribute [local instance] OAI.MetricKMedian.RationalPhysicalKernel.UpdateProgram.instLinearOrderSubtypeCopyFinMemFinset
def Input.law (x : Input) := x.proposal.law.map x.update

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 Table)
open CopyList UpdateProgram

def ctxInputs (x : Context) : List UpdateProgram.Input := x.toInput.law.states.toList.map (fun G => ⟨x,G⟩)

def ctxLaw (x : Context) : SparseIntegerLaw (Finset (CopyState.Copy (F:=Fin x.f) x.Δ)) := x.toInput.law.bindIndexed
  (fun i => (UpdateProgram.Input.mk x x.toInput.law.states[i.val]).law)

 local instance instLinearOrderCopyFin_r804517_1 {f Δ : ℕ} : LinearOrder (CopyState.Copy (F:=Fin f) Δ) := copyOrder
local instance instLinearOrderSubtypeCopyFinMemFinset_r804517_1 {f Δ : ℕ} (A : Finset (CopyState.Copy (F:=Fin f) Δ)) : LinearOrder ↥A := activeOrder A
theorem law_step (x : Context) (s : State (Fin x.f) x.Δ x.g x.β) (hs : s.1=x.A) :
    (ctxLaw x)=(step x.d x.g x.β x.p x.φ x.P x.hp x.hφ x.hupper s).map Prod.fst := by
  unfold step
  erw [SparseIntegerLaw.map_map]
  unfold RationalBatchData.events
  erw [SparseIntegerLaw.map_bindIndexed]
  cases s with
  | mk A payload =>
    dsimp only at hs
    subst A
    unfold ctxLaw
    congr 1
    funext i
    erw [SparseIntegerLaw.map_map]
    rfl
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 Table)
open CopyList UpdateProgram
def law (P : ℕ → ℚ) (T : ℕ) (x : Context) := histories x.d x.g x.β x.p x.φ P x.hp x.hφ x.hupper x.A T

def inputs (P : ℕ → ℚ) (T : ℕ) (hP : 0<P T) (x : Context) : List Context :=
  (law P T x).states.toList.map (fun z => nextCtx x (P T) hP z.1.1)
end MetricKMedian.RationalPhysicalKernel.HistoryProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_MaximumProgram
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.MaskProgram
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView)
noncomputable def maxFold : PolyProgram (encodePair (encodeList Ratio.encode) Ratio.encode) Ratio.encode
    (fun x : List ℚ × ℚ => x.1.foldl max x.2) :=
  (listChoose ratLT 0).congr _ (fun x => by
    congr 1
    funext a b
    by_cases h : a<b
    · simp [h,max_eq_right h.le]
    · simp [h,max_eq_left (le_of_not_gt h)])
end MetricKMedian.MaskProgram
end

end OAI
end