Main.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Integral and fractional expectation thresholds

The fractional threshold is genuinely attained with budget one half. Rounding that attained cover gives an integral cover at the threshold divided by 25 * 512^4, still with budget one half and without a support-size restriction.

theorem OAI.TalagrandThreshold.talagrand_expectation_threshold_equivalence line 21
Source documentation
Talagrand's threshold comparison with the explicit constant 25 * 512^4. The coefficient 25 is an integer factor, and both feasible sets use budget one half. The fractional cover ranges over every subset of the ground set.
Distinct definitions of this name: ComparatorChallenges/TalagrandExpectationThreshold.lean:52 (same statement text; different proof or body). Qualify references as OAI.TalagrandThreshold.talagrand_expectation_threshold_equivalence@path.
```
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
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.Increasing, OAI.TalagrandThreshold.q