:: Average Value Theorems for Real Functions of One Variable
:: by Jaros{\l}aw Kotowicz, Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received June 18, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users


theorem Th1: :: ROLLE:1
for p, g being Real st p < g holds
for f being PartFunc of REAL,REAL st [.p,g.] c= dom f & f | [.p,g.] is continuous & f . p = f . g & f is_differentiable_on ].p,g.[ holds
ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = 0 )
proof end;

:: WP: Rolle Theorem
theorem :: ROLLE:2
for x, t being Real st 0 < t holds
for f being PartFunc of REAL,REAL st [.x,(x + t).] c= dom f & f | [.x,(x + t).] is continuous & f . x = f . (x + t) & f is_differentiable_on ].x,(x + t).[ holds
ex s being Real st
( 0 < s & s < 1 & diff (f,(x + (s * t))) = 0 )
proof end;

:: WP: The Mean Value Theorem
theorem Th3: :: ROLLE:3
for p, g being Real st p < g holds
for f being PartFunc of REAL,REAL st [.p,g.] c= dom f & f | [.p,g.] is continuous & f is_differentiable_on ].p,g.[ holds
ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) )
proof end;

:: WP: Lagrange Theorem
theorem :: ROLLE:4
for x, t being Real st 0 < t holds
for f being PartFunc of REAL,REAL st [.x,(x + t).] c= dom f & f | [.x,(x + t).] is continuous & f is_differentiable_on ].x,(x + t).[ holds
ex s being Real st
( 0 < s & s < 1 & f . (x + t) = (f . x) + (t * (diff (f,(x + (s * t))))) )
proof end;

theorem Th5: :: ROLLE:5
for p, g being Real st p < g holds
for f1, f2 being PartFunc of REAL,REAL st [.p,g.] c= dom f1 & [.p,g.] c= dom f2 & f1 | [.p,g.] is continuous & f1 is_differentiable_on ].p,g.[ & f2 | [.p,g.] is continuous & f2 is_differentiable_on ].p,g.[ holds
ex x0 being Real st
( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) )
proof end;

:: WP: Cauchy Theorem
theorem :: ROLLE:6
for x, t being Real st 0 < t holds
for f1, f2 being PartFunc of REAL,REAL st [.x,(x + t).] c= dom f1 & [.x,(x + t).] c= dom f2 & f1 | [.x,(x + t).] is continuous & f1 is_differentiable_on ].x,(x + t).[ & f2 | [.x,(x + t).] is continuous & f2 is_differentiable_on ].x,(x + t).[ & ( for x1 being Real st x1 in ].x,(x + t).[ holds
diff (f2,x1) <> 0 ) holds
ex s being Real st
( 0 < s & s < 1 & ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff (f1,(x + (s * t)))) / (diff (f2,(x + (s * t)))) )
proof end;

theorem Th7: :: ROLLE:7
for p, g being Real
for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f,x) = 0 ) holds
f | ].p,g.[ is V8()
proof end;

theorem :: ROLLE:8
for p, g being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on ].p,g.[ & f2 is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f1,x) = diff (f2,x) ) holds
( (f1 - f2) | ].p,g.[ is V8() & ex r being Real st
for x being Real st x in ].p,g.[ holds
f1 . x = (f2 . x) + r )
proof end;

theorem :: ROLLE:9
for p, g being Real
for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
0 < diff (f,x) ) holds
f | ].p,g.[ is increasing
proof end;

theorem :: ROLLE:10
for p, g being Real
for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f,x) < 0 ) holds
f | ].p,g.[ is decreasing
proof end;

theorem :: ROLLE:11
for p, g being Real
for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
0 <= diff (f,x) ) holds
f | ].p,g.[ is non-decreasing
proof end;

theorem :: ROLLE:12
for p, g being Real
for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f,x) <= 0 ) holds
f | ].p,g.[ is non-increasing
proof end;