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

Open

OAI.MetricKMedian.RationalBatchData.proposal_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.RationalBatchData, with open Finset PhysicalPotential Analytic FixedBatch):

theorem proposal_local_bound (G : I → Finset I) (S F : Finset I) (Δ : ℕ)
    (g β p φ : ℚ) (hp : 0 ≤ p) (hφ : 0 ≤ φ) (hupper : (1+φ)*p ≤ 1)
    (enum : Fin n ≃ HeavyAction (graph G) (heavySet (graphMass G g) β))
    {x 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φ1 : (φ:ℝ) ≤ 1)
    (hsmall : (16*((Δ^2+Δ:ℕ):ℝ)+10)*h ≤ savingsFraction (g:ℝ))
    (hy : mass (g:ℝ) S ≤ 1) (hF : F ⊆ S) (hHS : heavySet (graphMass G g) β ∩ 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 ∈ heavySet (graphMass G g) β, b' ≤ d i) :
    let D := heavy (graph G) (heavySet (graphMass G g) β)
    (proposal G Δ g β p φ hp hφ hupper enum).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.expect, OAI.MetricKMedian.FixedBatch.Actions, OAI.MetricKMedian.FixedBatch.HeavyAction, OAI.MetricKMedian.FixedBatch.graphActions, 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 and OAI.MetricKMedian.RationalBatchData.heavySet (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.RationalBatchData.graph, OAI.MetricKMedian.RationalBatchData.graphMass and OAI.MetricKMedian.RationalBatchData.heavy (definitions bundle OAIQ035K017 of this split); 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.RationalBatchData.proposal (definitions bundle OAIQ035K039 of this split).

Used by. The proof of OAI.MetricKMedian.CopyState.rational_conditional_round_drift 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.RationalBatchData
open Finset PhysicalPotential Analytic FixedBatch
variable {I : Type} [DecidableEq I] [Fintype I] {n : ℕ}

theorem proposal_local_bound (G : I → Finset I) (S F : Finset I) (Δ : ℕ)
    (g β p φ : ℚ) (hp : 0 ≤ p) (hφ : 0 ≤ φ) (hupper : (1+φ)*p ≤ 1)
    (enum : Fin n ≃ HeavyAction (graph G) (heavySet (graphMass G g) β))
    {x 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φ1 : (φ:ℝ) ≤ 1)
    (hsmall : (16*((Δ^2+Δ:ℕ):ℝ)+10)*h ≤ savingsFraction (g:ℝ))
    (hy : mass (g:ℝ) S ≤ 1) (hF : F ⊆ S) (hHS : heavySet (graphMass G g) β ∩ 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 ∈ heavySet (graphMass G g) β, b' ≤ d i) :
    let D := heavy (graph G) (heavySet (graphMass G g) β)
    (proposal G Δ g β p φ hp hφ hupper enum).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.RationalBatchData
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