Homogeneous polynomials
A multivariate polynomial φ is homogeneous of degree n
if all monomials occuring in φ have degree n.
Main definitions/lemmas
is_homogeneous φ n: a predicate that asserts thatφis homogeneous of degreen.homogeneous_component n: the additive morphism that projects polynomials onto their summand that is homogeneous of degreen.sum_homogeneous_component: every polynomial is the sum of its homogeneous components
def
mv_polynomial.is_homogeneous
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(φ : mv_polynomial σ R)
(n : ℕ) :
Prop
A multivariate polynomial φ is homogeneous of degree n
if all monomials occuring in φ have degree n.
Equations
- φ.is_homogeneous n = ∀ ⦃d : σ →₀ ℕ⦄, mv_polynomial.coeff d φ ≠ 0 → ∑ (i : σ) in d.support, ⇑d i = n
theorem
mv_polynomial.is_homogeneous_monomial
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(d : σ →₀ ℕ)
(r : R)
(n : ℕ)
(hn : ∑ (i : σ) in d.support, ⇑d i = n) :
(mv_polynomial.monomial d r).is_homogeneous n
theorem
mv_polynomial.is_homogeneous_zero
(σ : Type u_1)
(R : Type u_3)
[comm_semiring R]
(n : ℕ) :
0.is_homogeneous n
theorem
mv_polynomial.is_homogeneous_one
(σ : Type u_1)
(R : Type u_3)
[comm_semiring R] :
1.is_homogeneous 0
theorem
mv_polynomial.is_homogeneous.coeff_eq_zero
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
{φ : mv_polynomial σ R}
{n : ℕ}
(hφ : φ.is_homogeneous n)
(d : σ →₀ ℕ)
(hd : ∑ (i : σ) in d.support, ⇑d i ≠ n) :
mv_polynomial.coeff d φ = 0
theorem
mv_polynomial.is_homogeneous.inj_right
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
{φ : mv_polynomial σ R}
{m n : ℕ}
(hm : φ.is_homogeneous m)
(hn : φ.is_homogeneous n)
(hφ : φ ≠ 0) :
m = n
theorem
mv_polynomial.is_homogeneous.add
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
{φ ψ : mv_polynomial σ R}
{n : ℕ}
(hφ : φ.is_homogeneous n)
(hψ : ψ.is_homogeneous n) :
(φ + ψ).is_homogeneous n
theorem
mv_polynomial.is_homogeneous.sum
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
{ι : Type u_2}
(s : finset ι)
(φ : ι → mv_polynomial σ R)
(n : ℕ)
(h : ∀ (i : ι), i ∈ s → (φ i).is_homogeneous n) :
(∑ (i : ι) in s, φ i).is_homogeneous n
theorem
mv_polynomial.is_homogeneous.mul
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
{φ ψ : mv_polynomial σ R}
{m n : ℕ}
(hφ : φ.is_homogeneous m)
(hψ : ψ.is_homogeneous n) :
(φ * ψ).is_homogeneous (m + n)
theorem
mv_polynomial.is_homogeneous.prod
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
{ι : Type u_2}
(s : finset ι)
(φ : ι → mv_polynomial σ R)
(n : ι → ℕ)
(h : ∀ (i : ι), i ∈ s → (φ i).is_homogeneous (n i)) :
(∏ (i : ι) in s, φ i).is_homogeneous (∑ (i : ι) in s, n i)
theorem
mv_polynomial.is_homogeneous.total_degree
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
{φ : mv_polynomial σ R}
{n : ℕ}
(hφ : φ.is_homogeneous n)
(h : φ ≠ 0) :
φ.total_degree = n
def
mv_polynomial.homogeneous_component
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(n : ℕ) :
mv_polynomial σ R →+ mv_polynomial σ R
homogeneous_component n φ is the part of φ that is homogeneous of degree n.
See sum_homogeneous_component for the statement that φ is equal to the sum
of all its homogeneous components.
Equations
- mv_polynomial.homogeneous_component n = {to_fun := λ (φ : mv_polynomial σ R), ∑ (d : σ →₀ ℕ) in finset.filter (λ (d : σ →₀ ℕ), ∑ (i : σ) in d.support, ⇑d i = n) φ.support, mv_polynomial.monomial d (mv_polynomial.coeff d φ), map_zero' := _, map_add' := _}
theorem
mv_polynomial.homogeneous_component_apply
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(n : ℕ)
(φ : mv_polynomial σ R) :
⇑(mv_polynomial.homogeneous_component n) φ = ∑ (d : σ →₀ ℕ) in finset.filter (λ (d : σ →₀ ℕ), ∑ (i : σ) in d.support, ⇑d i = n) φ.support, mv_polynomial.monomial d (mv_polynomial.coeff d φ)
theorem
mv_polynomial.homogeneous_component_is_homogeneous
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(n : ℕ)
(φ : mv_polynomial σ R) :
theorem
mv_polynomial.homogeneous_component_zero
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(φ : mv_polynomial σ R) :
theorem
mv_polynomial.homogeneous_component_eq_zero'
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(n : ℕ)
(φ : mv_polynomial σ R)
(h : ∀ (d : σ →₀ ℕ), d ∈ φ.support → ∑ (i : σ) in d.support, ⇑d i ≠ n) :
theorem
mv_polynomial.homogeneous_component_eq_zero
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(n : ℕ)
(φ : mv_polynomial σ R)
(h : φ.total_degree < n) :
theorem
mv_polynomial.sum_homogeneous_component
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(φ : mv_polynomial σ R) :
∑ (i : ℕ) in finset.range (φ.total_degree + 1), ⇑(mv_polynomial.homogeneous_component i) φ = φ