awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
⊢ binEntropy p = log 2 ↔ p = 2⁻¹
have rw : ¬binEntropy p < log 2 ↔ p = 2⁻¹
Tactic: rw [← binEntropy_le_log_two.not_lt_iff_eq, binEntropy_lt_log_two, not_ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
rw : ¬binEntropy p < log 2 ↔ p = 2⁻¹
⊢ binEntropy p = log 2 ↔ p = 2⁻¹
have rw₁ : ¬p ≠ 2⁻¹ ↔ p = 2⁻¹
Tactic: rw [← binEntropy_le_log_two.not_lt_iff_eq, binEntropy_lt_log_two, not_ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
rw : ¬binEntropy p < log 2 ↔ p = 2⁻¹
rw₁ : ¬p ≠ 2⁻¹ ↔ p = 2⁻¹
⊢ binEntropy p = log 2 ↔ p = 2⁻¹
have rw₂ : p = 2⁻¹ ↔ p = 2⁻¹
Tactic: rw [← binEntropy_le_log_two.not_lt_iff_eq, binEntropy_lt_log_two, not_ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
⊢ Continuous binEntropy
have rw : Continuous (Y := ℝ) fun (p : ℝ) ↦ p.negMulLog + (1 - p).negMulLog
Tactic: rw [binEntropy_eq_negMulLog_add_negMulLog_one_sub']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ binEntropy p
have hp₂ : 1 - p ≠ 0
Tactic: rw [ne_comm, ← sub_ne_zero] at hp₁
Cleared hypotheses: hp₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) p
have simp : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ -(p * log p) + -((1 - p) * log (1 - p))) p
Tactic: simp only [log_inv, mul_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
⊢ DifferentiableAt ℝ binEntropy p ↔ p ≠ 0 ∧ p ≠ 1
have refine_1 : ∀ (h : DifferentiableAt ℝ binEntropy p), p ≠ 0
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ differentiableAt_binEntropy h.1 h.2⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
refine_1 : ∀ (h : DifferentiableAt ℝ binEntropy p), p ≠ 0
⊢ DifferentiableAt ℝ binEntropy p ↔ p ≠ 0 ∧ p ≠ 1
have refine_2 : ∀ (h : DifferentiableAt ℝ binEntropy p), p ≠ 1
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ differentiableAt_binEntropy h.1 h.2⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
h : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 0
⊢ False
have refine_1 : ∀ (h : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹) 0), False
Tactic: rw [DifferentiableAt.fun_add_iff_left] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
h : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 0
refine_1 : ∀ (h : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹) 0), False
⊢ False
have refine_1₁ : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ (1 - p) * log (1 - p)⁻¹) 0
Tactic: rw [DifferentiableAt.fun_add_iff_left] at h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
h : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ (1 - p) * log (1 - p)⁻¹) 0
have funProp : HSub.hSub (α := ℝ) 1 0 ≠ 0
Tactic: fun_prop (disch := simp)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
h : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 0
funProp : HSub.hSub (α := ℝ) 1 0 ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ (1 - p) * log (1 - p)⁻¹) 0
have funProp₁ : (HSub.hSub (α := ℝ) 1 0)⁻¹ ≠ 0
Tactic: fun_prop (disch := simp)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
h : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 1
⊢ False
have refine_2 : ∀ (h : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ (1 - (1 - x)) * log (1 - (1 - x))⁻¹) (HSub.hSub (α := ℝ) 1 1)), False
Tactic: rw [DifferentiableAt.fun_add_iff_right, differentiableAt_iff_comp_const_sub (b := 1)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
h : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 1
refine_2 :
  ∀ (h : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ (1 - (1 - x)) * log (1 - (1 - x))⁻¹) (HSub.hSub (α := ℝ) 1 1)),
    False
