OAI.MetricKMedian.SparseEnumeratedFixedBatch.actual_local_bound: intermediate lemma from OpenAI, The approximation threshold for metric k-median (result family 125)

Open

OAI.MetricKMedian.SparseEnumeratedFixedBatch.actual_local_bound

by dbenbenn · Oct 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

openai-math

An intermediate lemma of the split of OpenAI's proof of OAI.MetricKMedian.main_finite_work, carved from OpenAI's openai/math development for this platform. The statement and its proof are OpenAI's (OpenAI, The approximation threshold for metric k-median (result family 125), OpenAI Math Release, September 24, 2026, result family 125, github.com/openai/math, Apache License 2.0), ported to Lean 4.33.1 and Mathlib 0df444a.

The statement, as published (namespace OAI.MetricKMedian.SparseEnumeratedFixedBatch, with open Finset PhysicalPotential Analytic FixedBatch):

theorem actual_local_bound (G : I → Finset I) (H S F : Finset I) (Δ : ℕ)
    (enum : Fin n ≃ HeavyAction (graphActions G) H)
    (p : ℚ) (q : HeavyAction (graphActions G) H → ℚ) (hp : 0 ≤ p ∧ p ≤ 1)
    (hq0 : ∀ e, 0 ≤ q e ∧ q e ≤ 1) {x g h φ R b b' : ℝ} (d : I → ℝ)
    (hprob : (p:ℝ)=2*h*g)
    (hG : ∀ i, (G i).card=Δ) (hg : 0 < g) (hg1 : g ≤ 1) (hunit : g*(Δ:ℝ)=1)
    (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hh0 : 0 ≤ h) (hh1 : h ≤ 1)
    (hφ0 : 0 ≤ φ) (hφ1 : φ ≤ 1)
    (hq : ∀ e, (p:ℝ) ≤ q e ∧ (q e:ℝ) ≤ (1+φ)*(p:ℝ))
    (hsmall : (16*((Δ^2+Δ:ℕ):ℝ)+10)*h ≤ savingsFraction g)
    (hy : mass g S ≤ 1) (hF : F ⊆ S) (hHS : H ∩ S ⊆ F)
    (hd0 : ∀ i, 0 ≤ d i) (hR0 : 0 ≤ R) (hdR : ∀ i ∈ S, d i ≤ R)
    (hbQ : b ≤ 5*((PhysicalPotential.cost g d S+(1-mass g S)*b)/g))
    (hb0 : 0 ≤ b) (hbR : b ≤ 5*R) (hb'0 : 0 ≤ b') (hb' : b' ≤ b)
    (hbF : ∀ i ∈ F, b' ≤ d i) (hbH : ∀ i ∈ H, b' ≤ d i) :
    let D := heavyActions (graphActions G) H
    let μ := (SparseEnumeratedBatch.law enum (balancedActions D Δ) (balancedConflicts D Δ)
      p q hp hq0).real
    μ.expect (fun A => potential (x*Real.exp (-h)) g d
      (nextAliveAt D (coefficient x (mass g S)) d (S \ F) A)
      (nextCap D d b' A)-potential x g d S b) ≤
      h*(timeRate x (mass g S)*PhysicalPotential.cost g d S+
        g*(∑ e ∈ relevant (graphActions G) S, charge (graphActions G) x g b d S e))+
      batchConstant Δ*h*(φ+h)*R

Definitions. The statement is written with OAI.MetricKMedian.Analytic.coefficient and OAI.MetricKMedian.Analytic.timeRate (definitions bundle OAIQ035K000 of this split); OAI.MetricKMedian.PhysicalPotential.mass (definitions bundle OAIQ035K003 of this split); OAI.MetricKMedian.FiniteLaw, OAI.MetricKMedian.FiniteLaw.expect, OAI.MetricKMedian.FixedBatch.Actions, OAI.MetricKMedian.FixedBatch.HeavyAction, OAI.MetricKMedian.FixedBatch.graphActions, OAI.MetricKMedian.FixedBatch.heavyActions, OAI.MetricKMedian.FixedBatch.instDecidableEqHeavyAction, OAI.MetricKMedian.FixedBatch.instFintypeHeavyAction, OAI.MetricKMedian.FixedBatch.nextAliveAt and OAI.MetricKMedian.FixedBatch.relevant (definitions bundle OAIQ035K004 of this split); OAI.MetricKMedian.FixedBatch.batchConstant (definitions bundle OAIQ035K005 of this split); OAI.MetricKMedian.PhysicalPotential.cost (definitions bundle OAIQ035K007 of this split); OAI.MetricKMedian.PhysicalPotential.savingsFraction (definitions bundle OAIQ035K016 of this split); OAI.MetricKMedian.FixedBatch.balancedActions, OAI.MetricKMedian.FixedBatch.balancedConflicts, OAI.MetricKMedian.FixedBatch.charge, OAI.MetricKMedian.FixedBatch.nextCap and OAI.MetricKMedian.PhysicalPotential.potential (definitions bundle OAIQ035K021 of this split); OAI.MetricKMedian.SparseIntegerLaw.real (definitions bundle OAIQ035K029 of this split); OAI.MetricKMedian.SparseEnumeratedBatch.law (definitions bundle OAIQ035K039 of this split).

Used by. The proof of OAI.MetricKMedian.RationalBatchData.proposal_local_bound of this split imports it.

Preamble

import Mathlib
import Definitions.Def_OAIQ035K021
import Definitions.Def_OAIQ035K039

Formal statement

section

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.SparseEnumeratedFixedBatch
open Finset PhysicalPotential Analytic FixedBatch
variable {I : Type} [DecidableEq I] [Fintype I] {n : ℕ}

theorem actual_local_bound (G : I → Finset I) (H S F : Finset I) (Δ : ℕ)
    (enum : Fin n ≃ HeavyAction (graphActions G) H)
    (p : ℚ) (q : HeavyAction (graphActions G) H → ℚ) (hp : 0 ≤ p ∧ p ≤ 1)
    (hq0 : ∀ e, 0 ≤ q e ∧ q e ≤ 1) {x g h φ R b b' : ℝ} (d : I → ℝ)
    (hprob : (p:ℝ)=2*h*g)
    (hG : ∀ i, (G i).card=Δ) (hg : 0 < g) (hg1 : g ≤ 1) (hunit : g*(Δ:ℝ)=1)
    (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hh0 : 0 ≤ h) (hh1 : h ≤ 1)
    (hφ0 : 0 ≤ φ) (hφ1 : φ ≤ 1)
    (hq : ∀ e, (p:ℝ) ≤ q e ∧ (q e:ℝ) ≤ (1+φ)*(p:ℝ))
    (hsmall : (16*((Δ^2+Δ:ℕ):ℝ)+10)*h ≤ savingsFraction g)
    (hy : mass g S ≤ 1) (hF : F ⊆ S) (hHS : H ∩ S ⊆ F)
    (hd0 : ∀ i, 0 ≤ d i) (hR0 : 0 ≤ R) (hdR : ∀ i ∈ S, d i ≤ R)
    (hbQ : b ≤ 5*((PhysicalPotential.cost g d S+(1-mass g S)*b)/g))
    (hb0 : 0 ≤ b) (hbR : b ≤ 5*R) (hb'0 : 0 ≤ b') (hb' : b' ≤ b)
    (hbF : ∀ i ∈ F, b' ≤ d i) (hbH : ∀ i ∈ H, b' ≤ d i) :
    let D := heavyActions (graphActions G) H
    let μ := (SparseEnumeratedBatch.law enum (balancedActions D Δ) (balancedConflicts D Δ)
      p q hp hq0).real
    μ.expect (fun A => potential (x*Real.exp (-h)) g d
      (nextAliveAt D (coefficient x (mass g S)) d (S \ F) A)
      (nextCap D d b' A)-potential x g d S b) ≤
      h*(timeRate x (mass g S)*PhysicalPotential.cost g d S+
        g*(∑ e ∈ relevant (graphActions G) S, charge (graphActions G) x g b d S e))+
      batchConstant Δ*h*(φ+h)*R := by
  sorry

end MetricKMedian.SparseEnumeratedFixedBatch
end
end

end OAI
end

Source

OpenAI, The approximation threshold for metric k-median (result family 125), OpenAI Math Release, September 24, 2026, https://github.com/openai/math (result family 125; paper: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Approximation-Threshold-for-Metric-k-Median-September-24-2026/main.pdf; Apache License 2.0)

View graph