logDeriv_prod_sineTerm_eq_sum_cotTerm

English

The log derivative of the finite product equals the sum of cotTerm terms.

Русский

Логарифмическая производная произведения равна сумме cotTerm по индексам.

LaTeX

$$$$\forall x \in \mathbb{C},\; x \in \mathbb{C}_{\mathbb{Z}} \Rightarrow \\ \logDeriv\left( z \mapsto \prod_{j=0}^{n-1} (1 + \text{sineTerm}(z,j))\right) x = \sum_{j=0}^{n-1} \cotTerm(x,j).$$$$

Lean4

theorem logDeriv_prod_sineTerm_eq_sum_cotTerm (hx : x ∈ ℂ_ℤ) (n : ℕ) :
    logDeriv (fun (z : ℂ) ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x = ∑ j ∈ Finset.range n, cotTerm x j :=
  by
  rw [logDeriv_prod]
  · simp_rw [logDeriv_sineTerm_eq_cotTerm hx]
  · exact fun i _ ↦ sineTerm_ne_zero hx i
  · fun_prop

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