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

import Mathlib
import Definitions.Def_OAIQ037K000
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_ComputedPivot
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 leastRatio {n : ℕ} (μ : IntegerLaw (Fin n)) (z : Fin n → ℤ)
    (h : (positiveSet z).Nonempty) : ℚ :=
  ((positiveSet z).image (ratio μ z)).min' (h.image _)

end MetricKMedian.IntegerLaw

end OAI
end

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_pos (q : Ω → ℚ) : 0 < denominator q := by
  apply prod_pos
  intro i _
  exact_mod_cast (q i).den_pos

end MetricKMedian.RationalScaling

end OAI
end

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

namespace OAI

namespace MetricKMedian.RationalLaw
open Finset
variable {Ω : Type} [Fintype Ω] [DecidableEq Ω]

def integer (μ : RationalLaw Ω) : IntegerLaw Ω where
  denominator := RationalScaling.denominator μ.weight
  denominator_pos := RationalScaling.denominator_pos μ.weight
  numerator := RationalScaling.numerator μ.weight
  numerator_nonneg i := by
    have hh : (0:ℚ) ≤ (RationalScaling.numerator μ.weight i:ℚ) := by
      rw [RationalScaling.numerator_cast]
      exact mul_nonneg (μ.nonneg i) (by exact_mod_cast (RationalScaling.denominator_pos μ.weight).le)
    exact_mod_cast hh
  total := by
    apply Int.cast_injective (α:=ℚ)
    rw [Int.cast_sum]
    simp only [RationalScaling.numerator_cast,← sum_mul,μ.total,one_mul]

@[simp] theorem integer_weight (μ : RationalLaw Ω) (i : Ω) :
    μ.integer.rational.weight i=μ.weight i := by
  change (RationalScaling.numerator μ.weight i:ℚ)/(RationalScaling.denominator μ.weight:ℚ)=_
  rw [RationalScaling.numerator_cast,mul_div_cancel_right₀]
  exact_mod_cast (RationalScaling.denominator_pos μ.weight).ne'

@[simp] theorem integer_numerator_zero (μ : RationalLaw Ω) (i : Ω) :
    μ.integer.numerator i=0 ↔ μ.weight i=0 := by
  have hD : (RationalScaling.denominator μ.weight:ℚ) ≠ 0 := by
    exact_mod_cast (RationalScaling.denominator_pos μ.weight).ne'
  change RationalScaling.numerator μ.weight i=0 ↔ _
  rw [← Int.cast_eq_zero (α:=ℚ),RationalScaling.numerator_cast,mul_eq_zero,or_iff_left hD]

end MetricKMedian.RationalLaw

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Geometry_RationalNearestCopies
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.RationalNearest
open Finset
variable {α : Type} [LinearOrder α]

theorem takeNearest_spec (d : α → ℚ) (k : ℕ) (U : Finset α) (hk : k ≤ U.card) :
    takeNearest d k U ⊆ U ∧ (takeNearest d k U).card=k ∧
    ∀ S : Finset α, S ⊆ U → S.card=k → (∑ a∈takeNearest d k U,d a) ≤ ∑ a∈S,d a := by
  induction k generalizing U with
  | zero =>
    simp only [takeNearest,empty_subset,card_empty,true_and,sum_empty]
    intro S _ hS
    simp [card_eq_zero.mp hS]
  | succ k ih =>
    have hU : U.Nonempty := card_pos.mp (by omega)
    let a := least U d hU
    have ha : a∈U := (least_spec U d hU).1
    have hamin : ∀ b∈U, d a ≤ d b := (least_spec U d hU).2
    have hk' : k ≤ (U.erase a).card := by rw [card_erase_of_mem ha]; omega
    obtain ⟨hsub,hcard,hmin⟩ := ih (U.erase a) hk'
    have han : a∉takeNearest d k (U.erase a) := fun h => (mem_erase.mp (hsub h)).1 rfl
    simp only [takeNearest,dite_eq_left hU]
    change insert a (takeNearest d k (U.erase a)) ⊆ U ∧ _
    refine ⟨insert_subset ha (hsub.trans (erase_subset _ _)),?_,?_⟩
    · rw [card_insert_of_notMem han,hcard]
    · intro S hSU hSk
      rw [sum_insert han]
      by_cases haS : a∈S
      · have hsubS : S.erase a ⊆ U.erase a := erase_subset_erase a hSU
        have hSc : (S.erase a).card=k := by rw [card_erase_of_mem haS,hSk]; omega
        have hh := hmin _ hsubS hSc
        have he := sum_erase_add S d haS
        linarith only [hh,he]
      · have hS : S.Nonempty := card_pos.mp (by omega)
        obtain ⟨b,hb⟩ := hS
        have hsubS : S.erase b ⊆ U.erase a := by
          intro z hz
          have hzS := mem_of_mem_erase hz
          exact mem_erase.mpr ⟨fun he => haS (he ▸ hzS),hSU hzS⟩
        have hSc : (S.erase b).card=k := by rw [card_erase_of_mem hb,hSk]; omega
        have hh := hmin _ hsubS hSc
        have he := sum_erase_add S d hb
        have hd := hamin b (hSU hb)
        linarith only [hh,he,hd]

