Checks of the definitions: flips, degree zero, the dictator

flipSet / diffSet are mutually inverse, HasDegreeLE is monotone, degree 0 means constant, and the dictator x ↦ (-1)^{x_j} has degree exactly 1, variance 1 and influence 1; so the hypotheses of MainTheorem are satisfiable (aa_hyps_satisfiable). These are checks of the definitions of Defs.lean; the proofs of Chain.lean do not depend on them.

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

theorem AaronsonAmbainis.Bridge.flipSet_empty {ι : Type u_1} [DecidableEq ι] (x : Cube ι) : flipSet x ∅ = x

theorem AaronsonAmbainis.Bridge.flipSet_singleton_self {ι : Type u_1} [DecidableEq ι] (x : Cube ι) (j : ι) : flipSet x {j} j = !x j

theorem AaronsonAmbainis.Bridge.flipSet_singleton_ne {ι : Type u_1} [DecidableEq ι] (x : Cube ι) {i j : ι} (h : i ≠ j) : flipSet x {j} i = x i

noncomputable def AaronsonAmbainis.Bridge.dict {ι : Type u_1} (j : ι) : Cube ι → ℝ

The dictator x ↦ (-1)^{x_j}.

Equations

• AaronsonAmbainis.Bridge.dict j x = if x j = true then -1 else 1

theorem AaronsonAmbainis.Bridge.dict_abs_le_one {ι : Type u_1} (j : ι) (x : Cube ι) : |dict j x| ≤ 1

theorem AaronsonAmbainis.Bridge.dict_sq {ι : Type u_1} (j : ι) (x : Cube ι) : dict j x ^ 2 = 1

theorem AaronsonAmbainis.Bridge.dict_flip {ι : Type u_1} [DecidableEq ι] (j : ι) (x : Cube ι) : dict j (flipSet x {j}) = -dict j x

theorem AaronsonAmbainis.Bridge.diffSet_flipSet {ι : Type u_1} [Fintype ι] [DecidableEq ι] (x : Cube ι) (S : Finset ι) : diffSet x (flipSet x S) = S

Δ(x, x^S) = S.

theorem AaronsonAmbainis.Bridge.flipSet_diffSet {ι : Type u_1} [Fintype ι] [DecidableEq ι] (x y : Cube ι) : flipSet x (diffSet x y) = y

x^{Δ(x,y)} = y.

theorem AaronsonAmbainis.Bridge.antipode_eq_flipSet_univ {ι : Type u_1} [Fintype ι] [DecidableEq ι] (x : Cube ι) : antipode x = flipSet x Finset.univ

antipode x = x^{[n]}.

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

The cube over ι has 2^n points.

theorem AaronsonAmbainis.Bridge.hasDegreeLE_mono {ι : Type u_1} [Fintype ι] {f : Cube ι → ℝ} {d d' : ℕ} (h : HasDegreeLE f d) (hdd : d ≤ d') : HasDegreeLE f d'

Monotonicity of HasDegreeLE in the degree.

theorem AaronsonAmbainis.Bridge.chi_empty {ι : Type u_1} (x : Cube ι) : chi ∅ x = 1

theorem AaronsonAmbainis.Bridge.hasDegreeLE_zero_iff {ι : Type u_1} [Fintype ι] {f : Cube ι → ℝ} : HasDegreeLE f 0 ↔ ∃ (a : ℝ), ∀ (x : Cube ι), f x = a

Degree at most 0 is the same as constant.

theorem AaronsonAmbainis.Bridge.hasDegreeLE_zero_const {ι : Type u_1} [Fintype ι] {f : Cube ι → ℝ} (h : HasDegreeLE f 0) (x y : Cube ι) : f x = f y

HasDegreeLE f 0 implies f constant.

The dictator

theorem AaronsonAmbainis.Bridge.dict_eq_chi {ι : Type u_1} (j : ι) (x : Cube ι) : dict j x = chi {j} x

theorem AaronsonAmbainis.Bridge.dict_hasDegreeLE_one {ι : Type u_1} [Fintype ι] (j : ι) : HasDegreeLE (dict j) 1

theorem AaronsonAmbainis.Bridge.dict_not_hasDegreeLE_zero {ι : Type u_1} [Fintype ι] (j : ι) : ¬HasDegreeLE (dict j) 0

A dictator does not have degree at most 0.

theorem AaronsonAmbainis.Bridge.sum_dict {ι : Type u_1} [Fintype ι] [DecidableEq ι] (j : ι) : ∑ x : Cube ι, dict j x = 0

theorem AaronsonAmbainis.Bridge.mean_dict {ι : Type u_1} [Fintype ι] [DecidableEq ι] (j : ι) : mean (dict j) = 0

theorem AaronsonAmbainis.Bridge.variance_dict {ι : Type u_1} [Fintype ι] [DecidableEq ι] (j : ι) : variance (dict j) = 1

theorem AaronsonAmbainis.Bridge.inflR_dict_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] (j : ι) : inflR (dict j) j = 1

theorem AaronsonAmbainis.Bridge.aa_hyps_dict {ι : Type u_1} [Fintype ι] [DecidableEq ι] (j : ι) : (∀ (x : Cube ι), |dict j x| ≤ 1) ∧ HasDegreeLE (dict j) 1 ∧ 0 < variance (dict j) ∧ variance (dict j) = 1 ∧ inflR (dict j) j = 1

Non-vacuity of MainTheorem: on any index type with a chosen coordinate j, the dictator satisfies all three hypotheses with d = 1, has variance 1 and influence 1 at j.

theorem AaronsonAmbainis.Bridge.aa_hyps_satisfiable : ∃ (f : Cube (Fin 1) → ℝ), (∀ (x : Cube (Fin 1)), |f x| ≤ 1) ∧ HasDegreeLE f 1 ∧ 0 < variance f ∧ variance f = 1 ∧ inflR f 0 = 1

Same, on the concrete index type Fin 1.

theorem AaronsonAmbainis.Bridge.aa_conclusion_dict {ι : Type u_1} [Fintype ι] [DecidableEq ι] (j : ι) : ∃ (j' : ι), 3 * variance (dict j) ^ 5 ≤ 50000 * Real.pi ^ 8 * ↑1 ^ 12 * inflR (dict j) j' ^ 2

The conclusion of MainTheorem (with d = 1) is true for the dictator.

theorem AaronsonAmbainis.Bridge.rowBound_conclusion_dict {ι : Type u_1} [Fintype ι] (j : ι) : ∃ (c : Cube ι → ι → ℝ), (∀ (x y : Cube ι), |(1 + dict j x) / 2 - (1 + dict j y) / 2| ≤ ∑ i ∈ diffSet x y, c x i) ∧ ∀ (x : Cube ι), ∑ i : ι, c x i ≤ Real.pi ^ 2 / 4 * ↑1 ^ 2

The conclusion of RowBound (with d = 1) is true for h = (1 + dictator)/2, with the weights c x i = [i = j].