awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
tendstoBot : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
a : ℝ
h : HSub.hSub (α := ℝ) 1 2⁻¹ < a ∧ a < 1
linarith : a = 0 → 2 / 2 = 1
⊢ ¬a = 0
have linarith₁ : a = 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [show (1 : ℝ) = 2⁻¹ + 2⁻¹ by norm_num]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
tendstoBot : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
a : ℝ
h : HSub.hSub (α := ℝ) 1 2⁻¹ < a ∧ a < 1
linarith : a = 0 → 2 / 2 = 1
linarith₁ : a = 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ ¬a = 0
have linarith₂ : a = 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [show (1 : ℝ) = 2⁻¹ + 2⁻¹ by norm_num]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
tendstoBot : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
a : ℝ
h : HSub.hSub (α := ℝ) 1 2⁻¹ < a ∧ a < 1
linarith : a = 0 → 2 / 2 = 1
linarith₁ : a = 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : a = 0 → GT.gt (α := ℝ) 2 0
⊢ ¬a = 0
have linarith₃ : a = 0 → HMul.hMul (α := ℝ) 1 1 - 2 * a + (a - 1) + (a - 0) = 0
Tactic: linarith [show (1 : ℝ) = 2⁻¹ + 2⁻¹ by norm_num]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
tendstoBot : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
a : ℝ
h : a ∈ Ioo (HSub.hSub (α := ℝ) 1 2⁻¹) 1
⊢ a ≠ 1
have a : HSub.hSub (α := ℝ) 1 2⁻¹ < a ∧ a < 1
Tactic: simp_all only [mem_Ioo, ne_eq]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
tendstoBot : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
a : ℝ
h : HSub.hSub (α := ℝ) 1 2⁻¹ < a ∧ a < 1
⊢ ¬a = 1
have linarith : a = 1 → 2 / 2 = 1
Tactic: linarith [two_inv_lt_one (α := ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
tendstoBot : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
a : ℝ
h : HSub.hSub (α := ℝ) 1 2⁻¹ < a ∧ a < 1
linarith : a = 1 → 2 / 2 = 1
⊢ ¬a = 1
have linarith₁ : a = 1 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [two_inv_lt_one (α := ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
tendstoBot : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
a : ℝ
h : HSub.hSub (α := ℝ) 1 2⁻¹ < a ∧ a < 1
linarith : a = 1 → 2 / 2 = 1
linarith₁ : a = 1 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ ¬a = 1
have linarith₂ : a = 1 → GT.gt (α := ℝ) 2 0
Tactic: linarith [two_inv_lt_one (α := ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
tendstoBot : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
a : ℝ
h : HSub.hSub (α := ℝ) 1 2⁻¹ < a ∧ a < 1
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
⊢ ¬a = 1
have linarith₆ : a = 1 → a - 1 + -(a - 1) = 0
Tactic: linarith [two_inv_lt_one (α := ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
have this : Eq (α := (p : ℝ) → ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) fun (p : ℝ) ↦
  log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + (log (1 - p) - log p)
Tactic: have : (fun p ↦ log (q - 1) + log (1 - p) - log p)
        = (fun p ↦ log (q - 1) + (log (1 - p) - log p)) := by ext; ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
this :
  Eq (α := (p : ℝ) → ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) fun (p : ℝ) ↦
    log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + (log (1 - p) - log p)
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
have rw : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + (log (1 - p) - log p)) (𝓝[>] 0) atTop
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 0
have tendstoTop : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
Tactic: have tendstoTop : Tendsto (fun p ↦ log (q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop := by
    have : (fun p ↦ log (q - 1) + log (1 - p) - log p)
        = (fun p ↦ log (q - 1) + (log (1 - p) - log p)) := by ext; ring
    rw [this]
    exact tendsto_atTop_add_const_left _ _ tendsto_log_one_sub_sub_log_nhdsGT_atAtop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
tendstoTop : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 0
have apply : Disjoint (𝓝 (deriv (qaryEntropy q) 0)) atTop
Tactic: apply not_continuousAt_of_tendsto (Filter.Tendsto.congr' _ tendstoTop) nhdsWithin_le_nhds
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 0
have apply₁ : (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) =ᶠ[𝓝[>] 0] deriv (qaryEntropy q)
Tactic: apply not_continuousAt_of_tendsto (Filter.Tendsto.congr' _ tendstoTop) nhdsWithin_le_nhds
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
tendstoTop : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
⊢ (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) =ᶠ[𝓝[>] 0] deriv (qaryEntropy q)
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ) (Ioo 0 2⁻¹) a →
    log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - a) - log a = deriv (qaryEntropy q) a
Tactic: filter_upwards [Ioo_mem_nhdsGT (show (0 : ℝ) < 2⁻¹ by norm_num)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - a) - log a = deriv (qaryEntropy q) a
have apply : a ≠ 0
Tactic: apply (deriv_qaryEntropy _ _).symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - a) - log a = deriv (qaryEntropy q) a
have apply₁ : a ≠ 1
Tactic: apply (deriv_qaryEntropy _ _).symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
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
⊢ a ≠ 0
have a : 0 < a ∧ a < 2⁻¹
Tactic: simp_all only [mem_Ioo, ne_eq]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
tendstoTop : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a : ℝ
h : 0 < a ∧ a < 2⁻¹
⊢ ¬a = 0
have linarith : a = 0 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ ¬a = 0
have linarith₁ : a = 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ ¬a = 0
have linarith₂ : a = 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ ¬a = 0
have linarith₃ : a = 0 → 0 - a + (a - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
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
⊢ a ≠ 1
have a : 0 < a ∧ a < 2⁻¹
Tactic: simp_all only [mem_Ioo, ne_eq]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
tendstoTop : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a : ℝ
h : 0 < a ∧ a < 2⁻¹
⊢ ¬a = 1
have linarith : a = 1 → 2 / 2 = 1
Tactic: linarith [two_inv_lt_one (α := ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ ¬a = 1
have linarith₁ : a = 1 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [two_inv_lt_one (α := ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ ¬a = 1
have linarith₂ : a = 1 → GT.gt (α := ℝ) 2 0
Tactic: linarith [two_inv_lt_one (α := ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ ¬a = 1
have linarith₆ : a = 1 → 0 - a + (2 * a - HMul.hMul (α := ℝ) 1 1) + -(a - 1) = 0
Tactic: linarith [two_inv_lt_one (α := ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
p : ℝ
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))
have pos : ∀ (is_x_where_nondiff : p ≠ 0 ∧ p ≠ 1), deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))
Tactic: by_cases is_x_where_nondiff : p ≠ 0 ∧ p ≠ 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
p : ℝ
pos : ∀ (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))
have neg : ∀ (is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)), deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))
Tactic: by_cases is_x_where_nondiff : p ≠ 0 ∧ p ≠ 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : p ≠ 0 ∧ p ≠ 1
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))
have xne0 : p ≠ 0
Tactic: obtain ⟨xne0, xne1⟩ := is_x_where_nondiff
Cleared hypotheses: is_x_where_nondiff
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : p ≠ 0 ∧ p ≠ 1
xne0 : p ≠ 0
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))
have xne1 : p ≠ 1
Tactic: obtain ⟨xne0, xne1⟩ := is_x_where_nondiff
Cleared hypotheses: is_x_where_nondiff
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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))
have refine : deriv (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x) - log x) p = -1 / (p * (1 - p))
Tactic: refine (Filter.EventuallyEq.deriv_eq this).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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 (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x) - log x) p = -1 / (p * (1 - p))
have rw : deriv (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x)) p - deriv log p = -1 / (p * (1 - p))
Tactic: rw [deriv_fun_sub ?_ (differentiableAt_log xne0)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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))
⊢ deriv (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x) - log x) p = -1 / (p * (1 - p))
have rw₁ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x)) p
Tactic: rw [deriv_fun_sub ?_ (differentiableAt_log xne0)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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 (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x)) p - deriv log p = -1 / (p * (1 - p))
have rw : deriv (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x)) p - deriv (fun (x : ℝ) ↦ x) p / p =
  -1 / (p * (1 - p))
