English
The second derivative of qaryEntropy q with respect to p equals -1/(p(1 − p)).
Русский
Вторая производная qaryEntropy q по p равна −1/(p(1 − p)).
LaTeX
$$$ \mathrm{deriv}^{[2]} (qaryEntropy q) p = -\dfrac{1}{p\,(1 - p)} $$$
Lean4
/-- Second derivative of q-ary entropy. -/
theorem deriv2_qaryEntropy : deriv^[2] (qaryEntropy q) p = -1 / (p * (1 - p)) :=
by
simp only [Function.iterate_succ, Function.iterate_zero, Function.id_comp, Function.comp_apply]
by_cases is_x_where_nondiff :
p ≠ 0 ∧
p ≠
1 -- normal case
· obtain ⟨xne0, xne1⟩ := is_x_where_nondiff
suffices ∀ᶠ y in (𝓝 p), deriv (fun p ↦ (qaryEntropy q) p) y = log (q - 1) + log (1 - y) - log y
by
refine (Filter.EventuallyEq.deriv_eq this).trans ?_
rw [deriv_fun_sub ?_ (differentiableAt_log xne0)]
· rw [deriv.log differentiableAt_fun_id xne0]
simp only [deriv_id'', one_div]
· have {q : ℝ} (p : ℝ) : DifferentiableAt ℝ (fun p => q - p) p := by fun_prop
have d_oneminus (p : ℝ) : deriv (fun (y : ℝ) ↦ 1 - y) p = -1 := by rw [deriv_const_sub 1, deriv_id'']
simp [field, sub_ne_zero_of_ne xne1.symm, this, d_oneminus]
ring
· apply DifferentiableAt.add
simp only [differentiableAt_const]
exact DifferentiableAt.log (by fun_prop) (sub_ne_zero.mpr xne1.symm)
filter_upwards [eventually_ne_nhds xne0, eventually_ne_nhds xne1] with y xne0 h2 using deriv_qaryEntropy xne0 h2
· have : p = 0 ∨ p = 1 := Decidable.or_iff_not_not_and_not.mpr is_x_where_nondiff
rw [deriv_zero_of_not_differentiableAt]
· simp_all only [ne_eq, not_and, Decidable.not_not]
cases this <;> simp_all only [mul_zero, one_ne_zero, zero_ne_one, sub_zero, mul_one, div_zero, sub_self]
· intro h
have contAt := h.continuousAt
cases this <;> simp_all [not_continuousAt_deriv_qaryEntropy_zero, not_continuousAt_deriv_qaryEntropy_one]