⊢ False
have refine_2₁ : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹) 1
Tactic: rw [DifferentiableAt.fun_add_iff_right, differentiableAt_iff_comp_const_sub (b := 1)] at h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
h : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 1
⊢ DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹) 1
have funProp : Ne (α := ℝ) 1 0
Tactic: fun_prop (disch := simp)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
h : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 1
funProp : Ne (α := ℝ) 1 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹) 1
have funProp₁ : Ne (α := ℝ) 1⁻¹ 0
Tactic: fun_prop (disch := simp)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
⊢ deriv binEntropy p = log (1 - p) - log p
have pos : ∀ (hp : p ≠ 0 ∧ p ≠ 1), deriv binEntropy p = log (1 - p) - log p
Tactic: by_cases hp : p ≠ 0 ∧ p ≠ 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
pos : ∀ (hp : p ≠ 0 ∧ p ≠ 1), deriv binEntropy p = log (1 - p) - log p
⊢ deriv binEntropy p = log (1 - p) - log p
have neg : ∀ (hp : ¬(p ≠ 0 ∧ p ≠ 1)), deriv binEntropy p = log (1 - p) - log p
Tactic: by_cases hp : p ≠ 0 ∧ p ≠ 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
p : ℝ
hp : p ≠ 0 ∧ p ≠ 1
⊢ deriv binEntropy p = log (1 - p) - log p
have hp₀ : p ≠ 0
Tactic: obtain ⟨hp₀, hp₁⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
p : ℝ
hp : p ≠ 0 ∧ p ≠ 1
hp₀ : p ≠ 0
⊢ deriv binEntropy p = log (1 - p) - log p
have hp₁ : p ≠ 1
Tactic: obtain ⟨hp₀, hp₁⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ deriv binEntropy p = log (1 - p) - log p
have hp₂ : 1 - p ≠ 0
Tactic: rw [ne_comm, ← sub_ne_zero] at hp₁
Cleared hypotheses: hp₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ deriv binEntropy p = log (1 - p) - log p
have pos : -log p - 1 + -(-log (1 - p) - 1) = log (1 - p) - log p
Tactic: rw [binEntropy_eq_negMulLog_add_negMulLog_one_sub', deriv_fun_add, deriv_comp_const_sub,
      deriv_negMulLog hp₀, deriv_negMulLog hp₁]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
pos : -log p - 1 + -(-log (1 - p) - 1) = log (1 - p) - log p
⊢ deriv binEntropy p = log (1 - p) - log p
have pos₁ : DifferentiableAt ℝ negMulLog p
Tactic: rw [binEntropy_eq_negMulLog_add_negMulLog_one_sub', deriv_fun_add, deriv_comp_const_sub,
      deriv_negMulLog hp₀, deriv_negMulLog hp₁]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
pos : -log p - 1 + -(-log (1 - p) - 1) = log (1 - p) - log p
pos₁ : DifferentiableAt ℝ negMulLog p
⊢ deriv binEntropy p = log (1 - p) - log p
have pos₂ : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ (1 - p).negMulLog) p
Tactic: rw [binEntropy_eq_negMulLog_add_negMulLog_one_sub', deriv_fun_add, deriv_comp_const_sub,
      deriv_negMulLog hp₀, deriv_negMulLog hp₁]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp : ¬(p ≠ 0 ∧ p ≠ 1)
