HasDegreeLE with 0/1 monomials

HasDegreeLE is defined with the characters ∏_{i∈S} (-1)^{x_i}. Theorem 1.7 of arXiv:2410.19062 and Conjecture 6 of arXiv:0911.0996 speak of polynomials in the 0/1 variables. The definition with the 0/1 monomials ∏_{i∈S} x_i is equivalent (hasDegreeLE_iff_01).

noncomputable def AaronsonAmbainis.Bridge.mon {ι : Type u_1} (φ : Bool → ℝ) (S : Finset ι) (x : Cube ι) : ℝ

Monomial in the letters φ (x i).

Equations

• AaronsonAmbainis.Bridge.mon φ S x = ∏ i ∈ S, φ (x i)

def AaronsonAmbainis.Bridge.HasDegLE {ι : Type u_1} [Fintype ι] (φ : Bool → ℝ) (f : Cube ι → ℝ) (d : ℕ) : Prop

Degree at most d with respect to the monomials built from the letter φ.

Equations

• One or more equations did not get rendered due to their size.

def AaronsonAmbainis.Bridge.HasDegreeLE01 {ι : Type u_1} [Fintype ι] (f : Cube ι → ℝ) (d : ℕ) : Prop

The analogue of HasDegreeLE with the 0/1 monomials ∏_{i∈S} x_i.

Equations

• One or more equations did not get rendered due to their size.

theorem AaronsonAmbainis.Bridge.hasDegreeLE_iff_hasDegLE {ι : Type u_1} [Fintype ι] {f : Cube ι → ℝ} {d : ℕ} : HasDegreeLE f d ↔ HasDegLE (fun (b : Bool) => if b = true then -1 else 1) f d

theorem AaronsonAmbainis.Bridge.hasDegreeLE01_iff_hasDegLE {ι : Type u_1} [Fintype ι] {f : Cube ι → ℝ} {d : ℕ} : HasDegreeLE01 f d ↔ HasDegLE (fun (b : Bool) => if b = true then 1 else 0) f d

theorem AaronsonAmbainis.Bridge.mon_affine {ι : Type u_1} [Fintype ι] [DecidableEq ι] {φ ψ : Bool → ℝ} {α β : ℝ} (hψ : ∀ (b : Bool), ψ b = β * φ b + α) (S : Finset ι) (x : Cube ι) : mon ψ S x = ∑ T : Finset ι, if T ⊆ S then β ^ T.card * α ^ (S \ T).card * mon φ T x else 0

Expansion of a monomial after an affine change of letter ψ = β φ + α.

theorem AaronsonAmbainis.Bridge.hasDegLE_of_affine {ι : Type u_1} [Fintype ι] {φ ψ : Bool → ℝ} {α β : ℝ} (hψ : ∀ (b : Bool), ψ b = β * φ b + α) {f : Cube ι → ℝ} {d : ℕ} (h : HasDegLE ψ f d) : HasDegLE φ f d

An affine change of letter does not raise the degree.

theorem AaronsonAmbainis.Bridge.hasDegreeLE_iff_01 {ι : Type u_1} [Fintype ι] {f : Cube ι → ℝ} {d : ℕ} : HasDegreeLE f d ↔ HasDegreeLE01 f d

HasDegreeLE (characters) is equivalent to the definition with 0/1 monomials.