awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
tendstoTop : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
apply : Disjoint (𝓝 (deriv (qaryEntropy q) 0)) atTop
apply₁ : (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) =ᶠ[𝓝[>] 0] deriv (qaryEntropy q)
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 0

Tactic:
apply not_continuousAt_of_tendsto (Filter.Tendsto.congr' _ tendstoTop) nhdsWithin_le_nhds

Premises used: not_continuousAt_of_tendsto, nhdsWithin_le_nhds, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
tendstoTop : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
⊢ Disjoint (𝓝 (deriv (qaryEntropy q) 0)) atTop

Tactic:
simp only [disjoint_nhds_atTop_iff, not_isTop, not_false_eq_true]

Premises used: not_isTop, disjoint_nhds_atTop_iff, not_false_eq_true
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
tendstoTop : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
⊢ LT.lt (α := ℝ) 0 2⁻¹

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
tendstoTop : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 2⁻¹) a →
      log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - a) - log a = deriv (qaryEntropy q) a
⊢ (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) =ᶠ[𝓝[>] 0] deriv (qaryEntropy q)

Tactic:
filter_upwards [Ioo_mem_nhdsGT (show (0 : ℝ) < 2⁻¹ by norm_num)]

Premises used: Ioo_mem_nhdsGT
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
tendstoTop : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a : ℝ
h : Membership.mem (γ := Set ℝ) (Ioo 0 2⁻¹) a
apply : a ≠ 0
apply₁ : a ≠ 1
⊢ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - a) - log a = deriv (qaryEntropy q) a

Tactic:
apply (deriv_qaryEntropy _ _).symm

Premises used: Real.deriv_qaryEntropy, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
tendstoTop : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a : ℝ
h : Membership.mem (γ := Set ℝ) (Ioo 0 2⁻¹) a
⊢ 0 < a ∧ a < 2⁻¹

Tactic:
simp_all only [mem_Ioo, ne_eq]

Premises used: Set.mem_Ioo, ne_eq
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
tendstoTop : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a : ℝ
h : 0 < a ∧ a < 2⁻¹
linarith : a = 0 → 2 / 2 = 1
linarith₁ : a = 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : a = 0 → GT.gt (α := ℝ) 2 0
linarith₃ : a = 0 → 0 - a + (a - 0) = 0
⊢ ¬a = 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
tendstoTop : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a : ℝ
h : 0 < a ∧ a < 2⁻¹
linarith : a = 1 → 2 / 2 = 1
linarith₁ : a = 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : a = 1 → GT.gt (α := ℝ) 2 0
linarith₃ : a = 1 → 2 / 2 = 1
linarith₄ : a = 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : a = 1 → GT.gt (α := ℝ) 2 0
linarith₆ : a = 1 → 0 - a + (2 * a - HMul.hMul (α := ℝ) 1 1) + -(a - 1) = 0
⊢ ¬a = 1

Tactic:
linarith [two_inv_lt_one (α := ℝ)]

Premises used: two_inv_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
pos : ∀ (is_x_where_nondiff : p ≠ 0 ∧ p ≠ 1), deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))
neg : ∀ (is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)), deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))

Tactic:
by_cases is_x_where_nondiff : p ≠ 0 ∧ p ≠ 1
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : p ≠ 0 ∧ p ≠ 1
⊢ p ≠ 0

Tactic:
obtain ⟨xne0, xne1⟩ := is_x_where_nondiff
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : p ≠ 0 ∧ p ≠ 1
xne0 : p ≠ 0
⊢ p ≠ 1

Tactic:
obtain ⟨xne0, xne1⟩ := is_x_where_nondiff
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this :
  ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun (p : ℝ) ↦ qaryEntropy q p) y = log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - y) - log y
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))

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

Premises used: Filter.EventuallyEq.deriv_eq, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this :
  ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun (p : ℝ) ↦ qaryEntropy q p) y = log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - y) - log y
refine : deriv (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x) - log x) p = -1 / (p * (1 - p))
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))

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

