Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Average Value Theorems for Real Functions of One Variable

by
Jaroslaw Kotowicz,

MML identifier: ROLLE
[ Mizar article, MML identifier index ]

```environ

vocabulary SEQ_1, PARTFUN1, FCONT_1, RCOMP_1, FUNCT_1, FDIFF_1, PRE_TOPC,
RELAT_1, COMPTS_1, ARYTM, SEQ_4, LATTICES, SEQ_2, PARTFUN2, ARYTM_3,
BOOLE, ARYTM_1, SEQM_3, ORDINAL2, RFUNCT_2;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, NAT_1, RELSET_1, SEQ_1, SEQ_2, SEQM_3, SEQ_4, PARTFUN1, PARTFUN2,
RFUNCT_2, RCOMP_1, FCONT_1, FDIFF_1;
constructors REAL_1, SEQ_2, SEQM_3, SEQ_4, PARTFUN2, RFUNCT_2, RCOMP_1,
FCONT_1, FDIFF_1, PARTFUN1, MEMBERED, XBOOLE_0;
clusters RCOMP_1, FDIFF_1, RELSET_1, XREAL_0, SEQ_1, NAT_1, MEMBERED,
ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin

reserve y for set;
reserve g,r,s,p,t,x,x0,x1,x2 for Real;
reserve n,n1 for Nat;
reserve s1,s2,s3 for Real_Sequence;
reserve f,f1,f2,f3 for PartFunc of REAL,REAL;

theorem :: ROLLE:1
for p,g st p<g for f st
f is_continuous_on [.p,g.] & f.p=f.g & f is_differentiable_on ].p,g.[
ex x0 st x0 in ].p,g.[ & diff(f,x0)=0;

theorem :: ROLLE:2
for x,t st 0<t for f st f is_continuous_on [.x,x+t.] &
f.x=f.(x+t) & f is_differentiable_on ].x,x+t.[
ex s st 0<s & s<1 & diff(f,x+s*t)=0;

theorem :: ROLLE:3
for p,g st p<g for f st
f is_continuous_on [.p,g.] & f is_differentiable_on ].p,g.[
ex x0 st x0 in ].p,g.[ & diff(f,x0)=(f.g-f.p)/(g-p);

theorem :: ROLLE:4
for x,t st 0<t for f st f is_continuous_on [.x,x+t.] &
f is_differentiable_on ].x,x+t.[
ex s st 0<s & s<1 & f.(x+t) = f.x + t*diff(f,x+s*t);

theorem :: ROLLE:5
for p,g st p<g for f1,f2 st
f1 is_continuous_on [.p,g.] & f1 is_differentiable_on ].p,g.[ &
f2 is_continuous_on [.p,g.] & f2 is_differentiable_on ].p,g.[
ex x0 st x0 in ].p,g.[ & (f1.g-f1.p)*diff(f2,x0)=(f2.g-f2.p)*diff(f1,x0);

theorem :: ROLLE:6
for x,t st 0<t for f1,f2 st f1 is_continuous_on [.x,x+t.] &
f1 is_differentiable_on ].x,x+t.[ & f2 is_continuous_on [.x,x+t.] &
f2 is_differentiable_on ].x,x+t.[ &
(for x1 st x1 in ].x,x+t.[ holds diff(f2,x1)<>0)
ex s 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);

theorem :: ROLLE:7
for p,g st p<g for f st f is_differentiable_on ].p,g.[ &
(for x st x in ].p,g.[ holds diff(f,x) = 0)
holds f is_constant_on ].p,g.[;

theorem :: ROLLE:8
for p,g st p<g for f1,f2 st f1 is_differentiable_on ].p,g.[ &
f2 is_differentiable_on ].p,g.[ &
(for x st x in ].p,g.[ holds diff(f1,x) = diff(f2,x))
holds f1-f2 is_constant_on ].p,g.[ &
ex r st for x st x in ].p,g.[ holds f1.x = f2.x+r;

theorem :: ROLLE:9
for p,g st p<g for f st f is_differentiable_on ].p,g.[ &
(for x st x in ].p,g.[ holds 0<diff(f,x))
holds f is_increasing_on ].p,g.[;

theorem :: ROLLE:10
for p,g st p<g for f st f is_differentiable_on ].p,g.[ &
(for x st x in ].p,g.[ holds diff(f,x)<0)
holds f is_decreasing_on ].p,g.[;

theorem :: ROLLE:11
for p,g st p<g for f st f is_differentiable_on ].p,g.[ &
(for x st x in ].p,g.[ holds 0<=diff(f,x))
holds f is_non_decreasing_on ].p,g.[;

theorem :: ROLLE:12
for p,g st p<g for f st f is_differentiable_on ].p,g.[ &
(for x st x in ].p,g.[ holds diff(f,x)<=0)
holds f is_non_increasing_on ].p,g.[;
```