awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : ¬(p ≠ 0 ∧ p ≠ 1)
neg : 0 = log (1 - p) - log p
⊢ deriv binEntropy p = log (1 - p) - log p

Tactic:
rw [deriv_zero_of_not_differentiableAt (differentiableAt_binEntropy_iff_ne_zero_one.not.2 hp)]

Premises used: Iff.mpr, deriv_zero_of_not_differentiableAt, Iff.not, Real.differentiableAt_binEntropy_iff_ne_zero_one
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : ¬(p ≠ 0 ∧ p ≠ 1)
⊢ p = 0 ∨ p = 1

Tactic:
push +distrib Not at hp

Premises used: Not
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p = 0 ∨ p = 1
neg : 0 = log (HSub.hSub (α := ℝ) 1 0) - log 0
neg₁ : 0 = log (HSub.hSub (α := ℝ) 1 1) - log 1
⊢ 0 = log (1 - p) - log p

Tactic:
obtain rfl | rfl := hp

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ 0 = log (HSub.hSub (α := ℝ) 1 0) - log 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ 0 = log (HSub.hSub (α := ℝ) 1 1) - log 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
⊢ qaryEntropy q 0 = 0

Tactic:
simp [qaryEntropy]

Premises used: Real.qaryEntropy
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
⊢ qaryEntropy q 1 = log (↑(HSub.hSub (α := ℤ) (↑q : ℤ) 1) : ℝ)

Tactic:
simp [qaryEntropy]

Premises used: Real.qaryEntropy
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
h : ∀ (x : ℝ), qaryEntropy 2 x = binEntropy x
⊢ qaryEntropy 2 = binEntropy

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
x : ℝ
⊢ qaryEntropy 2 x = binEntropy x

Tactic:
simp [qaryEntropy]

Premises used: Real.qaryEntropy
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
positivity positivity₁ positivity₂ positivity₃ :
  0 < binEntropy p → 0 < p * log (↑(HSub.hSub (α := ℤ) (↑q : ℤ) 1) : ℝ) + binEntropy p
⊢ 0 < p * log (↑(HSub.hSub (α := ℤ) (↑q : ℤ) 1) : ℝ) + binEntropy p

Tactic:
positivity [binEntropy_pos hp₀ hp₁]

Premises used: Real.binEntropy_pos
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
inl : ∀ (hp₀ : LE.le (α := ℝ) 0 0) (hp₁ : LE.le (α := ℝ) 0 1), 0 ≤ qaryEntropy q 0
inr : ∀ (hp₀ : 0 < p), 0 ≤ qaryEntropy q p
⊢ 0 ≤ qaryEntropy q p

Tactic:
obtain rfl | hp₀ := hp₀.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
hp₀ : LE.le (α := ℝ) 0 0
hp₁ : LE.le (α := ℝ) 0 1
⊢ 0 ≤ qaryEntropy q 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
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
inr₁ : ∀ (hp₁ : p < 1), 0 ≤ qaryEntropy q p
⊢ 0 ≤ qaryEntropy q p

Tactic:
obtain rfl | hp₁ := hp₁.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
hp₀_1 : LE.le (α := ℝ) 0 1
hp₁ : LE.le (α := ℝ) 1 1
hp₀ : LT.lt (α := ℝ) 0 1
⊢ 0 ≤ qaryEntropy q 1

Tactic:
simpa [qaryEntropy, -Int.cast_sub] using log_intCast_nonneg _

Premises used: Real.qaryEntropy, Int.cast_sub, Real.log_intCast_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
hp₀_1 : 0 ≤ p
hp₁_1 : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 ≤ qaryEntropy q p

Tactic:
(qaryEntropy_pos hp₀ hp₁).le

Premises used: LT.lt.le, Real.qaryEntropy_pos
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
hp₀_1 : 0 ≤ p
hp₁_1 : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 ≤ qaryEntropy q p

Tactic:
exact (qaryEntropy_pos hp₀ hp₁).le

Premises used: LT.lt.le, Real.qaryEntropy_pos
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
hp : p < 0
⊢ qaryEntropy q p < 0

Tactic:
add_neg_of_nonpos_of_neg (mul_nonpos_of_nonpos_of_nonneg hp.le (log_intCast_nonneg _))
    (binEntropy_neg_of_neg hp)

Premises used: Real.qaryEntropy, mul_nonpos_of_nonpos_of_nonneg, Real.binEntropy_neg_of_neg, LT.lt.le, add_neg_of_nonpos_of_neg, Real.log_intCast_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
hp : p ≤ 0
⊢ qaryEntropy q p ≤ 0

Tactic:
add_nonpos (mul_nonpos_of_nonpos_of_nonneg hp (log_intCast_nonneg _))
    (binEntropy_nonpos_of_nonpos hp)

