English
There exists c ∈ Ioo(a,b) such that deriv f c equals slope f a b.
Русский
Существует c ∈ Ioo(a,b), такое что производная f в c равна наклону от a до b: deriv f c = slope f a b.
LaTeX
$$$\\exists c\\in I^{oo}_{a,b},\\; \\mathrm{deriv}\\ f\\ c = \\operatorname{slope} f\\ a\\ b$$$
Lean4
/-- A real function whose derivative tends to minus infinity from the left at a point is not
differentiable on the left at that point -/
theorem not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio (f : ℝ → ℝ) {a : ℝ}
(hf : Tendsto (deriv f) (𝓝[<] a) atBot) : ¬DifferentiableWithinAt ℝ f (Iio a) a :=
by
let f' := f ∘ Neg.neg
have hderiv : deriv f' =ᶠ[𝓝[>] (-a)] -(deriv f ∘ Neg.neg) :=
by
rw [atBot_basis.tendsto_right_iff] at hf
specialize hf (-1) trivial
rw [(nhdsLT_basis a).eventually_iff] at hf
rw [EventuallyEq, (nhdsGT_basis (-a)).eventually_iff]
obtain ⟨b, hb₁, hb₂⟩ := hf
refine ⟨-b, by linarith, fun x hx => ?_⟩
simp only [Pi.neg_apply, Function.comp_apply]
suffices deriv f' x = deriv f (-x) * deriv (Neg.neg : ℝ → ℝ) x by simpa using this
refine deriv_comp x (differentiableAt_of_deriv_ne_zero ?_) (by fun_prop)
rw [mem_Ioo] at hx
have h₁ : -x ∈ Ioo b a := ⟨by linarith, by linarith⟩
have h₂ : deriv f (-x) ≤ -1 := hb₂ h₁
exact ne_of_lt (by linarith)
have hmain : ¬DifferentiableWithinAt ℝ f' (Ioi (-a)) (-a) :=
by
refine not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi f' <| Tendsto.congr' hderiv.symm ?_
refine Tendsto.comp (g := -deriv f) ?_ tendsto_neg_nhdsGT_neg
exact Tendsto.comp (g := Neg.neg) tendsto_neg_atBot_atTop hf
intro h
have : DifferentiableWithinAt ℝ f' (Ioi (-a)) (-a) :=
by
refine DifferentiableWithinAt.comp (g := f) (f := Neg.neg) (t := Iio a) (-a) ?_ ?_ ?_
· simp [h]
· fun_prop
· intro x
simp [neg_lt]
exact hmain this
