Averaging over a set of coordinates

exists_avg_set (Lemma 8.2 of the paper): let f have a row of cost at most K at every point, and let R be a set of coordinates. Averaging f over the coordinates of R, one after the other, gives a function g with rows of cost at most K such that

• Var f ≤ Var g + ∑_{j ∈ R} Inf_j f,
• Inf_k g ≤ Inf_k f and L_k g ≤ L_k f for every coordinate k,
• L_j g = 0 for j ∈ R.

(g is the average of f over the coordinates in R, that is, the conditional expectation of f given the coordinates outside R; only the listed properties are used, so the function is not named.) Induction on R with the lemmas of Coordinate.lean.

theorem AaronsonAmbainis.Average.exists_avg_set {ι : Type} [Fintype ι] [DecidableEq ι] (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) (R : Finset ι) : ∃ (g : Cube ι → ℝ) (b : Cube ι → ι → ℝ), (∀ (x : Cube ι) (i : ι), 0 ≤ b x i) ∧ (∀ (x : Cube ι), ∑ i : ι, b x i ≤ K) ∧ (∀ (x y : Cube ι), |g x - g y| ≤ ∑ i ∈ diffSet x y, b x i) ∧ variance f ≤ variance g + ∑ j ∈ R, inflR f j ∧ (∀ (k : ι), inflR g k ≤ inflR f k) ∧ (∀ (k : ι), meanAbsIncr g k ≤ meanAbsIncr f k) ∧ ∀ j ∈ R, meanAbsIncr g j = 0

Averaging over the coordinates of a set R (Lemma 8.2 of the paper): a function g with rows of the same cost, with Var f ≤ Var g + ∑_{j ∈ R} Inf_j f, with influences and mean absolute increments not larger than those of f, and with L_j g = 0 for j ∈ R.