:: 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 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,
ORDINAL1, CARD_3, XREAL_0, 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, 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;
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;
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 0the carrier of X by A50;
hence q.z=0.X by A50,RLVECT_1:43;
end;
B521: p = <*>the carrier of X by A46;
B53:len q = len q;
now
let k be Nat, v be Element of X;
assume C1: k in dom q & v = q.k; then
q.k = 0.X by B511;
hence q.k = -v by C1;
end; then
Sum q = - Sum q by B53,RLVECT_1:40; then
Sum q = 0.X by RLVECT_1:19;
hence Sum p = Sum q by RLVECT_1:43,B521;
end;
then
A53: P[0];
thus for n be Nat holds P[n] from NAT_1:sch 2(A53,A1);
end;
definition
let A be Subset of REAL;
func xvol A -> Real equals :Defvol:
0 if A is empty otherwise vol A;
correctness;
end;
reserve n for Element of NAT;
reserve a,b for Real;
Lm3: 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 LmVOL1:
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 Defvol;
end;
suppose A = {};
hence 0 <= xvol A by Defvol;
end;
end;
theorem LmTh404a:
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
AS1: 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 AS1
.= Seg len p by INTEGRA1:def 7; then
A1: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 X0: k in dom q; then
X2: q.k = vol divset(D,k) by AS1;
k in dom D by X0,AS1,FINSEQ_1:def 3;
hence thesis by X2,INTEGRA1:19;
end;
then q = lower_volume ((chi (A,A)),D) by A1,FINSEQ_1:13;
hence thesis by INTEGRA1:23;
end;
theorem LmTh404b:
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
B2: <*>(the carrier of Y) = S & <*> REAL = q; then
(Sum q)*E = 0.Y by RLVECT_1:10,RVSUM_1:72;
hence thesis by B2,RLVECT_1:43;
end;
A2:now let i be Nat;
assume A3: P[i];
now let q be FinSequence of REAL, S be FinSequence of Y;
set S0=S|i, q0=q|i;
assume A4: 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;
A5: 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
A6: k in Seg i & k in dom S by RELAT_1:57; then
consider r be Real such that
A7: r = q.k & S.k= r * E by A4;
take r;
thus thesis by A7,A6,FUNCT_1:49;
end;
dom S = Seg(i+1) by A4,FINSEQ_1:def 3; then
consider r be Real such that
A8: r = q.(i+1) & S.(i+1)= r * E by A4,FINSEQ_1:4;
A9: 1 <= i + 1 & i + 1 <= len q by A4,NAT_1:11;
q = (q|i)^<*q/.(i+1)*> by A4,FINSEQ_5:21; then
q = q0^<*q.(i+1)*> by A9,FINSEQ_4:15; then
(Sum q)*E = (Sum q0 + q.(i+1))*E by RVSUM_1:74; then
A10: (Sum q)*E = (Sum q0)*E + q.(i+1)*E by RLVECT_1:def 6;
A11: i = len S0 & i = len q0 by FINSEQ_1:59,A4,NAT_1:11;
reconsider v=S.(i+1) as Point of Y by A8;
S0 = S| dom S0 by FINSEQ_1:def 3,A11; then
Sum S = Sum S0 + v by A4,A11,RLVECT_1:38;
hence Sum S = (Sum q)*E by A8,A3,A5,A11,A10;
end;
hence P[i+1];
end;
for i being Nat holds P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th2AX1:
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
A81:v = v1^<*v.(i+1)*> by A7,FINSEQ_4:15;
H6: lower_bound A <= lower_bound B & upper_bound B <= upper_bound A
by A4,SEQ_4:47,48;
C8: rng D c= A by INTEGRA1:def 2;
C801:rng D1 c= rng D by RELAT_1:70;
B6A:Seg i c= dom D by A5,FINSEQ_1:5,NAT_1:11;
B3: i = len D1 & i = len v1 by FINSEQ_1:59,A4,NAT_1:11; then
H9: dom v1 = Seg i by FINSEQ_1:def 3;
per cases;
suppose B1: i <> 0; then
B6: i in dom D by B6A,FINSEQ_1:3; then
consider A1,A2 be non empty closed_interval Subset of REAL such that
B7: A1=[.lower_bound A, D.i .] & A2=[. D.i, upper_bound A.]
& A = A1 \/ A2 by INTEGRA1:32;
for y be element st y in rng D1 holds y in A1
proof
let y be element;
assume B81: y in rng D1; then
y in A by C801,C8; then
y in [.lower_bound A, upper_bound A.] by INTEGRA1:4; then
consider y1 be Real such that
B82: y=y1 & lower_bound A <= y1 & y1 <= upper_bound A;
consider x be element such that
B83: x in dom D1 & y1=D1.x by B81,B82,FUNCT_1:def 3;
reconsider x as Nat by B83;
B84: x in Seg i by B3,FINSEQ_1:def 3,B83; then
B85A: x <= i by FINSEQ_1:1;
now assume x <> i; then
x < i by B85A,XXREAL_0:1;
hence D.x <= D.i by B6,B6A,B84,VALUED_0:def 13;
end; then
y1 <= D.i by B83,B84,FUNCT_1:49;
hence y in A1 by B82,B7;
end; then
B8: rng D1 c= A1;
B9: D1.i = D.i by B1,FINSEQ_1:3,FUNCT_1:49;
for e1,e2 being ext-real number st
e1 in dom D1 & e2 in dom D1 & e1 < e2 holds D1.e1 < D1.e2
proof
let e1, e2 being ext-real number;
assume B90: e1 in dom D1 & e2 in dom D1 & e1 < e2; then
B84: e1 in Seg i & e2 in Seg i by B3,FINSEQ_1:def 3; then
D1.e1=D.e1 & D1.e2=D.e2 by FUNCT_1:49;
hence thesis by B90,VALUED_0:def 13,B84,B6A;
end; then
reconsider D1 as non empty increasing FinSequence of REAL
by B3,B1,VALUED_0:def 13;
H1: A1 = [. lower_bound A1, upper_bound A1 .] by INTEGRA1:4; then
D1.(len D1) = upper_bound A1 by B3,B9,B7,INTEGRA1:5; then
reconsider D1 as Division of A1 by B8,INTEGRA1:def 2;
H2: 1 < i+1 by B1,NAT_1:16;
i+1 in dom D by A5,FINSEQ_1:4; then
H3: lower_bound divset(D,i+1) = D.(i+1-1)
& upper_bound divset(D,i+1) = D.(i+1) by H2,INTEGRA1:def 4; then
H4: B = [. lower_bound B, upper_bound B .]
& divset(D,i+1) = [. D.i, D.(i+1) .] by INTEGRA1:4;
H5: D.i <= D.(i+1) by H3,SEQ_4:11;
per cases;
suppose C1: upper_bound B <= D.i; then
[. lower_bound B, upper_bound B .]
c= [. lower_bound A, D.i .] by H6,XXREAL_1:34; then
C2: B c= A1 by B7,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 E1: k in dom v1; then
E2: k in Seg i & k in dom v by RELAT_1:57; then
E4: v.k = v1.k by FUNCT_1:49;
E4A: k in dom D & k in dom D1 by E1,E2,B3,A4,FINSEQ_3:29;
H7: 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
E42: 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 E4A,INTEGRA1:def 4;
lower_bound A = lower_bound A1 by B7,H1,INTEGRA1:5;
hence divset(D,k) = divset(D1,k) by E42,E2,H7,FUNCT_1:49;
end;
suppose E42A: k<>1; then
E42: 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 E4A,INTEGRA1:def 4;
F43: 1 <= k by E2,FINSEQ_1:1; then
k-1 in NAT by INT_1:5; then
reconsider k1=k-1 as Nat;
1 < k by E42A,F43,XXREAL_0:1; then
D.k1 = D1.k1 by E2,FINSEQ_3:12,FUNCT_1:49;
hence divset(D,k) = divset(D1,k) by E42,E2,H7,FUNCT_1:49;
end;
end;
hence thesis by A4,E2,E4;
end; then
E5: Sum v1 = vol B by A3,C2,B3;
C5: [. D.i, upper_bound B .] c= {D.i} by C1,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 C1,H5,XXREAL_0:2; then
C11: B /\ divset(D,i+1) c= {D.i} by C5,H4,XXREAL_1:143;
reconsider BD = B /\ divset(D,i+1) as real-bounded Subset of REAL
by XBOOLE_1:17,XXREAL_2:45;
C13: 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 Defvol;
hence xvol (B /\ divset(D,i+1)) <= xvol ({D.i}) by LmVOL1;
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;
C131: xvol BD = vol BD & xvol {D.i} = vol {D.i} by Defvol;
lower_bound Di <= lower_bound BD
& upper_bound BD <= upper_bound Di by C11,SEQ_4:47,48;
hence xvol (B /\ divset(D,i+1)) <= xvol {D.i} by C131,XREAL_1:13;
end;
end;
C141: vol {D.i} = upper_bound {D.i} - upper_bound {D.i} by SEQ_4:10;
0 <= xvol BD by LmVOL1; then
v.(i+1) = 0 by A6,C13,C141,Defvol; then
Sum v = vol B + 0 by E5,A81,RVSUM_1:74;
hence Sum v = vol B;
end;
suppose G1: D.i < upper_bound B;
per cases;
suppose D0: 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,G1,MEASURE5:def 3;
B1 \/ B2 = [. lower_bound B, upper_bound B .] by D0,G1,XXREAL_1:165;
then
C1A: B1 \/ B2 = B by INTEGRA1:4;
B1 = [. lower_bound B1, upper_bound B1 .]
& B2 = [. lower_bound B2, upper_bound B2 .] by INTEGRA1:4; then
C2: 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 E1: k in dom v1; then
E2: k in Seg i & k in dom v by RELAT_1:57; then
E3: v.k = xvol (B /\ divset(D,k)) by A4;
E4: v.k = v1.k by E2,FUNCT_1:49;
E4A: k in dom D & k in dom D1 by E1,E2,A4,B3,FINSEQ_3:29;
H7: 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;
E6: divset(D,k) = divset(D1,k)
proof
per cases;
suppose k=1; then
E42: 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 E4A,INTEGRA1:def 4;
lower_bound A = lower_bound A1 by H1,B7,INTEGRA1:5;
hence divset(D,k) = divset(D1,k) by E42,E2,H7,FUNCT_1:49;
end;
suppose E42A: k<>1; then
E42: 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 E4A,INTEGRA1:def 4;
F43: 1 <= k by E2,FINSEQ_1:1; then
k-1 in NAT by INT_1:5; then
reconsider k1=k-1 as Nat;
1 < k by E42A,F43,XXREAL_0:1; then
D.k1 = D1.k1 by E2,FINSEQ_3:12,FUNCT_1:49;
hence divset(D,k) = divset(D1,k) by E42,E2,H7,FUNCT_1:49;
end;
end; then
E7: B1 /\ divset(D1,k) c= B /\ divset(D,k) by C1A,XBOOLE_1:7,26;
for x be element st x in B /\ divset(D,k)
holds x in B1 /\ divset(D1,k)
proof
let x be element;
assume E71: x in B /\ divset(D,k); then
reconsider r=x as Real;
E72: x in B & x in divset(D,k) by E71,XBOOLE_0:def 4; then
E741: ex r0 be real number
st r=r0 & lower_bound B <=r0 & r0 <= upper_bound B by H4;
E761: ex r1 be real number
st r=r1 & lower_bound divset(D,k) <=r1
& r1 <= upper_bound divset(D,k) by H7,E72;
B85A: k <= i by E2,FINSEQ_1:1;
E77: now assume k <> i; then
k < i by B85A,XXREAL_0:1;
hence D.k <= D.i by B6,E4A,VALUED_0:def 13;
end;
k = 1 or k <> 1; then
upper_bound divset(D,k) <= D.i by E77,E4A,INTEGRA1:def 4;
then r <= D.i by E761,XXREAL_0:2;
then r in B1 by E741;
hence x in B1 /\ divset(D1,k) by XBOOLE_0:def 4,E6,E72;
end;
then B /\ divset(D,k) c= B1 /\ divset(D1,k);
hence thesis by E3,E4,E7,XBOOLE_0:def 10;
end; then
E5: Sum v1 = vol B1 by A3,B7,H6,XXREAL_1:34,B3;
B /\ divset(D,i+1) = B1 /\ divset(D,i+1) \/ B2 /\ divset(D,i+1)
by C1A,XBOOLE_1:23; then
B /\ divset(D,i+1)
= [. D.i, D.i .] \/ B2 /\ [. D.i, D.(i+1) .]
by H4,D0,H5,XXREAL_1:143; then
D8: 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 C2,SEQ_4:11; then
D9: [. 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 H5,XXREAL_1:165; then
D101: [. D.i, D.i .] \/ [. D.i, D.(i+1) .]
= divset(D,i+1) by H3,INTEGRA1:4;
F11: upper_bound B <= D.(i+1) by A4,H6,INTEGRA1:def 2;
for x be element st x in B2 holds x in divset(D,i+1)
proof
let x be element;
assume E71: x in B2; then
reconsider r=x as Real;
E721: ex r0 be real number
st r=r0 & D.i <= r0 & r0 <= upper_bound B by E71;
r <= D.(i+1) by F11,XXREAL_0:2,E721;
hence x in divset(D,i+1) by H4,E721;
end; then
D111: 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 D111,D101,D8,D9,XBOOLE_1:28; then
v.(i+1) = vol B2 by Defvol; then
Sum v = vol B1 + vol B2 by A81,RVSUM_1:74,E5;
hence Sum v = vol B by C2;
end;
suppose F0: D.i < lower_bound B; then
F1: [. 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 element;
assume E1: k0 in dom v1; then
E2: k0 in Seg i & k0 in dom v by RELAT_1:57;
reconsider k=k0 as Nat by E1;
E4A: k in dom D & k in dom D1 by E1,E2,A4,B3,FINSEQ_3:29;
H7: 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;
E5: divset(D,k) = divset(D1,k)
proof
per cases;
suppose k=1; then
E42: 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 E4A,INTEGRA1:def 4;
lower_bound A = lower_bound A1 by H1,B7,INTEGRA1:5;
hence divset(D,k) = divset(D1,k) by H7,E42,E2,FUNCT_1:49;
end;
suppose E42A: k<>1; then
E42: 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 E4A,INTEGRA1:def 4;
F43: 1 <= k by E2,FINSEQ_1:1; then
k-1 in NAT by INT_1:5; then
reconsider k1=k-1 as Nat;
1 < k by E42A,F43,XXREAL_0:1; then
D.k1 = D1.k1 by E2,FINSEQ_3:12,FUNCT_1:49;
hence divset(D,k) = divset(D1,k) by E42,E2,H7,FUNCT_1:49;
end;
end;
for x be element st x in B /\ divset(D,k)
holds x in B1 /\ divset(D1,k)
proof
let x be element;
assume E71: x in B /\ divset(D,k); then
reconsider r=x as Real;
E72: x in B & x in divset(D,k) by E71,XBOOLE_0:def 4; then
E741: (ex r0 be real number
st r=r0 & lower_bound B <=r0 & r0 <= upper_bound B)
& (ex r1 be real number
st r=r1 & lower_bound divset(D,k) <=r1
& r1 <= upper_bound divset(D,k)) by H4,H7;
k in Seg i by E1,RELAT_1:57; then
B85A: k <= i by FINSEQ_1:1;
E77: now assume k <> i; then
k < i by B85A,XXREAL_0:1;
hence D.k <= D.i by B6,E4A,VALUED_0:def 13;
end;
k = 1 or k <> 1; then
upper_bound divset(D,k) <= D.i by E77,E4A,INTEGRA1:def 4;
then r <= D.i by E741,XXREAL_0:2;
then r in B1 by E741;
hence x in B1 /\ divset(D1,k) by XBOOLE_0:def 4,E5,E72;
end; then
E61: B /\ divset(D,k) c= B1 /\ divset(D1,k);
v.k = xvol (B /\ divset(D,k)) by E2,A4; then
v.k0 = 0 by Defvol,F1,E61;
hence v1.k0 = 0 by E2,FUNCT_1:49;
end;
then v1 = dom v1 --> 0 by FUNCOP_1:11;
then v1 = i |-> 0 by H9,FINSEQ_2:def 2; then
F5: Sum v1 = 0 by RVSUM_1:81;
F11: upper_bound B <= D.(i+1) by A4,H6,INTEGRA1:def 2;
for x be element st x in B2 holds x in divset(D,i+1)
proof
let x be element;
assume E71: x in B2; then
reconsider r=x as Real;
B= [. lower_bound B, upper_bound B .] by INTEGRA1:4; then
ex r0 be real number
st r=r0 & lower_bound B <= r0 & r0 <= upper_bound B by E71; then
D.i <= r & r <= D.(i+1) by F11,XXREAL_0:2,F0;
hence x in divset(D,i+1) by H4;
end; then
F71: 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 F71,XBOOLE_1:28; then
v.(i+1) = vol B by Defvol; then
Sum v = 0 + vol B by A81,RVSUM_1:74,F5;
hence Sum v = vol B;
end;
end;
end;
suppose B1: i = 0; then
B4: D.1 = upper_bound A by A4,INTEGRA1:def 2;
dom D = Seg 1 by B1,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 B4,INTEGRA1:4; then
B51: divset(D,1) = A by INTEGRA1:4;
v.1 = xvol (B /\ divset(D,1)) by B1,A4,A5,FINSEQ_1:4; then
v.1 = xvol B by B51,A4,XBOOLE_1:28; then
B6: v.1 = vol B by Defvol;
Sum v = Sum v1 + v.1 by B1,A81,RVSUM_1:74; then
Sum v = 0 + vol B by B1,RVSUM_1:72,B6;
hence Sum v = vol B;
end;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
Th615:
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
X1:v=xseq.(len xseq) by PARTFUN1:def 6;
xseq| (len yseq) = xseq| dom (yseq) by FINSEQ_1:def 3;
hence thesis by A1,X1,RLVECT_1:38;
end;
theorem Th617:
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 X1: 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 X1,RLVECT_1:43;
hence thesis by RVSUM_1:72;
end;
A2:now let i be Nat;
assume A3: P[i];
now let xseq be FinSequence of Y, yseq be FinSequence of REAL;
set xseq0=xseq|i, yseq0=yseq|i;
assume
A4: 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.||);
A5: 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 B1: k in dom xseq0; then
A6: k in Seg i & k in dom xseq by RELAT_1:57; then
consider v be Point of Y such that
A7: v=xseq/.k & yseq.k=||.v.|| by A4;
take v;
xseq/.k = xseq.k by A6,PARTFUN1:def 6; then
xseq/.k = xseq0.k by A6,FUNCT_1:49;
hence thesis by A7,A6,B1,PARTFUN1:def 6,FUNCT_1:49;
end;
dom xseq = Seg(i+1) by A4,FINSEQ_1:def 3; then
consider w be Point of Y such that
A8: w=xseq/.(i+1) & yseq.(i+1)=||.w.|| by A4,FINSEQ_1:4;
A9: 1 <= i + 1 & i + 1 <= len yseq by A4,NAT_1:11;
yseq = (yseq|i)^<*yseq/.(i+1) *> by A4,FINSEQ_5:21; then
yseq = yseq0 ^<*(yseq.(i+1))*> by A9,FINSEQ_4:15; then
A10: Sum yseq = Sum yseq0 + yseq.(i+1) by RVSUM_1:74;
A11: i=len xseq0 by A4,FINSEQ_1:59,NAT_1:11; then
A12: ex v be Point of Y st v=xseq/.(len xseq)
& Sum xseq = Sum xseq0 + v by A4,Th615;
A13: ||. Sum xseq0 + w.||<= ||.Sum xseq0 .|| + ||. w .|| by NORMSP_1:def 1;
len xseq0 = len yseq0 by A4,A11,FINSEQ_1:59,NAT_1:11; then
||. Sum xseq0 .|| + ||. w .|| <= Sum yseq0 + yseq.(i+1)
by A8,XREAL_1:6,A3,A5,A11;
hence ||. Sum xseq .|| <= Sum yseq by A4,A8,A10,A12,A13,XXREAL_0:2;
end;
hence P[i+1];
end;
for i be Nat holds P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th2AX2:
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 .||;
A3: 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
A5: 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(A3);
A6: 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 A5;
end;
A7: len u = len p by A5,FINSEQ_1:def 3; then
A8: ||.Sum p.|| <= Sum u by A6,Th617;
set i = len p;
reconsider uu=u as Element of i-tuples_on REAL by A7,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
A10: j in dom p by FINSEQ_1:def 3; then
ex v be Point of Y st v = p/.j & u.j = ||. v .|| by A6;
hence uu.j <= qq.j by A10,A1;
end; then
Sum uu <= Sum qq by RVSUM_1:82;
hence thesis by A8,XXREAL_0:2;
end;
theorem Lm5:
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 Th2AX3:
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 AS1: delta(D) < r;
let i be Nat, s,t be Real;
assume AS2: i in dom D & s in divset(D,i) & t in divset(D,i); then
vol (divset (D,i)) <= delta D by Lm5; then
A3:upper_bound divset(D,i) - lower_bound divset(D,i) < r by AS1,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 AS2,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 Th2A:
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 0; then
B00A:0 < pp2 & pp2 < p by XREAL_1:215,216; then
B00B:0 < pv by VA0,XREAL_1:139; then
pv*(vol A) < pv *(vol A + 1) by XREAL_1:29,68; then
pv*(vol A) < pp2 by VA0,XCMPLX_1:87; then
B00C:pv*(vol A) < p by B00A,XXREAL_0:2;
set p2v = pv/2;
consider sk be Real such that
B01: 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 A0,B00B,XREAL_1:215;
consider k be Nat such that
K0: for i be Nat st k <= i holds |. (delta T).i - 0 .| < sk
by B01,A1,SEQ_2:def 7;
take k;
let n, m be Nat;
B2: 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 K0; then
|. delta(T.n) .| < sk & |. delta(T.m) .| < sk by INTEGRA3:def 2,B2; then
KTn: delta(T.n) < sk & delta(T.m) < sk by INTEGRA3:9,ABSVALUE:def 1;
B3: 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
B4: 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 C11,B2;
consider p2 be FinSequence of REAL such that
B5: 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 C12,B2;
defpred H1[element,element,element] 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;
B7Y: for x,y be element st x in Seg len(T.n) & y in Seg len (T.m)
ex w be element st w in the carrier of X & H1[x,y,w]
proof
let x,y be element;
assume AD1: 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,AD1;
then consider z be Point of X such that
AD2: z = (h|divset(T.n,i)).(p1.i)
& (S.n).i = (vol divset(T.n,i)) * z by B4;
(xvol (divset(T.n,i) /\ divset(T.m,j)))* z in the carrier of X;
hence thesis by AD2;
end;
consider Snm being Function of
[: Seg len (T.n),Seg len (T.m) :],the carrier of X such that
B7Z: for x,y be element 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(B7Y);
B7: 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 B7Z;
hence thesis;
end;
defpred P1[Nat,element] 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);
A71: for k be Nat st k in Seg len (T.n) ex x be element st P1[k,x]
proof
let k be Nat;
assume B71: k in Seg len (T.n);
deffunc G(set)= Snm.( k,$1 );
consider r being FinSequence such that
A72: len r = len (T.m) and
A73: for j be Nat st j in dom r holds r.j=G(j) from FINSEQ_1:sch 2;
A74: dom r = Seg len (T.m) by A72,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 B74: j in dom r; then
[k,j] in [: Seg len (T.n), Seg len (T.m) :]
by A74,B71,ZFMISC_1:87; then
Snm.(k,j) in the carrier of X by FUNCT_2:5;
hence thesis by A73,B74;
end;
then reconsider r as FinSequence of X by FINSEQ_2:12;
take x=Sum r;
thus thesis by A73,A74;
end;
consider Xp be FinSequence such that
B8X: 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(A71);
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 B8X;
hence thesis;
end;
then reconsider Xp as FinSequence of X by FINSEQ_2:12;
B82: len Xp = len (T.n) by FINSEQ_1:def 3,B8X;
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
B861: k in Seg len Xp & k in Seg len (T.n) by B82; then
B86: k in dom Xp & k in dom (T.n) by FINSEQ_1:def 3; then
consider z be Point of X such that
B87: z = (h|divset(T.n,k)).(p1.k)
& (S.n).k = (vol divset(T.n,k)) * z by B4;
consider r be FinSequence of X such that
B84: 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 B861,B8X;
defpred P11[Nat,set] means $2 = xvol (divset(T.n,k) /\ divset(T.m,$1));
XA14: 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
B92X: 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(XA14);
B92: 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 B92X,FINSEQ_1:def 3;
B94: len vtntm = len r & len (T.m) = len r by B84,B92X,FINSEQ_1:def 3; then
B95: Sum vtntm = vol (divset(T.n,k)) by Th2AX1,B92X,B86,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 B90: j in dom r; then
B99: 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 B7,B861,B84;
take vtntm.j;
r.j= (xvol (divset(T.n,k) /\ divset(T.m,j))) * z by B87,B99,B90,B84;
hence thesis by B92,B90;
end;
hence thesis by B87,B84,B95,LmTh404b,B94;
end; then
B101:Xp = S.n by INTEGR18:def 1,B82;
defpred P2[Nat,element] 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 );
A103:for k be Nat st k in Seg len (T.m) ex x be element st P2[k,x]
proof
let k be Nat;
assume B103: k in Seg len (T.m);
deffunc G(set)= Snm.($1,k);
consider s being FinSequence such that
A104: len s = len (T.n) and
A105: for i be Nat st i in dom s holds s.i=G(i) from FINSEQ_1:sch 2;
A106: dom s = Seg len (T.n) by A104,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 B106: i in dom s; then
[i,k] in [: Seg len (T.n), Seg len (T.m) :]
by A106,B103,ZFMISC_1:87; then
Snm.(i,k) in the carrier of X by FUNCT_2:5;
hence thesis by A105,B106;
end;
then reconsider s as FinSequence of X by FINSEQ_2:12;
take x = Sum s;
thus thesis by A105,A106;
end;
consider Xq be FinSequence such that
B9X: 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(A103);
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 B9X;
hence thesis;
end;
then reconsider Xq as FinSequence of X by FINSEQ_2:12;
defpred H2[element,element,element] 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;
B12Y:for x,y be element st x in Seg len (T.n) & y in Seg len (T.m)
ex w be element st w in the carrier of X & H2[x,y,w]
proof
let x,y be element;
assume AD1: 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,AD1;
then consider z be Point of X such that
AD2: z = (h|divset(T.m,j)).(p2.j)
& (S.m).j = (vol divset(T.m,j)) * z by B5;
(xvol (divset(T.n,i) /\ divset(T.m,j)))* z in the carrier of X;
hence thesis by AD2;
end;
consider Smn being Function of
[: Seg len (T.n),Seg len (T.m) :],the carrier of X such that
B12Z: for x,y be element 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(B12Y);
B12: 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 B12Z;
hence thesis;
end;
defpred P3[Nat,element] 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);
A103:for k be Nat st k in Seg len (T.m) ex x be element st P3[k,x]
proof
let k be Nat;
assume B103: k in Seg len (T.m);
deffunc G(set)= Smn.($1,k);
consider s being FinSequence such that
A104: len s = len (T.n) and
A105: for i be Nat st i in dom s holds s.i=G(i) from FINSEQ_1:sch 2;
A106: dom s = Seg len (T.n) by A104,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 B106: i in dom s; then
[i,k] in [: Seg len (T.n), Seg len (T.m) :]
by A106,B103,ZFMISC_1:87; then
Smn.(i,k) in the carrier of X by FUNCT_2:5;
hence thesis by A105,B106;
end;
then reconsider s as FinSequence of X by FINSEQ_2:12;
take x = Sum s;
thus thesis by A105,A106;
end;
consider Zq be FinSequence such that
B13X: 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(A103);
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 B13X;
hence thesis;
end;
then reconsider Zq as FinSequence of X by FINSEQ_2:12;
F82: len Zq = len (T.m) by FINSEQ_1:def 3,B13X;
for k be Nat st 1 <= k & k <= len Zq holds Zq.k = (S.m).k
proof
let k be Nat;
assume F860: 1 <= k & k <= len Zq; then
consider s be FinSequence of X such that
F84: 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 B13X,FINSEQ_3:25;
F89: k in Seg len (T.m) by F860,F82;
F86: k in dom (T.m) by F860,F82,FINSEQ_3:25; then
consider z be Point of X such that
F87: z = (h|divset((T.m),k)).(p2.k)
& (S.m).k = (vol divset((T.m),k)) * z by B5;
defpred P11[Nat,set] means
$2 = xvol (divset(T.n,$1) /\ divset(T.m,k));
XA14: 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
F92X: 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(XA14);
F94: dom vtntm = dom s & len vtntm = len s by F92X,FINSEQ_1:def 3;
F92: for j be Nat st j in dom vtntm holds
vtntm.j=xvol (divset(T.m,k) /\ divset(T.n,j)) by F92X;
len s = len (T.n) by F84,FINSEQ_1:def 3; then
F95: Sum vtntm = vol divset(T.m,k) by Th2AX1,F92,F94,F86,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 F90: j in dom s; then
F99: 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 B12,F89,F84;
take vtntm.j;
s.j= (xvol (divset(T.n,j) /\ divset(T.m,k)))* z by F87,F99,F90,F84;
hence thesis by F90,F92X,F94;
end;
hence thesis by F87,F84,F95,LmTh404b,F94;
end; then
Zq = S.m by INTEGR18:def 1,F82; then
B15: Sum(S.n) - Sum(S.m) = Sum Xq - Sum Zq by Th31,B8X,B9X,B101;
set XZq = Xq - Zq;
B17: dom XZq = dom Xq /\ dom Zq by VFUNCT_1:def 2; then
reconsider XZq = Xq - Zq as FinSequence by B9X,B13X,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,B9X,B13X; then
B16: Sum(S.n) - Sum(S.m) = Sum (XZq) by B15,INTEGR18:2;
G1: 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 G11: 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
G12: z1 = (h|divset(T.n,i)).(p1.i)
& Snm.(i,j) = (xvol (divset(T.n,i) /\ divset(T.m,j)))* z1 by B7;
consider z2 be Point of X such that
G22: z2 = (h|divset((T.m),j)).(p2.j)
& Smn.(i,j) = (xvol (divset(T.n,i) /\ divset(T.m,j))) * z2 by B12,G11;
G13: i in dom (T.n) & j in dom (T.m) by G11,FINSEQ_1:def 3; then
G14: p1.i in dom (h|divset(T.n,i))
& p2.j in dom (h|divset(T.m,j)) by B4,B5; then
p1.i in dom h /\ divset(T.n,i)
& p2.j in dom h /\ divset(T.m,j) by RELAT_1:61; then
G16: 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 G12,G22,G14,FUNCT_1:47; then
G15: z1 = h/.(p1.i) & z2 =h/.(p2.j) by G16,PARTFUN1:def 6;
per cases;
suppose C1:divset(T.n,i) /\ divset(T.m,j) = {}; then
C2: xvol (divset(T.n,i) /\ divset(T.m,j)) = (0 qua Real) by Defvol;
Snmij =0.X & Smnij = 0.X by G11,G12,G22,C1,Defvol,RLVECT_1:10;
hence ||. Snmij - Smnij .||
<= (xvol (divset(T.n,i) /\ divset(T.m,j))) * pv by C2;
end;
suppose divset(T.n,i) /\ divset(T.m,j) <> {}; then
consider t be element such that
NC20: t in divset(T.n,i) /\ divset(T.m,j) by XBOOLE_0:def 1;
reconsider t as Real by NC20;
NC21: dom h = A by FUNCT_2:def 1;
NC41: divset(T.m,j) c= A by G13,INTEGRA1:8;
NC2: t in divset(T.n,i) & t in divset(T.m,j) by NC20,XBOOLE_0:def 4; then
|. (p1.i)-t .| < sk & |. t-(p2.j) .| < sk by G13,G16,Th2AX3,KTn; then
NC5: ||. h/.(p1.i)-h/.t .|| < p2v
& ||. h/.t-h/.(p2.j) .|| < p2v by NC41,NC2,NC21,G16,B01;
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 G11,G12,G15,G22,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
NC7: ||. 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
NC7X: ||. (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 LmVOL1,ABSVALUE:def 1;
0<= xvol DMN by LmVOL1; then
||. (xvol DMN) * (h/.(p1.i) - h/.t) .|| <= (xvol DMN) * p2v
& ||. (xvol DMN) * (h/.t - h/.(p2.j)) .|| <= (xvol DMN) * p2v
by NC7X,NC5,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 NC7,XXREAL_0:2;
end;
end;
VB1: for j be Nat st j in dom XZq
holds ||. XZq/.j .|| <= vol divset(T.m,j) * pv
proof
let j be Nat;
assume A1: j in dom XZq; then
A2: XZq/.j = Xq/.j - Zq/.j by VFUNCT_1:def 2;
A5: Xq/.j = Xq.j & Zq/.j = Zq.j by A1,B13X,B9X,B17,PARTFUN1:def 6;
A1D: dom XZq = dom Xq /\ dom Zq by VFUNCT_1:def 2;
consider Xsq be FinSequence of X such that
A6: 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 A1,B9X,B13X,B17;
consider Zsq be FinSequence of X such that
A7: 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 A1,B13X,B9X,B17;
set XZsq = Xsq - Zsq;
A8: dom XZsq = dom Xsq /\ dom Zsq by VFUNCT_1:def 2; then
reconsider XZsq as FinSequence by A6,A7,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));
XA14: 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
F92X: 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(XA14);
F92: for i be Nat st i in dom vtntm holds
vtntm.i=xvol ( divset(T.m,j) /\ divset(T.n,i)) by F92X;
F94: len vtntm = len XZsq by F92X,FINSEQ_1:def 3;
F94X: len XZsq = len (T.n) by A6,A7,A8,FINSEQ_1:def 3;
reconsider pvtntm = pv*vtntm as FinSequence of REAL;
j in dom (T.m) by A1,A1D,B9X,B13X,FINSEQ_1:def 3; then
divset(T.m,j) c= A by INTEGRA1:8; then
Sum vtntm = vol divset(T.m,j) by Th2AX1,
F92,F94,A6,A7,A8,FINSEQ_1:def 3; then
F95X: 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 A6,A7,A8,F92X,FINSEQ_1:def 3; then
F94Y: 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 A10: i in dom XZsq; then
A11: XZsq/.i = Xsq/.i - Zsq/.i by VFUNCT_1:def 2;
Xsq/.i = Xsq.i & Zsq/.i = Zsq.i by PARTFUN1:def 6,A10,A7,A8,A6; then
A13: Xsq/.i =Snm.(i,j) & Zsq/.i =Smn.(i,j) by A10,A6,A8,A7;
dom vtntm = dom XZsq by F92X,FINSEQ_1:def 3; then
pv*(vtntm.i) = pv* (xvol (divset(T.n,i) /\ divset(T.m,j)))
by F92X,A10; then
(pv(#)vtntm).i = pv* (xvol (divset(T.n,i) /\ divset(T.m,j)))
by VALUED_1:6;
hence thesis by A11,A13,G1,A10,A6,A7,A8,A1,A1D,B9X,B13X;
end; then
XX1: ||. Sum XZsq .|| <= vol (divset(T.m,j)) * pv by F95X,Th2AX2,F94X,F94Y;
len Xsq = len Zsq by FINSEQ_3:29,A6,A7;
hence thesis by A2,A5,A6,A7,XX1,INTEGR18:2;
end;
defpred P12[Nat,set] means $2 = vol (divset(T.m,$1));
XA14: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
FF92X: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(XA14);
FF94X:len XZq = len (T.m) by B9X,B13X,B17,FINSEQ_1:def 3;
XA13:Seg len XZq = dom XZq by FINSEQ_1:def 3;
FF95A:Sum vtm = vol A by FF92X,LmTh404a,FF94X;
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 B9X,B13X,B17,FF92X,FINSEQ_1:def 3; then
XXA14:len pvtm = len (T.m) by FINSEQ_1:def 3;
FF95:Sum pvtm = pv * vol A by RVSUM_1:87,FF95A;
for j be Nat st j in dom XZq holds ||. XZq/.j .|| <= pvtm.j
proof
let j be Nat;
assume A1: j in dom XZq; then
vtm.j= vol (divset(T.m,j)) by FF92X,XA13;
then pvtm.j= vol (divset(T.m,j)) * pv by VALUED_1:6;
hence ||. XZq/.j .|| <= pvtm.j by A1,VB1;
end;
then ||. Sum XZq .|| <= (vol A) * pv by FF95,FF94X,XXA14,Th2AX2;
hence ||.(middle_sum(h,S).n) - (middle_sum(h,S).m).|| < p
by B3,B16,XXREAL_0:2,B00C;
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
A7: 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;
a3:m in NAT by ORDINAL1:def 12;
f.(2*n + 1) = G((2*n + 1 - 1)/2) by A7,A2;
hence f.(2*n) = F(n) & f.(2*n + 1) = G(n) by A1,A7,a3;
end;
theorem Lm2F:
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
A3: n+1 = 2*k1;
0 <> k1 by A3;
then reconsider k=k1-1 as Nat;
take k;
thus n=2*k or n=2*k+1 by A3;
end;
end;
theorem Lm2B:
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 element;
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 element;
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
P1: for n be Nat holds T1.(2*n) = F(n) & T1.(2*n+1) = G(n) from ExRealSeq2X;
A2:dom T1 = NAT by FUNCT_2:def 1;
now let i be element;
assume i in NAT; then
reconsider j=i as Nat;
consider k be Nat such that
P3: j=2*k or j=2*k+1 by Lm2F;
reconsider k as Element of NAT by ORDINAL1:def 12;
per cases by P3;
suppose j=2*k;
then T1.j = S0/.k by P1 .= T0.k;
hence T1.i in divs A by INTEGRA1:def 3;
end;
suppose j=2*k + 1;
then T1.j = S/.k by P1 .= T.k;
hence T1.i in divs A by INTEGRA1:def 3;
end;
end; then
reconsider T1 as DivSequence of A by A2,FUNCT_2:3;
take T1;
let i be Nat;
i in NAT by ORDINAL1:def 12; then
AB:i in dom S0 & i in dom S by FUNCT_2:def 1;
a1:T1.(2*i) = S0/.i by P1 .= T0.i by AB,PARTFUN1:def 6;
T1.(2*i+1) = S/.i by P1 .= T.i by AB,PARTFUN1:def 6;
hence thesis by a1;
end;
theorem Lm2C:
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;
B1:now let p be Real;
assume A4: 0