Mean, variance, mean absolute increments, rows: elementary facts

Helper lemmas about real functions on the cube, with no reference to the degree:

• the cube has 2 ^ n points (card_cube, sum_const_cube, four_pow_card);
• the variance is nonnegative (variance_nonneg); it is 0 for a function with all values equal, in particular on the empty index type (variance_eq_zero_of_const, variance_eq_zero_of_isEmpty); the mean minimises the mean square distance to a constant (variance_le_sq_dist);
• Inf_j(f) is nonnegative and is one quarter of E[(f(x) - f(x^j))^2] (inflR_nonneg, inflR_eq_quarter);
• the mean absolute increments L_j(f) = meanAbsIncr f j are nonnegative (meanAbsIncr_nonneg) and satisfy L_j(f)^2 ≤ 4 Inf_j(f) (meanAbsIncr_sq_le; Section 2 of the paper);
• rows of a real function f: the cost of a row at x is at least |f(x) - f(y)| for every y (abs_sub_le_rowSum), so it is positive if f is not constant (rowSum_pos), and a number K that bounds the costs of rows at all points is positive if Var(f) > 0 (cost_pos); every function has a row at every point (exists_rows_cost; Remark 7.12 of the paper);
• a row a of cost at most K at u gives |f(u) - f(u^j)| ≤ a_j and ∑_j |f(u) - f(u^j)| ≤ K (abs_incr_le_of_rows, sum_abs_incr_le_of_rows); a bound G for these sums at all points u gives L(f) = ∑_j L_j(f) ≤ G (sum_meanAbsIncr_le); so L(f) ≤ K for a function with rows of cost at most K (sum_meanAbsIncr_le_cost).

theorem AaronsonAmbainis.Level.card_cube {ι : Type u_1} [Fintype ι] [DecidableEq ι] : ↑(Fintype.card (Cube ι)) = 2 ^ Fintype.card ι

The cube has 2 ^ n points.

theorem AaronsonAmbainis.Level.sum_const_cube {ι : Type u_1} [Fintype ι] [DecidableEq ι] (c : ℝ) : ∑ _x : Cube ι, c = 2 ^ Fintype.card ι * c

Sum of a constant over the cube.

theorem AaronsonAmbainis.Level.four_pow_card {ι : Type u_1} [Fintype ι] [Nonempty ι] : 4 ^ Fintype.card ι = 4 * 4 ^ (Fintype.card ι - 1)

4 ^ n = 4 · 4 ^ (n - 1) for n ≥ 1.

Mean and variance

theorem AaronsonAmbainis.Level.variance_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Cube ι → ℝ) : 0 ≤ variance f

theorem AaronsonAmbainis.Level.variance_eq_zero_of_const {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Cube ι → ℝ) (h : ∀ (x y : Cube ι), f x = f y) : variance f = 0

A function with all values equal has variance zero.

theorem AaronsonAmbainis.Level.variance_eq_zero_of_isEmpty {ι : Type u_1} [Fintype ι] [DecidableEq ι] [IsEmpty ι] (f : Cube ι → ℝ) : variance f = 0

On the empty index type every variance is 0.

theorem AaronsonAmbainis.Level.sum_sub_mean {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Cube ι → ℝ) : ∑ x : Cube ι, (f x - mean f) = 0

E (f - E f) = 0, unnormalised.

theorem AaronsonAmbainis.Level.variance_le_sq_dist {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Cube ι → ℝ) (c : ℝ) : variance f ≤ (∑ x : Cube ι, (f x - c) ^ 2) / 2 ^ Fintype.card ι

The mean minimises the mean square distance to a constant.

Influences and mean absolute increments

theorem AaronsonAmbainis.Level.inflR_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Cube ι → ℝ) (j : ι) : 0 ≤ inflR f j

theorem AaronsonAmbainis.Level.inflR_eq_quarter {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Cube ι → ℝ) (j : ι) : inflR f j = (∑ x : Cube ι, (f x - f (flipSet x {j})) ^ 2) / 2 ^ Fintype.card ι / 4

inflR is one quarter of the unnormalised L2 influence E[(f(x) - f(x^j))^2].

theorem AaronsonAmbainis.Level.meanAbsIncr_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Cube ι → ℝ) (j : ι) : 0 ≤ meanAbsIncr f j

theorem AaronsonAmbainis.Level.meanAbsIncr_sq_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Cube ι → ℝ) (j : ι) : meanAbsIncr f j ^ 2 ≤ 4 * inflR f j

