OAI/Combinatorics/DiscreteConvexity/HalfDensity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Small exceptional families at a fixed fraction of the density

The actual biased Fourier weights satisfy both estimates needed by the finite bin construction. No monotonicity of the given family is assumed.

  1. theorem OAI.TalagrandDiscreteConvexity.halfDensity_small line 18