-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
/-- For probability `p ≠ 0.5`, `binEntropy p < log 2`. -/
lemma binEntropy_lt_log_two : binEntropy p < log 2 ↔ p ≠ 2⁻¹

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

Tactic:
norm_num

Result:
no goals

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

Tactic:
norm_num at *

Result:
p : ℝ
h : ¬p = 1 / 2
this : ∀ {p : ℝ}, ¬p = 1 / 2 → p < 1 / 2 → binEntropy p < log 2
hp : 1 / 2 ≤ p
⊢ 1 / 2 < p

Proof state:
case refine_2
p : ℝ
h : p ≠ 2⁻¹
⊢ binEntropy p < log 2

Tactic:
wlog hp : p < 2⁻¹

Result:
case refine_2.inr
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ}, p ≠ 2⁻¹ → p < 2⁻¹ → binEntropy p < log 2
hp : ¬p < 2⁻¹
⊢ binEntropy p < log 2

p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
⊢ binEntropy p < log 2

Proof state:
case inr
p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
⊢ binEntropy p < log 2

Tactic:
have hp₁ : 0 < 1 - p := sub_pos.2 <| hp.trans <| by norm_num

Result:
case inr
p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
hp₁ : 0 < 1 - p
⊢ binEntropy p < log 2

Proof state:
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:
rw [mul_inv_cancel₀, mul_inv_cancel₀, one_add_one_eq_two] <;> positivity

Result:
no goals

Proof state:
case refine_2.inr
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ}, p ≠ 2⁻¹ → p < 2⁻¹ → binEntropy p < log 2
hp✝ : ¬p < 2⁻¹
hp : 1 - p < 2⁻¹
⊢ binEntropy p < log 2

Tactic:
rw [← binEntropy_one_sub]

Result:
case refine_2.inr
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ}, p ≠ 2⁻¹ → p < 2⁻¹ → binEntropy p < log 2
hp✝ : ¬p < 2⁻¹
hp : 1 - p < 2⁻¹
⊢ binEntropy (1 - p) < log 2

Proof state:
case refine_1
p : ℝ
⊢ binEntropy p < log 2 → p ≠ 2⁻¹

Tactic:
rintro h rfl

Result:
case refine_1
h : binEntropy 2⁻¹ < log 2
⊢ False

Proof state:
p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
⊢ binEntropy p < log 2

Tactic:
obtain hp₀ | hp₀ := le_or_lt p 0

Result:
case inl
p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : p ≤ 0
⊢ binEntropy p < log 2

case inr
p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
⊢ binEntropy p < log 2

Proof state:
case refine_1
h : binEntropy 2⁻¹ < log 2
⊢ False

Tactic:
simp at h

Result:
no goals

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

Tactic:
simpa [eq_sub_iff_add_eq, ← two_mul, mul_comm, mul_eq_one_iff_eq_inv₀]

Result:
no goals

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

Tactic:
simp

Result:
no goals

Proof state:
p : ℝ
h : ¬p = 1 / 2
this : ∀ {p : ℝ}, ¬p = 1 / 2 → p < 1 / 2 → binEntropy p < log 2
hp : 1 / 2 ≤ p
⊢ 1 / 2 < p

Tactic:
linarith (config := { splitNe := true })

Result:
no goals

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

Tactic:
rw [sub_lt_comm]

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

Proof state:
case refine_2.inr
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ}, p ≠ 2⁻¹ → p < 2⁻¹ → binEntropy p < log 2
hp : ¬p < 2⁻¹
⊢ binEntropy p < log 2

Tactic:
have hp : 1 - p < 2⁻¹ := by
  rw [sub_lt_comm]; norm_num at *; linarith (config := { splitNe := true })

Result:
case refine_2.inr
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ}, p ≠ 2⁻¹ → p < 2⁻¹ → binEntropy p < log 2
hp✝ : ¬p < 2⁻¹
hp : 1 - p < 2⁻¹
⊢ binEntropy p < log 2

Proof state:
case refine_2.inr
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ}, p ≠ 2⁻¹ → p < 2⁻¹ → binEntropy p < log 2
hp✝ : ¬p < 2⁻¹
hp : 1 - p < 2⁻¹
⊢ binEntropy (1 - p) < log 2

Tactic:
exact this hp.ne hp

Result:
no goals

Proof state:
p : ℝ
⊢ binEntropy p < log 2 ↔ p ≠ 2⁻¹

Tactic:
refine ⟨?_, fun h ↦ ?_⟩

Result:
case refine_1
p : ℝ
⊢ binEntropy p < log 2 → p ≠ 2⁻¹

case refine_2
p : ℝ
h : p ≠ 2⁻¹
⊢ binEntropy p < log 2

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

Tactic:
norm_num

Result:
no goals

Proof state:
case inl
p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : p ≤ 0
⊢ binEntropy p < log 2

Tactic:
exact (binEntropy_nonpos_of_nonpos hp₀).trans_lt <| log_pos <| by norm_num

Result:
no goals

Proof state:
case inr
p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
hp₁ : 0 < 1 - p
⊢ binEntropy p < log 2

Tactic:
calc
_ < log (p * p⁻¹ + (1 - p) * (1 - p)⁻¹) :=
  strictConcaveOn_log_Ioi.2 (inv_pos.2 hp₀) (inv_pos.2 hp₁)
    (by simpa [eq_sub_iff_add_eq, ← two_mul, mul_comm, mul_eq_one_iff_eq_inv₀]) hp₀ hp₁ (by simp)
_ = log 2 := by rw [mul_inv_cancel₀, mul_inv_cancel₀, one_add_one_eq_two] <;> positivity

Result:
no goals