:: Riemann Integral of Functions from $\mathbbbR$ into Real {B}anach Space
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received June 18, 2013
:: Copyright (c) 2013-2026 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 PRE_TOPC, NORMSP_1, FUNCT_1, ARYTM_1, NAT_1, SUBSET_1, NUMBERS,
CARD_1, XXREAL_0, REAL_1, ARYTM_3, RELAT_1, ORDINAL2, SEQ_1, SEQ_2,
LOPBAN_1, STRUCT_0, COMPLEX1, VALUED_1, SUPINF_2, XBOOLE_0, ABIAN,
INTEGRA1, INTEGRA2, FINSEQ_1, TARSKI, INTEGRA5, INTEGR15, MEASURE7,
CARD_3, XXREAL_1, PARTFUN1, SEQ_4, FUNCT_2, RCOMP_1, VALUED_0, XXREAL_2,
FCONT_1, MEASURE5, FUNCOP_1, FINSEQ_2, FUNCT_3, ORDINAL4, FCONT_2,
ZFMISC_1, INTEGR20;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1,
VALUED_0, COMPLEX1, XXREAL_2, FINSEQ_1, FINSEQ_2, BINOP_1, VALUED_1,
SEQ_1, SEQ_2, RFUNCT_1, RVSUM_1, SEQ_4, RCOMP_1, ABIAN, MEASURE5,
INTEGRA1, INTEGRA2, INTEGRA3, INTEGRA5, STRUCT_0, PRE_TOPC, RLVECT_1,
VFUNCT_1, NORMSP_0, NORMSP_1, LOPBAN_1, BINOM, INTEGR18, NFCONT_3;
constructors ABIAN, SEQ_2, RSSPACE3, RELSET_1, SEQ_4, VFUNCT_1, NEWTON,
INTEGRA3, INTEGR18, RVSUM_1, COMSEQ_2, BINOM, ORDEQ_01, RFUNCT_1,
NDIFF_5;
registrations STRUCT_0, NAT_1, VALUED_1, NORMSP_0, NUMBERS, XBOOLE_0, FUNCT_2,
XREAL_0, MEMBERED, RELAT_1, RELSET_1, INTEGRA1, ORDINAL1, NFCONT_3,
XXREAL_2, RLVECT_1, VALUED_0, FINSEQ_1, FINSET_1, MEASURE5, ABIAN,
SEQM_3, INT_1, CARD_1, SUBSET_1, FINSEQ_2;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities RCOMP_1, ALGSTR_0, NORMSP_0, FINSEQ_1, INTEGRA1, INTEGRA3,
INTEGR18, XCMPLX_0, BINOP_1;
expansions RCOMP_1, ABIAN, FINSEQ_1, NFCONT_3, INTEGR18, NORMSP_1, TARSKI;
theorems ABSVALUE, RLVECT_1, XCMPLX_1, SEQ_2, PARTFUN1, FUNCT_1, NAT_1,
FUNCT_2, NORMSP_1, XREAL_1, RSSPACE3, LOPBAN_1, XXREAL_0, XREAL_0,
ORDINAL1, RELAT_1, SEQ_4, VFUNCT_1, XBOOLE_0, FUNCOP_1, FINSEQ_1,
XXREAL_1, RVSUM_1, VALUED_1, XBOOLE_1, INTEGRA4, INTEGRA3, INTEGRA1,
INT_1, INTEGR18, FINSEQ_4, FINSEQ_2, FINSEQ_3, FINSEQ_5, MEASURE5,
VALUED_0, XXREAL_2, ZFMISC_1, RFUNCT_2, BINOM, TARSKI;
schemes NAT_1, FUNCT_2, FINSEQ_1, BINOP_1, SUBSET_1;
begin :: Some Properties of Continuous Functions
reserve s1,s2,q1 for Real_Sequence;
definition
let X be RealNormSpace;
let f be PartFunc of REAL,the carrier of X;
attr f is uniformly_continuous means
for r be Real st 0<r ex s be Real st 0<s &
for x1,x2 be Real st x1 in dom f & x2 in dom f & |. x1-x2 .| < s
holds ||. f/.x1-f/.x2 .|| < r;
end;
theorem Th1:
for X be set, Y be RealNormSpace,
f be PartFunc of REAL,the carrier of Y
holds
f|X is uniformly_continuous iff
for r be Real st 0<r
ex s be Real st 0<s &
for x1,x2 be Real st x1 in dom(f|X) & x2 in dom(f|X) & |. x1-x2 .| < s
holds ||. f/.x1-f/.x2 .|| < r
proof
let X be set, Y be RealNormSpace,
f be PartFunc of REAL,the carrier of Y;
thus f|X is uniformly_continuous implies
for r be Real st 0<r ex s be Real st 0<s &
for x1,x2 be Real st x1 in dom(f|X) &
x2 in dom(f|X) & |. x1-x2 .| < s holds ||. f/.x1-f/.x2 .|| < r
proof
assume
A1: f|X is uniformly_continuous;
let r be Real;
assume 0<r;
then consider s be Real such that
A2: 0<s and
A3: for x1,x2 be Real st x1 in dom(f|X) & x2 in dom (f|X) & |. x1-x2 .| < s
holds ||. (f|X)/.x1 - (f|X)/.x2 .|| < r by A1;
take s;
thus 0<s by A2;
let x1,x2 be Real;
assume A4: x1 in dom(f|X) & x2 in dom(f|X); then
(f|X)/.x1 = f/.x1 & (f|X)/.x2 = f/.x2 by PARTFUN1:80;
hence thesis by A3,A4;
end;
assume
A5: for r be Real st 0<r ex s be Real st 0<s
& for x1,x2 be Real st x1 in dom(f|X) & x2 in dom(f|X)
& |. x1-x2 .| < s holds ||. f/.x1-f/.x2 .|| < r;
let r be Real;
assume 0<r;
then consider s be Real such that
A6: 0<s and
A7: for x1,x2 be Real st x1 in dom(f|X) & x2 in dom(f|X) &
|. x1-x2 .| < s holds ||. f/.x1-f/.x2 .|| < r by A5;
take s;
thus 0<s by A6;
let x1,x2 be Real;
assume A8: x1 in dom(f|X) & x2 in dom(f|X); then
(f|X)/.x1 = f/.x1 & (f|X)/.x2 = f/.x2 by PARTFUN1:80;
hence thesis by A7,A8;
end;
theorem
for X,X1 be set,
Y be RealNormSpace,
f be PartFunc of REAL,the carrier of Y
holds
f|X is uniformly_continuous & X1 c= X implies f|X1 is uniformly_continuous
proof
let X,X1 be set,
Y be RealNormSpace,
f be PartFunc of REAL,the carrier of Y;
assume that
A1: f|X is uniformly_continuous and
A2: X1 c= X;
now
let r be Real;
assume 0<r;
then consider s be Real such that
A3: 0<s and
A4: for x1,x2 be Real st x1 in dom(f|X) & x2 in dom(f|X) & |. x1-x2 .|<s holds
||. f/.x1-f/.x2 .||<r by A1,Th1;
take s;
thus 0<s by A3;
let x1,x2 be Real;
assume that
A5: x1 in dom(f|X1) & x2 in dom(f|X1) & |. x1-x2 .|<s;
f|X1 c= f|X by A2,RELAT_1:75;
then dom(f|X1) c= dom(f|X) by RELAT_1:11;
hence ||. f/.x1-f/.x2 .||<r by A4,A5;
end;
hence thesis by Th1;
end;
theorem Th3:
for X be RealNormSpace,
f be PartFunc of REAL,the carrier of X,
Z be Subset of REAL
st Z c= dom f & Z is compact &
f|Z is continuous holds f|Z is uniformly_continuous
proof
let X be RealNormSpace,
f be PartFunc of REAL,the carrier of X,
Z be Subset of REAL;
assume that
A1: Z c= dom f and
A2: Z is compact and
A3: f|Z is continuous;
assume not thesis; then
consider r be Real such that
A4: 0<r and
A5: for s be Real st 0<s ex x1,x2 be Real st
x1 in dom(f|Z) & x2 in dom(f|Z) &
|. x1-x2 .| < s & not||. f/.x1-f/.x2 .|| < r by Th1;
defpred P[Element of NAT,Real]
means $2 in Z & ex x2 being Element of REAL st x2 in Z &
|. $2-x2 .| <1/($1+1) & not ||. f/.($2)-f/.x2 .|| < r;
A6:now let n be Element of NAT;
consider x1 be Real such that
A7: ex x2 be Real st x1 in dom(f|Z) & x2 in dom(f|Z) & |. x1-x2 .| < 1/(n+1)
& not ||. f/.x1-f/.x2 .|| < r by A5;
reconsider x1 as Element of REAL by XREAL_0:def 1;
take x1;
dom(f|Z) = Z by A1,RELAT_1:62;
hence P[n,x1] by A7;
end;
consider s1 such that
A8: for n be Element of NAT holds P[n,s1.n] from FUNCT_2:sch 3(A6);
A9:now let x be object;
assume x in rng s1;
then ex n be Element of NAT st x=s1.n by FUNCT_2:113;
hence x in Z by A8;
end;
then rng s1 c= Z;
then consider q1 such that
A10: q1 is subsequence of s1 & q1 is convergent & lim q1 in Z by A2;
A11:
f|Z is_continuous_in (lim q1) by A3,A1,A10,RELAT_1:57;
rng q1 c= rng s1 by A10,VALUED_0:21; then
rng q1 c= Z & rng q1 c= dom f by A1,A9; then
rng q1 c= dom f /\ Z by XBOOLE_1:19; then
A12:
rng q1 c= dom (f|Z) by RELAT_1:61; then
A13:
(f|Z)/.(lim q1)=lim((f|Z)/*q1) & (f|Z)/*q1 is convergent by A10,A11;
defpred P[Element of NAT,Real] means $2 in Z &
|.s1.$1-$2.| < 1/($1+1) & not ||. f/.(s1.$1)-f/.$2 .|| < r;
A14:
for n be Element of NAT ex x2 being Element of REAL st P[n,x2] by A8;
consider s2 such that
A15:for n be Element of NAT holds P[n,s2.n] from FUNCT_2:sch 3(A14);
A16:
now let x be object;
assume x in rng s2;
then ex n be Element of NAT st x=s2.n by FUNCT_2:113;
hence x in Z by A15;
end;
consider Ns1 be increasing sequence of NAT such that
A17: q1=s1*Ns1 by A10,VALUED_0:def 17;
set q2 = q1 - (s1-s2)*Ns1;
now
let n be Element of NAT;
thus q2.n = (s1*Ns1).n - ((s1-s2)*Ns1).n by A17,RFUNCT_2:1
.= s1.(Ns1.n) - ((s1-s2)*Ns1).n by FUNCT_2:15
.= s1.(Ns1.n) - (s1-s2).(Ns1.n) by FUNCT_2:15
.= s1.(Ns1.n) - (s1.(Ns1.n)-s2.(Ns1.n)) by RFUNCT_2:1
.= (s2*Ns1).n by FUNCT_2:15;
end; then
A18:
q2 = s2*Ns1 & q2 is subsequence of s2 by FUNCT_2:63; then
rng q2 c= rng s2 by VALUED_0:21; then
rng q2 c= Z & rng q2 c= dom f by A1,A16; then
rng q2 c= dom f /\ Z by XBOOLE_1:19; then
A19:
rng q2 c= dom (f|Z) by RELAT_1:61;
A20:
now let p be Real;
assume A21: 0<p;
consider k be Nat such that
A22: p" < k by SEQ_4:3;
take k;
let m be Nat;
A23:m in NAT by ORDINAL1:def 12;
assume k <= m;
then k+1 <= m+1 by XREAL_1:6;
then 1/(m+1) <= 1/(k+1) by XREAL_1:118;
then
A24: |. s1.m-s2.m .| < 1/(k+1) by A15,XXREAL_0:2,A23;
k < k+1 by NAT_1:13;
then p" < k+1 by A22,XXREAL_0:2; then
A25:1/(k+1) < 1/p" by A21,XREAL_1:76;
|. (s1-s2).m - 0 .| = |. s1.m-s2.m .| by RFUNCT_2:1;
hence |. (s1-s2).m - 0 .| < p by A25,A24,XXREAL_0:2;
end;
then
A26: s1-s2 is convergent by SEQ_2:def 6;
A27: (s1-s2)*Ns1 is convergent by A20,SEQ_2:def 6,SEQ_4:16; then
A28: q2 is convergent by A10,SEQ_2:11;
lim (s1-s2) = 0 by A20,A26,SEQ_2:def 7;
then lim ((s1-s2)*Ns1) = 0 by A20,SEQ_2:def 6,SEQ_4:17;
then lim q2 = lim q1 - 0 by A10,A27,SEQ_2:12; then
A29: (f|Z)/*q2 is convergent & (f|Z)/.(lim q1) = lim ((f|Z)/*q2)
by A11,A28,A19; then
A30: (f|Z)/*q1 - (f|Z)/*q2 is convergent by A13,NORMSP_1:20;
lim ((f|Z)/*q1 - (f|Z)/*q2)
= (f|Z)/.(lim q1) - (f|Z)/.(lim q1) by A13,A29,NORMSP_1:26; then
A31: lim ((f|Z)/*q1 - (f|Z)/*q2) = 0.X by RLVECT_1:15;
now let n be Nat;
consider k be Nat such that
A32: for m being Nat st k<=m holds ||. ((f|Z)/*q1 - (f|Z)/*q2).m- 0.X .||<r
by A4,A30,A31,NORMSP_1:def 7;
A33:q1.k in dom(f|Z) & q2.k in dom(f|Z) by A12,A19,VALUED_0:28;
A34:k in NAT by ORDINAL1:def 12;
A35: ||. ((f|Z)/*q1 - (f|Z)/*q2).k - 0.X .||
= ||. ((f|Z)/*q1).k - ((f|Z)/*q2).k .|| by NORMSP_1:def 3;
((f|Z)/*q1).k = (f|Z)/.(q1.k) & ((f|Z)/*q2).k = (f|Z)/.(q2.k)
by A12,A19,FUNCT_2:109,A34; then
((f|Z)/*q1).k = f/.(q1.k) & ((f|Z)/*q2).k = f/.(q2.k)
by A33,PARTFUN1:80; then
||. ((f|Z)/*q1).k - ((f|Z)/*q2).k .||
= ||. f/.(s1.(Ns1.k)) - f/.((s2*Ns1).k) .||
by A17,A18,FUNCT_2:15,ORDINAL1:def 12
.= ||. f/.(s1.(Ns1.k)) - f/.(s2.(Ns1.k)) .||
by FUNCT_2:15,ORDINAL1:def 12;
hence contradiction by A15,A32,A35;
end;
hence contradiction;
end;
begin :: Some Properties of Sequences
theorem Th4:
for X be RealNormSpace, n,m be Nat, a be Function of [:Seg n,Seg m:],X
for p,q be FinSequence of X st
( dom p = Seg n
& for i be Nat st i in dom p holds
ex r be FinSequence of X st
(dom r = Seg m & p.i = Sum r
& for j be Nat st j in dom r holds r.j=a.(i,j) ) )
& ( dom q = Seg m
& for j be Nat st j in dom q holds
ex s be FinSequence of X st
(dom s = Seg n & q.j = Sum s
& for i be Nat st i in dom s holds s.i=a.(i,j) ) )
holds Sum p = Sum q
proof
let X be RealNormSpace;
defpred P[Nat] means for m be Nat, a be Function of [:Seg $1, Seg m:],X
for p,q be FinSequence of X st (dom p=Seg $1 & for i be Nat st i in dom p
holds ex r be FinSequence of X st (dom(r) = Seg m & p.i=Sum(r) & for j be
Nat st j in dom(r) holds r.j=a.( i,j ) ))
& ( dom q=Seg m & for j be Nat st j in
dom q holds ex s be FinSequence of X st (dom(s) = Seg $1 & q.j=Sum(s) & for
i be Nat st i in dom(s) holds s.i=a.( i,j ))) holds Sum(p)=Sum(q);
A1:for n be Nat st P[n] holds P[n+1]
proof
let n be Nat such that A2: P[n];
reconsider n as Element of NAT by ORDINAL1:def 12;
A3:Seg n c= Seg (n+1) by FINSEQ_1:5,NAT_1:11;
now
let m be Nat, a be Function of [:Seg (n+1),Seg m:],X;
let p,q be FinSequence of X such that
A4: dom p=Seg (n+1)
& for i be Nat st i in dom p holds
ex r be FinSequence of X st
( dom r = Seg m & p.i=Sum r
& for j be Nat st j in dom r holds r.j=a.(i,j) )
and
A5: dom q=Seg m
& for j be Nat st j in dom q holds
ex s be FinSequence of X st
( dom s = Seg (n+1) & q.j=Sum s
& for i be Nat st i in dom s holds s.i=a.(i,j) );
A6: len p=n+1 by A4,FINSEQ_1:def 3;
set a0=a| [:Seg n, Seg m:];
[:Seg n,Seg m:] c= [:Seg (n+1),Seg m:] by A3,ZFMISC_1:95;
then reconsider a0 as Function of [:Seg n,Seg m:],X by FUNCT_2:32;
A7: dom a0 = [:Seg n,Seg m:] by FUNCT_2:def 1;
deffunc F(Nat)=a.( [n+1,$1] );
reconsider p0= p|(Seg n) as FinSequence of X by FINSEQ_1:18;
A8: dom p0=Seg n by A4,A3,RELAT_1:62; then
A9: len p0 = n by FINSEQ_1:def 3;
A10: now let i be Nat;
assume A11: i in dom p0;
then consider r be FinSequence of X such that
A12: dom r = Seg m & p.i=Sum r
& for j be Nat st j in dom r holds r.j=a.(i,j) by A4,A8,FINSEQ_2:8;
take r;
thus dom r = Seg m & p0.i = Sum r by A11,A12,FUNCT_1:47;
thus for j be Nat st j in dom r holds r.j=a0.(i,j)
proof
let j be Nat;
assume A13: j in dom r;
then r.j=a.(i,j) by A12;
hence r.j = a0.(i,j) by A8,A11,A12,A13,ZFMISC_1:87,A7,FUNCT_1:47;
end;
end;
reconsider m as Element of NAT by ORDINAL1:def 12;
consider an be FinSequence such that
A14: len an=m & for j be Nat st j in dom an holds an.j=F(j)
from FINSEQ_1:sch 2;
A15: dom an=Seg m by A14,FINSEQ_1:def 3;
now
let i be Nat;
assume A16:i in dom an;
n+1 in Seg(n+1) by FINSEQ_1:4; then
[n+1,i] in [:Seg (n+1),Seg m:] by A16,A15,ZFMISC_1:87; then
a.(n+1,i) in the carrier of X by FUNCT_2:5;
hence an.i in the carrier of X by A16,A14;
end; then
reconsider an as FinSequence of X by FINSEQ_2:12;
A17: Sum an = p.(n+1)
proof
consider r be FinSequence of X such that
A18: dom r = Seg m & p.(n+1)=Sum r
& for j be Nat st j in dom r holds r.j=a.(n+1,j) by A4,FINSEQ_1:4;
now let j be Nat;
assume A19: j in dom r; then
r.j=a.(n+1,j) by A18;
hence r.j=an.j by A14,A15,A18,A19;
end;
hence thesis by A14,FINSEQ_1:def 3,A18,FINSEQ_1:13;
end;
set q0 = q-an;
A20: dom q0 = dom q /\ dom an by VFUNCT_1:def 2;
then reconsider q0=q-an as FinSequence by A15,A5,FINSEQ_1:def 2;
for i be Nat st i in dom q0 holds q0.i in the carrier of X
proof
let i be Nat;
assume i in dom q0; then
q0.i = (q-an)/.i by PARTFUN1:def 6;
hence thesis;
end;
then reconsider q0 as FinSequence of the carrier of X by FINSEQ_2:12;
A21: len q0 = m by A5,A15,A20,FINSEQ_1:def 3;
A22: now
let j be Nat such that
A23: j in dom q0;
consider s be FinSequence of X such that
A24: dom s = Seg(n+1) & q.j=Sum s
& for i be Nat st i in dom s holds s.i=a.(i,j) by A5,A15,A20,A23;
A25: s.(n+1)=a.(n+1,j) by A24,FINSEQ_1:4;
reconsider sn=s|Seg n as FinSequence of X by FINSEQ_1:18;
take sn;
A26: len s = n+1 by A24,FINSEQ_1:def 3;
an/.j = an.j by A23,A15,A5,A20,PARTFUN1:def 6; then
an/.j = s.(n+1) by A25,A14,A15,A5,A20,A23; then
A27: an/.j = s.(len s) by A24,FINSEQ_1:def 3;
thus
A28: dom sn = Seg n by A24,A3,RELAT_1:62; then
A29: len s = len sn + 1 by A26,FINSEQ_1:def 3;
q/.j = Sum s by A24,A23,A5,A15,A20,PARTFUN1:def 6; then
q/.j - an/.j = Sum sn + an/.j - an/.j by A29,A28,RLVECT_1:38,A27
.= Sum sn + (an/.j - an/.j) by RLVECT_1:def 3; then
q/.j - an/.j = Sum sn + 0.X by RLVECT_1:15;
then q0/.j = Sum sn by A23,VFUNCT_1:def 2;
hence q0.j = Sum sn by A23,PARTFUN1:def 6;
thus for i be Nat st i in dom sn holds sn.i=a0.(i,j)
proof
let i be Nat such that
A30: i in dom sn;
sn.i=s.i by A30,FUNCT_1:47; then
sn.i=a.(i,j) by A24,A28,A30,A3;
hence sn.i=a0.(i,j)
by A5,A15,A20,A23,A28,A30,ZFMISC_1:87,A7,FUNCT_1:47;
end;
end;
for i be Nat st 1<=i & i <= len q holds q/.i = (q0/.i) + (an/.i)
proof
let i be Nat;
assume 1<=i & i <= len q;
then i in dom q by FINSEQ_3:25; then
(q0/.i) + (an/.i) = (q/.i-an/.i) + (an/.i) by A5,A15,A20,VFUNCT_1:def 2
.= q/.i - (an/.i - an/.i) by RLVECT_1:29; then
(q0/.i) + (an/.i) = q/.i - 0.X by RLVECT_1:15;
hence thesis;
end;
then
A31: q0+an=q by A5,A15,A20,BINOM:def 1;
Sum p = Sum p0 + Sum an by A8,A6,A9,RLVECT_1:38,A17; then
Sum p = Sum q0 + Sum an by A2,A10,A8,A5,A15,A20,A22;
hence Sum p = Sum q by A31,INTEGR18:1,A14,A21;
end;
hence thesis;
end;
now let m be Nat, a be Function of [:Seg 0,Seg m:],X;
let p,q be FinSequence of X such that
A32: dom p=Seg 0 and
for i be Nat st i in dom p holds
ex r be FinSequence of X st (dom r = Seg m & p.i=Sum r
& for j be Nat st j in dom r holds r.j=a.(i,j) ) and
dom q=Seg m and
A33: for j be Nat st j in dom q holds
ex s be FinSequence of X st (dom s = Seg 0 & q.j=Sum s
& for i be Nat st i in dom s holds s.i=a.(i,j) );
A34:
now let z be object;
assume
A35: z in dom q;
then reconsider j=z as Nat;
consider s be FinSequence of X such that
A36: dom s = Seg 0 & q.j=Sum s &
for i be Nat st i in dom s holds s.i=a.(i,j) by A33,A35;
s = <*>the carrier of X by A36;
hence q.z=0.X by A36,RLVECT_1:43;
end;
A37: p = <*>the carrier of X by A32;
A38:len q = len q;
now
let k be Nat, v be Element of X;
assume A39: k in dom q & v = q.k; then
q.k = 0.X by A34;
hence q.k = -v by A39;
end; then
Sum q = - Sum q by A38,RLVECT_1:40; then
Sum q = 0.X by RLVECT_1:19;
hence Sum p = Sum q by RLVECT_1:43,A37;
end;
then
A40: P[0];
thus for n be Nat holds P[n] from NAT_1:sch 2(A40,A1);
end;
definition
let A be Subset of REAL;
func xvol A -> Real equals :Def2:
0 if A is empty otherwise vol A;
correctness;
end;
reserve n for Element of NAT;
reserve a,b for Real;
Lm1: for X,Y,Z be non empty set, f be PartFunc of X,Y
st Z c= dom f holds f|Z is Function of Z,Y
proof
let X,Y,Z be non empty set, f be PartFunc of X,Y;
rng f c= Y; then
f is Function of dom f,Y by FUNCT_2:2;
hence thesis by FUNCT_2:32;
end;
theorem Th5:
for A be real-bounded Subset of REAL holds 0 <= xvol A
proof
let A be real-bounded Subset of REAL;
per cases;
suppose A <> {};
then 0<= vol A by INTEGRA1:9;
hence 0 <= xvol A by Def2;
end;
suppose A = {};
hence 0 <= xvol A by Def2;
end;
end;
theorem Th6:
for A be non empty closed_interval Subset of REAL,
D be Division of A, q be FinSequence of REAL
st dom q = Seg len D
& for i be Nat st i in Seg len D holds q.i = vol divset(D,i)
holds Sum q = vol A
proof
let A be non empty closed_interval Subset of REAL,
D be Division of A, q be FinSequence of REAL;
assume
A1: dom q = Seg len D
& for i be Nat st i in Seg len D holds q.i = vol divset(D,i);
set p = lower_volume(chi(A,A),D);
dom q = Seg len D by A1
.= Seg len p by INTEGRA1:def 7; then
A2:dom q = dom p by FINSEQ_1:def 3;
for k be Nat st k in dom q holds q.k = p.k
proof
let k be Nat;
assume A3: k in dom q; then
A4: q.k = vol divset(D,k) by A1;
k in dom D by A3,A1,FINSEQ_1:def 3;
hence thesis by A4,INTEGRA1:19;
end;
then q = lower_volume ((chi (A,A)),D) by A2,FINSEQ_1:13;
hence thesis by INTEGRA1:23;
end;
theorem Th7:
for Y be RealNormSpace, E be Point of Y, q be FinSequence of REAL,
S be FinSequence of Y
st len S = len q
& for i be Nat st i in dom S holds ex r be Real st r = q.i & S.i= r * E
holds Sum S = (Sum q)*E
proof
let Y be RealNormSpace, E be Point of Y;
defpred P[Nat] means
for q be FinSequence of REAL, S be FinSequence of Y st
$1 = len S & len S = len q &
for i be Nat st i in dom S holds ex r be Real st r = q.i & S.i= r * E
holds Sum S = (Sum q)*E;
A1:P[0]
proof
let q be FinSequence of REAL, S be FinSequence of Y;
assume 0 = len S & len S = len q &
for i be Nat st i in dom S holds
ex r be Real st r = q.i & S.i= r * E; then
A2: <*>(the carrier of Y) = S & <*> REAL = q; then
(Sum q)*E = 0.Y by RLVECT_1:10,RVSUM_1:72;
hence thesis by A2,RLVECT_1:43;
end;
A3:now let i be Nat;
assume A4: P[i];
now let q be FinSequence of REAL, S be FinSequence of Y;
set S0=S|i, q0=q|i;
assume A5: i+1 = len S & len S = len q
& for i be Nat st i in dom S holds
ex r be Real st r = q.i & S.i= r * E;
A6: for k be Nat st k in dom S0 holds
ex r be Real st r = q0.k & S0.k= r * E
proof
let k be Nat;
assume k in dom S0; then
A7: k in Seg i & k in dom S by RELAT_1:57; then
consider r be Real such that
A8: r = q.k & S.k= r * E by A5;
take r;
thus thesis by A8,A7,FUNCT_1:49;
end;
dom S = Seg(i+1) by A5,FINSEQ_1:def 3; then
consider r be Real such that
A9: r = q.(i+1) & S.(i+1)= r * E by A5,FINSEQ_1:4;
A10: 1 <= i + 1 & i + 1 <= len q by A5,NAT_1:11;
q = (q|i)^<*q/.(i+1)*> by A5,FINSEQ_5:21; then
q = q0^<*q.(i+1)*> by A10,FINSEQ_4:15; then
(Sum q)*E = (Sum q0 + q.(i+1))*E by RVSUM_1:74; then
A11: (Sum q)*E = (Sum q0)*E + q.(i+1)*E by RLVECT_1:def 6;
A12: i = len S0 & i = len q0 by FINSEQ_1:59,A5,NAT_1:11;
reconsider v=S.(i+1) as Point of Y by A9;
S0 = S| dom S0 by FINSEQ_1:def 3,A12; then
Sum S = Sum S0 + v by A5,A12,RLVECT_1:38;
hence Sum S = (Sum q)*E by A9,A4,A6,A12,A11;
end;
hence P[i+1];
end;
for i being Nat holds P[i] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
theorem Th8:
for A being non empty closed_interval Subset of REAL,
D being Division of A,
B be non empty closed_interval Subset of REAL,
v be FinSequence of REAL
st B c= A & len D = len v &
for i be Nat st i in dom v
holds v.i = xvol (B /\ divset(D,i))
holds Sum v = vol B
proof
defpred P[Nat] means
for A being non empty closed_interval Subset of REAL,
D being Division of A,
B be non empty closed_interval Subset of REAL,
v be FinSequence of REAL
st $1 = len D & B c= A & len D = len v &
for k be Nat st k in dom v
holds v.k = xvol (B /\ divset(D,k)) holds Sum v = vol B;
A1:P[0];
A2:for i be Nat st P[i] holds P[i+1]
proof let i be Nat;
assume A3: P[i];
let A being non empty closed_interval Subset of REAL,
D being Division of A,
B be non empty closed_interval Subset of REAL,
v be FinSequence of REAL;
set D1=D|i, v1=v|i;
assume A4: i+1 = len D & B c= A & len D = len v &
for k be Nat st k in dom v holds v.k = xvol (B /\ divset(D,k));
A5: dom D = Seg(i+1) & dom D = dom v by A4,FINSEQ_1:def 3,FINSEQ_3:29; then
A6: v.(i+1) = xvol (B /\ divset(D,i+1)) by A4,FINSEQ_1:4;
A7: 1 <= i + 1 & i + 1 <= len v by A4,NAT_1:11;
v = (v|i)^<*v/.(i+1)*> by A4,FINSEQ_5:21; then
A8:v = v1^<*v.(i+1)*> by A7,FINSEQ_4:15;
A9: lower_bound A <= lower_bound B & upper_bound B <= upper_bound A
by A4,SEQ_4:47,48;
A10: rng D c= A by INTEGRA1:def 2;
A11:rng D1 c= rng D by RELAT_1:70;
A12:Seg i c= dom D by A5,FINSEQ_1:5,NAT_1:11;
A13: i = len D1 & i = len v1 by FINSEQ_1:59,A4,NAT_1:11; then
A14: dom v1 = Seg i by FINSEQ_1:def 3;
per cases;
suppose A15: i <> 0; then
A16: i in dom D by A12,FINSEQ_1:3; then
consider A1,A2 be non empty closed_interval Subset of REAL such that
A17: A1=[.lower_bound A, D.i .] & A2=[. D.i, upper_bound A.]
& A = A1 \/ A2 by INTEGRA1:32;
for y be object st y in rng D1 holds y in A1
proof
let y be object;
assume A18: y in rng D1; then
y in A by A11,A10; then
y in [.lower_bound A, upper_bound A.] by INTEGRA1:4; then
consider y1 be Real such that
A19: y=y1 & lower_bound A <= y1 & y1 <= upper_bound A;
consider x be object such that
A20: x in dom D1 & y1=D1.x by A18,A19,FUNCT_1:def 3;
reconsider x as Nat by A20;
A21: x in Seg i by A13,FINSEQ_1:def 3,A20; then
A22: x <= i by FINSEQ_1:1;
now assume x <> i; then
x < i by A22,XXREAL_0:1;
hence D.x <= D.i by A16,A12,A21,VALUED_0:def 13;
end; then
y1 <= D.i by A20,A21,FUNCT_1:49;
hence y in A1 by A19,A17;
end; then
A23: rng D1 c= A1;
A24: D1.i = D.i by A15,FINSEQ_1:3,FUNCT_1:49;
reconsider D1 as non empty increasing FinSequence of REAL
by A15;
A27: A1 = [. lower_bound A1, upper_bound A1 .] by INTEGRA1:4; then
D1.(len D1) = upper_bound A1 by A13,A24,A17,INTEGRA1:5; then
reconsider D1 as Division of A1 by A23,INTEGRA1:def 2;
A28: 1 < i+1 by A15,NAT_1:16;
i+1 in dom D by A5,FINSEQ_1:4; then
A29: lower_bound divset(D,i+1) = D.(i+1-1)
& upper_bound divset(D,i+1) = D.(i+1) by A28,INTEGRA1:def 4; then
A30: B = [. lower_bound B, upper_bound B .]
& divset(D,i+1) = [. D.i, D.(i+1) .] by INTEGRA1:4;
A31: D.i <= D.(i+1) by A29,SEQ_4:11;
per cases;
suppose A32: upper_bound B <= D.i; then
[. lower_bound B, upper_bound B .]
c= [. lower_bound A, D.i .] by A9,XXREAL_1:34; then
A33: B c= A1 by A17,INTEGRA1:4;
for k be Nat st k in dom v1 holds v1.k = xvol (B /\ divset(D1,k))
proof
let k be Nat;
assume A34: k in dom v1; then
A35: k in Seg i & k in dom v by RELAT_1:57; then
A36: v.k = v1.k by FUNCT_1:49;
A37: k in dom D & k in dom D1 by A34,A35,A13,A4,FINSEQ_3:29;
A38: divset(D,k) = [. lower_bound divset(D,k), upper_bound divset(D,k) .]
& divset(D1,k) = [. lower_bound divset(D1,k), upper_bound divset(D1,k) .]
by INTEGRA1:4;
divset(D,k) = divset(D1,k)
proof
per cases;
suppose k=1; then
A39: lower_bound(divset(D,k)) = lower_bound A
& upper_bound(divset(D,k)) = D.k
& lower_bound(divset(D1,k)) = lower_bound A1
& upper_bound(divset(D1,k)) = D1.k by A37,INTEGRA1:def 4;
lower_bound A = lower_bound A1 by A17,A27,INTEGRA1:5;
hence divset(D,k) = divset(D1,k) by A39,A35,A38,FUNCT_1:49;
end;
suppose A40: k<>1; then
A41: lower_bound(divset(D,k)) = D.(k-1)
& upper_bound(divset(D,k)) = D.k
& lower_bound(divset(D1,k)) = D1.(k-1)
& upper_bound(divset(D1,k)) = D1.k by A37,INTEGRA1:def 4;
A42: 1 <= k by A35,FINSEQ_1:1; then
k-1 in NAT by INT_1:5; then
reconsider k1=k-1 as Nat;
1 < k by A40,A42,XXREAL_0:1; then
D.k1 = D1.k1 by A35,FINSEQ_3:12,FUNCT_1:49;
hence divset(D,k) = divset(D1,k) by A41,A35,A38,FUNCT_1:49;
end;
end;
hence thesis by A4,A35,A36;
end; then
A43: Sum v1 = vol B by A3,A33,A13;
A44: [. D.i, upper_bound B .] c= {D.i} by A32,XXREAL_1:85;
lower_bound B <= upper_bound B by SEQ_4:11; then
lower_bound B <= D.i & upper_bound B <= D.(i+1) by A32,A31
,XXREAL_0:2; then
A45: B /\ divset(D,i+1) c= {D.i} by A44,A30,XXREAL_1:143;
reconsider BD = B /\ divset(D,i+1) as real-bounded Subset of REAL
by XBOOLE_1:17,XXREAL_2:45;
A46: xvol (B /\ divset(D,i+1)) <= xvol ({D.i})
proof
per cases;
suppose B /\ divset(D,i+1) = {};
then xvol (B /\ divset(D,i+1)) = 0 by Def2;
hence xvol (B /\ divset(D,i+1)) <= xvol ({D.i}) by Th5;
end;
suppose B /\ divset(D,i+1) <> {};
then reconsider BD = B /\ divset(D,i+1) as non empty real-bounded
Subset of REAL by XBOOLE_1:17,XXREAL_2:45;
reconsider Di = {D.i} as non empty real-bounded Subset of REAL;
A47: xvol BD = vol BD & xvol {D.i} = vol {D.i} by Def2;
lower_bound Di <= lower_bound BD
& upper_bound BD <= upper_bound Di by A45,SEQ_4:47,48;
hence xvol (B /\ divset(D,i+1)) <= xvol {D.i} by A47,XREAL_1:13;
end;
end;
A48: vol {D.i} = upper_bound {D.i} - upper_bound {D.i} by SEQ_4:10;
0 <= xvol BD by Th5; then
v.(i+1) = 0 by A6,A46,A48,Def2; then
Sum v = vol B + 0 by A43,A8,RVSUM_1:74;
hence Sum v = vol B;
end;
suppose A49: D.i < upper_bound B;
per cases;
suppose A50: lower_bound B <= D.i; then
reconsider B1=[. lower_bound B, D.i .], B2=[. D.i, upper_bound B .]
as non empty closed_interval Subset of REAL
by XXREAL_1:30,A49,MEASURE5:def 3;
B1 \/ B2 = [. lower_bound B, upper_bound B .] by A50,A49,XXREAL_1:165;
then
A51: B1 \/ B2 = B by INTEGRA1:4;
B1 = [. lower_bound B1, upper_bound B1 .]
& B2 = [. lower_bound B2, upper_bound B2 .] by INTEGRA1:4; then
A52: lower_bound B = lower_bound B1 & D.i = upper_bound B1
& D.i = lower_bound B2 & upper_bound B = upper_bound B2 by INTEGRA1:5;
for k be Nat st k in dom v1 holds v1.k = xvol (B1 /\ divset(D1,k))
proof
let k be Nat;
assume A53: k in dom v1; then
A54: k in Seg i & k in dom v by RELAT_1:57; then
A55: v.k = xvol (B /\ divset(D,k)) by A4;
A56: v.k = v1.k by A54,FUNCT_1:49;
A57: k in dom D & k in dom D1 by A53,A54,A4,A13,FINSEQ_3:29;
A58: divset(D,k) = [. lower_bound divset(D,k), upper_bound divset(D,k) .]
& divset(D1,k) = [. lower_bound divset(D1,k), upper_bound divset(D1,k) .]
by INTEGRA1:4;
A59: divset(D,k) = divset(D1,k)
proof
per cases;
suppose k=1; then
A60: lower_bound(divset(D,k)) = lower_bound A
& upper_bound(divset(D,k)) = D.k
& lower_bound(divset(D1,k)) = lower_bound A1
& upper_bound(divset(D1,k)) = D1.k by A57,INTEGRA1:def 4;
lower_bound A = lower_bound A1 by A27,A17,INTEGRA1:5;
hence divset(D,k) = divset(D1,k) by A60,A54,A58,FUNCT_1:49;
end;
suppose A61: k<>1; then
A62: lower_bound(divset(D,k)) = D.(k-1)
& upper_bound(divset(D,k)) = D.k
& lower_bound(divset(D1,k)) = D1.(k-1)
& upper_bound(divset(D1,k)) = D1.k by A57,INTEGRA1:def 4;
A63: 1 <= k by A54,FINSEQ_1:1; then
k-1 in NAT by INT_1:5; then
reconsider k1=k-1 as Nat;
1 < k by A61,A63,XXREAL_0:1; then
D.k1 = D1.k1 by A54,FINSEQ_3:12,FUNCT_1:49;
hence divset(D,k) = divset(D1,k) by A62,A54,A58,FUNCT_1:49;
end;
end; then
A64: B1 /\ divset(D1,k) c= B /\ divset(D,k) by A51,XBOOLE_1:7,26;
for x be object st x in B /\ divset(D,k)
holds x in B1 /\ divset(D1,k)
proof
let x be object;
assume A65: x in B /\ divset(D,k); then
reconsider r=x as Real;
A66: x in B & x in divset(D,k) by A65,XBOOLE_0:def 4; then
A67: ex r0 be Real
st r=r0 & lower_bound B <=r0 & r0 <= upper_bound B by A30;
A68: ex r1 be Real
st r=r1 & lower_bound divset(D,k) <=r1
& r1 <= upper_bound divset(D,k) by A58,A66;
A69: k <= i by A54,FINSEQ_1:1;
A70: now assume k <> i; then
k < i by A69,XXREAL_0:1;
hence D.k <= D.i by A16,A57,VALUED_0:def 13;
end;
k = 1 or k <> 1; then
upper_bound divset(D,k) <= D.i by A70,A57,INTEGRA1:def 4;
then r <= D.i by A68,XXREAL_0:2;
then r in B1 by A67;
hence x in B1 /\ divset(D1,k) by XBOOLE_0:def 4,A59,A66;
end;
then B /\ divset(D,k) c= B1 /\ divset(D1,k);
hence thesis by A55,A56,A64,XBOOLE_0:def 10;
end; then
A71: Sum v1 = vol B1 by A3,A17,A9,XXREAL_1:34,A13;
B /\ divset(D,i+1) = B1 /\ divset(D,i+1) \/ B2 /\ divset(D,i+1)
by A51,XBOOLE_1:23; then
B /\ divset(D,i+1)
= [. D.i, D.i .] \/ B2 /\ [. D.i, D.(i+1) .]
by A30,A50,A31,XXREAL_1:143; then
A72: B /\ divset(D,i+1)
= ( [. D.i, D.i .] \/ [. D.i, upper_bound B .] )
/\ ([. D.i, D.i .] \/ [. D.i, D.(i+1) .]) by XBOOLE_1:24;
D.i <= upper_bound B by A52,SEQ_4:11; then
A73: [. D.i, D.i .] \/ [. D.i, upper_bound B .] = B2 by XXREAL_1:165;
[. D.i, D.i .] \/ [. D.i, D.(i+1) .]
= [. D.i, D.(i+1) .] by A31,XXREAL_1:165; then
A74: [. D.i, D.i .] \/ [. D.i, D.(i+1) .]
= divset(D,i+1) by A29,INTEGRA1:4;
A75: upper_bound B <= D.(i+1) by A4,A9,INTEGRA1:def 2;
for x be object st x in B2 holds x in divset(D,i+1)
proof
let x be object;
assume A76: x in B2; then
reconsider r=x as Real;
A77: ex r0 be Real
st r=r0 & D.i <= r0 & r0 <= upper_bound B by A76;
r <= D.(i+1) by A75,XXREAL_0:2,A77;
hence x in divset(D,i+1) by A30,A77;
end; then
A78: B2 c= divset(D,i+1);
v.(i+1) = xvol ( B /\ divset(D,i+1)) by A4,A5,FINSEQ_1:4; then
v.(i+1) = xvol B2 by A78,A74,A72,A73,XBOOLE_1:28; then
v.(i+1) = vol B2 by Def2; then
Sum v = vol B1 + vol B2 by A8,RVSUM_1:74,A71;
hence Sum v = vol B by A52;
end;
suppose A79: D.i < lower_bound B; then
A80: [. lower_bound B, D.i .] = {} by XXREAL_1:29;
reconsider B1=[. lower_bound B, D.i .] as Subset of REAL;
reconsider B2=B as non empty closed_interval Subset of REAL;
now let k0 be object;
assume A81: k0 in dom v1; then
A82: k0 in Seg i & k0 in dom v by RELAT_1:57;
reconsider k=k0 as Nat by A81;
A83: k in dom D & k in dom D1 by A81,A82,A4,A13,FINSEQ_3:29;
A84: divset(D,k) = [. lower_bound divset(D,k), upper_bound divset(D,k) .]
& divset(D1,k)= [. lower_bound divset(D1,k), upper_bound divset(D1,k) .]
by INTEGRA1:4;
A85: divset(D,k) = divset(D1,k)
proof
per cases;
suppose k=1; then
A86: lower_bound(divset(D,k)) = lower_bound A
& upper_bound(divset(D,k)) = D.k
& lower_bound(divset(D1,k)) = lower_bound A1
& upper_bound(divset(D1,k)) = D1.k by A83,INTEGRA1:def 4;
lower_bound A = lower_bound A1 by A27,A17,INTEGRA1:5;
hence divset(D,k) = divset(D1,k) by A84,A86,A82,FUNCT_1:49;
end;
suppose A87: k<>1; then
A88: lower_bound(divset(D,k)) = D.(k-1)
& upper_bound(divset(D,k)) = D.k
& lower_bound(divset(D1,k)) = D1.(k-1)
& upper_bound(divset(D1,k)) = D1.k by A83,INTEGRA1:def 4;
A89: 1 <= k by A82,FINSEQ_1:1; then
k-1 in NAT by INT_1:5; then
reconsider k1=k-1 as Nat;
1 < k by A87,A89,XXREAL_0:1; then
D.k1 = D1.k1 by A82,FINSEQ_3:12,FUNCT_1:49;
hence divset(D,k) = divset(D1,k) by A88,A82,A84,FUNCT_1:49;
end;
end;
for x be object st x in B /\ divset(D,k)
holds x in B1 /\ divset(D1,k)
proof
let x be object;
assume A90: x in B /\ divset(D,k); then
reconsider r=x as Real;
A91: x in B & x in divset(D,k) by A90,XBOOLE_0:def 4; then
A92: (ex r0 be Real
st r=r0 & lower_bound B <=r0 & r0 <= upper_bound B)
& (ex r1 be Real
st r=r1 & lower_bound divset(D,k) <=r1
& r1 <= upper_bound divset(D,k)) by A30,A84;
k in Seg i by A81,RELAT_1:57; then
A93: k <= i by FINSEQ_1:1;
A94: now assume k <> i; then
k < i by A93,XXREAL_0:1;
hence D.k <= D.i by A16,A83,VALUED_0:def 13;
end;
k = 1 or k <> 1; then
upper_bound divset(D,k) <= D.i by A94,A83,INTEGRA1:def 4;
then r <= D.i by A92,XXREAL_0:2;
then r in B1 by A92;
hence x in B1 /\ divset(D1,k) by XBOOLE_0:def 4,A85,A91;
end; then
A95: B /\ divset(D,k) c= B1 /\ divset(D1,k);
v.k = xvol (B /\ divset(D,k)) by A82,A4; then
v.k0 = 0 by Def2,A80,A95;
hence v1.k0 = 0 by A82,FUNCT_1:49;
end;
then v1 = dom v1 --> 0 by FUNCOP_1:11;
then v1 = i |-> 0 by A14,FINSEQ_2:def 2; then
A96: Sum v1 = 0 by RVSUM_1:81;
A97: upper_bound B <= D.(i+1) by A4,A9,INTEGRA1:def 2;
for x be object st x in B2 holds x in divset(D,i+1)
proof
let x be object;
assume A98: x in B2; then
reconsider r=x as Real;
B= [. lower_bound B, upper_bound B .] by INTEGRA1:4; then
ex r0 be Real
st r=r0 & lower_bound B <= r0 & r0 <= upper_bound B by A98; then
D.i <= r & r <= D.(i+1) by A97,XXREAL_0:2,A79;
hence x in divset(D,i+1) by A30;
end; then
A99: B2 c= divset(D,i+1);
v.(i+1) = xvol (B /\ divset(D,i+1)) by A4,A5,FINSEQ_1:4; then
v.(i+1) = xvol B by A99,XBOOLE_1:28; then
v.(i+1) = vol B by Def2; then
Sum v = 0 + vol B by A8,RVSUM_1:74,A96;
hence Sum v = vol B;
end;
end;
end;
suppose A100: i = 0; then
A101: D.1 = upper_bound A by A4,INTEGRA1:def 2;
dom D = Seg 1 by A100,A4,FINSEQ_1:def 3; then
1 in dom D; then
lower_bound divset(D,1) = lower_bound A
& upper_bound divset(D,1) = D.1 by INTEGRA1:def 4; then
divset(D,1) = [. lower_bound A, upper_bound A .] by A101,INTEGRA1:4; then
A102: divset(D,1) = A by INTEGRA1:4;
v.1 = xvol (B /\ divset(D,1)) by A100,A4,A5,FINSEQ_1:4; then
v.1 = xvol B by A102,A4,XBOOLE_1:28; then
A103: v.1 = vol B by Def2;
Sum v = Sum v1 + v.1 by A100,A8,RVSUM_1:74; then
Sum v = 0 + vol B by A100,RVSUM_1:72,A103;
hence Sum v = vol B;
end;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
Lm2:
for Y be RealNormSpace,
xseq,yseq be FinSequence of Y st
len xseq = len yseq + 1 & xseq| (len yseq) = yseq holds
ex v be Point of Y st v=xseq/.(len xseq) & Sum xseq = Sum yseq + v
proof
let Y be RealNormSpace;
let xseq,yseq be FinSequence of Y;
assume A1: len xseq = len yseq + 1 & xseq| (len yseq) = yseq;
take v = xseq/.(len xseq);
len xseq in Seg (len xseq) by A1,FINSEQ_1:4;
then (len xseq) in dom (xseq) by FINSEQ_1:def 3;
then
A2:v=xseq.(len xseq) by PARTFUN1:def 6;
xseq| (len yseq) = xseq| dom (yseq) by FINSEQ_1:def 3;
hence thesis by A1,A2,RLVECT_1:38;
end;
theorem Th9:
for Y be RealNormSpace,
xseq be FinSequence of Y, yseq be FinSequence of REAL st
len xseq = len yseq &
( for i be Element of NAT st i in dom xseq holds
ex v be Point of Y st v = xseq/.i & yseq.i = ||.v.|| )
holds ||.Sum xseq.|| <= Sum yseq
proof
let Y be RealNormSpace;
defpred P[Nat] means
for xseq be FinSequence of Y, yseq be FinSequence of REAL st
$1=len xseq & len xseq = len yseq &
( for i be Element of NAT st i in dom xseq holds
ex v be Point of Y st v=xseq/.i & yseq.i=||.v.|| )
holds ||.Sum xseq.|| <= Sum yseq;
A1:P[0]
proof
let xseq be FinSequence of Y, yseq be FinSequence of REAL;
assume A2: 0=len xseq & len xseq = len yseq &
( for i be Element of NAT st i in dom xseq holds
ex v be Point of Y st v = xseq/.i & yseq.i = ||.v.|| ); then
<*>(the carrier of Y) = xseq;
then Sum xseq = 0.Y & <*> REAL = yseq by A2,RLVECT_1:43;
hence thesis by RVSUM_1:72;
end;
A3:now let i be Nat;
assume A4: P[i];
now let xseq be FinSequence of Y, yseq be FinSequence of REAL;
set xseq0=xseq|i, yseq0=yseq|i;
assume
A5: i+1=len xseq & len xseq = len yseq &
( for i be Element of NAT st i in dom xseq holds
ex v be Point of Y st v=xseq/.i & yseq.i=||.v.||);
A6: for k be Element of NAT st k in dom xseq0 holds
ex v be Point of Y st v=xseq0/.k & yseq0.k=||.v.||
proof
let k be Element of NAT;
assume A7: k in dom xseq0; then
A8: k in Seg i & k in dom xseq by RELAT_1:57; then
consider v be Point of Y such that
A9: v=xseq/.k & yseq.k=||.v.|| by A5;
take v;
xseq/.k = xseq.k by A8,PARTFUN1:def 6; then
xseq/.k = xseq0.k by A8,FUNCT_1:49;
hence thesis by A9,A8,A7,PARTFUN1:def 6,FUNCT_1:49;
end;
dom xseq = Seg(i+1) by A5,FINSEQ_1:def 3; then
consider w be Point of Y such that
A10: w=xseq/.(i+1) & yseq.(i+1)=||.w.|| by A5,FINSEQ_1:4;
A11: 1 <= i + 1 & i + 1 <= len yseq by A5,NAT_1:11;
yseq = (yseq|i)^<*yseq/.(i+1) *> by A5,FINSEQ_5:21; then
yseq = yseq0 ^<*(yseq.(i+1))*> by A11,FINSEQ_4:15; then
A12: Sum yseq = Sum yseq0 + yseq.(i+1) by RVSUM_1:74;
A13: i=len xseq0 by A5,FINSEQ_1:59,NAT_1:11; then
A14: ex v be Point of Y st v=xseq/.(len xseq)
& Sum xseq = Sum xseq0 + v by A5,Lm2;
A15: ||. Sum xseq0 + w.||<= ||.Sum xseq0 .|| + ||. w .|| by NORMSP_1:def 1;
len xseq0 = len yseq0 by A5,A13,FINSEQ_1:59,NAT_1:11; then
||. Sum xseq0 .|| + ||. w .|| <= Sum yseq0 + yseq.(i+1)
by A10,XREAL_1:6,A4,A6,A13;
hence ||. Sum xseq .|| <= Sum yseq by A5,A10,A12,A14,A15,XXREAL_0:2;
end;
hence P[i+1];
end;
for i be Nat holds P[i] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
theorem Th10:
for Y be RealNormSpace,
p be FinSequence of Y,
q be FinSequence of REAL st len p = len q
& (for j be Nat st j in dom p holds ||. p/.j .|| <= q.j)
holds ||. Sum(p) .|| <= Sum(q)
proof
let Y be RealNormSpace;
let p be FinSequence of Y, q be FinSequence of REAL;
assume A1: len p = len q
& (for j be Nat st j in dom p holds ||. p/.j .|| <= q.j);
defpred P1[Nat,set] means
ex v be Point of Y st v = p/.$1 & $2 = ||. v .||;
A2: for i be Nat st i in Seg len p ex x be Element of REAL st P1[i,x]
proof
let i be Nat;
assume i in Seg len p;
reconsider w = ||.p/.i.|| as Element of REAL;
take w;
thus thesis;
end;
consider u be FinSequence of REAL such that
A3: dom u = Seg len p & for i be Nat st
i in Seg len p holds P1[i,u.i] from FINSEQ_1:sch 5(A2);
A4: for i be Element of NAT st i in dom p holds
ex v be Point of Y st v = p/.i & u.i = ||. v .||
proof
let i be Element of NAT;
assume i in dom p; then
i in Seg len p by FINSEQ_1:def 3;
hence ex v be Point of Y st v = p/.i & u.i = ||. v .|| by A3;
end;
A5: len u = len p by A3,FINSEQ_1:def 3; then
A6: ||.Sum p.|| <= Sum u by A4,Th9;
set i = len p;
reconsider uu=u as Element of i-tuples_on REAL by A5,FINSEQ_2:92;
reconsider qq=q as Element of i-tuples_on REAL by A1,FINSEQ_2:92;
now let j be Nat;
assume j in Seg i; then
A7: j in dom p by FINSEQ_1:def 3; then
ex v be Point of Y st v = p/.j & u.j = ||. v .|| by A4;
hence uu.j <= qq.j by A7,A1;
end; then
Sum uu <= Sum qq by RVSUM_1:82;
hence thesis by A6,XXREAL_0:2;
end;
theorem Th11:
for j being Element of NAT
for A being non empty closed_interval Subset of REAL
for D1 being Division of A st j in dom D1 holds
vol (divset (D1,j)) <= delta D1
proof
let j be Element of NAT;
let A be non empty closed_interval Subset of REAL;
let D1 be Division of A;
assume A1: j in dom D1;
then j in Seg (len D1) by FINSEQ_1:def 3;
then j in Seg (len (upper_volume ((chi (A,A)),D1))) by INTEGRA1:def 6;
then j in dom (upper_volume ((chi (A,A)),D1)) by FINSEQ_1:def 3;
then (upper_volume ((chi (A,A)),D1)) . j
in rng (upper_volume ((chi (A,A)),D1)) by FUNCT_1:def 3;
then (upper_volume ((chi (A,A)),D1)) . j
<= max (rng (upper_volume ((chi (A,A)),D1))) by XXREAL_2:def 8;
hence vol (divset (D1,j)) <= delta D1 by A1,INTEGRA1:20;
end;
theorem Th12:
for A being non empty closed_interval Subset of REAL,
D being Division of A, r be Real st delta(D) < r
holds
for i be Nat, s,t be Real
st i in dom D & s in divset(D,i) & t in divset(D,i)
holds |.s-t.| < r
proof
let A being non empty closed_interval Subset of REAL,
D being Division of A, r be Real;
assume A1: delta(D) < r;
let i be Nat, s,t be Real;
assume A2: i in dom D & s in divset(D,i) & t in divset(D,i); then
vol (divset (D,i)) <= delta D by Th11; then
A3:upper_bound divset(D,i) - lower_bound divset(D,i) < r by A1,XXREAL_0:2;
s <= upper_bound divset(D,i) & t <= upper_bound divset(D,i)
& lower_bound divset(D,i) <= s & lower_bound divset(D,i) <= t
by A2,SEQ_4:def 1,def 2; then
A4: t-s <= upper_bound divset(D,i) - lower_bound divset (D,i)
& s-t <= upper_bound divset(D,i) - lower_bound divset(D,i) by XREAL_1:13;
per cases;
suppose s < t;
then s-t < t- t by XREAL_1:14; then
|.s-t.| = - (s-t) by ABSVALUE:def 1;
hence |.s-t.| < r by A3,A4,XXREAL_0:2;
end;
suppose not s < t;
then t - t <= s- t by XREAL_1:9; then
|.s-t.| = s - t by ABSVALUE:def 1;
hence |.s-t.| < r by A3,A4,XXREAL_0:2;
end;
end;
theorem Th13:
for X be RealBanachSpace, A be non empty closed_interval Subset of REAL,
h be Function of A,the carrier of X
st
for r be Real st 0<r ex s be Real st 0<s &
for x1,x2 be Real st x1 in dom h & x2 in dom h & |. x1-x2 .| < s
holds ||. h/.x1-h/.x2 .|| < r
holds
for T being DivSequence of A, S be middle_volume_Sequence of h,T
st delta T is convergent & lim delta T = 0
holds middle_sum(h,S) is convergent
proof
let X be RealBanachSpace, A be non empty closed_interval Subset of REAL,
h be Function of A,the carrier of X;
assume
A1: for r be Real st 0<r ex s be Real st 0<s &
for x1,x2 be Real st x1 in dom h & x2 in dom h & |. x1-x2 .| < s
holds ||. h/.x1-h/.x2 .|| < r;
thus
for T being DivSequence of A, S be middle_volume_Sequence of h,T
st delta T is convergent & lim delta T = 0
holds middle_sum(h,S) is convergent
proof
let T being DivSequence of A, S be middle_volume_Sequence of h,T;
assume A2:delta T is convergent & lim delta T = 0;
defpred P[Element of NAT, set] means
ex p be FinSequence of REAL
st p = $2 & len p = len (T.$1)
& for i be Nat st i in dom (T.$1)
holds (p.i) in dom (h|divset((T.$1),i))
& ex z be Point of X
st z = (h|divset((T.$1),i)).(p.i)
& (S.$1).i = (vol divset((T.$1),i)) * z;
A3: for k be Element of NAT ex p be Element of (REAL)* st P[k, p]
proof
let k be Element of NAT;
defpred P1[Nat,set] means $2 in dom (h|divset((T.k),$1)) &
ex c be Point of X st c = (h|divset((T.k),$1)).$2 &
(S.k).$1 = (vol divset((T.k),$1)) * c;
A4: Seg len(T.k) = dom(T.k) by FINSEQ_1:def 3;
A5: for i be Nat st i in Seg len (T.k) ex x be Element of REAL st P1[i,x]
proof
let i be Nat;
assume i in Seg len(T.k); then
i in dom (T.k) by FINSEQ_1:def 3; then
consider c be Point of X such that
A6: c in rng (h|divset((T.k),i)) &
(S.k).i = vol divset(T.k,i)*c by INTEGR18:def 1;
consider x be object such that
A7: x in dom (h|divset(T.k,i)) &
c = (h|divset(T.k,i)).x by A6,FUNCT_1:def 3;
x in dom h & x in divset(T.k,i) by A7,RELAT_1:57; then
reconsider x as Element of REAL;
take x;
thus thesis by A6,A7;
end;
consider p be FinSequence of REAL such that
A8: dom p = Seg len(T.k)
& for i be Nat st i in Seg len(T.k) holds P1[i,p.i]
from FINSEQ_1:sch 5(A5);
take p;
len p = len (T.k) by A8,FINSEQ_1:def 3;
hence thesis by A8,A4,FINSEQ_1:def 11;
end;
consider Fn be sequence of (REAL)* such that
A9: for x be Element of NAT holds P[x, Fn.x] from FUNCT_2:sch 3(A3);
consider Fm be sequence of (REAL)* such that
A10: for x be Element of NAT holds P[x, Fm.x] from FUNCT_2:sch 3(A3);
A11:0<= vol A by INTEGRA1:9;
now let p be Real;
set pp2= p/2;
set pv = pp2 / (vol A + 1);
assume p > 0; then
A12:0 < pp2 & pp2 < p by XREAL_1:215,216; then
A13:0 < pv by A11,XREAL_1:139; then
pv*(vol A) < pv *(vol A + 1) by XREAL_1:29,68; then
pv*(vol A) < pp2 by A11,XCMPLX_1:87; then
A14:pv*(vol A) < p by A12,XXREAL_0:2;
set p2v = pv/2;
consider sk be Real such that
A15: 0 < sk
& for x1,x2 be Real st x1 in dom h & x2 in dom h & |. x1-x2 .| < sk
holds ||. h/.x1-h/.x2 .|| < p2v by A1,A13,XREAL_1:215;
consider k be Nat such that
A16: for i be Nat st k <= i holds |. (delta T).i - 0 .| < sk
by A15,A2,SEQ_2:def 7;
take k;
let n, m be Nat;
A17: n in NAT & m in NAT by ORDINAL1:def 12;
assume n >= k & m >= k; then
|. (delta T).n - 0 .| < sk & |. (delta T).m - 0 .| < sk by A16; then
|. delta(T.n) .| < sk & |. delta(T.m) .| < sk by INTEGRA3:def 2,A17; then
A18: delta(T.n) < sk & delta(T.m) < sk by INTEGRA3:9,ABSVALUE:def 1;
A19: middle_sum(h,S).n = middle_sum(h,S.n)
& middle_sum(h,S).m = middle_sum(h,S.m) by INTEGR18:def 4;
consider p1 be FinSequence of REAL such that
A20: p1 = Fn.n & len p1 = len (T.n)
& for i be Nat st i in dom (T.n)
holds p1.i in dom (h|divset(T.n,i))
& ex z be Point of X st z = (h|divset(T.n,i)).(p1.i)
& (S.n).i = (vol divset(T.n,i)) * z by A9,A17;
consider p2 be FinSequence of REAL such that
A21: p2 = Fm.m & len p2 = len (T.m)
& for i be Nat st i in dom (T.m)
holds p2.i in dom (h|divset(T.m,i))
& ex z be Point of X st z = (h|divset(T.m,i)).(p2.i)
& (S.m).i = (vol divset(T.m,i)) * z by A10,A17;
defpred H1[object,object,object] means
ex i,j being Nat, z be Point of X
st $1=i & $2=j & z = (h|divset(T.n,i)).(p1.i)
& $3 = (xvol (divset(T.n,i) /\ divset(T.m,j)))* z;
A22: for x,y be object st x in Seg len(T.n) & y in Seg len (T.m)
ex w be object st w in the carrier of X & H1[x,y,w]
proof
let x,y be object;
assume A23: x in Seg len (T.n) & y in Seg len (T.m);
then reconsider i=x,j=y as Nat;
i in dom (T.n) by FINSEQ_1:def 3,A23;
then consider z be Point of X such that
A24: z = (h|divset(T.n,i)).(p1.i)
& (S.n).i = (vol divset(T.n,i)) * z by A20;
(xvol (divset(T.n,i) /\ divset(T.m,j)))* z in the carrier of X;
hence thesis by A24;
end;
consider Snm being Function of
[: Seg len (T.n),Seg len (T.m) :],the carrier of X such that
A25: for x,y be object st x in Seg len(T.n) & y in Seg len(T.m)
holds H1[x,y,Snm.(x,y)] from BINOP_1:sch 1(A22);
A26: for i,j being Nat st i in Seg len (T.n) & j in Seg len (T.m)
holds
ex z be Point of X
st z = (h|divset(T.n,i)).(p1.i)
& Snm.(i,j) = (xvol (divset(T.n,i) /\ divset(T.m,j)))* z
proof
let i,j being Nat;
assume i in Seg len (T.n) & j in Seg len (T.m);
then ex i1,j1 being Nat, z be Point of X
st i=i1 & j=j1 & z = (h|divset(T.n,i1)).(p1.i1)
& Snm.(i,j)= (xvol (divset(T.n,i1) /\ divset(T.m,j1)))* z by A25;
hence thesis;
end;
defpred P1[Nat,object] means
ex r be FinSequence of X st
dom r = Seg len (T.m) & $2=Sum r &
for j be Nat st j in dom r holds r.j=Snm.($1,j);
A27: for k be Nat st k in Seg len (T.n) ex x be object st P1[k,x]
proof
let k be Nat;
assume A28: k in Seg len (T.n);
deffunc G(set)= Snm.( k,$1 );
consider r being FinSequence such that
A29: len r = len (T.m) and
A30: for j be Nat st j in dom r holds r.j=G(j) from FINSEQ_1:sch 2;
A31: dom r = Seg len (T.m) by A29,FINSEQ_1:def 3;
for j be Nat st j in dom r holds r.j in the carrier of X
proof
let j be Nat;
assume A32: j in dom r; then
[k,j] in [: Seg len (T.n), Seg len (T.m) :]
by A31,A28,ZFMISC_1:87; then
Snm.(k,j) in the carrier of X by FUNCT_2:5;
hence thesis by A30,A32;
end;
then reconsider r as FinSequence of X by FINSEQ_2:12;
take x=Sum r;
thus thesis by A30,A31;
end;
consider Xp be FinSequence such that
A33: dom Xp = Seg len (T.n)
& for k be Nat st k in Seg len (T.n) holds P1[k,Xp.k]
from FINSEQ_1:sch 1(A27);
for i be Nat st i in dom Xp holds Xp.i in the carrier of X
proof
let i be Nat;
assume i in dom Xp;
then ex r be FinSequence of X st dom r = Seg len (T.m) & Xp.i=Sum r
& for j be Nat st j in dom r holds r.j=Snm.(i,j) by A33;
hence thesis;
end;
then reconsider Xp as FinSequence of X by FINSEQ_2:12;
A34: len Xp = len (T.n) by FINSEQ_1:def 3,A33;
for k be Nat st 1 <= k & k <= len Xp holds Xp.k = (S.n).k
proof
let k be Nat;
assume 1 <= k & k <= len Xp; then
A35: k in Seg len Xp & k in Seg len (T.n) by A34; then
A36: k in dom Xp & k in dom (T.n) by FINSEQ_1:def 3; then
consider z be Point of X such that
A37: z = (h|divset(T.n,k)).(p1.k)
& (S.n).k = (vol divset(T.n,k)) * z by A20;
consider r be FinSequence of X such that
A38: dom r = Seg len (T.m) & Xp.k = Sum r
& for j be Nat st j in dom r holds r.j=Snm.(k,j) by A35,A33;
defpred P11[Nat,set] means $2 = xvol (divset(T.n,k) /\ divset(T.m,$1));
A39: for i be Nat st i in Seg len r holds
ex x be Element of REAL st P11[i,x]
proof
let i be Nat;
assume i in Seg len r;
xvol (divset(T.n,k) /\ divset(T.m,i)) in REAL by XREAL_0:def 1;
hence thesis;
end;
consider vtntm be FinSequence of REAL such that
A40: dom vtntm = Seg len r & for i be Nat st i in Seg len r
holds P11[i,vtntm.i] from FINSEQ_1:sch 5(A39);
A41: dom vtntm = dom r
& for j be Nat st j in dom vtntm holds
vtntm.j=xvol (divset(T.n,k) /\ divset(T.m,j)) by A40,FINSEQ_1:def 3;
A42: len vtntm = len r & len (T.m) = len r by A38,A40,FINSEQ_1:def 3; then
A43: Sum vtntm = vol (divset(T.n,k)) by Th8,A40,A36,INTEGRA1:8;
for j be Nat st j in dom r holds
ex x be Real st x = vtntm.j & r.j = x*z
proof
let j be Nat;
assume A44: j in dom r; then
A45: ex w be Point of X
st w = (h|divset(T.n,k)).(p1.k)
& Snm.(k,j) = (xvol (divset(T.n,k) /\ divset(T.m,j))) * w
by A26,A35,A38;
take vtntm.j;
r.j= (xvol (divset(T.n,k) /\ divset(T.m,j))) * z by A37,A45,A44,A38;
hence thesis by A41,A44;
end;
hence thesis by A37,A38,A43,Th7,A42;
end; then
A46:Xp = S.n by INTEGR18:def 1,A34;
defpred P2[Nat,object] means
ex s be FinSequence of X st
dom s = Seg len (T.n) & $2=Sum s &
for i be Nat st i in dom s holds s.i=Snm.( i,$1 );
A47:for k be Nat st k in Seg len (T.m) ex x be object st P2[k,x]
proof
let k be Nat;
assume A48: k in Seg len (T.m);
deffunc G(set)= Snm.($1,k);
consider s being FinSequence such that
A49: len s = len (T.n) and
A50: for i be Nat st i in dom s holds s.i=G(i) from FINSEQ_1:sch 2;
A51: dom s = Seg len (T.n) by A49,FINSEQ_1:def 3;
for i be Nat st i in dom s holds s.i in the carrier of X
proof
let i be Nat;
assume A52: i in dom s; then
[i,k] in [: Seg len (T.n), Seg len (T.m) :]
by A51,A48,ZFMISC_1:87; then
Snm.(i,k) in the carrier of X by FUNCT_2:5;
hence thesis by A50,A52;
end;
then reconsider s as FinSequence of X by FINSEQ_2:12;
take x = Sum s;
thus thesis by A50,A51;
end;
consider Xq be FinSequence such that
A53: dom Xq = Seg len (T.m)
& for k be Nat st k in Seg len (T.m) holds P2[k,Xq.k]
from FINSEQ_1:sch 1(A47);
for j be Nat st j in dom Xq holds Xq.j in the carrier of X
proof
let j be Nat;
assume j in dom Xq;
then ex s be FinSequence of X st dom s = Seg len (T.n)
& Xq.j=Sum s
& for i be Nat st i in dom s holds s.i=Snm.(i,j) by A53;
hence thesis;
end;
then reconsider Xq as FinSequence of X by FINSEQ_2:12;
defpred H2[object,object,object] means
ex i,j being Nat, z be Point of X
st $1=i & $2=j & z = (h|divset(T.m,j)).(p2.j)
& $3 = (xvol (divset(T.n,i) /\ divset(T.m,j))) * z;
A54:for x,y be object st x in Seg len (T.n) & y in Seg len (T.m)
ex w be object st w in the carrier of X & H2[x,y,w]
proof
let x,y be object;
assume A55: x in Seg len (T.n) & y in Seg len (T.m);
then reconsider i=x,j=y as Nat;
j in dom (T.m) by FINSEQ_1:def 3,A55;
then consider z be Point of X such that
A56: z = (h|divset(T.m,j)).(p2.j)
& (S.m).j = (vol divset(T.m,j)) * z by A21;
(xvol (divset(T.n,i) /\ divset(T.m,j)))* z in the carrier of X;
hence thesis by A56;
end;
consider Smn being Function of
[: Seg len (T.n),Seg len (T.m) :],the carrier of X such that
A57: for x,y be object st x in Seg len (T.n) & y in Seg len (T.m)
holds H2[x,y,Smn.(x,y)] from BINOP_1:sch 1(A54);
A58: for i,j being Nat st i in Seg len (T.n) & j in Seg len (T.m)
holds
ex z be Point of X st z = (h|divset(T.m,j)).(p2.j)
& Smn.(i,j) = (xvol (divset(T.n,i) /\ divset(T.m,j)))* z
proof
let i,j being Nat;
assume i in Seg len (T.n) & j in Seg len (T.m);
then ex i1,j1 being Nat, z be Point of X
st i=i1 & j=j1 & z = (h|divset(T.m,j1)).(p2.j1)
& Smn.(i,j)= (xvol (divset(T.n,i1) /\ divset(T.m,j1))) * z by A57;
hence thesis;
end;
defpred P3[Nat,object] means
ex s be FinSequence of X st
dom s = Seg len (T.n) & $2=Sum s &
for i be Nat st i in dom s holds s.i=Smn.(i,$1);
A59:for k be Nat st k in Seg len (T.m) ex x be object st P3[k,x]
proof
let k be Nat;
assume A60: k in Seg len (T.m);
deffunc G(set)= Smn.($1,k);
consider s being FinSequence such that
A61: len s = len (T.n) and
A62: for i be Nat st i in dom s holds s.i=G(i) from FINSEQ_1:sch 2;
A63: dom s = Seg len (T.n) by A61,FINSEQ_1:def 3;
for i be Nat st i in dom s holds s.i in the carrier of X
proof
let i be Nat;
assume A64: i in dom s; then
[i,k] in [: Seg len (T.n), Seg len (T.m) :]
by A63,A60,ZFMISC_1:87; then
Smn.(i,k) in the carrier of X by FUNCT_2:5;
hence thesis by A62,A64;
end;
then reconsider s as FinSequence of X by FINSEQ_2:12;
take x = Sum s;
thus thesis by A62,A63;
end;
consider Zq be FinSequence such that
A65: dom Zq = Seg len (T.m)
& for k be Nat st k in Seg len (T.m) holds P3[k,Zq.k]
from FINSEQ_1:sch 1(A59);
for j be Nat st j in dom Zq holds Zq.j in the carrier of X
proof
let j be Nat;
assume j in dom Zq;
then ex s be FinSequence of X st dom s = Seg len (T.n)
& Zq.j=Sum s
& for i be Nat st i in dom s holds s.i=Smn.( i,j ) by A65;
hence thesis;
end;
then reconsider Zq as FinSequence of X by FINSEQ_2:12;
A66: len Zq = len (T.m) by FINSEQ_1:def 3,A65;
for k be Nat st 1 <= k & k <= len Zq holds Zq.k = (S.m).k
proof
let k be Nat;
assume A67: 1 <= k & k <= len Zq; then
consider s be FinSequence of X such that
A68: dom s = Seg len (T.n) & Zq.k = Sum s
& for i be Nat st i in dom s holds s.i=Smn.(i,k) by A65,FINSEQ_3:25;
A69: k in Seg len (T.m) by A67,A66;
A70: k in dom (T.m) by A67,A66,FINSEQ_3:25; then
consider z be Point of X such that
A71: z = (h|divset((T.m),k)).(p2.k)
& (S.m).k = (vol divset((T.m),k)) * z by A21;
defpred P11[Nat,set] means
$2 = xvol (divset(T.n,$1) /\ divset(T.m,k));
A72: for i be Nat st i in Seg len s holds
ex x be Element of REAL st P11[i,x]
proof
let i be Nat;
assume i in Seg len s;
xvol (divset(T.n,i) /\ divset(T.m,k)) in REAL by XREAL_0:def 1;
hence thesis;
end;
consider vtntm be FinSequence of REAL such that
A73: dom vtntm = Seg len s & for i be Nat st i in Seg len s
holds P11[i,vtntm.i] from FINSEQ_1:sch 5(A72);
A74: dom vtntm = dom s & len vtntm = len s by A73,FINSEQ_1:def 3;
A75: for j be Nat st j in dom vtntm holds
vtntm.j=xvol (divset(T.m,k) /\ divset(T.n,j)) by A73;
len s = len (T.n) by A68,FINSEQ_1:def 3; then
A76: Sum vtntm = vol divset(T.m,k) by Th8,A75,A74,A70,INTEGRA1:8;
for j be Nat st j in dom s holds
ex x be Real st x= vtntm.j & s.j=x * z
proof
let j be Nat;
assume A77: j in dom s; then
A78: ex w be Point of X
st w = (h|divset((T.m),k)).(p2.k)
& Smn.(j,k) = (xvol (divset(T.n,j) /\ divset(T.m,k))) * w
by A58,A69,A68;
take vtntm.j;
s.j= (xvol (divset(T.n,j) /\ divset(T.m,k)))* z by A71,A78,A77,A68;
hence thesis by A77,A73,A74;
end;
hence thesis by A71,A68,A76,Th7,A74;
end; then
Zq = S.m by INTEGR18:def 1,A66; then
A79: Sum(S.n) - Sum(S.m) = Sum Xq - Sum Zq by Th4,A33,A53,A46;
set XZq = Xq - Zq;
A80: dom XZq = dom Xq /\ dom Zq by VFUNCT_1:def 2; then
reconsider XZq = Xq - Zq as FinSequence by A53,A65,FINSEQ_1:def 2;
now let i be Nat;
assume i in dom XZq; then
XZq.i = (Xq - Zq)/.i by PARTFUN1:def 6;
hence XZq.i in the carrier of X;
end; then
reconsider XZq = Xq - Zq as FinSequence of X by FINSEQ_2:12;
len Xq = len Zq by FINSEQ_3:29,A53,A65; then
A81: Sum(S.n) - Sum(S.m) = Sum (XZq) by A79,INTEGR18:2;
A82: for i,j be Nat, Snmij,Smnij be Point of X
st i in Seg len (T.n) & j in Seg len (T.m) & Snmij = Snm.(i,j)
& Smnij = Smn.(i,j) holds
||. Snmij - Smnij .|| <= (xvol (divset(T.n,i) /\ divset(T.m,j))) * pv
proof
let i,j be Nat, Snmij,Smnij be Point of X;
assume A83: i in Seg len (T.n) & j in Seg len (T.m)
& Snmij = Snm.(i,j) & Smnij = Smn.(i,j); then
consider z1 be Point of X such that
A84: z1 = (h|divset(T.n,i)).(p1.i)
& Snm.(i,j) = (xvol (divset(T.n,i) /\ divset(T.m,j)))* z1 by A26;
consider z2 be Point of X such that
A85: z2 = (h|divset((T.m),j)).(p2.j)
& Smn.(i,j) = (xvol (divset(T.n,i) /\ divset(T.m,j))) * z2 by A58,A83;
A86: i in dom (T.n) & j in dom (T.m) by A83,FINSEQ_1:def 3; then
A87: p1.i in dom (h|divset(T.n,i))
& p2.j in dom (h|divset(T.m,j)) by A20,A21; then
p1.i in dom h /\ divset(T.n,i)
& p2.j in dom h /\ divset(T.m,j) by RELAT_1:61; then
A88: p1.i in dom h & p1.i in divset(T.n,i)
& p2.j in dom h & p2.j in divset(T.m,j) by XBOOLE_0:def 4;
z1 = h.(p1.i) & z2 = h.(p2.j) by A84,A85,A87,FUNCT_1:47; then
A89: z1 = h/.(p1.i) & z2 =h/.(p2.j) by A88,PARTFUN1:def 6;
per cases;
suppose A90:divset(T.n,i) /\ divset(T.m,j) = {}; then
A91: xvol (divset(T.n,i) /\ divset(T.m,j)) = (0 qua Real) by Def2;
Snmij =0.X & Smnij = 0.X by A83,A84,A85,A90,Def2,RLVECT_1:10;
hence ||. Snmij - Smnij .||
<= (xvol (divset(T.n,i) /\ divset(T.m,j))) * pv by A91;
end;
suppose divset(T.n,i) /\ divset(T.m,j) <> {}; then
consider t be object such that
A92: t in divset(T.n,i) /\ divset(T.m,j) by XBOOLE_0:def 1;
reconsider t as Real by A92;
A93: dom h = A by FUNCT_2:def 1;
A94: divset(T.m,j) c= A by A86,INTEGRA1:8;
A95: t in divset(T.n,i) & t in divset(T.m,j) by A92,XBOOLE_0:def 4; then
|. (p1.i)-t .| < sk & |. t-(p2.j) .| < sk by A86,A88,Th12,A18; then
A96: ||. h/.(p1.i)-h/.t .|| < p2v
& ||. h/.t-h/.(p2.j) .|| < p2v by A94,A95,A93,A88,A15;
reconsider DMN = divset(T.n,i) /\ divset(T.m,j)
as real-bounded Subset of REAL by XBOOLE_1:17,XXREAL_2:45;
Snmij - Smnij = (xvol DMN) * (h/.(p1.i) - 0.X - h/.(p2.j))
by A83,A84,A89,A85,RLVECT_1:34; then
Snmij - Smnij = (xvol DMN) * (h/.(p1.i) - (h/.t - h/.t) - h/.(p2.j))
by RLVECT_1:15; then
Snmij - Smnij = (xvol DMN) * (h/.(p1.i) - h/.t + h/.t - h/.(p2.j))
by RLVECT_1:29; then
Snmij - Smnij = (xvol DMN) * ((h/.(p1.i) - h/.t) + (h/.t - h/.(p2.j)))
by RLVECT_1:28; then
Snmij - Smnij
= (xvol DMN) * (h/.(p1.i) - h/.t) + (xvol DMN) * (h/.t - h/.(p2.j))
by RLVECT_1:def 5; then
A97: ||. Snmij - Smnij .||
<= ||. (xvol DMN) * (h/.(p1.i) -h/.t) .||
+ ||. (xvol DMN) * (h/.t - h/.(p2.j)) .|| by NORMSP_1:def 1;
||. (xvol DMN) * (h/.(p1.i) - h/.t) .||
= |. xvol DMN .| * ||. h/.(p1.i) - h/.t .||
& ||. (xvol DMN) * (h/.t - h/.(p2.j)) .||
= |. xvol DMN .| * ||. h/.t - h/.(p2.j) .|| by NORMSP_1:def 1; then
A98: ||. (xvol DMN) * (h/.(p1.i) - h/.t) .||
= xvol DMN * ||. h/.(p1.i) - h/.t .||
& ||. (xvol DMN) * (h/.t - h/.(p2.j)) .||
= xvol DMN * ||. h/.t - h/.(p2.j) .|| by Th5,ABSVALUE:def 1;
0<= xvol DMN by Th5; then
||. (xvol DMN) * (h/.(p1.i) - h/.t) .|| <= (xvol DMN) * p2v
& ||. (xvol DMN) * (h/.t - h/.(p2.j)) .|| <= (xvol DMN) * p2v
by A98,A96,XREAL_1:64; then
||. (xvol DMN) * (h/.(p1.i) - h/.t) .||
+ ||. (xvol DMN) * (h/.t - h/.(p2.j)) .||
<= (xvol DMN) * p2v + (xvol DMN) * p2v by XREAL_1:7;
hence
||. Snmij - Smnij .|| <= (xvol (divset(T.n,i) /\ divset(T.m,j))) *pv
by A97,XXREAL_0:2;
end;
end;
A99: for j be Nat st j in dom XZq
holds ||. XZq/.j .|| <= vol divset(T.m,j) * pv
proof
let j be Nat;
assume A100: j in dom XZq; then
A101: XZq/.j = Xq/.j - Zq/.j by VFUNCT_1:def 2;
A102: Xq/.j = Xq.j & Zq/.j = Zq.j by A100,A65,A53,A80,PARTFUN1:def 6;
A103: dom XZq = dom Xq /\ dom Zq by VFUNCT_1:def 2;
consider Xsq be FinSequence of X such that
A104: dom Xsq = Seg len (T.n) & Xq.j = Sum Xsq
& for i be Nat st i in dom Xsq holds Xsq.i=Snm.(i,j) by A100,A53,A65,A80;
consider Zsq be FinSequence of X such that
A105: dom Zsq = Seg len (T.n) & Zq.j = Sum Zsq
& for i be Nat st i in dom Zsq holds Zsq.i=Smn.(i,j) by A100,A65,A53,A80;
set XZsq = Xsq - Zsq;
A106: dom XZsq = dom Xsq /\ dom Zsq by VFUNCT_1:def 2; then
reconsider XZsq as FinSequence by A104,A105,FINSEQ_1:def 2;
now let i be Nat;
assume i in dom XZsq; then
XZsq.i = (Xsq - Zsq)/.i by PARTFUN1:def 6;
hence XZsq.i in the carrier of X;
end; then
reconsider XZsq as FinSequence of X by FINSEQ_2:12;
defpred P11[Nat,set] means $2 = xvol (divset(T.n,$1) /\ divset(T.m,j));
A107: for i be Nat st i in Seg len XZsq holds
ex x be Element of REAL st P11[i,x]
proof
let i be Nat;
assume i in Seg len XZsq;
xvol (divset(T.n,i) /\ divset(T.m,j)) in REAL by XREAL_0:def 1;
hence thesis;
end;
consider vtntm be FinSequence of REAL such that
A108: dom vtntm = Seg len XZsq & for i be Nat st i in Seg len XZsq
holds P11[i,vtntm.i] from FINSEQ_1:sch 5(A107);
A109: for i be Nat st i in dom vtntm holds
vtntm.i=xvol ( divset(T.m,j) /\ divset(T.n,i)) by A108;
A110: len vtntm = len XZsq by A108,FINSEQ_1:def 3;
A111: len XZsq = len (T.n) by A104,A105,A106,FINSEQ_1:def 3;
reconsider pvtntm = pv*vtntm as FinSequence of REAL;
j in dom (T.m) by A100,A103,A53,A65,FINSEQ_1:def 3; then
divset(T.m,j) c= A by INTEGRA1:8; then
Sum vtntm = vol divset(T.m,j) by Th8,
A109,A110,A104,A105,A106,FINSEQ_1:def 3; then
A112: Sum pvtntm = pv * vol divset(T.m,j) by RVSUM_1:87;
dom pvtntm = dom vtntm by VALUED_1:def 5; then
dom pvtntm = Seg len (T.n) by A104,A105,A106,A108,FINSEQ_1:def 3; then
A113: len pvtntm =len (T.n) by FINSEQ_1:def 3;
for i be Nat st i in dom XZsq holds ||. XZsq/.i .|| <= (pvtntm).i
proof
let i be Nat;
assume A114: i in dom XZsq; then
A115: XZsq/.i = Xsq/.i - Zsq/.i by VFUNCT_1:def 2;
Xsq/.i = Xsq.i & Zsq/.i = Zsq.i by PARTFUN1:def 6,A114,A105,A106,A104;
then
A116: Xsq/.i =Snm.(i,j) & Zsq/.i =Smn.(i,j) by A114,A104,A106,A105;
dom vtntm = dom XZsq by A108,FINSEQ_1:def 3; then
pv*(vtntm.i) = pv* (xvol (divset(T.n,i) /\ divset(T.m,j)))
by A108,A114; then
(pv(#)vtntm).i = pv* (xvol (divset(T.n,i) /\ divset(T.m,j)))
by VALUED_1:6;
hence thesis by A115,A116,A82,A114,A104,A105,A106,A100,A103,A53,A65;
end; then
A117: ||. Sum XZsq .|| <= vol (divset(T.m,j)) * pv by A112,Th10,A111,A113;
len Xsq = len Zsq by FINSEQ_3:29,A104,A105;
hence thesis by A101,A102,A104,A105,A117,INTEGR18:2;
end;
defpred P12[Nat,set] means $2 = vol (divset(T.m,$1));
A118:for i be Nat st i in Seg len XZq holds
ex x be Element of REAL st P12[i,x]
proof
let i be Nat;
assume i in Seg len XZq;
vol (divset(T.m,i)) in REAL by XREAL_0:def 1;
hence thesis;
end;
consider vtm be FinSequence of REAL such that
A119:dom vtm = Seg len XZq & for i be Nat st i in Seg len XZq
holds P12[i,vtm.i] from FINSEQ_1:sch 5(A118);
A120:len XZq = len (T.m) by A53,A65,A80,FINSEQ_1:def 3;
A121:Seg len XZq = dom XZq by FINSEQ_1:def 3;
A122:Sum vtm = vol A by A119,Th6,A120;
reconsider pvtm = pv*vtm as FinSequence of REAL;
dom pvtm = dom vtm by VALUED_1:def 5; then
dom pvtm = Seg len (T.m) by A53,A65,A80,A119,FINSEQ_1:def 3; then
A123:len pvtm = len (T.m) by FINSEQ_1:def 3;
A124:Sum pvtm = pv * vol A by RVSUM_1:87,A122;
for j be Nat st j in dom XZq holds ||. XZq/.j .|| <= pvtm.j
proof
let j be Nat;
assume A125: j in dom XZq; then
vtm.j= vol (divset(T.m,j)) by A119,A121;
then pvtm.j= vol (divset(T.m,j)) * pv by VALUED_1:6;
hence ||. XZq/.j .|| <= pvtm.j by A125,A99;
end;
then ||. Sum XZq .|| <= (vol A) * pv by A124,A120,A123,Th10;
hence ||.(middle_sum(h,S).n) - (middle_sum(h,S).m).|| < p
by A19,A81,XXREAL_0:2,A14;
end;
hence middle_sum(h,S) is convergent by RSSPACE3:8,LOPBAN_1:def 15;
end;
end;
scheme
ExRealSeq2X{D()->non empty set, F,G(set)->Element of D() }:
ex s being sequence of D()
st for n be Nat
holds s.(2*n) = F(n) & s.(2*n+1) = G(n);
defpred X[set] means ex m be Nat st $1 = 2*m;
consider N be Subset of NAT such that
A1: for n be Element of NAT holds n in N iff X[n] from SUBSET_1:sch 3;
defpred Y[set] means ex m be Nat st $1 = 2*m+1;
consider M be Subset of NAT such that
A2: for n be Element of NAT holds n in M iff Y[n] from SUBSET_1:sch 3;
defpred X[Nat, set] means
($1 in N implies $2 = F($1/2)) & ($1 in M implies $2 = G(($1-1)/2));
A3:for n ex r being Element of D() st X[n,r]
proof
let n be Element of NAT;
now assume A4: n in N;
reconsider r = F(n/2) as Element of D();
take r;
hereby assume n in M; then
A5: ex k be Nat st n = 2*k + 1 by A2;
ex m be Nat st n = 2*m by A1,A4;
hence contradiction by A5;
end;
end;
hence thesis;
end;
consider f being sequence of D() such that
A6: for n be Element of NAT holds X[n,f.n] from FUNCT_2:sch 3(A3);
reconsider f as sequence of D();
take f;
let n be Nat;
reconsider m = 2*n as Nat;
A7:m in NAT by ORDINAL1:def 12;
f.(2*n + 1) = G((2*n + 1 - 1)/2) by A6,A2;
hence f.(2*n) = F(n) & f.(2*n + 1) = G(n) by A1,A6,A7;
end;
theorem Th14:
for n be Nat holds ex k be Nat st n=2*k or n=2*k+1
proof
let n be Nat;
per cases;
suppose n is even; then
consider k be Nat such that
A1: n = 2*k;
take k;
thus n=2*k or n=2*k+1 by A1;
end;
suppose n is odd; then
n+1 is even; then
consider k1 be Nat such that
A2: n+1 = 2*k1;
0 <> k1 by A2;
then reconsider k=k1-1 as Nat;
take k;
thus n=2*k or n=2*k+1 by A2;
end;
end;
theorem Th15:
for A be non empty closed_interval Subset of REAL,
T0,T be DivSequence of A
holds ex T1 be DivSequence of A st
for i be Nat holds T1.(2*i) = T0.i & T1.(2*i+1) = T.i
proof
let A be non empty closed_interval Subset of REAL,
T0,T be DivSequence of A;
A1:dom T0 = NAT & dom T = NAT by FUNCT_2:def 1;
now let i be object;
assume i in NAT; then
reconsider i1=i as Nat;
rng (T0.i1) c= REAL;
hence T0.i in (REAL)* by FINSEQ_1:def 11;
end; then
reconsider S0=T0 as sequence of (REAL)* by A1,FUNCT_2:3;
now let i be object;
assume i in NAT; then
reconsider i1=i as Nat;
rng (T.i1) c= REAL;
hence T.i in (REAL)* by FINSEQ_1:def 11;
end; then
reconsider S=T as sequence of (REAL)* by A1,FUNCT_2:3;
deffunc F(Nat) = S0/.$1;
deffunc G(Nat) = S/.$1;
consider T1 being sequence of (REAL)* such that
A2: for n be Nat holds T1.(2*n) = F(n) & T1.(2*n+1) = G(n) from ExRealSeq2X;
A3:dom T1 = NAT by FUNCT_2:def 1;
now let i be object;
assume i in NAT; then
reconsider j=i as Nat;
consider k be Nat such that
A4: j=2*k or j=2*k+1 by Th14;
reconsider k as Element of NAT by ORDINAL1:def 12;
per cases by A4;
suppose j=2*k;
then T1.j = S0/.k by A2 .= T0.k;
hence T1.i in divs A by INTEGRA1:def 3;
end;
suppose j=2*k + 1;
then T1.j = S/.k by A2 .= T.k;
hence T1.i in divs A by INTEGRA1:def 3;
end;
end; then
reconsider T1 as DivSequence of A by A3,FUNCT_2:3;
take T1;
let i be Nat;
i in NAT by ORDINAL1:def 12; then
A5:i in dom S0 & i in dom S by FUNCT_2:def 1;
A6:T1.(2*i) = S0/.i by A2 .= T0.i by A5,PARTFUN1:def 6;
T1.(2*i+1) = S/.i by A2 .= T.i by A5,PARTFUN1:def 6;
hence thesis by A6;
end;
theorem Th16:
for A be non empty closed_interval Subset of REAL,
T0,T,T1 be DivSequence of A
st delta T0 is convergent & lim delta T0 = 0
& delta T is convergent & lim delta T = 0
& for i be Nat holds T1.(2*i) = T0.i & T1.(2*i+1) = T.i
holds delta T1 is convergent & lim delta T1 = 0
proof
let A be non empty closed_interval Subset of REAL,
T0,T,T1 be DivSequence of A;
assume that
A1: delta T0 is convergent & lim delta T0 = 0 and
A2: delta T is convergent & lim delta T = 0 and
A3: for i be Nat holds T1.(2*i) = T0.i & T1.(2*i+1) = T.i;
A4:now let p be Real;
assume A5: 0<p; then
consider n1 be Nat such that
A6: for m be Nat st n1 <= m holds |. (delta T0).m - 0 .|<p by A1,SEQ_2:def 7;
consider n2 be Nat such that
A7: for m be Nat st n2 <= m holds |. (delta T).m - 0 .|<p
by A5,A2,SEQ_2:def 7;
reconsider n3=max(n1,n2) as Nat by TARSKI:1;
A8: n1 <= n3 & n2 <= n3 by XXREAL_0:25;
reconsider n=2*n3+1 as Nat;
take n;
let m be Nat;
assume A9: n <= m;
consider k be Nat such that
A10: m=2*k or m=2*k+1 by Th14;
reconsider k1=k, m1=m as Element of NAT by ORDINAL1:def 12;
per cases by A10;
suppose A11: m=2*k;
(delta T1).m1 = delta(T1.m1) by INTEGRA3:def 2; then
(delta T1).m1 = delta(T0.k1) by A11,A3; then
A12: (delta T1).m1 = (delta T0).k1 by INTEGRA3:def 2;
A13: 2*n3 <= (2*k)-1 by XREAL_1:19,A9,A11;
2*k-1 < (2*k-1)+1 by XREAL_1:145; then
2*n3 <= 2*k by A13,XXREAL_0:2; then
2*n3/2 <= 2*k/2 by XREAL_1:72; then
n1 <= k by A8,XXREAL_0:2;
hence |. (delta T1).m - 0 .|<p by A12,A6;
end;
suppose A14: m=2*k+1;
(delta T1).m1 = delta(T1.m1) by INTEGRA3:def 2; then
(delta T1).m1 = delta(T.k1) by A14,A3; then
A15: (delta T1).m1 = (delta T).k1 by INTEGRA3:def 2;
(2*n3+1)-1 <= (2*k+1)-1 by XREAL_1:13,A9,A14; then
2*n3/2 <= 2*k/2 by XREAL_1:72; then
n2 <= k by A8,XXREAL_0:2;
hence |. (delta T1).m - 0 .|<p by A15,A7;
end;
end;
hence delta T1 is convergent by SEQ_2:def 6;
hence lim delta T1 = 0 by A4,SEQ_2:def 7;
end;
theorem Th17:
for X be RealNormSpace, A be non empty closed_interval Subset of REAL,
h be Function of A,the carrier of X, T0,T,T1 be DivSequence of A,
S0 be middle_volume_Sequence of h,T0,
S be middle_volume_Sequence of h,T
st for i be Nat holds T1.(2*i) = T0.i & T1.(2*i+1) = T.i
ex S1 be middle_volume_Sequence of h,T1
st for i be Nat holds S1.(2*i) = S0.i & S1.(2*i+1) = S.i
proof
let X be RealNormSpace, A be non empty closed_interval Subset of REAL,
h be Function of A,the carrier of X, T0,T,T1 be DivSequence of A,
S0 be middle_volume_Sequence of h,T0,
S be middle_volume_Sequence of h,T;
assume A1: for k be Nat holds T1.(2*k) = T0.k & T1.(2*k+1) = T.k;
reconsider SS0=S0, SS=S as sequence of (the carrier of X)*;
deffunc F(Nat) = SS0/.$1;
deffunc G(Nat) = SS/.$1;
consider S1 being sequence of (the carrier of X)* such that
A2: for n be Nat holds S1.(2*n) = F(n) & S1.(2*n+1) = G(n)
from ExRealSeq2X;
for i be Element of NAT holds S1.i is middle_volume of h,T1.i
proof
let i be Element of NAT;
consider k be Nat such that
A3: i=2*k or i=2*k+1 by Th14;
reconsider k as Element of NAT by ORDINAL1:def 12;
per cases by A3;
suppose A4: i=2*k;
then S1.i = SS0/.k by A2 .= S0.k;
hence S1.i is middle_volume of h,T1.i by A4,A1;
end;
suppose A5: i=2*k + 1; then
S1.i = SS/.k by A2 .= S.k;
hence S1.i is middle_volume of h,T1.i by A5,A1;
end;
end;
then reconsider S1 as middle_volume_Sequence of h,T1 by INTEGR18:def 3;
take S1;
let i be Nat;
i in NAT by ORDINAL1:def 12; then
A6:i in dom SS0 & i in dom SS by FUNCT_2:def 1;
A7:S1.(2*i) = SS0/.i by A2 .= S0.i by PARTFUN1:def 6,A6;
S1.(2*i+1) = SS/.i by A2 .= S.i by PARTFUN1:def 6,A6;
hence thesis by A7;
end;
theorem Th18:
for X be RealNormSpace, Sq0,Sq,Sq1 be sequence of X
st Sq1 is convergent
& for i be Nat holds Sq1.(2*i) = Sq0.i & Sq1.(2*i+1) = Sq.i
holds Sq0 is convergent & lim Sq0=lim Sq1
& Sq is convergent & lim Sq=lim Sq1
proof
let X be RealNormSpace, Sq0,Sq,Sq1 be sequence of X;
assume that
A1: Sq1 is convergent and
A2: for i be Nat holds Sq1.(2*i) = Sq0.i & Sq1.(2*i+1) = Sq.i;
A3:for r be Real st 0<r
ex m1 be Nat st for i be Nat st m1<=i holds ||. Sq0.i - lim Sq1 .|| <r
proof
let r be Real;
assume 0<r; then
consider m be Nat such that
A4: for n be Nat st m <= n holds
||. Sq1.n - lim Sq1 .||<r by A1,NORMSP_1:def 7;
consider k be Nat such that
A5: m=2*k or m=2*k+1 by Th14;
2*k+1 <= 2*k+1 +1 by NAT_1:11; then
A6:m <= 2*k +2 by A5,XREAL_1:31;
reconsider m1=k+1 as Nat;
take m1;
thus for i be Nat st m1 <= i holds ||. Sq0.i - lim Sq1 .|| <r
proof
let i be Nat;
assume m1 <= i;
then 2*m1 <= 2*i by XREAL_1:64;
then m <= 2*i by A6,XXREAL_0:2; then
||. Sq1.(2*i) - lim Sq1 .|| < r by A4;
hence ||. Sq0.i - lim Sq1 .|| < r by A2;
end;
end;
hence Sq0 is convergent;
hence lim Sq0=lim Sq1 by A3,NORMSP_1:def 7;
A7:for r be Real st 0<r
ex m1 be Nat st for i be Nat st m1<=i holds ||. Sq.i - lim Sq1 .|| <r
proof
let r be Real;
assume 0<r; then
consider m be Nat such that
A8: for n be Nat st m <= n holds
||. Sq1.n - lim Sq1 .||<r by A1,NORMSP_1:def 7;
consider k be Nat such that
A9: m=2*k or m=2*k+1 by Th14;
2*k+1 <= 2*k+1 +1 by NAT_1:11; then
A10:m <= 2*k +2 by A9,XREAL_1:31;
reconsider m1=k+1 as Nat;
take m1;
thus for i be Nat st m1 <= i holds ||. Sq.i - lim Sq1 .|| <r
proof
let i be Nat;
assume m1 <= i;
then 2*m1 <= 2*i by XREAL_1:64;
then m <= 2*i by A10,XXREAL_0:2;
then m <= 2*i+1 by XREAL_1:145; then
||. Sq1.(2*i+1) - lim Sq1 .|| < r by A8;
hence ||. Sq.i - lim Sq1 .|| < r by A2;
end;
end;
hence Sq is convergent;
hence lim Sq=lim Sq1 by NORMSP_1:def 7,A7;
end;
theorem
for X be RealBanachSpace, f be continuous PartFunc of REAL,the carrier of X
st a <= b & [' a,b '] c= dom f holds f is_integrable_on [' a,b ']
proof
let X be RealBanachSpace,
f be continuous PartFunc of REAL,the carrier of X;
set A = [' a,b '];
assume A1: a <= b & [' a,b '] c= dom f; then
reconsider h=f|A as Function of A,the carrier of X by Lm1;
A2: f|A is uniformly_continuous by A1,Th3;
consider T0 being DivSequence of A such that
A3: delta T0 is convergent & lim delta T0=0 by INTEGRA4:11;
set S0 = the middle_volume_Sequence of h,T0;
set I = lim middle_sum(h,S0);
for T being DivSequence of A,
S be middle_volume_Sequence of h,T
st delta T is convergent & lim delta T = 0
holds middle_sum(h,S) is convergent & lim middle_sum(h,S) = I
proof
let T be DivSequence of A, S be middle_volume_Sequence of h,T;
assume A4: delta T is convergent & lim delta T = 0;
hence middle_sum(h,S) is convergent by A2,Th13;
consider T1 be DivSequence of A such that
A5: for i be Nat holds
T1.(2*i) = T0.i & T1.(2*i+1) = T.i by Th15;
consider S1 be middle_volume_Sequence of h,T1 such that
A6: for i be Nat holds S1.(2*i) = S0.i & S1.(2*i+1) = S.i by A5,Th17;
delta T1 is convergent & lim delta T1 = 0 by A4,A5,A3,Th16; then
A7: middle_sum(h,S1) is convergent by A2,Th13;
A8: for i be Nat holds
(middle_sum(h,S1)).(2*i) = (middle_sum(h,S0)).i
& (middle_sum(h,S1)).(2*i+1) = (middle_sum(h,S)).i
proof
let i be Nat;
reconsider S1 as middle_volume_Sequence of h,T1;
(middle_sum(h,S1)).(2*i) = middle_sum(h,S1.(2*i))
& (middle_sum(h,S1)).(2*i+1) = middle_sum(h,S1.(2*i+1))
by INTEGR18:def 4; then
(middle_sum(h,S1)).(2*i) = middle_sum(h,S0.i)
& (middle_sum(h,S1)).(2*i+1) = middle_sum(h,S.i) by A6;
hence thesis by INTEGR18:def 4;
end;
lim middle_sum(h,S) = lim middle_sum(h,S1) by A7,A8,Th18;
hence lim middle_sum(h,S) = lim middle_sum(h,S0) by A7,A8,Th18;
end;
then h is integrable;
hence thesis;
end;