OAI.TalagrandThreshold.talagrand_expectation_threshold_equivalence
OpenThe theorem states that, for a finite nonempty ground type α and a family F of subsets of α that is nonempty, is not the entire power set, and is increasing (any superset of a member of F is again in F), the fractional threshold qf(F) is at most 25·512⁴ times the integral threshold q(F). Here q(F) is the supremum of those p in [0,1] for which F is small: some family G of sets covers F, meaning every H in F contains a member of G, with total cost Σ_{S∈G} p^{|S|} at most 1/2. The fractional threshold qf(F) is the analogous supremum of p in [0,1] for which there is a weight function g from subsets of α to [0,1] such that every H in F has Σ_{S⊆H} g(S) ≥ 1 and the fractional cost Σ_S g(S)·p^{|S|} is at most 1/2. The theorem is admitted with sorry in the source and is not proved there.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/TalagrandExpectationThreshold.lean; bytes 1516..1749
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.
import Mathlib.Data.Fintype.Powerset
import Mathlib.Data.Finset.Union
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.Order.Archimedean.Real.Basic
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
import Definitions.Def_TalagrandExpectationThreshold
namespace OAI
namespace TalagrandThreshold
open scoped BigOperators
variable {α : Type*} [Fintype α] [DecidableEq α]
theorem talagrand_expectation_threshold_equivalence [Nonempty α]
(F : Family α) (_hF : F.Nonempty) (hproper : F ≠ Finset.univ)
(hIncreasing : Increasing F) :
qf F ≤ ((25 : ℝ) * (512 : ℝ) ^ 4) * q F := by
sorry
end TalagrandThreshold
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.