OAI/Combinatorics/DiscreteConvexity/ElementaryCovering.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The elementary covering lemma

The initial generators and regular edges are constructed from weighted degrees. The remaining generators come from an actual finite Bernoulli sample of ordered pairs. Every outcome is a containment cover, and finite averaging selects an outcome meeting the claimed cost budget.

  1. theorem OAI.TalagrandDiscreteConvexity.Covering.elementary_covering line 22