English
A simplification of the weighted sum identity for all algebraic contexts; expresses distributivity with scalar weights.
Русский
Упрощение идентичности со взвешенной суммой для всех контекстов алгебры; выражает дистрибутивность по весам.
LaTeX
$$$\\text{(simp version)}\\;\\text{(details omitted)}$$$
Lean4
/-- Euler's identity for weighted homogeneous polynomials. -/
theorem sum_weight_X_mul_pderiv {w : σ → ℕ} (h : φ.IsWeightedHomogeneous w n) :
∑ i : σ, w i • (X i * pderiv i φ) = n • φ :=
by
rw [← mem_weightedHomogeneousSubmodule, weightedHomogeneousSubmodule_eq_finsupp_supported,
supported_eq_span_single] at h
refine Submodule.span_induction ?_ ?_ (fun p q _ _ hp hq ↦ ?_) (fun r p _ h ↦ ?_) h
· rintro _ ⟨m, hm, rfl⟩
simp_rw [single_eq_monomial, X_mul_pderiv_monomial, smul_smul, ← sum_smul, mul_comm (w _)]
congr
rwa [Set.mem_setOf, weight_apply, sum_fintype] at hm
intro; apply zero_smul
· simp
· simp_rw [map_add, left_distrib, smul_add, sum_add_distrib, hp, hq]
· simp_rw [(pderiv _).map_smul, nsmul_eq_mul, mul_smul_comm, ← Finset.smul_sum, ← nsmul_eq_mul, h]
