§3.1.1 — Pr[B] < 3/4: the preallocation's welfare falls below OPT*/3 with probability < 3/4
ProvedComplementFreeCA.CFRounding.eventB_boundLet be normalized, monotone valuations and let be LP-feasible with value . Suppose for every bidder , i.e. . Let be the welfare of the randomized-rounding preallocation and the event . Then
Together with the items bound, this shows that one round of randomized rounding produces a preallocation with both required properties with constant probability.
Formalization Note The paper normalizes and assumes ; the statement uses the scale-free equivalent . The paper's definition of drops the sum (""); the display fixes the meaning used here. The paper's text announces and its display ends with ; the strict inequality is stated, which the display's middle bound with gives. The statement assumes only LP feasibility of (the paper uses the optimal , which is a special case).
import Mathlib import Definitions.Def_ComplementFreeCA_CFRounding_Auction import Definitions.Def_ComplementFreeCA_CFRounding_LP
namespace ComplementFreeCA.CFRounding
theorem eventB_bound {n m : ℕ} (v : Fin n → Finset (Fin m) → ℝ)
(hnorm : ∀ i, IsNormalized (v i)) (hmono : ∀ i, IsMonotone (v i))
(x : Fin n → Finset (Fin m) → ℝ) (hx : IsLPFeasible x)
(hlarge : ∀ i, 3 * v i Finset.univ < lpValue v x) :
roundProb x (fun σ => welfare v σ < lpValue v x / 3) < 3 / 4 := by sorry
end ComplementFreeCA.CFRounding
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.