長めの例: 閉区間上の Rolle の定理を使う

次の例は，Rolle の定理を直接使う演習です． 関数 f が閉区間 [a, b] で連続で，端点で同じ値を取るなら， 開区間 (a, b) のどこかで導関数が 0 になります．

この statement はこの章の前半にも出しましたが，ここでは「学部解析の定理をそのまま Lean の命題として読む」ことに注目します．

section RolleExample

open Set

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

end RolleExample

この定理を使うには，ContinuousOn f (Icc a b) が必要です． 微分可能性の仮定が statement に現れていないように見えますが， Mathlib のこの定理は，一般の Rolle の定理のうち，導関数が定義上 0 になる点を含む形になっています． より強い形や平均値の定理を使うときは，DifferentiableOn ℝ f (Ioo a b) が明示的に必要になります．