Rolle の定理と平均値の定理

Mathlib には，実解析の基本定理も登録されています． 区間は Set.Icc a b，開区間は Set.Ioo a b として表します．

#check exists_deriv_eq_zero
#check exists_deriv_eq_slope

section MeanValue

open Set

example {f : ℝ → ℝ} {a b : ℝ}
    (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (hfI : f a = f b) :
    ∃ c ∈ Ioo a b, deriv f c = 0 := by
  exact exists_deriv_eq_zero hab hfc hfI

example (f : ℝ → ℝ) {a b : ℝ}
    (hab : a < b) (hf : ContinuousOn f (Icc a b))
    (hf' : DifferentiableOn ℝ f (Ioo a b)) :
    ∃ c ∈ Ioo a b, deriv f c = (f b - f a) / (b - a) := by
  exact exists_deriv_eq_slope f hab hf hf'

end MeanValue

演習問題

平均値の定理の statement を読み，ContinuousOn と DifferentiableOn の役割を説明してください．

-- 解答例: 閉区間上で連続，開区間上で微分可能という仮定から，
-- ある点で導関数が割線の傾きになることを述べます．
#check exists_deriv_eq_slope