Premises used: Real.qaryEntropy, mul_nonpos_of_nonpos_of_nonneg, Real.binEntropy_nonpos_of_nonpos, add_nonpos, Real.log_intCast_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
⊢ Continuous (Y := ℝ) fun (p : ℝ) ↦ p * log (↑(HSub.hSub (α := ℤ) (↑q : ℤ) 1) : ℝ) + binEntropy p

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
funProp : p ≠ 0
funProp₁ : p ≠ 1
⊢ DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log (↑(HSub.hSub (α := ℤ) (↑q : ℤ) 1) : ℝ) + binEntropy p) p

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
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
hg : DifferentiableAt ℝ binEntropy p
⊢ deriv (fun (p : ℝ) ↦ p * log (↑(HSub.hSub (α := ℤ) (↑q : ℤ) 1) : ℝ) + binEntropy p) p =
    log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p

Tactic:
rw [deriv_fun_add]

Premises used: deriv_fun_add
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ deriv (fun (p : ℝ) ↦ p * log (↑(HSub.hSub (α := ℤ) (↑q : ℤ) 1) : ℝ)) p + deriv binEntropy p =
    log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p

Tactic:
simp only [Int.cast_sub, Int.cast_natCast, Int.cast_one, differentiableAt_fun_id,
      deriv_mul_const, deriv_id'', one_mul, deriv_binEntropy, add_sub_assoc]

Premises used: add_sub_assoc, Int.cast_natCast, Real.deriv_binEntropy, deriv_mul_const, Int.cast_sub, deriv_id'', differentiableAt_fun_id, one_mul, Int.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log (↑(HSub.hSub (α := ℤ) (↑q : ℤ) 1) : ℝ)) p

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
funProp : p ≠ 0
funProp₁ : p ≠ 1
⊢ DifferentiableAt ℝ binEntropy p

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ HasDerivAt binEntropy (log (1 - p) - log p) p

Tactic:
deriv_binEntropy _ ▸ (differentiableAt_binEntropy hp₀ hp₁).hasDerivAt

Premises used: Real.deriv_binEntropy, DifferentiableAt.hasDerivAt, Eq.rec, Real.differentiableAt_binEntropy
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ HasDerivAt (qaryEntropy q) (log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) p

Tactic:
deriv_qaryEntropy hp₀ hp₁ ▸ (differentiableAt_qaryEntropy hp₀ hp₁).hasDerivAt

Premises used: DifferentiableAt.hasDerivAt, Eq.rec, Real.deriv_qaryEntropy, Real.differentiableAt_qaryEntropy
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
hf : ∀ᶠ (x : ℝ) in 𝓝[>] 0, log (1 / 2) ≤ log (1 - x)
hg : Tendsto (β := ℝ) (fun (x : ℝ) ↦ -log x) (𝓝[>] 0) atTop
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (1 - p) - log p) (𝓝[>] 0) atTop

Tactic:
apply Filter.tendsto_atTop_add_left_of_le' (𝓝[>] 0) (log (1 / 2) : ℝ)

Premises used: Set.Ioi, nhdsWithin, HDiv.hDiv, Real.log, Filter.tendsto_atTop_add_left_of_le', OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ 0 < 1 / 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ 0 < 1 / 2

Tactic:
have h₁ : (0 : ℝ) < 1 / 2 := by simp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
h₁ : 0 < 1 / 2
h : ∀ (p : ℝ) (hx : p ∈ Ioc 0 (1 / 2)), log (1 / 2) ≤ log (1 - p)
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, log (1 / 2) ≤ log (1 - x)

Tactic:
filter_upwards [Ioc_mem_nhdsGT h₁] with p hx

Premises used: Ioc_mem_nhdsGT
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
h₁ : 0 < 1 / 2
p : ℝ
hx : p ∈ Ioc 0 (1 / 2)
h : 1 / 2 ≤ 1 - p
⊢ log (1 / 2) ≤ log (1 - p)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
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
linarith₉ :
  1 - p < 1 / 2 → HMul.hMul (α := ℝ) 2 1 - 2 * p - HMul.hMul (α := ℝ) 1 1 + (2 * p - HMul.hMul (α := ℝ) 1 1) = 0
⊢ 1 / 2 ≤ 1 - p

Tactic:
linarith [hx.2]

Premises used: And.right
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ -log x) (𝓝[>] 0) atTop

Tactic:
apply tendsto_neg_atTop_iff.mpr tendsto_log_nhdsGT_zero