Tactic: rw [deriv.log differentiableAt_fun_id xne0]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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 (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x)) p - deriv (fun (x : ℝ) ↦ x) p / p =
    -1 / (p * (1 - p))
have simp : deriv (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x)) p - p⁻¹ = -1 / (p * (1 - p))
Tactic: simp only [deriv_id'', one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
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 (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x)) p - p⁻¹ = -1 / (p * (1 - p))
have this₁ : ∀ {q : ℝ} (p : ℝ), DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ q - p) p
Tactic: have {q : ℝ} (p : ℝ) : DifferentiableAt ℝ (fun p => q - p) p := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ deriv (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x)) p - p⁻¹ = -1 / (p * (1 - p))
have simp : -p - (1 - p) = -1
Tactic: simp [field, sub_ne_zero_of_ne xne1.symm, this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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) + log (1 - x)) p
have hf : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1)) p
Tactic: apply DifferentiableAt.add
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x)) p
have hg : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ log (1 - x)) p
Tactic: apply DifferentiableAt.add
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))
have pos : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun (p : ℝ) ↦ qaryEntropy q p) y = log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - y) - log y
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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
⊢ ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun (p : ℝ) ↦ qaryEntropy q p) y = log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - y) - log y
have 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
Tactic: filter_upwards [eventually_ne_nhds xne0, eventually_ne_nhds xne1]
      with y xne0 h2 using deriv_qaryEntropy xne0 h2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun (p : ℝ) ↦ qaryEntropy q p) y = log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - y) - log y
