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

import Mathlib
import Definitions.Def_OAIQ035K026

section
-- module Solutions.OAIQ035_KM.KMedian_Rounding_RationalTaperZero
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] [LinearOrder I]

theorem zero_data (g : ℚ) (d : I → ℚ) (own : Finset I) (Δ : ℕ)
    (_hg : 0 < (g:ℝ)) (hunit : (g:ℝ)*(Δ:ℝ)=1)
    (hcol : 1 ≤ colocatedMass g (fun i => (d i:ℝ)))
    (hown : ∀ i ∈ own, d i=0) (howncard : own.card ≤ Δ) :
    let q := zeroMarginal d own Δ
    (∀ i, 0 ≤ q i) ∧ (∀ i, q i ≤ 1) ∧ (∑ i, g*q i=1) ∧
      (∑ i, q i=Δ) ∧ (∀ i ∈ own, q i=1) ∧ (∀ i, 0 < q i → d i=0) := by
  let Z := zeroSources d
  have hz : (Z.card:ℝ)*(g:ℝ)=colocatedMass g (fun i => (d i:ℝ)) := by
    simp only [Z,zeroSources,colocatedMass,← sum_filter,sum_const,nsmul_eq_mul,
      Rat.cast_eq_zero]
  have hzcard : Δ ≤ Z.card := by
    have hh : (Δ:ℝ) ≤ Z.card := by nlinarith only [hcol,hz,hunit]
    exact_mod_cast hh
  have hsub : own ⊆ Z := by intro i hi; exact mem_filter.mpr ⟨mem_univ _,hown i hi⟩
  obtain ⟨hownS,hSZ,hcard⟩ := extend_spec own Z Δ hsub howncard hzcard
  change (∀ i, 0 ≤ zeroMarginal d own Δ i) ∧ _
  have hsum : (∑ i, zeroMarginal d own Δ i)=(Δ:ℚ) := by
    simp only [zeroMarginal,← sum_filter,filter_univ_mem,sum_const,nsmul_eq_mul,mul_one]
    exact_mod_cast hcard
  refine ⟨?_,?_,?_,hsum,?_,?_⟩
  · intro i; unfold zeroMarginal; split_ifs <;> norm_num
  · intro i; unfold zeroMarginal; split_ifs <;> norm_num
  · rw [← mul_sum,hsum]; exact_mod_cast hunit
  · intro i hi; exact ite_eq_left (hownS hi)
  · intro i hi
    have hm : i ∈ zeroSelection d own Δ := by
      by_contra hn
      simp only [zeroMarginal,ite_eq_right hn] at hi
      exact lt_irrefl _ hi
    exact (mem_filter.mp (hSZ hm)).2

end MetricKMedian.Taper
end
end

end OAI
end