Premises used: Iff.mpr, Real.tendsto_log_nhdsGT_zero, Filter.tendsto_neg_atTop_iff
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (1 - x)) (𝓝[<] 1) atBot
hg : ∀ᶠ (x : ℝ) in 𝓝[<] 1, -log x ≤ -log (HSub.hSub (α := ℝ) 1 2⁻¹)
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (1 - p) - log p) (𝓝[<] 1) atBot

Tactic:
apply Filter.tendsto_atBot_add_right_of_ge' (𝓝[<] 1) (-log (1 - 2⁻¹))

Premises used: nhdsWithin, HSub.hSub, Filter.tendsto_atBot_add_right_of_ge', Real.log, Inv.inv, OfNat.ofNat, Set.Iio, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ Tendsto log (𝓝[>] 0) atBot

Tactic:
have : Tendsto log (𝓝[>] 0) atBot := Real.tendsto_log_nhdsGT_zero
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
this : Tendsto log (𝓝[>] 0) atBot
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 - x) (𝓝[<] 1) (𝓝[>] 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (1 - x)) (𝓝[<] 1) atBot

Tactic:
apply Tendsto.comp (f := (1 - ·)) (g := log) this

Premises used: Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
this : Tendsto log (𝓝[>] 0) atBot
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ 1 - x

Tactic:
have contF : Continuous ((1 : ℝ) - ·) := continuous_sub_left 1
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
this : Tendsto log (𝓝[>] 0) atBot
contF : Continuous (Y := ℝ) fun (x : ℝ) ↦ 1 - x
p : ℝ
hx : Membership.mem (γ := Set ℝ) (Iio 1) p
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) ((fun (x : ℝ) ↦ 1 - x) p)

Tactic:
simp_all only [mem_Iio, mem_Ioi, sub_pos]

Premises used: sub_pos, Set.mem_Iio, Set.mem_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
this : Tendsto log (𝓝[>] 0) atBot
contF : Continuous (Y := ℝ) fun (x : ℝ) ↦ 1 - x
⊢ 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]
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
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) (𝓝[Ioi 0] HSub.hSub (α := ℝ) 1 1)

Tactic:
ContinuousWithinAt.tendsto_nhdsWithin (x := (1 : ℝ)) contF.continuousWithinAt this

Premises used: ContinuousWithinAt.tendsto_nhdsWithin, Continuous.continuousWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
this_1 : Tendsto log (𝓝[>] 0) atBot
contF : Continuous (Y := ℝ) fun (x : ℝ) ↦ 1 - x
this : MapsTo (β := ℝ) (fun (x : ℝ) ↦ 1 - x) (Iio 1) (Ioi 0)
h : 0 = HSub.hSub (α := ℝ) 1 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 - x) (𝓝[<] 1) (𝓝[>] 0)

Tactic:
convert! ContinuousWithinAt.tendsto_nhdsWithin (x := (1 : ℝ)) contF.continuousWithinAt this

Premises used: ContinuousWithinAt.tendsto_nhdsWithin, Continuous.continuousWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
this_1 : Tendsto log (𝓝[>] 0) atBot
contF : Continuous (Y := ℝ) fun (x : ℝ) ↦ 1 - x
this : MapsTo (β := ℝ) (fun (x : ℝ) ↦ 1 - x) (Iio 1) (Ioi 0)
⊢ 0 = HSub.hSub (α := ℝ) 1 1

Tactic:
Eq.symm (sub_eq_zero_of_eq rfl)

Premises used: sub_eq_zero_of_eq, Eq.symm, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
this_1 : Tendsto log (𝓝[>] 0) atBot
contF : Continuous (Y := ℝ) fun (x : ℝ) ↦ 1 - x
this : MapsTo (β := ℝ) (fun (x : ℝ) ↦ 1 - x) (Iio 1) (Ioi 0)
⊢ 0 = HSub.hSub (α := ℝ) 1 1

Tactic:
exact Eq.symm (sub_eq_zero_of_eq rfl)

Premises used: sub_eq_zero_of_eq, Eq.symm, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ HSub.hSub (α := ℝ) 1 2⁻¹ < 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ HSub.hSub (α := ℝ) 1 2⁻¹ < 1

Tactic:
have h₁ : (1 : ℝ) - (2 : ℝ)⁻¹ < 1 := by norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
h₁ : HSub.hSub (α := ℝ) 1 2⁻¹ < 1
h : ∀ (p : ℝ) (hx : p ∈ Ico (HSub.hSub (α := ℝ) 1 2⁻¹) 1), -log p ≤ -log (HSub.hSub (α := ℝ) 1 2⁻¹)
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, -log x ≤ -log (HSub.hSub (α := ℝ) 1 2⁻¹)

Tactic:
filter_upwards [Ico_mem_nhdsLT h₁] with p hx

