Main.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Talagrand discrete convexity at the original density

Independent coordinate choices produce dependent rows with full Bernoulli subset laws. The label construction raises the union density when L p < 1; the mandatory-row construction covers every coordinate when 1 ≤ L p. Both cases use the same row-failure budget, without independence between rows.

theorem OAI.TalagrandDiscreteConvexity.original_density_small line 23
Source documentation
The density reduction works on any finite ground set.
```
theorem original_density_small (p : ℝ) (hp0 : 0 < p) (hp1 : p < 1)
    (D : Family α) (hD : 1 - 1 / (2 : ℝ) ^ 75 ≤ familyMeasure p D) :
    Small p (exceptional ((2 : ℕ) ^ 75) D) := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.familyMeasure, OAI.TalagrandDiscreteConvexity.Small, OAI.TalagrandDiscreteConvexity.exceptional
theorem OAI.TalagrandDiscreteConvexity.talagrand_discrete_convexity line 61
Distinct definitions of this name: ComparatorChallenges/TalagrandDiscreteConvexity.lean:47 (same statement text; different proof or body). Qualify references as OAI.TalagrandDiscreteConvexity.talagrand_discrete_convexity@path.