Multilinear extension (one variable)

The one-variable multilinear extension of a Boolean-indexed value into a commutative ring, mle₁ f x = f false · (1 - x) + f true · x, and its defining interpolation identities at the Boolean points 0 and 1 (roadmap track L1, toward arithmetization and the sum-check protocol). This is the atomic building block of the multilinear extension of a full Boolean function, and the reason arithmetized formulas agree with their Boolean originals on the cube.

Main results

• mle₁ — the one-variable multilinear interpolant
• mle₁_zero, mle₁_one — it recovers f false at 0 and f true at 1
• mle₁_bool — it agrees with f at both Boolean points

def Complexity.mle₁ {R : Type u_1} [CommRing R] (f : Bool → R) (x : R) : R

The one-variable multilinear extension of f : Bool → R into a commutative ring R: the unique degree-≤ 1 polynomial interpolating f false at 0 and f true at 1.

Equations

• Complexity.mle₁ f x = f false * (1 - x) + f true * x

@[simp]

theorem Complexity.mle₁_zero {R : Type u_1} [CommRing R] (f : Bool → R) : mle₁ f 0 = f false

@[simp]

theorem Complexity.mle₁_one {R : Type u_1} [CommRing R] (f : Bool → R) : mle₁ f 1 = f true

theorem Complexity.mle₁_bool {R : Type u_1} [CommRing R] (f : Bool → R) (b : Bool) : mle₁ f (if b = true then 1 else 0) = f b

At either Boolean point (0 or 1), the extension agrees with f.