mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
⊢ x.agm y = (sqrt (x * y)).agm ((x + y) / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-1) 1
⊢ cosh (artanh x) = 1 / √(1 - x ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-1) 1
⊢ tanh (artanh x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
⊢ 0 < 1 + tanh x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
⊢ 0 < 1 - tanh x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
n : ℕ
⊢ (x.agmSequences y n).1 < x.agm y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x ↦ -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ Odd (2 * k + 0 + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
⊢ artanh (tanh x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
hn : x ≠ y
n : ℕ
⊢ x.agm y < (x.agmSequences y n).2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: ⊢ StrictMonoOn (fun x ↦ (1 + x) / (1 - x)) (Ioo (-1) 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-1) 1
⊢ 0 ≤ 1 + x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-1) 1
⊢ 0 ≤ 1 - x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: ⊢ StrictMonoOn artanh (Ioo (-1) 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x y : ℝ
hx : -1 < x
hy : y < 1
hxy : x ≤ y
⊢ x ∈ Ioo (-1) 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x y : ℝ
hx : -1 < x
hy : y < 1
hxy : x ≤ y
⊢ y ∈ Ioo (-1) 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x y : ℝ
hx : -1 < x
hy : y < 1
hxy : x < y
⊢ x ∈ Ioo (-1) 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x y : ℝ
hx : -1 < x
hy : y < 1
hxy : x < y
⊢ y ∈ Ioo (-1) 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
⊢ artanh x = 0 ↔ x ≤ -1 ∨ x = 0 ∨ 1 ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo 0 1
⊢ 0 ∈ Ioo (-1) 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo 0 1
⊢ x ∈ Ioo (-1) 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo 0 1
⊢ 0 < artanh x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-1) 0
⊢ x ∈ Ioo (-1) 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-1) 0
⊢ 0 ∈ Ioo (-1) 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x ↦ -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ Even (2 * (k + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-1) 0
⊢ artanh x < 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
⊢ min x y < x.agm y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
h✝ : x < 1
⊢ 0 ∈ Ioo (-1) 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
h✝ : x < 1
⊢ x ∈ Ioo (-1) 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ artanh x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ≤ 0
h✝ : -1 < x
⊢ x ∈ Ioo (-1) 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ≤ 0
h✝ : -1 < x
⊢ 0 ∈ Ioo (-1) 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
hn : x ≠ y
⊢ x.agm y < max x y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ≤ 0
⊢ artanh x ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y k : ℝ≥0
⊢ (k * x).agm (k * y) = k * x.agm y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun n ↦ (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: x : ℝ
hx : ‖x‖ < 1
⊢ ‖↑x‖ < 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: ⊢ binEntropy 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: ⊢ binEntropy 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: ⊢ binEntropy 2⁻¹ = log 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ binEntropy p = p.negMulLog + (1 - p).negMulLog

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ binEntropy (1 - p) = binEntropy p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ binEntropy (2⁻¹ + p) = binEntropy (2⁻¹ - p)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Choose

Goal state before:
pp: k : ℕ
⊢ (fun n ↦ ↑(n.descFactorial k)) ~[atTop] fun n ↦ ↑n ^ k

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 < binEntropy p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Choose

Goal state before:
pp: k : ℕ
⊢ (fun n ↦ ↑(n.choose k)) ~[atTop] fun n ↦ ↑n ^ k / ↑k !

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
⊢ 0 ≤ binEntropy p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp : p < 0
this : -p * log p < (1 - p) * log (1 - p)
⊢ p * -log p + (1 - p) * -log (1 - p) < 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Choose

Goal state before:
pp: k : ℕ
⊢ (fun n ↦ ↑(n.choose k)) =Θ[atTop] fun n ↦ ↑n ^ k

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp : p < 0
hp' : p < -1
⊢ -p < 1 - p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp : p < 0
hp' : p < -1
⊢ log p < log (1 - p)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case pos
p : ℝ
hp : p < 0
hp' : p < -1
⊢ -p * log p < (1 - p) * log (1 - p)

Tactic:
have : log p < log (1 - p) := by
      rw [← log_neg_eq_log]
      exact log_lt_log (Left.neg_pos_iff.mpr hp) (by linarith)
    nlinarith [log_pos_of_lt_neg_one hp']

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
hre : Tendsto re l atTop
r : ℝ
hr : im =O[l] fun z ↦ z.re ^ r
n : ℕ
z : ℂ
hz : 0 ≤ z.re
⊢ (fun z ↦ (z.re ^ r) ^ n) z = (fun z ↦ z.re ^ (r * ↑n)) z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
hre : Tendsto re l atTop
him : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun z ↦ |z.im|
⊢ im =O[l] fun z ↦ z.re ^ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ (fun z ↦ (z.im ^ n) ^ 2) = fun z ↦ z.im ^ (2 * n)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ (fun z ↦ Real.exp z.re) = fun z ↦ Real.exp z.re ^ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ (fun z ↦ |z.im| ^ n) ≤ᶠ[l] fun z ↦ Real.exp z.re

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
⊢ 0 < √2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp : p < 0
hp' : ¬p < -1
⊢ -p * log p ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp : p < 0
hp' : ¬p < -1
this : -p * log p ≤ 0
⊢ 1 < 1 - p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp : p < 0
⊢ binEntropy p < 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp : p ≤ 0
⊢ binEntropy p ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp : 1 < p
⊢ binEntropy p < 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp : 1 ≤ p
⊢ binEntropy p ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ p = 0 ∨ p = 1 → binEntropy p = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ binEntropy p = 0 ↔ p = 0 ∨ p = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
⊢ (fun x ↦ ‖Real.log ‖x‖‖) z ≤ (fun z ↦ Real.log √2 + Real.log (max z.re |z.im|)) z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ}, p ≠ 2⁻¹ → p < 2⁻¹ → binEntropy p < log 2
hp : ¬p < 2⁻¹
⊢ 1 - p < 2⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : p ≤ 0
⊢ 1 < 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
⊢ 2⁻¹ < 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
hp₁ : 0 < 1 - p
⊢ p⁻¹ ≠ (1 - p)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
hp₁ : 0 < 1 - p
⊢ p + (1 - p) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: case inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
hle : z.re ≤ |z.im|
h₁ : 1 < z.re
H : 1 < |z.im|
⊢ ↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖

Tactic:
rwa [max_eq_right hle, Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (Real.log_pos H),
              ← Real.log_pow, Real.log_le_iff_le_exp (pow_pos (one_pos.trans H) _),
              abs_of_pos (one_pos.trans h₁)]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ ∀ᶠ (x : ℂ) in l, ↑n * ‖Real.log (max x.re |x.im|)‖ ≤ ‖x.re‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
hl : IsExpCmpFilter l
a z : ℂ
hz : z ≠ 0
⊢ (fun z ↦ ‖z‖ ^ a.re) z = (fun z ↦ Real.exp (a.re * Real.log ‖z‖)) z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
⊢ (fun z ↦ Real.exp (a.re * Real.log ‖z‖)) =o[l] fun x ↦ ‖cexp (↑b * x)‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
hp₁ : 0 < 1 - p
⊢ log (p * p⁻¹ + (1 - p) * (1 - p)⁻¹) = log 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
⊢ (fun z ↦ z ^ a₁ * cexp (↑b₁ * z)) z = (fun z ↦ z ^ a₂ * cexp (↑b₁ * z) * z ^ (a₁ - a₂)) z

Tactic:
simp only

Goal state after:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
⊢ z ^ a₁ * cexp (↑b₁ * z) = z ^ a₂ * cexp (↑b₁ * z) * z ^ (a₁ - a₂)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ binEntropy p < log 2 ↔ p ≠ 2⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ binEntropy p ≤ log 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ binEntropy p = log 2 ↔ p = 2⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
⊢ (fun z ↦ z ^ a₁ * cexp (↑b₁ * z)) z = (fun z ↦ z ^ a₂ * cexp (↑b₁ * z) * z ^ (a₁ - a₂)) z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: ⊢ Continuous binEntropy

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ : ℂ
⊢ (fun z ↦ z ^ a₂ * cexp (↑b₁ * z) * cexp (↑(b₂ - b₁) * z)) =ᶠ[l] fun z ↦ z ^ a₂ * cexp (↑b₂ * z)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : b < 0
⊢ (fun z ↦ cexp (↑b * z)) =o[l] fun z ↦ z ^ a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
m n : ℕ
⊢ (fun z ↦ z ^ m * cexp (↑b₁ * z)) =o[l] fun z ↦ z ^ n * cexp (↑b₂ * z)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ binEntropy p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
m n : ℤ
⊢ (fun z ↦ z ^ m * cexp (↑b₁ * z)) =o[l] fun z ↦ z ^ n * cexp (↑b₂ * z)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ DifferentiableAt ℝ binEntropy p ↔ p ≠ 0 ∧ p ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ deriv binEntropy p = log (1 - p) - log p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
⊢ qaryEntropy q 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
⊢ qaryEntropy q 1 = log ↑(↑q - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: ⊢ qaryEntropy 2 = binEntropy

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 < qaryEntropy q p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
⊢ 0 ≤ qaryEntropy q p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
⊢ Continuous (qaryEntropy q)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ (qaryEntropy q) p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ deriv (qaryEntropy q) p = log (↑q - 1) + log (1 - p) - log p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: ⊢ 0 < 1 / 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: ⊢ Tendsto (fun p ↦ log (1 - p) - log p) (𝓝[>] 0) atTop

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: this : Tendsto log (𝓝[>] 0) atBot
contF : Continuous fun x ↦ 1 - x
⊢ MapsTo (fun x ↦ 1 - x) (Iio 1) (Ioi 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: ⊢ 1 - 2⁻¹ < 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: ⊢ Tendsto (fun p ↦ log (1 - p) - log p) (𝓝[<] 1) atBot

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
⊢ (fun p ↦ log (↑q - 1) + log (1 - p) - log p) = fun p ↦ log (↑q - 1) + (log (1 - p) - log p)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
⊢ Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
x : ℝ
⊢ u₂' x = (2 * ↑n + 1) * f x ^ n - 2 * ↑n * f x ^ (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
⊢ Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q✝ : ℕ
p✝ : ℝ
xne0 : p✝ ≠ 0
xne1 : p✝ ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p✝, deriv (fun p ↦ qaryEntropy q✝ p) y = log (↑q✝ - 1) + log (1 - y) - log y
q p : ℝ
⊢ DifferentiableAt ℝ (fun p ↦ q - p) p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
this : ∀ (x : ℝ), u₂' x = (2 * ↑n + 1) * f x ^ n - 2 * ↑n * f x ^ (n - 1)
⊢ Continuous v₂

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - 1 / ↑q)
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - 1 / ↑q))
this : 2 ≤ ↑q
⊢ 0 < (↑q)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - 1 / ↑q)
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - 1 / ↑q))
this : 2 ≤ ↑q
zero_le_qinv : 0 < (↑q)⁻¹
⊢ p < 1 - (↑q)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - 1 / ↑q)
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - 1 / ↑q))
this : 2 ≤ ↑q
zero_le_qinv : 0 < (↑q)⁻¹
⊢ 0 < 1 - p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - 1 / ↑q)
p1le2 : p1 < p2
p : ℝ
this✝ : 2 ≤ ↑q
zero_le_qinv : 0 < (↑q)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < 1 - (↑q)⁻¹
⊢ p ≠ 0

Tactic:
by

Goal state after: