The influences of a function with rows of bounded cost

Let f have a row of cost at most K at every point and V = Var f > 0. Let L = L(f) = ∑_k L_k(f) be the sum of the mean absolute increments (it is positive, by the bound for the mean absolute increments) and R = {j : 5 L · Inf_j f < 2 V · L_j f} (the coordinates whose influence is small compared with the mean absolute increment). Then ∑_{j ∈ R} Inf_j f ≤ (2/5) V, so the average g of f over the coordinates of R (Average.exists_avg_set) has Var g ≥ (3/5) V. The bound for the mean absolute increments, applied to g, gives j with Var(g)^3 ≤ 36 K^4 L_j(g)² and L_j(g) > 0; so j ∉ R, and 2 V L_j(g) ≤ 2 V L_j(f) ≤ 5 L · Inf_j f. Together (Theorem 8.3 of the paper):

3 V^5 ≤ 3125 L(f)² K^4 (Inf_j f)² (influence_of_meanIncrement : MeanIncrementBound → InfluenceBound),

that is, Inf_j f ≥ (√15 / 125) · V^{5/2} / (L(f) K²).

Further statements of this file:

• Average.sum_meanAbsIncr_pos — L(f) > 0 (and L(f) ≤ K is Level.sum_meanAbsIncr_le_cost);
• Average.influence_of_incr — if ∑_j |f(u) - f(u^j)| ≤ G at every point u, then L(f) ≤ G and 3 V^5 ≤ 3125 G² K^4 (Inf_j f)²;
• Average.influence_cost — in particular, since L(f) ≤ K: 3 V^5 ≤ 3125 K^6 (Inf_j f)²;
• Average.exists_inflR_ge_sqrt — the bound for the influences with the power 5/2 written as V² · √V: √15 V^{5/2} ≤ 125 L(f) K² Inf_j f (the two forms are equivalent: Average.pow_le_iff_sqrt_mul_le).

theorem AaronsonAmbainis.Average.exists_meanAbsIncr_pos {ι : Type} [Fintype ι] [DecidableEq ι] (hMI : MeanIncrementBound) (g : Cube ι → ℝ) (b : Cube ι → ι → ℝ) {K : ℝ} (hb0 : ∀ (x : Cube ι) (i : ι), 0 ≤ b x i) (hbK : ∀ (x : Cube ι), ∑ i : ι, b x i ≤ K) (hbrow : ∀ (x y : Cube ι), |g x - g y| ≤ ∑ i ∈ diffSet x y, b x i) (hg : 0 < variance g) : ∃ (j : ι), 0 < meanAbsIncr g j ∧ variance g ^ 3 ≤ 36 * K ^ 4 * meanAbsIncr g j ^ 2

The bound for the mean absolute increments, with the positivity of the increment that it gives.

theorem AaronsonAmbainis.Average.sum_meanAbsIncr_pos {ι : Type} [Fintype ι] [DecidableEq ι] (hMI : MeanIncrementBound) (f : Cube ι → ℝ) (a : Cube ι → ι → ℝ) {K : ℝ} (ha : ∀ (x : Cube ι) (i : ι), 0 ≤ a x i) (hsum : ∀ (x : Cube ι), ∑ i : ι, a x i ≤ K) (hrow : ∀ (x y : Cube ι), |f x - f y| ≤ ∑ i ∈ diffSet x y, a x i) (hvar : 0 < variance f) : 0 < ∑ k : ι, meanAbsIncr f k

The sum L(f) of the mean absolute increments of a function with rows of cost at most K and positive variance is positive.

theorem AaronsonAmbainis.influence_of_meanIncrement : MeanIncrementBound → InfluenceBound

The bound for the influences (Theorem 8.3 of the paper) from the bound for the mean absolute increments (Theorem 7.10): if f has a row of cost at most K at every point and Var f > 0, then some coordinate j has 3 Var(f)^5 ≤ 3125 L(f)² K^4 (Inf_j f)², where L(f) = ∑_k L_k(f).

theorem AaronsonAmbainis.Average.influence_of_incr {ι : Type} [Fintype ι] [DecidableEq ι] (hI : InfluenceBound) (f : Cube ι → ℝ) (a : Cube ι → ι → ℝ) {K G : ℝ} (ha : ∀ (x : Cube ι) (i : ι), 0 ≤ a x i) (hsum : ∀ (x : Cube ι), ∑ i : ι, a x i ≤ K) (hrow : ∀ (x y : Cube ι), |f x - f y| ≤ ∑ i ∈ diffSet x y, a x i) (hG : ∀ (u : Cube ι), ∑ j : ι, |f u - f (flipSet u {j})| ≤ G) (hvar : 0 < variance f) : ∃ (j : ι), 3 * variance f ^ 5 ≤ 3125 * G ^ 2 * K ^ 4 * inflR f j ^ 2

The bound for the influences with a bound G for the sums of the increments at the points: 3 Var(f)^5 ≤ 3125 G² K^4 (Inf_j f)².

theorem AaronsonAmbainis.Average.influence_cost {ι : Type} [Fintype ι] [DecidableEq ι] (hI : InfluenceBound) (f : Cube ι → ℝ) (a : Cube ι → ι → ℝ) {K : ℝ} (ha : ∀ (x : Cube ι) (i : ι), 0 ≤ a x i) (hsum : ∀ (x : Cube ι), ∑ i : ι, a x i ≤ K) (hrow : ∀ (x y : Cube ι), |f x - f y| ≤ ∑ i ∈ diffSet x y, a x i) (hvar : 0 < variance f) : ∃ (j : ι), 3 * variance f ^ 5 ≤ 3125 * K ^ 6 * inflR f j ^ 2

The bound for the influences in terms of the cost alone: if f has a row of cost at most K at every point and Var f > 0, then some coordinate j has 3 Var(f)^5 ≤ 3125 K^6 (Inf_j f)².

theorem AaronsonAmbainis.Average.pow_le_iff_sqrt_mul_le {V L K I : ℝ} (hV : 0 ≤ V) (hL : 0 ≤ L) (hI : 0 ≤ I) : 3 * V ^ 5 ≤ 3125 * L ^ 2 * K ^ 4 * I ^ 2 ↔ √15 * (V ^ 2 * √V) ≤ 125 * L * K ^ 2 * I

For V, L, I ≥ 0: 3 V^5 ≤ 3125 L² K^4 I² if and only if √15 V^{5/2} ≤ 125 L K² I, where V^{5/2} is written V² · √V.

theorem AaronsonAmbainis.Average.exists_inflR_ge_sqrt {ι : Type} [Fintype ι] [DecidableEq ι] (hI : InfluenceBound) (f : Cube ι → ℝ) (a : Cube ι → ι → ℝ) {K : ℝ} (ha : ∀ (x : Cube ι) (i : ι), 0 ≤ a x i) (hsum : ∀ (x : Cube ι), ∑ i : ι, a x i ≤ K) (hrow : ∀ (x y : Cube ι), |f x - f y| ≤ ∑ i ∈ diffSet x y, a x i) (hvar : 0 < variance f) : ∃ (j : ι), √15 * (variance f ^ 2 * √(variance f)) ≤ (125 * ∑ k : ι, meanAbsIncr f k) * K ^ 2 * inflR f j

The bound for the influences with the power 5/2 written as Var² · √Var: some coordinate j has √15 Var(f)^{5/2} ≤ 125 L(f) K² Inf_j(f), that is, Inf_j(f) ≥ (√15 / 125) Var(f)^{5/2} / (L(f) K²), where L(f) = ∑_k L_k(f).