-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
/-- Second derivative of q-ary entropy. -/
lemma deriv2_qaryEntropy :
    deriv^[2] (qaryEntropy q) p = -1 / (p * (1 - p))

Proof state:
q : ℕ
p✝ : ℝ
xne0 : p✝ ≠ 0
xne1 : p✝ ≠ 1
this✝ : ∀ᶠ (y : ℝ) in 𝓝 p✝, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
this : ∀ {q : ℝ} (p : ℝ), DifferentiableAt ℝ (fun p => q - p) p
p : ℝ
⊢ deriv (fun y => 1 - y) p = -1

Tactic:
rw [deriv_const_sub 1, deriv_id'']

Result:
no goals

Proof state:
case pos
q : ℕ
p : ℝ
is_x_where_nondiff : p ≠ 0 ∧ p ≠ 1
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))

Tactic:
obtain ⟨xne0, xne1⟩ := is_x_where_nondiff

Result:
case pos.intro
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))

Proof state:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ deriv (fun x => log (↑q - 1) + log (1 - x)) p - deriv (fun x => x) p / p = -1 / (p * (1 - p))

Tactic:
simp only [deriv_id'', one_div]

Result:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ deriv (fun x => log (↑q - 1) + log (1 - x)) p - p⁻¹ = -1 / (p * (1 - p))

Proof state:
q : ℕ
p : ℝ
⊢ deriv^[2] (qaryEntropy q) p = -1 / (p * (1 - p))

Tactic:
simp only [Function.iterate_succ, Function.iterate_zero, Function.id_comp, Function.comp_apply]

Result:
q : ℕ
p : ℝ
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))

Proof state:
case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))

Tactic:
have : p = 0 ∨ p = 1 := Decidable.or_iff_not_and_not.mpr is_x_where_nondiff

Result:
case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))

Proof state:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))

Tactic:
refine (Filter.EventuallyEq.deriv_eq this).trans ?_

Result:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ deriv (fun x => log (↑q - 1) + log (1 - x) - log x) p = -1 / (p * (1 - p))

Proof state:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ DifferentiableAt ℝ (fun x => log (↑q - 1) + log (1 - x)) p

Tactic:
apply DifferentiableAt.add

Result:
case hf
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ DifferentiableAt ℝ (fun y => log (↑q - 1)) p

case hg
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ DifferentiableAt ℝ (fun y => log (1 - y)) p

Proof state:
case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))

Tactic:
rw [deriv_zero_of_not_differentiableAt]

Result:
case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
⊢ 0 = -1 / (p * (1 - p))

case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
⊢ ¬DifferentiableAt ℝ (deriv (qaryEntropy q)) p

Proof state:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ deriv (fun x => log (↑q - 1) + log (1 - x)) p - p⁻¹ = -1 / (p * (1 - p))

Tactic:
have {q : ℝ} (p : ℝ) : DifferentiableAt ℝ (fun p => q - p) p := by fun_prop

Result:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this✝ : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
this : ∀ {q : ℝ} (p : ℝ), DifferentiableAt ℝ (fun p => q - p) p
⊢ deriv (fun x => log (↑q - 1) + log (1 - x)) p - p⁻¹ = -1 / (p * (1 - p))

Proof state:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ deriv (fun x => log (↑q - 1) + log (1 - x)) p - deriv log p = -1 / (p * (1 - p))

Tactic:
rw [deriv.log differentiableAt_id' xne0]

Result:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ deriv (fun x => log (↑q - 1) + log (1 - x)) p - deriv (fun x => x) p / p = -1 / (p * (1 - p))

Proof state:
q : ℕ
p : ℝ
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))

Tactic:
by_cases is_x_where_nondiff : p ≠ 0 ∧ p ≠ 1

Result:
case pos
q : ℕ
p : ℝ
is_x_where_nondiff : p ≠ 0 ∧ p ≠ 1
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))

case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))

Proof state:
case pos.intro
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
⊢ ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y

Tactic:
filter_upwards [eventually_ne_nhds xne0, eventually_ne_nhds xne1]
  with y xne0 h2 using deriv_qaryEntropy xne0 h2

Result:
no goals

Proof state:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this✝ : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
this : ∀ {q : ℝ} (p : ℝ), DifferentiableAt ℝ (fun p => q - p) p
⊢ deriv (fun x => log (↑q - 1) + log (1 - x)) p - p⁻¹ = -1 / (p * (1 - p))

Tactic:
have d_oneminus (p : ℝ) : deriv (fun (y : ℝ) ↦ 1 - y) p = -1 := by
  rw [deriv_const_sub 1, deriv_id'']

Result:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this✝ : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
this : ∀ {q : ℝ} (p : ℝ), DifferentiableAt ℝ (fun p => q - p) p
d_oneminus : ∀ (p : ℝ), deriv (fun y => 1 - y) p = -1
⊢ deriv (fun x => log (↑q - 1) + log (1 - x)) p - p⁻¹ = -1 / (p * (1 - p))

Proof state:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ deriv (fun x => log (↑q - 1) + log (1 - x) - log x) p = -1 / (p * (1 - p))

Tactic:
rw [deriv_sub ?_ (differentiableAt_log xne0)]

Result:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ deriv (fun x => log (↑q - 1) + log (1 - x)) p - deriv log p = -1 / (p * (1 - p))

q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ DifferentiableAt ℝ (fun x => log (↑q - 1) + log (1 - x)) p

Proof state:
case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
⊢ 0 = -1 / (p * (1 - p))

Tactic:
simp_all only [ne_eq, not_and, Decidable.not_not]

Result:
case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬p = 0 → p = 1
this : p = 0 ∨ p = 1
⊢ 0 = -1 / (p * (1 - p))

Proof state:
case hg
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ DifferentiableAt ℝ (fun y => log (1 - y)) p

Tactic:
exact DifferentiableAt.log (by fun_prop) (sub_ne_zero.mpr xne1.symm)

Result:
no goals

Proof state:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ DifferentiableAt ℝ (HSub.hSub 1) p

Tactic:
fun_prop

Result:
no goals

Proof state:
case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬p = 0 → p = 1
this : p = 0 ∨ p = 1
⊢ 0 = -1 / (p * (1 - p))

Tactic:
cases this <;> simp_all only [
  mul_zero, one_ne_zero, zero_ne_one, sub_zero, mul_one, div_zero, sub_self]

Result:
no goals