The block inequality from Markov's inequality

blockInequality_of_markov : MarkovEndpoint → BlockInequality is the block inequality (Lemma 6.4 of the paper), with Markov's inequality at an endpoint as a hypothesis.

The gadget G = Row.gadget a x S m c with c = 1 - cos (π / m) is bounded by 1, has degree at most d * m, and satisfies G(0) = f x, G(e_b) = f (flipSet x (S b)); the sensitivity lemma (Row.sum_abs_sub_unit_le) then gives the bound 4 (d m)².

theorem AaronsonAmbainis.blockInequality_of_markov : MarkovEndpoint → BlockInequality

The block inequality, given Markov's inequality at an endpoint.