English
If the derivative tends to +∞ along the right side at a, then the function is not differentiable on the right at a.
Русский
Если производная стремится к +∞ слева/справа по отношению к a при подходе справа, функция не дифференцируема справа в точке a.
LaTeX
$$$\\text{not }\\text{DifferentiableWithinAt} \\big(\\mathbb{R}\\to\\mathbb{R},\\ I_{>a}, a\\big)$$$
Lean4
/-- A real function whose derivative tends to infinity from the right at a point is not
differentiable on the right at that point. -/
theorem not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi (f : ℝ → ℝ) {a : ℝ}
(hf : Tendsto (deriv f) (𝓝[>] a) atTop) : ¬DifferentiableWithinAt ℝ f (Ioi a) a :=
by
replace hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop :=
by
refine hf.congr' ?_
filter_upwards [eventually_mem_nhdsWithin] with x hx
have : Ioi a ∈ 𝓝 x := by simp [← mem_interior_iff_mem_nhds, hx]
exact (derivWithin_of_mem_nhds this).symm
by_cases hcont_at_a : ContinuousWithinAt f (Ici a) a
case neg =>
intro hcontra
have := hcontra.continuousWithinAt
rw [← ContinuousWithinAt.diff_iff this] at hcont_at_a
simp at hcont_at_a
case pos =>
intro hdiff
replace hdiff := hdiff.hasDerivWithinAt
rw [hasDerivWithinAt_iff_tendsto_slope, Set.diff_singleton_eq_self notMem_Ioi_self] at hdiff
have h₀ : ∀ᶠ b in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x :=
by
rw [(nhdsGT_basis a).eventually_iff]
rw [(nhdsGT_basis a).tendsto_left_iff] at hf
obtain ⟨b, hab, hb⟩ := hf (Ioi (max (derivWithin f (Ioi a) a + 1) 0)) (Ioi_mem_atTop _)
refine ⟨b, hab, fun x hx z hz => ?_⟩
simp only [MapsTo, mem_Ioo, mem_Ioi, and_imp] at hb
exact hb hz.1 <| hz.2.trans_lt hx.2
have h₁ : ∀ᶠ b in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1 :=
by
rw [(nhds_basis_Ioo _).tendsto_right_iff] at hdiff
specialize hdiff ⟨derivWithin f (Ioi a) a - 1, derivWithin f (Ioi a) a + 1⟩ <| by simp
filter_upwards [hdiff] with z hz using hz.2
have hcontra : ∀ᶠ _ in 𝓝[>] a, False :=
by
filter_upwards [h₀, h₁, eventually_mem_nhdsWithin] with b hb hslope (hab : a < b)
have hdiff' : DifferentiableOn ℝ f (Ioc a b) := fun z hz =>
by
refine DifferentiableWithinAt.mono (t := Ioi a) ?_ Ioc_subset_Ioi_self
have : derivWithin f (Ioi a) z ≠ 0 := ne_of_gt <| by simp_all only [and_imp, mem_Ioc, max_lt_iff]
exact differentiableWithinAt_of_derivWithin_ne_zero this
have hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z :=
by
intro z hz''
refine (hdiff'.continuousOn z hz'').mono_of_mem_nhdsWithin ?_
have hfinal : 𝓝[Ioc a b] z = 𝓝[Icc a b] z :=
by
refine nhdsWithin_eq_nhdsWithin' (s := Ioi a) (Ioi_mem_nhds hz''.1) ?_
simp only [Ioc_inter_Ioi, le_refl, sup_of_le_left]
ext y
exact ⟨fun h => ⟨mem_Icc_of_Ioc h, mem_of_mem_inter_left h⟩, fun ⟨H1, H2⟩ => ⟨H2, H1.2⟩⟩
rw [← hfinal]
exact self_mem_nhdsWithin
have hcont : ContinuousOn f (Icc a b) := by
intro z hz
by_cases hz' : z = a
· rw [hz']
exact hcont_at_a.mono Icc_subset_Ici_self
· exact hcont_Ioc z ⟨lt_of_le_of_ne hz.1 (Ne.symm hz'), hz.2⟩
obtain ⟨x, hx₁, hx₂⟩ := exists_deriv_eq_slope' f hab hcont (hdiff'.mono (Ioo_subset_Ioc_self))
specialize hb x ⟨hx₁.1, le_of_lt hx₁.2⟩
replace hx₂ : derivWithin f (Ioi a) x = slope f a b :=
by
have : Ioi a ∈ 𝓝 x := by simp [← mem_interior_iff_mem_nhds, hx₁.1]
rwa [derivWithin_of_mem_nhds this]
rw [hx₂, max_lt_iff] at hb
linarith
simp [Filter.eventually_false_iff_eq_bot, ← notMem_closure_iff_nhdsWithin_eq_bot] at hcontra
