The sensitivity lemma

Lemma 6.3 (Sensitivity) of the paper, Row.sum_abs_sub_unit_le: if G on a cube is bounded by 1 and has degree at most D, then ∑_b |G(0) - G(e_b)| ≤ 4 D². Here 0 = Row.zero β and e_b = Row.unit b are the points (1,…,1) and (1,…,1)^b of the paper. Markov's inequality at an endpoint enters as the hypothesis MarkovEndpoint, which is proved in Row/Markov.lean.

theorem AaronsonAmbainis.Row.sum_abs_le_of_abs_sum_le {β : Type u_1} [Fintype β] (d : β → ℝ) (K : ℝ) (h : ∀ (R : Finset β), |∑ b ∈ R, d b| ≤ K) : ∑ b : β, |d b| ≤ 2 * K

If every partial sum of d is bounded by K in absolute value, then ∑ |d| ≤ 2 K.

noncomputable def AaronsonAmbainis.Row.phi {β : Type u_1} [Fintype β] [DecidableEq β] (g : Finset β → ℝ) (R : Finset β) : Polynomial ℝ

The restriction polynomial φ_R(s) = ∑_U g_U (1 - s)^{|U ∩ R|}.

Equations

• AaronsonAmbainis.Row.phi g R = ∑ U : Finset β, Polynomial.C (g U) * (1 - Polynomial.X) ^ (U ∩ R).card

theorem AaronsonAmbainis.Row.natDegree_phi_le {β : Type u_1} [Fintype β] [DecidableEq β] (g : Finset β → ℝ) (R : Finset β) (D : ℕ) (hg : ∀ (U : Finset β), D < U.card → g U = 0) : (phi g R).natDegree ≤ D

theorem AaronsonAmbainis.Row.eval_phi {β : Type u_1} [Fintype β] [DecidableEq β] (g : Finset β → ℝ) (R : Finset β) (s : ℝ) : Polynomial.eval s (phi g R) = ∑ U : Finset β, g U * ∏ b ∈ U, if b ∈ R then 1 - s else 1

theorem AaronsonAmbainis.Row.derivative_phi_eval_zero {β : Type u_1} [Fintype β] [DecidableEq β] (g : Finset β → ℝ) (R : Finset β) : Polynomial.eval 0 (Polynomial.derivative (phi g R)) = -∑ U : Finset β, g U * ↑(U ∩ R).card

theorem AaronsonAmbainis.Row.sum_sub_unit {β : Type u_1} [Fintype β] [DecidableEq β] (g : Finset β → ℝ) (R : Finset β) : ∑ b ∈ R, (∑ U : Finset β, g U * chi U (zero β) - ∑ U : Finset β, g U * chi U (unit b)) = 2 * ∑ U : Finset β, g U * ↑(U ∩ R).card

∑_{b ∈ R} (G(0) - G(e_b)) = 2 ∑_U g_U |U ∩ R| for G = ∑_U g_U chi_U.

theorem AaronsonAmbainis.Row.abs_sum_sub_unit_le {β : Type u_1} [Fintype β] [DecidableEq β] (hM : MarkovEndpoint) (G : Cube β → ℝ) (D : ℕ) (hG : ∀ (w : Cube β), |G w| ≤ 1) (hdeg : HasDegreeLE G D) (R : Finset β) : |∑ b ∈ R, (G (zero β) - G (unit b))| ≤ 2 * ↑D ^ 2

For every set R of coordinates, |∑_{b ∈ R} (G(0) - G(e_b))| ≤ 2 D².

theorem AaronsonAmbainis.Row.sum_abs_sub_unit_le {β : Type u_1} [Fintype β] [DecidableEq β] (hM : MarkovEndpoint) (G : Cube β → ℝ) (D : ℕ) (hG : ∀ (w : Cube β), |G w| ≤ 1) (hdeg : HasDegreeLE G D) : ∑ b : β, |G (zero β) - G (unit b)| ≤ 4 * ↑D ^ 2

The sensitivity lemma (Lemma 6.3 of the paper), given Markov's inequality at an endpoint.