Bounded multilinear extension

Lemma 6.2 (Extension) of the paper, Row.abs_multilinear_le_one: if ∑_T a_T chi_T is bounded by 1 in absolute value on the cube, then ∑_T a_T ∏_{i ∈ T} u_i is bounded by 1 for every real vector u with |u_i| ≤ 1. The proof averages over the product measure weight u.

noncomputable def AaronsonAmbainis.Row.weight {ι : Type u_1} [Fintype ι] (u : ι → ℝ) (z : Cube ι) : ℝ

The product weight W_u(z) = ∏_i (1 + sgn(z_i) u_i) / 2.

Equations

• AaronsonAmbainis.Row.weight u z = ∏ i : ι, (1 + AaronsonAmbainis.Row.sgn (z i) * u i) / 2

theorem AaronsonAmbainis.Row.weight_nonneg {ι : Type u_1} [Fintype ι] (u : ι → ℝ) (hu : ∀ (i : ι), |u i| ≤ 1) (z : Cube ι) : 0 ≤ weight u z

theorem AaronsonAmbainis.Row.sum_weight_mul_chi {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : ι → ℝ) (T : Finset ι) : ∑ z : Cube ι, weight u z * chi T z = ∏ i ∈ T, u i

The weight u-average of the character chi T is ∏_{i ∈ T} u_i.

theorem AaronsonAmbainis.Row.sum_weight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : ι → ℝ) : ∑ z : Cube ι, weight u z = 1

theorem AaronsonAmbainis.Row.abs_multilinear_le_one {ι : Type u_1} [Fintype ι] (a : Finset ι → ℝ) (h : ∀ (z : Cube ι), |∑ T : Finset ι, a T * chi T z| ≤ 1) (u : ι → ℝ) (hu : ∀ (i : ι), |u i| ≤ 1) : |∑ T : Finset ι, a T * ∏ i ∈ T, u i| ≤ 1

Bounded multilinear extension (Lemma 6.2 of the paper).