English
For every q, qaryEntropy q is continuous on ℝ.
Русский
Для каждого q функция qaryEntropy q непрерывна на ℝ.
LaTeX
$$$ \operatorname{Continuous}(qaryEntropy q) $$$
Lean4
/-- Qary entropy is strictly decreasing in the interval [1 - q⁻¹, 1]. -/
theorem qaryEntropy_strictAntiOn (qLe2 : 2 ≤ q) : StrictAntiOn (qaryEntropy q) (Icc (1 - 1 / q) 1) :=
by
intro p1 hp1 p2 hp2 p1le2
apply strictAntiOn_of_deriv_neg (convex_Icc (1 - 1 / (q : ℝ)) 1) _ _ hp1 hp2 p1le2
· exact qaryEntropy_continuous.continuousOn
· intro p hp
have : 2 ≤ (q : ℝ) := Nat.ofNat_le_cast.mpr qLe2
have qinv_lt_1 : (q : ℝ)⁻¹ < 1 := inv_lt_one_of_one_lt₀ (by linarith)
have zero_lt_1_sub_p : 0 < 1 - p := by simp_all only [sub_pos, interior_Icc, mem_Ioo]
simp only [one_div, interior_Icc, mem_Ioo] at hp
rw [deriv_qaryEntropy (by linarith)]
· simp only [sub_neg, gt_iff_lt]
rw [← log_mul (by linarith) (by linarith)]
apply Real.strictMonoOn_log (mem_Ioi.mpr (show 0 < (↑q - 1) * (1 - p) by nlinarith))
· simp_all only [mem_Ioi]
linarith
· have qpos : 0 < (q : ℝ) := by positivity
ring_nf
simp only [add_lt_iff_neg_right, neg_add_lt_iff_lt_add, add_zero, gt_iff_lt]
have : (q : ℝ) - 1 < p * q := by
have tmp := mul_lt_mul_of_pos_right hp.1 qpos
have : (q : ℝ) ≠ 0 := (ne_of_lt qpos).symm
have asdfasfd : (1 - (q : ℝ)⁻¹) * ↑q = q - 1 := by
calc
(1 - (q : ℝ)⁻¹) * ↑q
_ = q - (q : ℝ)⁻¹ * (q : ℝ) := by ring
_ = q - 1 := by simp_all only [ne_eq, isUnit_iff_ne_zero, not_false_eq_true, IsUnit.inv_mul_cancel]
rwa [asdfasfd] at tmp
nlinarith
exact (ne_of_gt (lt_add_neg_iff_lt.mp zero_lt_1_sub_p : p < 1)).symm
