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