English
The derivative of qaryEntropy q is not continuous at p = 0.
Русский
Производная qaryEntropy q не непрерывна в точке p = 0.
LaTeX
$$¬ ContinuousAt (deriv (qaryEntropy q)) 0$$
Lean4
theorem not_continuousAt_deriv_qaryEntropy_zero : ¬ContinuousAt (deriv (qaryEntropy q)) 0 :=
by
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
apply not_continuousAt_of_tendsto (Filter.Tendsto.congr' _ tendstoTop) nhdsWithin_le_nhds
· simp only [disjoint_nhds_atTop_iff, not_isTop, not_false_eq_true]
filter_upwards [Ioo_mem_nhdsGT (show (0 : ℝ) < 2⁻¹ by norm_num)]
intros
apply (deriv_qaryEntropy _ _).symm
· simp_all only [mem_Ioo, ne_eq]
linarith
· simp_all only [mem_Ioo, ne_eq]
linarith [two_inv_lt_one (α := ℝ)]
