補題
R を実数体とする。
E を R 上の分離的な前Hilbert空間(過去スレ010の598)とする。
f: [a, b] → E を連続写像とし、
f は (a, b) で微分可能とする。

このとき、
|f(b) - f(a)| ≦ (b - a)|f’(c)| となる c ∈ (a, b) が存在する。

証明
v = f(b) - f(a) とおく。
ψ(t) = <v, f(t)> とおく。
ψ(t) は [a, b] 上の実数値連続関数であり、(a, b) で微分可能である。

平均値の定理より、
ψ(b) - ψ(a) = (b - a)ψ’(c) = (b - a)<v, f’(c)>
となる c ∈ (a, b) が存在する。

Cauchy-Schwarzの不等式(過去スレ010の594)より
|ψ(b) - ψ(a)| ≦ (b - a)|v||f’(c)|

他方、
ψ(b) - ψ(a) = <v, f(b) - f(a)> = <v, v>

よって、
|v|^2 ≦ (b - a)|v||f’(c)|

よって、
|v| ≦ (b - a)|f’(c)|
証明終