mean, variance, inflR under affine maps; degenerate cases

• mean, variance, inflR of a + b * g (mean_affine, variance_affine, inflR_affine): the change of normalisation [0,1] ↔ [-1,1] multiplies variance and influence by the same factor 4.
• The hypothesis 0 < variance f of MainTheorem forces 1 ≤ d and a nonempty index type (aa_hyps_force): the instances d = 0 and ι = ∅ of MainTheorem are vacuous, and these are exactly the instances in which no coordinate can have positive influence.
• variance f ≤ 1 if |f| ≤ 1, variance P ≤ 1/4 if 0 ≤ P ≤ 1.

The elementary facts on the variance that are used here are in Level/Basic.lean.

theorem AaronsonAmbainis.Bridge.mean_affine {ι : Type u_1} [Fintype ι] [DecidableEq ι] (a b : ℝ) (g : Cube ι → ℝ) : (mean fun (x : Cube ι) => a + b * g x) = a + b * mean g

theorem AaronsonAmbainis.Bridge.variance_affine {ι : Type u_1} [Fintype ι] [DecidableEq ι] (a b : ℝ) (g : Cube ι → ℝ) : (variance fun (x : Cube ι) => a + b * g x) = b ^ 2 * variance g

theorem AaronsonAmbainis.Bridge.inflR_affine {ι : Type u_1} [Fintype ι] [DecidableEq ι] (a b : ℝ) (g : Cube ι → ℝ) (j : ι) : inflR (fun (x : Cube ι) => a + b * g x) j = b ^ 2 * inflR g j

Degenerate cases

theorem AaronsonAmbainis.Bridge.variance_eq_zero_of_degree_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : Cube ι → ℝ} (h : HasDegreeLE f 0) : variance f = 0

Degree 0 forces variance 0: the d = 0 instance of MainTheorem is vacuous.

theorem AaronsonAmbainis.Bridge.aa_hyps_force {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : Cube ι → ℝ} {d : ℕ} (hdeg : HasDegreeLE f d) (hv : 0 < variance f) : 1 ≤ d ∧ Nonempty ι

The hypotheses of MainTheorem force d ≥ 1 and a nonempty index type. In particular the division by a power of d in the printed forms of the bounds is never a division by zero under the hypotheses.

Size of the variance

theorem AaronsonAmbainis.Bridge.variance_le_quarter {ι : Type u_1} [Fintype ι] [DecidableEq ι] {P : Cube ι → ℝ} (h : ∀ (x : Cube ι), 0 ≤ P x ∧ P x ≤ 1) : variance P ≤ 1 / 4

A [0,1]-valued function has variance at most 1/4.

theorem AaronsonAmbainis.Bridge.variance_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : Cube ι → ℝ} (h : ∀ (x : Cube ι), |f x| ≤ 1) : variance f ≤ 1

A [-1,1]-valued function has variance at most 1.