Pairwise disjoint blocks, and the sensitivity at every point

For pairwise disjoint blocks the block inequality (BlockInequality, Lemma 6.4 of the paper) applies with N = 1 and m = 1, where 1 - cos (π / 1) = 2, and gives the bound 4 d² (Row.disjoint_blocks_of_block). For the blocks {j} this is the sensitivity bound at every point (Corollary 6.10 of the paper), ∑_j |f(x) - f(x^j)| ≤ 4 d² (sensitivity_of_block : BlockInequality → SensitivityBound).

theorem AaronsonAmbainis.Row.disjoint_blocks_of_block (hBlock : BlockInequality) (ι : Type) [Fintype ι] [DecidableEq ι] (d : ℕ) (f : Cube ι → ℝ) (hf : ∀ (x : Cube ι), |f x| ≤ 1) (hdeg : HasDegreeLE f d) (x : Cube ι) (β : Type) [Fintype β] (S : β → Finset ι) (hS : ∀ (b b' : β), b ≠ b' → Disjoint (S b) (S b')) : ∑ b : β, |f x - f (flipSet x (S b))| ≤ 4 * ↑d ^ 2

For pairwise disjoint blocks S b, ∑_b |f(x) - f(x^{S b})| ≤ 4 d².

theorem AaronsonAmbainis.sensitivity_of_block : BlockInequality → SensitivityBound

The sensitivity bound at every point (Corollary 6.10 of the paper), from the block inequality (Lemma 6.4): the blocks {j} are pairwise disjoint.