fwdDiff_iter_comp_add

Mathlib.Algebra.Group.ForwardDiff

URI: https://scilib.ai/kg/mathlib#fwdDiff_iter_comp_add

← MathLib Explorer

English

For all j, k ∈ ℕ, Δ_1^[k] (x ↦ C(x, k + j)) = x ↦ C(x, j).

Русский

Для всех j, k ∈ ℕ, Δ_1^[k] (x ↦ C(x, k + j)) = x ↦ C(x, j).

LaTeX

$$$ \Delta_1^{[k]} \bigl(x \mapsto {x \choose k + j}\bigr) = \bigl(x \mapsto {x \choose j}\bigr) $$$

Lean4

theorem fwdDiff_iter_comp_add (f : M → G) (m : M) (n : ℕ) (y : M) :
    Δ_[h]^[n] (fun r ↦ f (r + m)) y = (Δ_[h]^[n] f) (y + m) := by simp [fwdDiff_iter_eq_sum_shift, add_right_comm]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru