sumTransform_def — Mathlib

English

An explicit form of sumTransform expresses the same quantity via powers and divisions, aligning with the definition.

Русский

Явное представление sumTransform через степени и деления согласуется с определением.

LaTeX

$$$\text{sumTransform}(p,g;n_0,n) = n^p \cdot \sum_{u=n_0}^{n-1} \dfrac{g(u)}{u^{p+1}}$$$

Lean4

theorem sumTransform_def {p : ℝ} {g : ℝ → ℝ} {n₀ n : ℕ} :
    sumTransform p g n₀ n = n ^ p * ∑ u ∈ Finset.Ico n₀ n, g u / u ^ (p + 1) :=
  rfl

Похожие утверждения