⊢ deriv binEntropy p = log (1 - p) - log p
have neg : 0 = log (1 - p) - log p
Tactic: rw [deriv_zero_of_not_differentiableAt (differentiableAt_binEntropy_iff_ne_zero_one.not.2 hp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
p : ℝ
hp : ¬(p ≠ 0 ∧ p ≠ 1)
⊢ 0 = log (1 - p) - log p
have hp₁ : p = 0 ∨ p = 1
Tactic: push +distrib Not at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp : p = 0 ∨ p = 1
⊢ 0 = log (1 - p) - log p
have neg : 0 = log (HSub.hSub (α := ℝ) 1 0) - log 0
Tactic: obtain rfl | rfl := hp
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp : p = 0 ∨ p = 1
neg : 0 = log (HSub.hSub (α := ℝ) 1 0) - log 0
⊢ 0 = log (1 - p) - log p
have neg₁ : 0 = log (HSub.hSub (α := ℝ) 1 1) - log 1
Tactic: obtain rfl | rfl := hp
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
⊢ qaryEntropy 2 = binEntropy
have h : ∀ (x : ℝ), qaryEntropy 2 x = binEntropy x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 < p * log (↑(HSub.hSub (α := ℤ) (↑q : ℤ) 1) : ℝ) + binEntropy p
have positivity : 0 < binEntropy p → 0 < p * log (↑(HSub.hSub (α := ℤ) (↑q : ℤ) 1) : ℝ) + binEntropy p
Tactic: positivity [binEntropy_pos hp₀ hp₁]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
⊢ 0 ≤ qaryEntropy q p
have inl : ∀ (hp₀ : LE.le (α := ℝ) 0 0) (hp₁ : LE.le (α := ℝ) 0 1), 0 ≤ qaryEntropy q 0
Tactic: obtain rfl | hp₀ := hp₀.eq_or_lt
Cleared hypotheses: p, hp₀, hp₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
inl : ∀ (hp₀ : LE.le (α := ℝ) 0 0) (hp₁ : LE.le (α := ℝ) 0 1), 0 ≤ qaryEntropy q 0
⊢ 0 ≤ qaryEntropy q p
have inr : ∀ (hp₀ : 0 < p), 0 ≤ qaryEntropy q p
Tactic: obtain rfl | hp₀ := hp₀.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
p : ℝ
hp₀_1 : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ 0 ≤ qaryEntropy q p
have inr : ∀ (hp₀ : LE.le (α := ℝ) 0 1) (hp₁ : LE.le (α := ℝ) 1 1) (hp₀ : LT.lt (α := ℝ) 0 1), 0 ≤ qaryEntropy q 1
Tactic: obtain rfl | hp₁ := hp₁.eq_or_lt
Cleared hypotheses: p, hp₀_1, hp₁, hp₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
p : ℝ
hp₀_1 : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
inr : ∀ (hp₀ : LE.le (α := ℝ) 0 1) (hp₁ : LE.le (α := ℝ) 1 1) (hp₀ : LT.lt (α := ℝ) 0 1), 0 ≤ qaryEntropy q 1
⊢ 0 ≤ qaryEntropy q p
have inr₁ : ∀ (hp₁ : p < 1), 0 ≤ qaryEntropy q p
Tactic: obtain rfl | hp₁ := hp₁.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ deriv (fun (p : ℝ) ↦ p * log (↑(HSub.hSub (α := ℤ) (↑q : ℤ) 1) : ℝ) + binEntropy p) p =
    log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p
have rw : deriv (fun (p : ℝ) ↦ p * log (↑(HSub.hSub (α := ℤ) (↑q : ℤ) 1) : ℝ)) p + deriv binEntropy p =
  log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p
Tactic: rw [deriv_fun_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
rw :
  deriv (fun (p : ℝ) ↦ p * log (↑(HSub.hSub (α := ℤ) (↑q : ℤ) 1) : ℝ)) p + deriv binEntropy p =
    log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p
⊢ deriv (fun (p : ℝ) ↦ p * log (↑(HSub.hSub (α := ℤ) (↑q : ℤ) 1) : ℝ) + binEntropy p) p =
    log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p
have hf : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log (↑(HSub.hSub (α := ℤ) (↑q : ℤ) 1) : ℝ)) p
Tactic: rw [deriv_fun_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
rw :
  deriv (fun (p : ℝ) ↦ p * log (↑(HSub.hSub (α := ℤ) (↑q : ℤ) 1) : ℝ)) p + deriv binEntropy p =
    log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p
hf : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log (↑(HSub.hSub (α := ℤ) (↑q : ℤ) 1) : ℝ)) p
⊢ deriv (fun (p : ℝ) ↦ p * log (↑(HSub.hSub (α := ℤ) (↑q : ℤ) 1) : ℝ) + binEntropy p) p =
    log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p
have hg : DifferentiableAt ℝ binEntropy p
Tactic: rw [deriv_fun_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (1 - p) - log p) (𝓝[>] 0) atTop
have hf : ∀ᶠ (x : ℝ) in 𝓝[>] 0, log (1 / 2) ≤ log (1 - x)
Tactic: apply Filter.tendsto_atTop_add_left_of_le' (𝓝[>] 0) (log (1 / 2) : ℝ)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
hf : ∀ᶠ (x : ℝ) in 𝓝[>] 0, log (1 / 2) ≤ log (1 - x)
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (1 - p) - log p) (𝓝[>] 0) atTop
have hg : Tendsto (β := ℝ) (fun (x : ℝ) ↦ -log x) (𝓝[>] 0) atTop
Tactic: apply Filter.tendsto_atTop_add_left_of_le' (𝓝[>] 0) (log (1 / 2) : ℝ)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, log (1 / 2) ≤ log (1 - x)
have h₁ : 0 < 1 / 2
Tactic: have h₁ : (0 : ℝ) < 1 / 2 := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
h₁ : 0 < 1 / 2
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, log (1 / 2) ≤ log (1 - x)
have h : ∀ (p : ℝ) (hx : p ∈ Ioc 0 (1 / 2)), log (1 / 2) ≤ log (1 - p)
Tactic: filter_upwards [Ioc_mem_nhdsGT h₁] with p hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
h₁ : 0 < 1 / 2
p : ℝ
hx : p ∈ Ioc 0 (1 / 2)
⊢ log (1 / 2) ≤ log (1 - p)
have h : 1 / 2 ≤ 1 - p
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
h₁ : 0 < 1 / 2
p : ℝ
hx : p ∈ Ioc 0 (1 / 2)
⊢ 1 / 2 ≤ 1 - p
have linarith : 1 - p < 1 / 2 → 2 / 2 = 1
Tactic: linarith [hx.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
h₁ : 0 < 1 / 2
p : ℝ
hx : p ∈ Ioc 0 (1 / 2)
linarith : 1 - p < 1 / 2 → 2 / 2 = 1
⊢ 1 / 2 ≤ 1 - p
have linarith₁ : 1 - p < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [hx.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
h₁ : 0 < 1 / 2
p : ℝ
hx : p ∈ Ioc 0 (1 / 2)
linarith : 1 - p < 1 / 2 → 2 / 2 = 1
linarith₁ : 1 - p < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 1 / 2 ≤ 1 - p
have linarith₂ : 1 - p < 1 / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith [hx.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
h₁ : 0 < 1 / 2
p : ℝ
hx : p ∈ Ioc 0 (1 / 2)
linarith : 1 - p < 1 / 2 → 2 / 2 = 1
linarith₁ : 1 - p < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 - p < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : 1 - p < 1 / 2 → 2 / 2 = 1
linarith₄ : 1 - p < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : 1 - p < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₆ : 1 - p < 1 / 2 → 2 / 2 = 1
linarith₇ : 1 - p < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : 1 - p < 1 / 2 → GT.gt (α := ℝ) 2 0
⊢ 1 / 2 ≤ 1 - p
have linarith₉ : 1 - p < 1 / 2 → HMul.hMul (α := ℝ) 2 1 - 2 * p - HMul.hMul (α := ℝ) 1 1 + (2 * p - HMul.hMul (α := ℝ) 1 1) = 0
Tactic: linarith [hx.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (1 - p) - log p) (𝓝[<] 1) atBot
have hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (1 - x)) (𝓝[<] 1) atBot
Tactic: apply Filter.tendsto_atBot_add_right_of_ge' (𝓝[<] 1) (-log (1 - 2⁻¹))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (1 - x)) (𝓝[<] 1) atBot
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (1 - p) - log p) (𝓝[<] 1) atBot
have hg : ∀ᶠ (x : ℝ) in 𝓝[<] 1, -log x ≤ -log (HSub.hSub (α := ℝ) 1 2⁻¹)
Tactic: apply Filter.tendsto_atBot_add_right_of_ge' (𝓝[<] 1) (-log (1 - 2⁻¹))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (1 - x)) (𝓝[<] 1) atBot
have this : Tendsto log (𝓝[>] 0) atBot
Tactic: have : Tendsto log (𝓝[>] 0) atBot := Real.tendsto_log_nhdsGT_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
this : Tendsto log (𝓝[>] 0) atBot
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (1 - x)) (𝓝[<] 1) atBot
have hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 - x) (𝓝[<] 1) (𝓝[>] 0)
Tactic: apply Tendsto.comp (f := (1 - ·)) (g := log) this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
this : Tendsto log (𝓝[>] 0) atBot
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 - x) (𝓝[<] 1) (𝓝[>] 0)
have contF : Continuous (Y := ℝ) fun (x : ℝ) ↦ 1 - x
Tactic: have contF : Continuous ((1 : ℝ) - ·) := continuous_sub_left 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
this : Tendsto log (𝓝[>] 0) atBot
contF : Continuous (Y := ℝ) fun (x : ℝ) ↦ 1 - x
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 - x) (𝓝[<] 1) (𝓝[>] 0)
have this₁ : MapsTo (β := ℝ) (fun (x : ℝ) ↦ 1 - x) (Iio 1) (Ioi 0)
Tactic: have : MapsTo ((1 : ℝ) - ·) (Iio 1) (Ioi 0) := by
      intro p hx
      simp_all only [mem_Iio, mem_Ioi, sub_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
this_1 : Tendsto log (𝓝[>] 0) atBot
contF : Continuous (Y := ℝ) fun (x : ℝ) ↦ 1 - x
this : MapsTo (β := ℝ) (fun (x : ℝ) ↦ 1 - x) (Iio 1) (Ioi 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 - x) (𝓝[<] 1) (𝓝[>] 0)
have h : 0 = HSub.hSub (α := ℝ) 1 1
Tactic: convert! ContinuousWithinAt.tendsto_nhdsWithin (x := (1 : ℝ)) contF.continuousWithinAt this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, -log x ≤ -log (HSub.hSub (α := ℝ) 1 2⁻¹)
have h₁ : HSub.hSub (α := ℝ) 1 2⁻¹ < 1
Tactic: have h₁ : (1 : ℝ) - (2 : ℝ)⁻¹ < 1 := by norm_num
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
h₁ : HSub.hSub (α := ℝ) 1 2⁻¹ < 1
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, -log x ≤ -log (HSub.hSub (α := ℝ) 1 2⁻¹)
have h : ∀ (p : ℝ) (hx : p ∈ Ico (HSub.hSub (α := ℝ) 1 2⁻¹) 1), -log p ≤ -log (HSub.hSub (α := ℝ) 1 2⁻¹)
Tactic: filter_upwards [Ico_mem_nhdsLT h₁] with p hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
h₁ : HSub.hSub (α := ℝ) 1 2⁻¹ < 1
p : ℝ
hx : p ∈ Ico (HSub.hSub (α := ℝ) 1 2⁻¹) 1
⊢ -log p ≤ -log (HSub.hSub (α := ℝ) 1 2⁻¹)
have h : HSub.hSub (α := ℝ) 1 2⁻¹ ≤ p
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
⊢ 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)
have h : ∀ (x : ℝ),
  log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x) - log x =
    log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + (log (1 - x) - log x)