end MetricKMedian.Preparation.RationalNearest
end

end OAI
end

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

namespace OAI

namespace MetricKMedian
open Finset

structure SparseIntegerLaw (α : Type) where
  length : ℕ
  states : Vector α length
  law : IntegerLaw (Fin length)

end MetricKMedian

end OAI
end

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

namespace OAI

namespace MetricKMedian.SparseIntegerLaw
variable {α β : Type}

def map (μ : SparseIntegerLaw α) (f : α → β) : SparseIntegerLaw β where
  length := μ.length
  law := μ.law
  states := μ.states.map f

end MetricKMedian.SparseIntegerLaw

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_RationalBatchData
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.RationalBatchData
open Finset FixedBatch PhysicalPotential
variable {I E : Type} [DecidableEq I] [Fintype I] [DecidableEq E] [Fintype E]

def graph (G : I → Finset I) : Actions I I where
  source := id
  erase := fun h => univ.filter (fun i => h ∈ G i)
  ordinary := univ

def heavy (Full : Actions I I) (H : Finset I) : Actions I (HeavyAction Full H) where
  source := fun e => Full.source (heavyParent Full H e)
  erase := Sum.elim (fun h => Full.erase h) (fun p => {p.val.2})
  ordinary := univ.filter (fun e : HeavyAction Full H => e.isLeft = true)

def balanced (D : Actions I E) (Δ : ℕ) : Finset E :=
  D.ordinary.filter (fun e => (D.erase e).card=Δ)

def conflicts (D : Actions I E) (Δ : ℕ) (e : E) : Finset E :=
  if e ∈ balanced D Δ then
    (balanced D Δ).filter (fun f => f≠e ∧ (D.erase e ∩ D.erase f).Nonempty) else ∅

def graphMass (G : I → Finset I) (g : ℚ) (h : I) : ℚ := g*((graph G).erase h).card

end MetricKMedian.RationalBatchData
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_RationalBatchEnumeration
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.RationalBatchData
open Finset FixedBatch
variable {I : Type} [LinearOrder I] [Fintype I]

def enumeration (Full : Actions I I) (H : Finset I) :
    Fin (Fintype.card (HeavyAction Full H)) ≃ HeavyAction Full H := by
  letI : LinearOrder (I × I) :=
    LinearOrder.lift' (fun p : I × I => toLex p) (fun _ _ h => h)
  letI : LinearOrder (HeavyAction Full H) :=
    LinearOrder.lift' (fun e : HeavyAction Full H => toLex e) (fun _ _ h => h)
  exact (Fintype.orderIsoFinOfCardEq (HeavyAction Full H) rfl).toEquiv

end MetricKMedian.RationalBatchData
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Probability_SumLaws
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 Ξ]

