:: 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
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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 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;
constructors 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;
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;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
equalities XCMPLX_0;
expansions 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;
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 for PartFunc of REAL,REAL;
theorem Th1:
for p,g st pr/(n+2) by A24,XREAL_1:139;
hence 0<>s2.n by A26;
end;
then
A27: s2 is non-zero by SEQ_1:5;
s2 is convergent & lim s2 = 0 by A26,SEQ_4:31;
then reconsider h1 = s2 as 0-convergent non-zero Real_Sequence by A27,
FDIFF_1:def 1;
consider s1 such that
A28: rng s1 = {x2} by SEQ_1:6;
reconsider c = s1 as constant Real_Sequence by A28,FUNCT_2:111;
A29: now
let n;
c.n in {x2} by A28,VALUED_0:28;
hence c.n = x2 by TARSKI:def 1;
end;
deffunc G(Nat) = -(r/($1+2));
consider s3 such that
A30: for n holds s3.n=G(n) from SEQ_1:sch 1;
now
let n;
s3.n = -(r/(n+2)) by A30;
hence s3.n = (-r)/(n+2);
end;
then
A31: s3 is convergent & lim s3 = 0 by SEQ_4:31;
now
let n;
-0<>-(r/(n+2)) by A24,XREAL_1:139;
hence 0<>s3.n by A30;
end;
then s3 is non-zero by SEQ_1:5;
then reconsider h2 = s3 as 0-convergent non-zero Real_Sequence by A31,
FDIFF_1:def 1;
A32: N1 c= dom f by A14,A23;
A33: now
let n;
0+1<=n+1 by XREAL_1:6;
then 1r/(n+2) by A57,XREAL_1:139;
hence 0<>s2.n by A59;
end;
then
A60: s2 is non-zero by SEQ_1:5;
s2 is convergent & lim s2 = 0 by A59,SEQ_4:31;
then reconsider h1 = s2 as 0-convergent non-zero Real_Sequence by A60,
FDIFF_1:def 1;
consider s1 such that
A61: rng s1 = {x1} by SEQ_1:6;
reconsider c = s1 as constant Real_Sequence by A61,FUNCT_2:111;
A62: now
let n;
c.n in {x1} by A61,VALUED_0:28;
hence c.n = x1 by TARSKI:def 1;
end;
deffunc G(Nat) = -(r/($1+2));
consider s3 such that
A63: for n holds s3.n=G(n) from SEQ_1:sch 1;
now
let n;
s3.n = -(r/(n+2)) by A63;
hence s3.n = (-r)/(n+2);
end;
then
A64: s3 is convergent & lim s3 = 0 by SEQ_4:31;
now
let n;
-0<>-(r/(n+2)) by A57,XREAL_1:139;
hence 0<>s3.n by A63;
end;
then s3 is non-zero by SEQ_1:5;
then reconsider h2 = s3 as 0-convergent non-zero Real_Sequence by A64,
FDIFF_1:def 1;
A65: N1 c= dom f by A14,A56;
A66: now
let n;
0+1<=n+1 by XREAL_1:6;
then 1g-p by A1;
reconsider Z=].p,g.[ as open Subset of REAL;
defpred P[set] means $1 in [.p,g.];
let f such that
A3: [.p,g.] c= dom f and
A4: f|[.p,g.] is continuous and
A5: f is_differentiable_on ].p,g.[;
set r = (f.g-f.p)/(g-p);
deffunc F(Real) =In(r*($1-p),REAL);
consider f1 such that
A6: (for x being Element of REAL holds x in dom f1 iff P[x]) &
for x being Element of REAL st x in dom f1 holds f1.x = F(x)
from SEQ_1:sch 3;
A7: for x being Real st x in dom f1 holds f1.x = r*(x-p)
proof let x be Real such that
A8: x in dom f1;
reconsider x as Real;
f1.x = F(x) by A6,A8;
hence thesis;
end;
set f2 = f - f1;
A9: [.p,g.] c= dom f1
by A6;
then
A10: [.p,g.] c= dom f /\ dom f1 by A3,XBOOLE_1:19;
then
A11: [.p,g.] c= dom f2 by VALUED_1:12;
[.p,g.] = ].p,g.[ \/ {p,g} by A1,XXREAL_1:128;
then
A12: {p,g} c= [.p,g.] by XBOOLE_1:7;
then
A13: p in [.p,g.] by ZFMISC_1:32;
then
A14: p in dom f1 by A6;
[.p,g.] c= dom f /\ dom f1 by A3,A9,XBOOLE_1:19;
then
A15: [.p,g.] c= dom f2 by VALUED_1:12;
then
A16: f2.p = f.p-f1.p by A13,VALUED_1:13
.= f.p - r*(p-p) by A14,A7
.= f.p;
A17: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
then
A18: Z c= dom f1 by A9;
A19: now
let x;
assume x in Z;
then x in dom f1 by A17,A6;
hence f1.x = r*(x-p) by A7
.= r*x + -r*p;
end;
then
A20: f1 is_differentiable_on Z by A18,FDIFF_1:23;
now
let x be Real;
assume x in [.p,g.];
then x in dom f1 by A6;
hence f1.x = r*(x-p) by A7
.= r*x + -r*p;
end;
then f1|[.p,g.] is continuous by FCONT_1:41;
then
A21: f2|[.p,g.] is continuous by A4,A10,FCONT_1:18;
A22: g in [.p,g.] by A12,ZFMISC_1:32;
then
A23: g in dom f1 by A6;
Z c= dom f by A3,A17;
then Z c= dom f /\ dom f1 by A18,XBOOLE_1:19;
then
A24: Z c= dom f2 by VALUED_1:12;
f2.g = f.g-f1.g by A22,A15,VALUED_1:13
.= f.g - ((f.g-f.p)/(g-p))*(g-p) by A7,A23
.= f.g - (f.g-f.p) by A2,XCMPLX_1:87
.= f2.p by A16;
then consider x0 such that
A25: x0 in ].p,g.[ and
A26: diff(f2,x0)=0 by A1,A5,A20,A11,A21,A24,Th1,FDIFF_1:19;
take x0;
f2 is_differentiable_on Z by A5,A20,A24,FDIFF_1:19;
then diff(f2,x0) = (f2`|Z).x0 by A25,FDIFF_1:def 7
.= diff(f,x0) - diff(f1,x0) by A5,A20,A24,A25,FDIFF_1:19
.= diff(f,x0) - (f1`|Z).x0 by A20,A25,FDIFF_1:def 7;
hence thesis by A18,A19,A25,A26,FDIFF_1:23;
end;
::$N Lagrange Theorem
theorem
for x,t st 0f2.g;
then
A11: f2.g-f2.p<>0;
reconsider Z=].p,g.[ as open Subset of REAL;
set s=(f1.g-f1.p)/(f2.g-f2.p);
reconsider fp = f1.p - f2.p*s as Element of REAL by XREAL_0:def 1;
reconsider f3 = [.p,g.] --> fp as PartFunc of [.p,g.], REAL
by FUNCOP_1:45;
reconsider f3 as PartFunc of REAL, REAL;
set f4 = s(#)f2;
set f5 = f3+f4;
set f=f5-f1;
A12: Z c= dom f3 by A8,FUNCOP_1:13;
A13: dom f4 = dom f2 by VALUED_1:def 5;
then
A14: Z c= dom f4 by A3,A8;
then Z c= dom f3 /\ dom f4 by A12,XBOOLE_1:19;
then
A15: Z c= dom f5 by VALUED_1:def 1;
reconsider f1pf2p =f1.p - f2.p*s as Element of REAL by XREAL_0:def 1;
A16: [.p,g.] = dom f3 by FUNCOP_1:13;
then for x being Element of REAL st x in [.p,g.] /\ dom f3
holds f3.x=f1pf2p by FUNCOP_1:7;
then
A17: f3|[.p,g.] is constant by PARTFUN2:57;
then
A18: f3|].p,g.[ is constant by PARTFUN2:38,XXREAL_1:25;
then
A19: f3 is_differentiable_on Z by A12,FDIFF_1:22;
A20: p in [.p,g.] by A1,XXREAL_1:1;
then p in dom f3 /\ dom f4 by A3,A16,A13,XBOOLE_0:def 4;
then
A21: p in dom f5 by VALUED_1:def 1;
then p in dom f5 /\ dom f1 by A2,A20,XBOOLE_0:def 4;
then p in dom f by VALUED_1:12;
then
A22: f.p = f5.p - f1.p by VALUED_1:13
.= f3.p + f4.p - f1.p by A21,VALUED_1:def 1
.= f3.p + s*f2.p - f1.p by A3,A13,A20,VALUED_1:def 5
.= f1.p - s*f2.p + s*f2.p - f1.p by A20,FUNCOP_1:7
.= 0;
A23: g in [.p,g.] by A1,XXREAL_1:1;
then g in dom f3 /\ dom f4 by A3,A16,A13,XBOOLE_0:def 4;
then
A24: g in dom f5 by VALUED_1:def 1;
then g in dom f5 /\ dom f1 by A2,A23,XBOOLE_0:def 4;
then g in dom f by VALUED_1:12;
then
A25: f.g = f5.g - f1.g by VALUED_1:13
.= f3.g + f4.g - f1.g by A24,VALUED_1:def 1
.= f3.g + s*f2.g - f1.g by A3,A13,A23,VALUED_1:def 5
.= f1.p - s*f2.p + s*f2.g - f1.g by A23,FUNCOP_1:7
.= -f1.g+(f1.p-(-(f1.g-f1.p))/(f2.g-f2.p)*(f2.g-f2.p))
.= -f1.g+(f1.p-(f1.p-f1.g)) by A11,XCMPLX_1:87
.= f.p by A22;
Z c= dom f1 by A2,A8;
then Z c= dom f5 /\ dom f1 by A15,XBOOLE_1:19;
then
A26: Z c= dom f by VALUED_1:12;
dom f4 = dom f2 by VALUED_1:def 5;
then
A27: [.p,g.] c= dom f3 /\ dom f4 by A3,A16,XBOOLE_1:19;
then [.p,g.] c= dom f5 by VALUED_1:def 1;
then
A28: [.p,g.] c= dom f5 /\ dom f1 by A2,XBOOLE_1:19;
f4|[.p,g.] is continuous by A3,A6,FCONT_1:20;
then f5|[.p,g.] is continuous by A17,A27,FCONT_1:18;
then
A29: f|[.p,g.] is continuous by A4,A28,FCONT_1:18;
A30: f4 is_differentiable_on Z by A7,A14,FDIFF_1:20;
then
A31: f5 is_differentiable_on Z by A19,A15,FDIFF_1:18;
[.p,g.] c= dom f by A28,VALUED_1:12;
then consider x0 such that
A32: x0 in ].p,g.[ and
A33: diff(f,x0)=0 by A1,A5,A29,A31,A26,A25,Th1,FDIFF_1:19;
take x0;
f is_differentiable_on Z by A5,A31,A26,FDIFF_1:19;
then diff(f,x0) = (f`|Z).x0 by A32,FDIFF_1:def 7
.= diff(f5,x0) - diff(f1,x0) by A5,A31,A26,A32,FDIFF_1:19
.= (f5`|Z).x0 - diff(f1,x0) by A31,A32,FDIFF_1:def 7
.= diff(f3,x0) + diff(f4,x0) - diff(f1,x0) by A19,A30,A15,A32,
FDIFF_1:18
.= (f3`|Z).x0 + diff(f4,x0) - diff(f1,x0) by A19,A32,FDIFF_1:def 7
.= 0 + diff(f4,x0) - diff(f1,x0) by A18,A12,A32,FDIFF_1:22
.= (f4`|Z).x0 - diff(f1,x0) by A30,A32,FDIFF_1:def 7
.= s*diff(f2,x0) - diff(f1,x0) by A7,A14,A32,FDIFF_1:20;
then
(diff(f2,x0)*(f1.g-f1.p))/(f2.g-f2.p)*(f2.g-f2.p) = diff(f1,x0)*(f2
.g-f2.p) by A33,XCMPLX_1:15;
hence x0 in ].p,g.[ & (f1.g-f1.p)*diff(f2,x0) = (f2.g-f2.p)*diff(f1,x0)
by A11,A32,XCMPLX_1:87;
end;
end;
hence thesis;
end;
::$N Cauchy Theorem
theorem
for x,t st 00) ex s st 0~~0;
consider x0 such that
A7: x0 in ].x,x+t.[ and
A8: (f1.(x+t)-f1.x)*diff(f2,x0)=(f2.(x+t)-f2.x)*diff(f1,x0) by A1,A2,A3,A4,A5
,Th5,XREAL_1:29;
diff(f2,x0)*((f1.(x+t)-f1.x)/diff(f2, x0))= (f2.(x+t)-f2.x)*diff(f1,x0)
/diff(f2,x0) by A8,XCMPLX_1:74;
then
(f1.(x+t)-f1.x)/(f2.(x+t)-f2.x) = (f2.(x+t)-f2.x)* (diff(f1,x0)/diff(f2
,x0))/(f2.(x+t)-f2.x) by A6,A7,XCMPLX_1:87;
then
A9: (f1.(x+t)-f1.x)/(f2.(x+t)-f2.x)=((diff(f1,x0)/diff(f2,x0))/(f2.(x+t) -
f2.x))* (f2.(x+t)-f2.x);
take s = (x0-x)/t;
x0 in {r: xf2.(x+t)-f2.x by A1,A3,A5,A6,Th1,XREAL_1:29;
hence thesis by A9,A11,XCMPLX_1:87;
end;
theorem Th7:
for p,g for f st ].p,g.[ c= dom f & f is_differentiable_on ].p,g
.[ & (for x st x in ].p,g.[ holds diff(f,x) = 0) holds f|].p,g.[ is constant
proof
let p,g;
let f such that
A1: ].p,g.[ c= dom f and
A2: f is_differentiable_on ].p,g.[ and
A3: for x st x in ].p,g.[ holds diff(f,x) = 0;
now
let x1,x2 be Element of REAL;
assume x1 in ].p,g.[ /\ dom f & x2 in ].p,g.[ /\ dom f;
then
A4: x1 in ].p,g.[ & x2 in ].p,g.[ by XBOOLE_0:def 4;
now
per cases;
suppose
x1=x2;
hence f.x1=f.x2;
end;
suppose
A5: not x1=x2;
now
per cases by A5,XXREAL_0:1;
suppose
A6: x1x2-x1;
then
A7: 0<>(x2-x1)" by XCMPLX_1:202;
reconsider Z=].x1,x2.[ as open Subset of REAL;
A8: [.x1,x2.] c= ].p,g.[ by A4,XXREAL_2:def 12;
f|].p,g.[ is continuous by A2,FDIFF_1:25;
then
A9: f|[.x1,x2.] is continuous by A8,FCONT_1:16;
A10: Z c= [.x1,x2.] by XXREAL_1:25;
then f is_differentiable_on Z by A2,A8,FDIFF_1:26,XBOOLE_1:1;
then
A11: ex x0 st x0 in ].x1,x2.[ & diff(f,x0) = (f.x2-f.x1)/(x2- x1)
by A1,A6,A8,A9,Th3,XBOOLE_1:1;
Z c= ].p,g.[ by A8,A10;
then 0 = (f.x2-f.x1) by A3,A7,A11,XCMPLX_1:6;
hence f.x1=f.x2;
end;
suppose
A12: x2x1-x2;
then
A13: 0<>(x1-x2)" by XCMPLX_1:202;
reconsider Z=].x2,x1.[ as open Subset of REAL;
A14: [.x2,x1.] c= ].p,g.[ by A4,XXREAL_2:def 12;
f|].p,g.[ is continuous by A2,FDIFF_1:25;
then
A15: f|[.x2,x1.] is continuous by A14,FCONT_1:16;
A16: Z c= [.x2,x1.] by XXREAL_1:25;
then f is_differentiable_on Z by A2,A14,FDIFF_1:26,XBOOLE_1:1;
then
A17: ex x0 st x0 in ].x2,x1.[ & diff(f,x0) = (f.x1-f.x2)/(x1- x2)
by A1,A12,A14,A15,Th3,XBOOLE_1:1;
Z c= ].p,g.[ by A14,A16;
then 0 = (f.x1-f.x2) by A3,A13,A17,XCMPLX_1:6;
hence f.x1=f.x2;
end;
end;
hence f.x1=f.x2;
end;
end;
hence f.x1=f.x2;
end;
hence thesis by PARTFUN2:58;
end;
theorem
for 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)|].p,g.[ is constant & ex r st for x st x in ].p,g.[ holds
f1.x = f2.x+r
proof
let p,g;
let f1,f2 such that
A1: f1 is_differentiable_on ].p,g.[ & f2 is_differentiable_on ].p,g.[ and
A2: for x st x in ].p,g.[ holds diff(f1,x) = diff(f2,x);
reconsider Z=].p,g.[ as open Subset of REAL;
].p,g.[ c= dom f1 & ].p,g.[ c= dom f2 by A1,FDIFF_1:def 6;
then ].p,g.[ c= dom f1 /\ dom f2 by XBOOLE_1:19;
then
A3: ].p,g.[ c= dom (f1-f2) by VALUED_1:12;
then
A4: f1-f2 is_differentiable_on Z by A1,FDIFF_1:19;
now
let x;
assume
A5: x in ].p,g.[;
hence diff(f1-f2,x) = ((f1-f2)`|Z).x by A4,FDIFF_1:def 7
.= diff(f1,x)-diff(f2,x) by A1,A3,A5,FDIFF_1:19
.= diff(f1,x)-diff(f1,x) by A2,A5
.= 0;
end;
hence (f1-f2)|].p,g.[ is constant by A1,A3,Th7,FDIFF_1:19;
then consider r being Element of REAL such that
A6: for x being Element of REAL
st x in ].p,g.[ /\ dom(f1-f2) holds (f1-f2).x = r
by PARTFUN2:57;
take r;
let x;
assume
A7: x in ].p,g.[;
then x in ].p,g.[ /\ dom(f1-f2) by A3,XBOOLE_1:28;
then r = (f1-f2).x by A6
.= f1.x - f2.x by A3,A7,VALUED_1:13;
hence thesis;
end;
theorem
for p,g for f st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & (
for x st x in ].p,g.[ holds 0x2-x1 by A5;
reconsider Z=].x1,x2.[ as open Subset of REAL;
x1 in ].p,g.[ & x2 in ].p,g.[ by A4,XBOOLE_0:def 4;
then
A7: [.x1,x2.] c= ].p,g.[ by XXREAL_2:def 12;
f|].p,g.[ is continuous by A2,FDIFF_1:25;
then
A8: f|[.x1,x2.] is continuous by A7,FCONT_1:16;
A9: Z c= [.x1,x2.] by XXREAL_1:25;
then
A10: Z c= ].p,g.[ by A7;
f is_differentiable_on Z by A2,A7,A9,FDIFF_1:26,XBOOLE_1:1;
then
ex x0 st x0 in ].x1,x2.[ & diff(f,x0) = (f.x2-f.x1)/(x2- x1) by A1,A5,A7,A8
,Th3,XBOOLE_1:1;
then
A11: 0<=(f.x2-f.x1)/(x2-x1) by A3,A10;
0<=x2-x1 by A5,XREAL_1:50;
then 0*(x2-x1)<=(f.x2-f.x1)/(x2-x1)*(x2-x1) by A11;
then 0<=f.x2-f.x1 by A6,XCMPLX_1:87;
then f.x1+0<=f.x2 by XREAL_1:19;
hence f.x1<=f.x2;
end;
hence thesis by RFUNCT_2:22;
end;
theorem
for p,g for f st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & (
for x st x in ].p,g.[ holds diff(f,x)<=0) holds f|].p,g.[ is non-increasing
proof
let p,g;
let f such that
A1: ].p,g.[ c= dom f and
A2: f is_differentiable_on ].p,g.[ and
A3: for x st x in ].p,g.[ holds diff(f,x)<=0;
now
let x1,x2 such that
A4: x1 in ].p,g.[ /\ dom f & x2 in ].p,g.[ /\ dom f and
A5: x1x2-x1 by A5;
Z c= ].p,g.[ by A7,A9;
then (f.x2-f.x1)/(x2-x1)*(x2-x1)<=0*(x2-x1) by A3,A6,A10,XREAL_1:64;
then f.x2-f.x1<=0 by A11,XCMPLX_1:87;
then f.x2<=f.x1+0 by XREAL_1:20;
hence f.x2<=f.x1;
end;
hence thesis by RFUNCT_2:23;
end;
~~