Tactic: ext
-- 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) (𝓝[<] 1) atBot
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) (𝓝[<] 1) atBot
have rw : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + (log (1 - p) - log p)) (𝓝[<] 1) atBot
Tactic: rw [this]
-- 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)) (𝓝[<] 1) atBot
have hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (1 - x) - log x) (𝓝[<] 1) atBot
Tactic: apply tendsto_atBot_add_const_left
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 1
have tendstoBot : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
Tactic: have tendstoBot : Tendsto (fun p ↦ log (q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot := 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]
    apply tendsto_atBot_add_const_left
    exact tendsto_log_one_sub_sub_log_nhdsLT_one_atBot
-- 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
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 1
have apply : Disjoint (𝓝 (deriv (qaryEntropy q) 1)) atBot
Tactic: apply not_continuousAt_of_tendsto (Filter.Tendsto.congr' _ tendstoBot) nhdsWithin_le_nhds
-- 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
apply : Disjoint (𝓝 (deriv (qaryEntropy q) 1)) atBot
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 1
have apply₁ : (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) =ᶠ[𝓝[<] 1] deriv (qaryEntropy q)
Tactic: apply not_continuousAt_of_tendsto (Filter.Tendsto.congr' _ tendstoBot) nhdsWithin_le_nhds
-- 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
⊢ (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) =ᶠ[𝓝[<] 1] deriv (qaryEntropy q)
have h : ∀ a ∈ Ioo (HSub.hSub (α := ℝ) 1 2⁻¹) 1,
  log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - a) - log a = deriv (qaryEntropy q) a
Tactic: filter_upwards [Ioo_mem_nhdsLT (show 1 - 2⁻¹ < (1 : ℝ) 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 : a ∈ Ioo (HSub.hSub (α := ℝ) 1 2⁻¹) 1
⊢ 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 : ℕ
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
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 : ℕ
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 ≠ 0
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 = 0
have linarith : a = 0 → 2 / 2 = 1
Tactic: linarith [show (1 : ℝ) = 2⁻¹ + 2⁻¹ by norm_num]