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 → ℕ → 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 → d.support.sum (λ (i : σ), ⇑d i) = n
theorem
mv_polynomial.is_homogeneous_monomial
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(d : σ →₀ ℕ)
(r : R)
(n : ℕ) :
d.support.sum (λ (i : σ), ⇑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 : σ →₀ ℕ) :
theorem
mv_polynomial.is_homogeneous.inj_right
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
{φ : mv_polynomial σ R}
{m n : ℕ} :
φ.is_homogeneous m → φ.is_homogeneous n → φ ≠ 0 → m = n
theorem
mv_polynomial.is_homogeneous.add
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
{φ ψ : mv_polynomial σ R}
{n : ℕ} :
φ.is_homogeneous n → ψ.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 : ℕ) :
(∀ (i : ι), i ∈ s → (φ i).is_homogeneous n) → (s.sum (λ (i : ι), φ 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 : ℕ} :
φ.is_homogeneous m → ψ.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 : ι → ℕ) :
(∀ (i : ι), i ∈ s → (φ i).is_homogeneous (n i)) → (s.prod (λ (i : ι), φ i)).is_homogeneous (s.sum (λ (i : ι), n i))
theorem
mv_polynomial.is_homogeneous.total_degree
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
{φ : mv_polynomial σ R}
{n : ℕ} :
φ.is_homogeneous n → φ ≠ 0 → φ.total_degree = n
def
mv_polynomial.homogeneous_component
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R] :
ℕ → 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), (finset.filter (λ (d : σ →₀ ℕ), d.support.sum (λ (i : σ), ⇑d i) = n) φ.support).sum (λ (d : σ →₀ ℕ), 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) φ = (finset.filter (λ (d : σ →₀ ℕ), d.support.sum (λ (i : σ), ⇑d i) = n) φ.support).sum (λ (d : σ →₀ ℕ), 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) :
theorem
mv_polynomial.homogeneous_component_eq_zero
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(n : ℕ)
(φ : mv_polynomial σ R) :
φ.total_degree < n → ⇑(mv_polynomial.homogeneous_component n) φ = 0
theorem
mv_polynomial.sum_homogeneous_component
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(φ : mv_polynomial σ R) :
(finset.range (φ.total_degree + 1)).sum (λ (i : ℕ), ⇑(mv_polynomial.homogeneous_component i) φ) = φ