HasDegreeLE and polynomials of bounded total degree

HasDegreeLE f d holds exactly when f is the restriction to the cube of a real polynomial (MvPolynomial ι ℝ, not necessarily multilinear) of total degree at most d; this is proved for both encodings of the cube (hasDegreeLE_iff_poly_zo, hasDegreeLE_iff_poly_pm):

• zoPt x: true ↦ 1, false ↦ 0 (the cube {0,1}^n of Conjecture 6 of arXiv:0911.0996 and of Theorem 1.7 of arXiv:2410.19062);
• pmPt x: true ↦ -1, false ↦ 1 (the cube {1,-1}^n in the convention of Defs.lean; the statement ExplicitBoundPM of Conjecture.lean sends true to 1, see PrintedAA.lean).

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

The point of {0,1}^ι attached to a point of the cube (true ↦ 1, false ↦ 0).

Equations

• AaronsonAmbainis.Bridge.zoPt x i = if x i = true then 1 else 0

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

The point of {1,-1}^ι attached to a point of the cube (true ↦ -1, false ↦ 1).

Equations

• AaronsonAmbainis.Bridge.pmPt x i = if x i = true then -1 else 1

theorem AaronsonAmbainis.Bridge.hasDegreeLE_eval {ι : Type u_1} [Fintype ι] {v : Cube ι → ι → ℝ} (hv : ∀ (i : ι), HasDegreeLE (fun (x : Cube ι) => v x i) 1) (p : MvPolynomial ι ℝ) {d : ℕ} (hp : p.totalDegree ≤ d) : HasDegreeLE (fun (x : Cube ι) => (MvPolynomial.eval (v x)) p) d

Restricting a polynomial of total degree ≤ d along a point map whose coordinates have degree ≤ 1 gives a function of degree ≤ d.

theorem AaronsonAmbainis.Bridge.hasDegreeLE_eval_zo {ι : Type u_1} [Fintype ι] (p : MvPolynomial ι ℝ) {d : ℕ} (hp : p.totalDegree ≤ d) : HasDegreeLE (fun (x : Cube ι) => (MvPolynomial.eval (zoPt x)) p) d

theorem AaronsonAmbainis.Bridge.hasDegreeLE_eval_pm {ι : Type u_1} [Fintype ι] (p : MvPolynomial ι ℝ) {d : ℕ} (hp : p.totalDegree ≤ d) : HasDegreeLE (fun (x : Cube ι) => (MvPolynomial.eval (pmPt x)) p) d

theorem AaronsonAmbainis.Bridge.totalDegree_letter {ι : Type u_1} (a b : ℝ) (i : ι) : (MvPolynomial.C a + MvPolynomial.C b * MvPolynomial.X i).totalDegree ≤ 1

theorem AaronsonAmbainis.Bridge.exists_poly_of_hasDegreeLE {ι : Type u_1} [Fintype ι] {v : Cube ι → ι → ℝ} {a b : ℝ} (hv : ∀ (x : Cube ι) (i : ι), (if x i = true then -1 else 1) = a + b * v x i) {f : Cube ι → ℝ} {d : ℕ} (h : HasDegreeLE f d) : ∃ (p : MvPolynomial ι ℝ), p.totalDegree ≤ d ∧ ∀ (x : Cube ι), f x = (MvPolynomial.eval (v x)) p

A function of degree ≤ d is the restriction of a polynomial of total degree ≤ d in the coordinates v x i, as soon as the sign (-1)^{x_i} is an affine function of v x i.

theorem AaronsonAmbainis.Bridge.hasDegreeLE_iff_poly_zo {ι : Type u_1} [Fintype ι] {f : Cube ι → ℝ} {d : ℕ} : HasDegreeLE f d ↔ ∃ (p : MvPolynomial ι ℝ), p.totalDegree ≤ d ∧ ∀ (x : Cube ι), f x = (MvPolynomial.eval (zoPt x)) p

HasDegreeLE f d iff f is a polynomial of total degree ≤ d in the 0/1 coordinates.

theorem AaronsonAmbainis.Bridge.hasDegreeLE_iff_poly_pm {ι : Type u_1} [Fintype ι] {f : Cube ι → ℝ} {d : ℕ} : HasDegreeLE f d ↔ ∃ (p : MvPolynomial ι ℝ), p.totalDegree ≤ d ∧ ∀ (x : Cube ι), f x = (MvPolynomial.eval (pmPt x)) p

HasDegreeLE f d iff f is a polynomial of total degree ≤ d in the ±1 coordinates.