OAI/Combinatorics/DiscreteConvexity/WeightedCover.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

From actual dyadic weights to a containment cover

The only inputs are the two weight inequalities. All bins, their finite index set, their covers, and the final union are constructed in the proof.

  1. theorem OAI.TalagrandDiscreteConvexity.weights_small line 21