L_j(f)^2 ≤ 4 Inf_j(f) (the Cauchy–Schwarz inequality; Section 2 of the paper).

Rows of a real function

theorem AaronsonAmbainis.Level.abs_sub_le_rowSum {ι : Type u_1} [Fintype ι] {f : Cube ι → ℝ} {a : Cube ι → ι → ℝ} (ha : ∀ (x : Cube ι) (j : ι), 0 ≤ a x j) (hrow : ∀ (x y : Cube ι), |f x - f y| ≤ ∑ j ∈ diffSet x y, a x j) (x y : Cube ι) : |f x - f y| ≤ ∑ j : ι, a x j

The cost of a row of f at x is at least |f(x) - f(y)|, for every y.

theorem AaronsonAmbainis.Level.rowSum_pos {ι : Type u_1} [Fintype ι] {f : Cube ι → ℝ} {a : Cube ι → ι → ℝ} (ha : ∀ (x : Cube ι) (j : ι), 0 ≤ a x j) (hrow : ∀ (x y : Cube ι), |f x - f y| ≤ ∑ j ∈ diffSet x y, a x j) {x y : Cube ι} (hxy : f x ≠ f y) : 0 < ∑ j : ι, a x j

A row at x has positive cost if f takes another value somewhere.

theorem AaronsonAmbainis.Level.cost_pos {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : Cube ι → ℝ} {a : Cube ι → ι → ℝ} {K : ℝ} (ha : ∀ (x : Cube ι) (j : ι), 0 ≤ a x j) (hsum : ∀ (x : Cube ι), ∑ j : ι, a x j ≤ K) (hrow : ∀ (x y : Cube ι), |f x - f y| ≤ ∑ j ∈ diffSet x y, a x j) (hvar : 0 < variance f) : 0 < K

If f has a row of cost at most K at every point and Var(f) > 0, then K > 0.

theorem AaronsonAmbainis.Level.abs_incr_le_of_rows {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : Cube ι → ℝ} {a : Cube ι → ι → ℝ} (hrow : ∀ (x y : Cube ι), |f x - f y| ≤ ∑ j ∈ diffSet x y, a x j) (u : Cube ι) (j : ι) : |f u - f (flipSet u {j})| ≤ a u j

A row at u bounds each increment of f at u: |f(u) - f(u^j)| ≤ a u j.

theorem AaronsonAmbainis.Level.sum_abs_incr_le_of_rows {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : Cube ι → ℝ} {a : Cube ι → ι → ℝ} {K : ℝ} (hsum : ∀ (x : Cube ι), ∑ j : ι, a x j ≤ K) (hrow : ∀ (x y : Cube ι), |f x - f y| ≤ ∑ j ∈ diffSet x y, a x j) (u : Cube ι) : ∑ j : ι, |f u - f (flipSet u {j})| ≤ K

A row at u of cost at most K bounds the sum of the increments of f at u: ∑_j |f(u) - f(u^j)| ≤ K.

theorem AaronsonAmbainis.Level.sum_meanAbsIncr_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Cube ι → ℝ) {G : ℝ} (hG : ∀ (u : Cube ι), ∑ j : ι, |f u - f (flipSet u {j})| ≤ G) : ∑ j : ι, meanAbsIncr f j ≤ G

If ∑_j |f(u) - f(u^j)| ≤ G at every point u, then L(f) = ∑_j L_j(f) ≤ G.

theorem AaronsonAmbainis.Level.sum_meanAbsIncr_le_cost {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : Cube ι → ℝ} {a : Cube ι → ι → ℝ} {K : ℝ} (hsum : ∀ (x : Cube ι), ∑ j : ι, a x j ≤ K) (hrow : ∀ (x y : Cube ι), |f x - f y| ≤ ∑ j ∈ diffSet x y, a x j) : ∑ j : ι, meanAbsIncr f j ≤ K

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

theorem AaronsonAmbainis.Level.exists_rows_cost {ι : Type u_1} [Fintype ι] (f : Cube ι → ℝ) : ∃ (K : ℝ) (a : Cube ι → ι → ℝ), (∀ (x : Cube ι) (j : ι), 0 ≤ a x j) ∧ (∀ (x : Cube ι), ∑ j : ι, a x j ≤ K) ∧ ∀ (x y : Cube ι), |f x - f y| ≤ ∑ j ∈ diffSet x y, a x j

Every real function on the cube has a row at every point, of cost at most some K: the hypotheses on rows can be met for every function (Remark 7.12 of the paper).