have h₁ : ∀ (a : ℝ),
  a ≠ 0 → a ≠ 1 → deriv (fun (p : ℝ) ↦ qaryEntropy q p) a = log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - a) - log a
Tactic: filter_upwards [eventually_ne_nhds xne0, eventually_ne_nhds xne1]
      with y xne0 h2 using deriv_qaryEntropy xne0 h2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))
have this : p = 0 ∨ p = 1
Tactic: have : p = 0 ∨ p = 1 := Decidable.or_iff_not_not_and_not.mpr is_x_where_nondiff
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))
have neg : 0 = -1 / (p * (1 - p))
Tactic: rw [deriv_zero_of_not_differentiableAt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
neg : 0 = -1 / (p * (1 - p))
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))
have neg₁ : ¬DifferentiableAt ℝ (deriv (qaryEntropy q)) p
Tactic: rw [deriv_zero_of_not_differentiableAt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
⊢ 0 = -1 / (p * (1 - p))
have is_x_where_nondiff₁ : ¬p = 0 → p = 1
Tactic: simp_all only [ne_eq, not_and, Decidable.not_not]
Cleared hypotheses: is_x_where_nondiff, this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : ¬p = 0 → p = 1
this : p = 0 ∨ p = 1
⊢ 0 = -1 / (p * (1 - p))
have neg : p = 0 → 0 = -1 / (p * (1 - p))
Tactic: cases this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : ¬p = 0 → p = 1
this : p = 0 ∨ p = 1
neg : p = 0 → 0 = -1 / (p * (1 - p))
⊢ 0 = -1 / (p * (1 - p))
have neg₁ : p = 1 → 0 = -1 / (p * (1 - p))
Tactic: cases this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
h : DifferentiableAt ℝ (deriv (qaryEntropy q)) p
⊢ False
have contAt : ContinuousAt (deriv (qaryEntropy q)) p
Tactic: have contAt := h.continuousAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ False
have neg : p = 0 → False
Tactic: cases this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ False
have neg₁ : p = 1 → False
Tactic: cases this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ qaryEntropy q p1 < qaryEntropy q p2
have apply : ContinuousOn (qaryEntropy q) (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)))
Tactic: apply strictMonoOn_of_deriv_pos (convex_Icc 0 (1 - 1 / (q : ℝ))) _ _ hp1 hp2 p1le2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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 : ℝ)))
⊢ qaryEntropy q p1 < qaryEntropy q p2
have apply₁ : ∀ x ∈ interior (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))), 0 < deriv (qaryEntropy q) x
Tactic: apply strictMonoOn_of_deriv_pos (convex_Icc 0 (1 - 1 / (q : ℝ))) _ _ hp1 hp2 p1le2