Definitions bundle OAIQ037K047 of the split of OpenAI, The approximation threshold for metric k-median (result family 125)
DefinitionOAIQ037K047A definitions bundle of the split of OpenAI's proof of OAI.MetricKMedian.main_finite_work, carved from OpenAI's openai/math development (OpenAI, The approximation threshold for metric k-median (result family 125), OpenAI Math Release, September 24, 2026, result family 125, github.com/openai/math at commit adc7f12, Apache License 2.0) and ported to Lean 4.33.1 and Mathlib 0df444a. The declarations and their proofs are OpenAI's.
Contents. It holds 1 declaration of OpenAI's Lean: 1 definition. The definitions and types are OAI.MetricKMedian.Taper.physicalGraphData.
Sources. They come from these modules of lean/OAI/Combinatorics/KMedian, in whole or in part: KMedian_Rounding_RationalPhysicalGraph.
Imports. It imports the bundle OAIQ037K042 of this split.
Imported by (directly, in this split): the statement OAI.MetricKMedian.Taper.physical_sparse_graph; the proofs of OAI.MetricKMedian.RationalPhysicalKernel.graph_data, OAI.MetricKMedian.RationalPhysicalKernel.graph_data_all and OAI.MetricKMedian.Taper.physical_sparse_graph.
import Mathlib
import Definitions.Def_OAIQ037K042
section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_RationalPhysicalGraph
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} [LinearOrder I] [Fintype I] {n : ℕ} {X : Type*} [PseudoMetricSpace X]
noncomputable def physicalGraphData (Δ : ℕ) (g P : ℚ) (d : I → I → ℚ)
(location : I → X) (own : I → Finset (I))
(hg : 0 < (g:ℝ)) (hunit : (g:ℝ)*(Δ:ℝ)=1)
(hP : 0 < (P:ℝ)) (hP1 : (P:ℝ) ≤ 1/2)
(hd : ∀ i h, 0 ≤ d i h) (hdist : ∀ i h, dist (location i) (location h)=(d i h:ℝ))
(htotal : 1 ≤ ∑ _i : I, (g:ℝ))
(hown : ∀ i h, h∈own i → d i h=0) (howncard : ∀ i, (own i).card ≤ Δ) :
GraphData Δ (g:ℝ) (P:ℝ) location own where
radius i := (rationalRadius g P (d i):ℝ)
marginal h i := (sourceMarginals g P (d i) (own i) Δ h:ℝ)
radius_nonneg i := by
exact_mod_cast (rational_data g P (d i) (own i) Δ hg hunit hP hP1 (hd i) htotal (hown i) (howncard i)).1
marginal_nonneg h i := by
exact_mod_cast (rational_data g P (d i) (own i) Δ hg hunit hP hP1 (hd i) htotal (hown i) (howncard i)).2.1 h
marginal_le_one h i := by
exact_mod_cast (rational_data g P (d i) (own i) Δ hg hunit hP hP1 (hd i) htotal (hown i) (howncard i)).2.2.1 h
incoming_mass i := by
exact_mod_cast (rational_data g P (d i) (own i) Δ hg hunit hP hP1 (hd i) htotal (hown i) (howncard i)).2.2.2.1
incoming_count i := by
exact_mod_cast (rational_data g P (d i) (own i) Δ hg hunit hP hP1 (hd i) htotal (hown i) (howncard i)).2.2.2.2.1
own_certain i h he := by
exact_mod_cast (rational_data g P (d i) (own i) Δ hg hunit hP hP1 (hd i) htotal (hown i) (howncard i)).2.2.2.2.2.1 h he
lower h i he := by
rw [hdist]
exact_mod_cast (rational_data g P (d i) (own i) Δ hg hunit hP hP1 (hd i) htotal (hown i) (howncard i)).2.2.2.2.2.2.1 h (by exact_mod_cast he)
upper h i he := by
rw [hdist]
exact_mod_cast (rational_data g P (d i) (own i) Δ hg hunit hP hP1 (hd i) htotal (hown i) (howncard i)).2.2.2.2.2.2.2.1 h (by exact_mod_cast he)
minimal i R hR he := by
simp only [hdist] at he
exact (rational_data g P (d i) (own i) Δ hg hunit hP hP1 (hd i) htotal (hown i) (howncard i)).2.2.2.2.2.2.2.2 R hR he
end MetricKMedian.Taper
end
end
end OAI
end