Density rectangles for the top-down adversary #
The invariant from Sections 3--4 of Oliver Korten, Top-Down Lower Bounds for All Depths, ECCC TR26-221 (2026), https://eccc.weizmann.ac.il/report/2026/221/.
The actual sampling rate may be smaller than the parameter bound. This is needed because density-limit conditions need not be monotone in the rate.
def
Complexity.KarchmerWigderson.DensityRectangle
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(X Y : Finset (ι → Bool))
(p k : ℝ)
:
A nonempty rectangle with both deficits at most k, and a positive
sampling rate at most p for which one side consists of density limits of
the other side.
Equations
- One or more equations did not get rendered due to their size.