Premises used: Filter.EventuallyEq.deriv_eq, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this :
  ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun (p : ℝ) ↦ qaryEntropy q p) y = log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - y) - log y
rw : deriv (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x)) p - deriv log p = -1 / (p * (1 - p))
rw₁ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x)) p
⊢ deriv (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x) - log x) p = -1 / (p * (1 - p))

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

Premises used: Real.differentiableAt_log, deriv_fun_sub
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this :
  ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun (p : ℝ) ↦ qaryEntropy q p) y = log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - y) - log y
rw :
  deriv (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x)) p - deriv (fun (x : ℝ) ↦ x) p / p =
    -1 / (p * (1 - p))
⊢ deriv (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x)) p - deriv log p = -1 / (p * (1 - p))

Tactic:
rw [deriv.log differentiableAt_fun_id xne0]

Premises used: deriv.log, differentiableAt_fun_id
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this :
  ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun (p : ℝ) ↦ qaryEntropy q p) y = log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - y) - log y
simp : deriv (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x)) p - p⁻¹ = -1 / (p * (1 - p))
⊢ deriv (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x)) p - deriv (fun (x : ℝ) ↦ x) p / p =
    -1 / (p * (1 - p))

Tactic:
simp only [deriv_id'', one_div]

Premises used: deriv_id'', one_div
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q_1 : ℕ
p_1 : ℝ
xne0 : p_1 ≠ 0
xne1 : p_1 ≠ 1
this :
  ∀ᶠ (y : ℝ) in 𝓝 p_1,
    deriv (fun (p : ℝ) ↦ qaryEntropy q_1 p) y = log (HSub.hSub (α := ℝ) (↑q_1 : ℝ) 1) + log (1 - y) - log y
q p : ℝ
⊢ DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ q - p) p

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this :
  ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun (p : ℝ) ↦ qaryEntropy q p) y = log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - y) - log y
⊢ ∀ {q : ℝ} (p : ℝ), DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ q - p) p

Tactic:
have {q : ℝ} (p : ℝ) : DifferentiableAt ℝ (fun p => q - p) p := by fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this_1 :
  ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun (p : ℝ) ↦ qaryEntropy q p) y = log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - y) - log y
this : ∀ {q : ℝ} (p : ℝ), DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ q - p) p
simp : -p - (1 - p) = -1
⊢ deriv (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x)) p - p⁻¹ = -1 / (p * (1 - p))

Tactic:
simp [field, sub_ne_zero_of_ne xne1.symm, this]

Premises used: Ne.symm, sub_ne_zero_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this_1 :
  ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun (p : ℝ) ↦ qaryEntropy q p) y = log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - y) - log y
this : ∀ {q : ℝ} (p : ℝ), DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ q - p) p
⊢ -p - (1 - p) = -1

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this :
  ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun (p : ℝ) ↦ qaryEntropy q p) y = log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - y) - log y
hf : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1)) p
hg : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ log (1 - x)) p
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x)) p

Tactic:
apply DifferentiableAt.add

Premises used: DifferentiableAt.add
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this :
  ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun (p : ℝ) ↦ qaryEntropy q p) y = log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - y) - log y
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1)) p

Tactic:
simp only [differentiableAt_const]

Premises used: differentiableAt_const
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this :
  ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun (p : ℝ) ↦ qaryEntropy q p) y = log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - y) - log y
⊢ DifferentiableAt ℝ (HSub.hSub (α := ℝ) 1) p

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this :
  ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun (p : ℝ) ↦ qaryEntropy q p) y = log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - y) - log y
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ log (1 - x)) p

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

Premises used: Iff.mpr, sub_ne_zero, DifferentiableAt.log, Ne.symm
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
pos :
  ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun (p : ℝ) ↦ qaryEntropy q p) y = log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - y) - log y
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))

