Degree calculus for HasDegreeLE

Rules for the predicate HasDegreeLE of Defs.lean: characters, constants, sums, constant multiples, monotonicity in the bound, products (the degrees add), powers, finite products, a real polynomial of a function of degree at most 1, and the indicator of a coordinate. They serve step (b) of the proof of the block inequality (Lemma 6.4 of the paper): the function G constructed there has degree at most d m (Row.hasDegreeLE_gadget in Row/Gadget.lean).

theorem AaronsonAmbainis.Row.hasDegreeLE_congr {β : Type u_1} [Fintype β] {f g : Cube β → ℝ} {k : ℕ} (h : HasDegreeLE f k) (hfg : ∀ (w : Cube β), g w = f w) : HasDegreeLE g k

theorem AaronsonAmbainis.Row.hasDegreeLE_chi {β : Type u_1} [Fintype β] (S : Finset β) {k : ℕ} (h : S.card ≤ k) : HasDegreeLE (chi S) k

theorem AaronsonAmbainis.Row.hasDegreeLE_zero {β : Type u_1} [Fintype β] (k : ℕ) : HasDegreeLE (fun (x : Cube β) => 0) k

theorem AaronsonAmbainis.Row.hasDegreeLE_add {β : Type u_1} [Fintype β] {f g : Cube β → ℝ} {k : ℕ} (hf : HasDegreeLE f k) (hg : HasDegreeLE g k) : HasDegreeLE (fun (w : Cube β) => f w + g w) k

theorem AaronsonAmbainis.Row.hasDegreeLE_const_mul {β : Type u_1} [Fintype β] (a : ℝ) {f : Cube β → ℝ} {k : ℕ} (hf : HasDegreeLE f k) : HasDegreeLE (fun (w : Cube β) => a * f w) k

theorem AaronsonAmbainis.Row.hasDegreeLE_const {β : Type u_1} [Fintype β] (a : ℝ) (k : ℕ) : HasDegreeLE (fun (x : Cube β) => a) k

theorem AaronsonAmbainis.Row.hasDegreeLE_sum {β : Type u_1} [Fintype β] {α : Type u_2} (s : Finset α) (F : α → Cube β → ℝ) {k : ℕ} (h : ∀ j ∈ s, HasDegreeLE (F j) k) : HasDegreeLE (fun (w : Cube β) => ∑ j ∈ s, F j w) k

theorem AaronsonAmbainis.Row.hasDegreeLE_mono {β : Type u_1} [Fintype β] {f : Cube β → ℝ} {k l : ℕ} (hkl : k ≤ l) (hf : HasDegreeLE f k) : HasDegreeLE f l

theorem AaronsonAmbainis.Row.hasDegreeLE_mul {β : Type u_1} [Fintype β] {f g : Cube β → ℝ} {k l : ℕ} (hf : HasDegreeLE f k) (hg : HasDegreeLE g l) : HasDegreeLE (fun (w : Cube β) => f w * g w) (k + l)

Products add degrees.

theorem AaronsonAmbainis.Row.hasDegreeLE_pow {β : Type u_1} [Fintype β] {f : Cube β → ℝ} {k : ℕ} (hf : HasDegreeLE f k) (n : ℕ) : HasDegreeLE (fun (w : Cube β) => f w ^ n) (n * k)

theorem AaronsonAmbainis.Row.hasDegreeLE_prod {β : Type u_1} [Fintype β] {α : Type u_2} (s : Finset α) (F : α → Cube β → ℝ) {k : ℕ} (h : ∀ j ∈ s, HasDegreeLE (F j) k) : HasDegreeLE (fun (w : Cube β) => ∏ j ∈ s, F j w) (s.card * k)

theorem AaronsonAmbainis.Row.hasDegreeLE_polyEval {β : Type u_1} [Fintype β] (Q : Polynomial ℝ) {g : Cube β → ℝ} (hg : HasDegreeLE g 1) : HasDegreeLE (fun (w : Cube β) => Polynomial.eval (g w) Q) Q.natDegree

A real polynomial of a function of degree at most 1 has degree at most its natDegree.

theorem AaronsonAmbainis.Row.hasDegreeLE_indicator {β : Type u_1} [Fintype β] (b : β) : HasDegreeLE (fun (w : Cube β) => if w b = true then 1 else 0) 1

The indicator of a coordinate has degree at most 1.