Derivatives at zero of a finite sum of logarithms log (1 - 2 t aⱼ)

For real weights a : ι → ℝ indexed by a finite type and a real constant c, consider t ↦ -c / 2 * ∑ j, log (1 - 2 * t * a j). When c is a positive natural number coerced to ℝ, this is locally the cumulant-generating function of a weighted sum of independent chi-squared variables, each with c degrees of freedom. For arbitrary real c, this file computes its first two derivatives at 0: c * ∑ j, a j and 2 * c * ∑ j, a j ^ 2.

Main results

• TauCeti.hasDerivAt_neg_half_mul_sum_log — the first derivative at 0 is c * ∑ j, a j;
• TauCeti.iteratedDeriv_two_neg_half_mul_sum_log — the second derivative at 0 is 2 * c * ∑ j, a j ^ 2.

theorem TauCeti.hasDerivAt_neg_half_mul_sum_log {ι : Type u_1} [Fintype ι] (c : ℝ) (a : ι → ℝ) : HasDerivAt (fun (t : ℝ) => -c / 2 * ∑ j : ι, Real.log (1 - 2 * t * a j)) (c * ∑ j : ι, a j) 0

The function t ↦ -c / 2 * ∑ j, log (1 - 2 * t * a j) has derivative c * ∑ j, a j at 0.

theorem TauCeti.iteratedDeriv_two_neg_half_mul_sum_log {ι : Type u_1} [Fintype ι] (c : ℝ) (a : ι → ℝ) : iteratedDeriv 2 (fun (t : ℝ) => -c / 2 * ∑ j : ι, Real.log (1 - 2 * t * a j)) 0 = 2 * c * ∑ j : ι, a j ^ 2

The function t ↦ -c / 2 * ∑ j, log (1 - 2 * t * a j) has second derivative 2 * c * ∑ j, a j ^ 2 at 0.