Tactic:
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
          simp [field, sub_ne_zero_of_ne xne1.symm, this]
          ring
      · apply DifferentiableAt.add
        · simp only [differentiableAt_const]
        exact DifferentiableAt.log (by fun_prop) (sub_ne_zero.mpr xne1.symm)
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
xne0_1 : p ≠ 0
xne1 : p ≠ 1
y : ℝ
xne0 : y ≠ 0
h2 : y ≠ 1
⊢ deriv (fun (p : ℝ) ↦ qaryEntropy q p) y = log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - y) - log y

Tactic:
deriv_qaryEntropy xne0 h2

Premises used: Real.deriv_qaryEntropy
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ≠ 0) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ≠ 1) x} x →
                Membership.mem (γ := Set ℝ)
                  {x : ℝ |
                    (fun (y : ℝ) ↦
                        deriv (fun (p : ℝ) ↦ qaryEntropy q p) y =
                          log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - y) - log y)
                      x}
                  x}
            x}
      a
h₁ h₂ :
  ∀ (y : ℝ) (xne0 : y ≠ 0) (h2 : y ≠ 1),
    deriv (fun (p : ℝ) ↦ qaryEntropy q p) y = log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - y) - log y
⊢ ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun (p : ℝ) ↦ qaryEntropy q p) y = log (HSub.hSub (α := ℝ) (↑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

Premises used: eventually_ne_nhds
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
⊢ p = 0 ∨ p = 1

Tactic:
have : p = 0 ∨ p = 1 := Decidable.or_iff_not_not_and_not.mpr is_x_where_nondiff
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
neg : 0 = -1 / (p * (1 - p))
neg₁ : ¬DifferentiableAt ℝ (deriv (qaryEntropy q)) p
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))

Tactic:
rw [deriv_zero_of_not_differentiableAt]

Premises used: deriv_zero_of_not_differentiableAt
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
⊢ ¬p = 0 → p = 1

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

Premises used: ne_eq, Decidable.not_not, not_and
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
is_x_where_nondiff₁ : ¬p = 0 → p = 1
⊢ p = 0 ∨ p = 1

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

Premises used: ne_eq, Decidable.not_not, not_and
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : ¬p = 0 → p = 1
this : p = 0 ∨ p = 1
neg : p = 0 → 0 = -1 / (p * (1 - p))
neg₁ : p = 1 → 0 = -1 / (p * (1 - p))
⊢ 0 = -1 / (p * (1 - p))

Tactic:
cases this
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : ¬p = 0 → p = 1
h : p = 0
⊢ 0 = -1 / (p * (1 - p))

Tactic:
simp_all only [mul_zero, one_ne_zero, zero_ne_one, sub_zero, mul_one, div_zero, sub_self]

Premises used: sub_self, sub_zero, zero_ne_one, MulZeroClass.mul_zero, mul_one, one_ne_zero, div_zero
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : ¬p = 0 → p = 1
h : p = 1
⊢ 0 = -1 / (p * (1 - p))

Tactic:
simp_all only [mul_zero, one_ne_zero, zero_ne_one, sub_zero, mul_one, div_zero, sub_self]

Premises used: sub_self, sub_zero, zero_ne_one, MulZeroClass.mul_zero, mul_one, one_ne_zero, div_zero
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
h : DifferentiableAt ℝ (deriv (qaryEntropy q)) p
⊢ ContinuousAt (deriv (qaryEntropy q)) p

Tactic:
have contAt := h.continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
h : DifferentiableAt ℝ (deriv (qaryEntropy q)) p
contAt : ContinuousAt (deriv (qaryEntropy q)) p
neg : p = 0 → False
neg₁ : p = 1 → False
⊢ False

Tactic:
cases this
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
h : DifferentiableAt ℝ (deriv (qaryEntropy q)) p
contAt : ContinuousAt (deriv (qaryEntropy q)) p
h_1 : p = 0
⊢ False

Tactic:
simp_all [not_continuousAt_deriv_qaryEntropy_zero, not_continuousAt_deriv_qaryEntropy_one]

Premises used: Real.not_continuousAt_deriv_qaryEntropy_zero, Real.not_continuousAt_deriv_qaryEntropy_one
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
h : DifferentiableAt ℝ (deriv (qaryEntropy q)) p
contAt : ContinuousAt (deriv (qaryEntropy q)) p
h_1 : p = 1
⊢ False

