Closure properties of HasDegreeLE #
HasDegreeLE is closed under constants, sums, scalar multiples, products (degrees add), powers
and finite products; the coordinate functions have degree at most 1.
These are what makes HasDegreeLE a degree in the usual sense.
theorem
AaronsonAmbainis.Bridge.hasDegreeLE_const
{ι : Type u_1}
[Fintype ι]
(a : ℝ)
(d : ℕ)
:
HasDegreeLE (fun (x : Cube ι) => a) d
theorem
AaronsonAmbainis.Bridge.hasDegreeLE_add
{ι : Type u_1}
[Fintype ι]
{f g : Cube ι → ℝ}
{d : ℕ}
(hf : HasDegreeLE f d)
(hg : HasDegreeLE g d)
:
HasDegreeLE (fun (x : Cube ι) => f x + g x) d
theorem
AaronsonAmbainis.Bridge.hasDegreeLE_smul
{ι : Type u_1}
[Fintype ι]
(r : ℝ)
{f : Cube ι → ℝ}
{d : ℕ}
(hf : HasDegreeLE f d)
:
HasDegreeLE (fun (x : Cube ι) => r * f x) d
theorem
AaronsonAmbainis.Bridge.hasDegreeLE_sum
{ι : Type u_1}
[Fintype ι]
{α : Type u_2}
(s : Finset α)
{F : α → Cube ι → ℝ}
{d : ℕ}
(h : ∀ k ∈ s, HasDegreeLE (F k) d)
:
HasDegreeLE (fun (x : Cube ι) => ∑ k ∈ s, F k x) d
theorem
AaronsonAmbainis.Bridge.hasDegreeLE_chi
{ι : Type u_1}
[Fintype ι]
(S : Finset ι)
:
HasDegreeLE (chi S) S.card
theorem
AaronsonAmbainis.Bridge.hasDegreeLE_mul
{ι : Type u_1}
[Fintype ι]
{f g : Cube ι → ℝ}
{d e : ℕ}
(hf : HasDegreeLE f d)
(hg : HasDegreeLE g e)
:
HasDegreeLE (fun (x : Cube ι) => f x * g x) (d + e)
Degrees add under multiplication.
theorem
AaronsonAmbainis.Bridge.hasDegreeLE_pow
{ι : Type u_1}
[Fintype ι]
{g : Cube ι → ℝ}
{k : ℕ}
(hg : HasDegreeLE g k)
(m : ℕ)
:
HasDegreeLE (fun (x : Cube ι) => g x ^ m) (m * k)
theorem
AaronsonAmbainis.Bridge.hasDegreeLE_prod
{ι : Type u_1}
[Fintype ι]
{α : Type u_2}
(s : Finset α)
{F : α → Cube ι → ℝ}
{k : α → ℕ}
(h : ∀ a ∈ s, HasDegreeLE (F a) (k a))
:
HasDegreeLE (fun (x : Cube ι) => ∏ a ∈ s, F a x) (∑ a ∈ s, k a)