bernoulliPowerSeries_mul_exp_sub_one

English

Bernoulli power series multiplied by (exp − 1) yields the indeterminate X: bernoulliPowerSeries ∙ (exp − 1) = X.

Русский

Умножение экспоненциальной порождающей функции Бернулли на (e^X − 1) даёт X.

LaTeX

$$$\text{bernoulliPowerSeries}(A) \cdot (\\exp A - 1) = X$$$

Lean4

theorem bernoulliPowerSeries_mul_exp_sub_one : bernoulliPowerSeries A * (exp A - 1) = X :=
  by
  ext n
  cases n with
  | zero => simp
  | succ
    n =>
    simp only [bernoulliPowerSeries, coeff_mul, coeff_X, sum_antidiagonal_succ', one_div, coeff_mk, coeff_one,
      coeff_exp, LinearMap.map_sub, factorial, if_pos, cast_succ, cast_mul, sub_zero, add_eq_zero, if_false,
      one_ne_zero, and_false, ← RingHom.map_mul, ← map_sum]
    cases n with
    | zero => simp
    | succ n =>
      rw [if_neg n.succ_succ_ne_one]
      have hfact : ∀ m, (m ! : ℚ) ≠ 0 := fun m => mod_cast factorial_ne_zero m
      have hite2 : ite (n.succ = 0) 1 0 = (0 : ℚ) := if_neg n.succ_ne_zero
      simp only [CharP.cast_eq_zero, zero_add, inv_one, map_one, sub_self, mul_zero]
      rw [← map_zero (algebraMap ℚ A), ← zero_div (n.succ ! : ℚ), ← hite2, ← bernoulli_spec', sum_div]
      refine congr_arg (algebraMap ℚ A) (sum_congr rfl fun x h => eq_div_of_mul_eq (hfact n.succ) ?_)
      rw [mem_antidiagonal] at h
      rw [← h, add_choose, cast_div_charZero (factorial_mul_factorial_dvd_factorial_add _ _)]
      simp [field, mul_comm _ (bernoulli x.1), mul_assoc]

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