Tactic:
simp_all [not_continuousAt_deriv_qaryEntropy_zero, not_continuousAt_deriv_qaryEntropy_one]

Premises used: Real.not_continuousAt_deriv_qaryEntropy_zero, Real.not_continuousAt_deriv_qaryEntropy_one
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
⊢ deriv^[2] binEntropy p = -1 / (p * (1 - p))

Tactic:
qaryEntropy_two ▸ deriv2_qaryEntropy

Premises used: Real.qaryEntropy_two, Eq.rec, Real.deriv2_qaryEntropy
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
apply : ContinuousOn (qaryEntropy q) (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)))
apply₁ : ∀ x ∈ interior (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))), 0 < deriv (qaryEntropy q) x
⊢ qaryEntropy q p1 < qaryEntropy q p2

Tactic:
apply strictMonoOn_of_deriv_pos (convex_Icc 0 (1 - 1 / (q : ℝ))) _ _ hp1 hp2 p1le2

Premises used: HSub.hSub, HDiv.hDiv, Nat.cast, convex_Icc, strictMonoOn_of_deriv_pos, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
⊢ ContinuousOn (qaryEntropy q) (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)))

Tactic:
qaryEntropy_continuous.continuousOn

Premises used: Continuous.continuousOn, Real.qaryEntropy_continuous
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
⊢ ContinuousOn (qaryEntropy q) (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)))

Tactic:
exact qaryEntropy_continuous.continuousOn

Premises used: Continuous.continuousOn, Real.qaryEntropy_continuous
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)))
⊢ LE.le (α := ℝ) 2 (↑q : ℝ)

Tactic:
have : 2 ≤ (q : ℝ) := Nat.ofNat_le_cast.mpr qLe2
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)))
this : LE.le (α := ℝ) 2 (↑q : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)))
this : LE.le (α := ℝ) 2 (↑q : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹

Tactic:
have zero_le_qinv : 0 < (q : ℝ)⁻¹ := by positivity
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)))
this : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
simp : p < 1
⊢ 0 < 1 - p

Tactic:
simp only [sub_pos]

Premises used: sub_pos
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)))
this : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
⊢ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹

Tactic:
simp_all only [inv_pos, interior_Icc, mem_Ioo, one_div]

Premises used: Set.mem_Ioo, interior_Icc, inv_pos, one_div
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)))
this : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
⊢ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹

Tactic:
have p_lt_1_minus_qinv : p < 1 - (q : ℝ)⁻¹ := by
        simp_all only [inv_pos, interior_Icc, mem_Ioo, one_div]
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)))
this : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
p_lt_1_minus_qinv : p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
linarith :
  1 ≤ p →
    HMul.hMul (α := ℝ) 1 0 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹ +
          (1 * p - (HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹)) +
        (1 - p) =
      0
⊢ p < 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)))
this : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
⊢ 0 < 1 - p

Tactic:
have : 0 < 1 - p := by
      simp only [sub_pos]
      have p_lt_1_minus_qinv : p < 1 - (q : ℝ)⁻¹ := by
        simp_all only [inv_pos, interior_Icc, mem_Ioo, one_div]
      linarith
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)))
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
⊢ 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹

Tactic:
simp only [one_div, interior_Icc, mem_Ioo] at hp

Premises used: Set.mem_Ioo, interior_Icc, one_div
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
linarith : p = 0 → 0 - p + (p - 0) = 0
⊢ p ≠ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
rw : 0 < log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p
rw₁ : p ≠ 1
⊢ 0 < deriv (qaryEntropy q) p

Tactic:
rw [deriv_qaryEntropy (by linarith)]

Premises used: Real.deriv_qaryEntropy
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
simp : log p < log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p)
⊢ 0 < log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p

Tactic:
simp only [sub_pos, gt_iff_lt]

Premises used: sub_pos, gt_iff_lt