Averaging a function over one coordinate

For a coordinate j let avg j f x = (f x + f (x^j)) / 2. Then (Lemma 8.1 of the paper)

• variance_avg — Var f = Var (avg j f) + Inf_j f (f = avg j f + (f - f ∘ flip_j)/2, and the two parts are even and odd under the flip of j);
• inflR_avg_le — Inf_k (avg j f) ≤ Inf_k f for every k;
• meanAbsIncr_avg_le — L_k (avg j f) ≤ L_k f for every k;
• meanAbsIncr_avg_self — L_j (avg j f) = 0;
• rows_avg — if a x is a row of f at x for every x, of cost at most K, then (a x + a (x^j)) / 2 is a row of avg j f at x, of cost at most K.

Here L_k(f) = meanAbsIncr f k is the mean absolute increment of f in the coordinate k.

theorem AaronsonAmbainis.Average.flipSet_comm {ι : Type u_1} [DecidableEq ι] (x : Cube ι) (S T : Finset ι) : flipSet (flipSet x S) T = flipSet (flipSet x T) S

Flips commute.

theorem AaronsonAmbainis.Average.diffSet_flip {ι : Type} [Fintype ι] [DecidableEq ι] (x y : Cube ι) (S : Finset ι) : diffSet (flipSet x S) (flipSet y S) = diffSet x y

Flipping the same coordinates in two points does not change the set where they differ.

theorem AaronsonAmbainis.Average.sum_flip {ι : Type} [Fintype ι] [DecidableEq ι] (j : ι) (F : Cube ι → ℝ) : ∑ x : Cube ι, F (flipSet x {j}) = ∑ x : Cube ι, F x

The flip of the coordinate j is a bijection of the cube.

noncomputable def AaronsonAmbainis.Average.avg {ι : Type} [DecidableEq ι] (j : ι) (f : Cube ι → ℝ) : Cube ι → ℝ

The average of f over the coordinate j.

Equations

• AaronsonAmbainis.Average.avg j f x = (f x + f (AaronsonAmbainis.flipSet x {j})) / 2

theorem AaronsonAmbainis.Average.avg_flip {ι : Type} [DecidableEq ι] (j : ι) (f : Cube ι → ℝ) (x : Cube ι) : avg j f (flipSet x {j}) = avg j f x

theorem AaronsonAmbainis.Average.mean_avg {ι : Type} [Fintype ι] [DecidableEq ι] (j : ι) (f : Cube ι → ℝ) : mean (avg j f) = mean f

theorem AaronsonAmbainis.Average.variance_avg {ι : Type} [Fintype ι] [DecidableEq ι] (j : ι) (f : Cube ι → ℝ) : variance f = variance (avg j f) + inflR f j

Var f = Var (avg j f) + Inf_j f.

theorem AaronsonAmbainis.Average.inflR_avg_le {ι : Type} [Fintype ι] [DecidableEq ι] (j k : ι) (f : Cube ι → ℝ) : inflR (avg j f) k ≤ inflR f k

Inf_k (avg j f) ≤ Inf_k f for every k.

theorem AaronsonAmbainis.Average.meanAbsIncr_avg_le {ι : Type} [Fintype ι] [DecidableEq ι] (j k : ι) (f : Cube ι → ℝ) : meanAbsIncr (avg j f) k ≤ meanAbsIncr f k

L_k (avg j f) ≤ L_k f for every k.

theorem AaronsonAmbainis.Average.meanAbsIncr_avg_self {ι : Type} [Fintype ι] [DecidableEq ι] (j : ι) (f : Cube ι → ℝ) : meanAbsIncr (avg j f) j = 0

L_j (avg j f) = 0.

theorem AaronsonAmbainis.Average.rows_avg {ι : Type} [Fintype ι] [DecidableEq ι] (j : ι) {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) : (∀ (x : Cube ι) (i : ι), 0 ≤ (a x i + a (flipSet x {j}) i) / 2) ∧ (∀ (x : Cube ι), ∑ i : ι, (a x i + a (flipSet x {j}) i) / 2 ≤ K) ∧ ∀ (x y : Cube ι), |avg j f x - avg j f y| ≤ ∑ i ∈ diffSet x y, (a x i + a (flipSet x {j}) i) / 2

Rows of f give rows of avg j f of the same cost.