English
If p ≤ weightedOrder of f and q ≤ weightedOrder of g, then the weighted homogeneous component of weight p+q of f*g equals the product of the components of weight p and q respectively.
Русский
Если p ≤ weightedOrder(f) и q ≤ weightedOrder(g), то весовая компонента веса p+q у произведения f*g равна произведению весовых компонентов p и q.
LaTeX
$$$ weightedHomogeneousComponent\ w (p+q) (f*g) = weightedHomogeneousComponent\ w p f * weightedHomogeneousComponent\ w q g $$$
Lean4
theorem weightedHomogeneousComponent_mul_of_le_weightedOrder {f g : MvPowerSeries σ R} {p q : ℕ}
(hf : p ≤ f.weightedOrder w) (hg : q ≤ g.weightedOrder w) :
weightedHomogeneousComponent w (p + q) (f * g) =
weightedHomogeneousComponent w p f * weightedHomogeneousComponent w q g :=
by
classical
ext d
rw [coeff_weightedHomogeneousComponent]
split_ifs with hd
· apply Finset.sum_congr rfl
intro x hx
rw [Finset.mem_antidiagonal] at hx
rw [← hx, map_add] at hd
simp only [coeff_weightedHomogeneousComponent]
rcases trichotomy_of_add_eq_add hd with h | h | h
· rw [if_pos h.1, if_pos h.2]
· rw [if_neg (ne_of_lt h), zero_mul]
rw [← ENat.coe_lt_coe] at h
rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hf), zero_mul]
· rw [if_neg (ne_of_lt h), mul_zero]
rw [← ENat.coe_lt_coe] at h
rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hg), mul_zero]
· symm
apply IsWeightedHomogeneous.coeff_eq_zero _ hd
exact
IsWeightedHomogeneous.mul (isWeightedHomogeneous_weightedHomogeneousComponent w f p)
(isWeightedHomogeneous_weightedHomogeneousComponent w g q)