noncomputable def sumMix (θ : ℝ) (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1)
    (μ : FiniteLaw Ω) (ν : FiniteLaw Ξ) : FiniteLaw (Ω ⊕ Ξ) where
  weight := Sum.elim (fun ω => θ*μ.weight ω) (fun ξ => (1-θ)*ν.weight ξ)
  nonneg := by
    intro z
    cases z with
    | inl ω => exact mul_nonneg hθ0 (μ.nonneg ω)
    | inr ξ => exact mul_nonneg (sub_nonneg.mpr hθ1) (ν.nonneg ξ)
  total := by
    rw [Fintype.sum_sum_type]
    simp only [Sum.elim_inl, Sum.elim_inr, ← Finset.mul_sum, μ.total, ν.total]
    ring

end MetricKMedian.FiniteLaw

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseRealLaw
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 RationalLaw
variable {α : Type} [Fintype α]

noncomputable def real (μ : RationalLaw α) : FiniteLaw α where
  weight a := (μ.weight a:ℝ)
  nonneg a := by exact_mod_cast μ.nonneg a
  total := by exact_mod_cast μ.total

end RationalLaw

end MetricKMedian

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_RationalRoundEvents
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.RationalBatchData
open Finset FixedBatch
variable {I : Type} [LinearOrder I] [Fintype I]

abbrev Event (I : Type) [DecidableEq I] [Fintype I] (g β : ℚ) :=
  (G : I → Finset I) × Finset (HeavyAction (graph G) (heavySet (graphMass G g) β))

end MetricKMedian.RationalBatchData
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] {Δ : ℕ}

abbrev Payload (F : Type) [LinearOrder F] (Δ : ℕ) (g β : ℚ) :=
  (A : Finset (CopyState.Copy (F := F) Δ)) × RationalBatchData.Event A g β

abbrev State (F : Type) [LinearOrder F] (Δ : ℕ) (g β : ℚ) :=
  Finset (CopyState.Copy (F := F) Δ) × Option (Payload F Δ g β)

end MetricKMedian.RationalPhysicalKernel
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Geometry_NearestReindex
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.RationalNearest
open Finset
variable {α β : Type} [LinearOrder α] [LinearOrder β]

 theorem takeNearest_map (e : α ≃o β) (d : α → ℚ) (t : ℕ) (U : Finset α) :
    takeNearest (fun b => d (e.symm b)) t (U.map e.toEmbedding)=(takeNearest d t U).map e.toEmbedding := by
  induction t generalizing U with
  | zero => simp only [takeNearest,map_empty]
  | succ t ih =>
    by_cases hU : U.Nonempty
    · rw [takeNearest,takeNearest,dite_eq_left hU,dite_eq_left (hU.map),least_map e U d hU]
      have he : (U.map e.toEmbedding).erase (e (least U d hU))=(U.erase (least U d hU)).map e.toEmbedding := by
        exact (map_erase e.toEmbedding U (least U d hU)).symm
      rw [he,ih,map_insert]
      rfl
    · have he := not_nonempty_iff_eq_empty.mp hU
      subst U
      simp [takeNearest]
end MetricKMedian.Preparation.RationalNearest

namespace MetricKMedian.RationalPhysicalKernel.CopyList
open CopyState
variable {f Δ : ℕ}

local instance instLinearOrderCopyFin_1_r938d53_1 : LinearOrder (Copy (F:=Fin f) Δ) := copyOrder
def orderEquiv : @OrderIso (Copy (F:=Fin f) Δ) (Fin (f*Δ)) (copyOrder (F:=Fin f) (Δ:=Δ)).toLE inferInstance where
  toEquiv := finProdFinEquiv
  map_rel_iff' := @StrictMono.le_iff_le _ _ (copyOrder (F:=Fin f) (Δ:=Δ)) _ _ rank_strictMono
end MetricKMedian.RationalPhysicalKernel.CopyList
end

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 variance_mul (μ : FiniteLaw Ω) (X : Ω → ℝ) (g : ℝ) :
    μ.variance (fun ω => g*X ω)=g^2*μ.variance X := by
  rw [variance_eq, variance_eq, expect_mul]
  simp_rw [mul_pow, expect_mul]
  ring

end MetricKMedian.FiniteLaw
end
end

end OAI
end