:: 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-2016 Association of Mizar Users

environ

vocabularies HIDDEN, NUMBERS, REAL_1, SUBSET_1, SEQ_1, PARTFUN1, ARYTM_3, XXREAL_1, TARSKI, RELAT_1, ORDINAL2, FUNCT_1, FDIFF_1, CARD_1, RCOMP_1, XXREAL_2, SEQ_4, XXREAL_0, XBOOLE_0, ARYTM_1, VALUED_0, SEQ_2, VALUED_1, FUNCT_2, FUNCOP_1, FUNCT_7, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_1, FUNCT_2, NUMBERS, XREAL_0, XXREAL_0, XXREAL_2, XCMPLX_0, REAL_1, RELSET_1, VALUED_0, VALUED_1, SEQ_1, SEQ_2, SEQ_4, PARTFUN1, PARTFUN2, RCOMP_1, FCONT_1, FDIFF_1;
definitions TARSKI;
theorems TARSKI, NAT_1, SEQ_1, SEQ_2, SEQ_4, PARTFUN2, RFUNCT_2, RCOMP_1, FCONT_1, FDIFF_1, ZFMISC_1, FUNCT_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1, FUNCOP_1, XREAL_1, XXREAL_0, VALUED_1, XXREAL_2, XXREAL_1, FUNCT_2, VALUED_0, ORDINAL1;
schemes SEQ_1;
registrations XBOOLE_0, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, RCOMP_1, FDIFF_1, VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, FCONT_1, ORDINAL1;
constructors HIDDEN, PARTFUN1, REAL_1, NAT_1, SEQ_2, SEQ_4, RCOMP_1, PARTFUN2, RFUNCT_2, FCONT_1, FDIFF_1, VALUED_1, XXREAL_2, COMPLEX1, RELSET_1, BINOP_2, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XCMPLX_0;
expansions TARSKI;


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;