Premises used: Ico_mem_nhdsLT
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
h₁ : HSub.hSub (α := ℝ) 1 2⁻¹ < 1
p : ℝ
hx : p ∈ Ico (HSub.hSub (α := ℝ) 1 2⁻¹) 1
h : HSub.hSub (α := ℝ) 1 2⁻¹ ≤ p
⊢ -log p ≤ -log (HSub.hSub (α := ℝ) 1 2⁻¹)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
h₁ : HSub.hSub (α := ℝ) 1 2⁻¹ < 1
p : ℝ
hx : p ∈ Ico (HSub.hSub (α := ℝ) 1 2⁻¹) 1
⊢ HSub.hSub (α := ℝ) 1 2⁻¹ ≤ p

Tactic:
hx.1

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
h₁ : HSub.hSub (α := ℝ) 1 2⁻¹ < 1
p : ℝ
hx : p ∈ Ico (HSub.hSub (α := ℝ) 1 2⁻¹) 1
⊢ HSub.hSub (α := ℝ) 1 2⁻¹ ≤ p

Tactic:
exact hx.1

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
h :
  ∀ (x : ℝ),
    log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x) - log x =
      log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + (log (1 - x) - log x)
⊢ 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:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
x : ℝ
⊢ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - x) - log x =
    log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + (log (1 - x) - log x)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
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)

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
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
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)
rw : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + (log (1 - p) - log p)) (𝓝[<] 1) atBot
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[<] 1) atBot

Tactic:
rw [this]
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
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)
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (1 - x) - log x) (𝓝[<] 1) atBot
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + (log (1 - p) - log p)) (𝓝[<] 1) atBot

Tactic:
apply tendsto_atBot_add_const_left

Premises used: Filter.tendsto_atBot_add_const_left
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
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 (x : ℝ) ↦ log (1 - x) - log x) (𝓝[<] 1) atBot

Tactic:
tendsto_log_one_sub_sub_log_nhdsLT_one_atBot

Premises used: _private.0.Real.tendsto_log_one_sub_sub_log_nhdsLT_one_atBot
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
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 (x : ℝ) ↦ log (1 - x) - log x) (𝓝[<] 1) atBot

Tactic:
exact tendsto_log_one_sub_sub_log_nhdsLT_one_atBot

Premises used: _private.0.Real.tendsto_log_one_sub_sub_log_nhdsLT_one_atBot
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
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
apply₁ : (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) =ᶠ[𝓝[<] 1] deriv (qaryEntropy q)
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 1

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

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

Tactic:
simp only [disjoint_nhds_atBot_iff, not_isBot, not_false_eq_true]

Premises used: disjoint_nhds_atBot_iff, not_isBot, not_false_eq_true
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
tendstoBot : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
⊢ HSub.hSub (α := ℝ) 1 2⁻¹ < 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
tendstoBot : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
h :
  ∀ a ∈ Ioo (HSub.hSub (α := ℝ) 1 2⁻¹) 1,
    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) =ᶠ[𝓝[<] 1] deriv (qaryEntropy q)

Tactic:
filter_upwards [Ioo_mem_nhdsLT (show 1 - 2⁻¹ < (1 : ℝ) by norm_num)]

Premises used: Ioo_mem_nhdsLT
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
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
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 : ℕ
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
⊢ HSub.hSub (α := ℝ) 1 2⁻¹ < a ∧ a < 1

Tactic:
simp_all only [mem_Ioo, ne_eq]

Premises used: Set.mem_Ioo, ne_eq
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
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
⊢ 1 = HAdd.hAdd (α := ℝ) 2⁻¹ 2⁻¹

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
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
linarith₃ : a = 0 → HMul.hMul (α := ℝ) 1 1 - 2 * a + (a - 1) + (a - 0) = 0
⊢ ¬a = 0

Tactic:
linarith [show (1 : ℝ) = 2⁻¹ + 2⁻¹ by norm_num]
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
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
linarith₆ : a = 1 → a - 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 : ℕ
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
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)
rw : Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + (log (1 - p) - log p)) (𝓝[>] 0) atTop
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p) (𝓝[>] 0) atTop

Tactic:
rw [this]
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
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

Tactic:
tendsto_atTop_add_const_left _ _ tendsto_log_one_sub_sub_log_nhdsGT_atAtop

Premises used: Filter.tendsto_atTop_add_const_left, _private.0.Real.tendsto_log_one_sub_sub_log_nhdsGT_atAtop
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
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

Tactic:
exact tendsto_atTop_add_const_left _ _ tendsto_log_one_sub_sub_log_nhdsGT_atAtop

Premises used: Filter.tendsto_atTop_add_const_left, _private.0.Real.tendsto_log_one_sub_sub_log_nhdsGT_atAtop
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
⊢ 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