:: The Basic Existence Theorem of Riemann-Stieltjes Integral
:: by Kazuhisa Nakasho , Keiko Narita and Yasunari Shidama
::
:: Received October 18, 2016
:: Copyright (c) 2016-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 NUMBERS, INTEGRA1, SUBSET_1, FUNCT_1, FINSEQ_1, NAT_1, RELAT_1,
MEASURE7, XBOOLE_0, XXREAL_2, XXREAL_0, SEQ_4, CARD_1, REAL_1, ARYTM_3,
ARYTM_1, CARD_3, FINSEQ_2, INTEGRA2, SEQ_1, SEQ_2, ORDINAL2, COMPLEX1,
XXREAL_1, FUNCT_3, PARTFUN1, TARSKI, FINSET_1, INTEGR15, MEASURE5,
FUNCT_7, INTEGR22, VALUED_0, ZFMISC_1, FCONT_2, ORDINAL4, FUNCOP_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1,
FUNCT_2, FUNCOP_1, BINOP_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, VALUED_0, COMPLEX1, XXREAL_2, FINSEQ_1, FINSEQ_2, SEQ_1,
SEQ_2, RVSUM_1, SEQ_4, RCOMP_1, FCONT_1, FCONT_2, MEASURE5, INTEGRA1,
INTEGRA2, INTEGRA3, INTEGR22;
constructors REAL_1, FINSEQOP, MONOID_0, SEQ_4, NAT_D, FCONT_1, FCONT_2,
RELSET_1, SEQ_2, INTEGRA3, COMSEQ_2, INTEGR22;
registrations NUMBERS, XREAL_0, INTEGRA1, NAT_1, MEMBERED, ORDINAL1, FCONT_1,
VALUED_0, RELSET_1, CARD_1, MEASURE5, FINSEQ_1, RVSUM_1, FINSET_1, SEQ_4,
FINSEQ_2, RELAT_1, SEQM_3, INT_1, XXREAL_2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
equalities XBOOLE_0, RCOMP_1, BINOP_1, FINSEQ_1, FINSEQ_2;
expansions FINSEQ_1, MEMBERED;
theorems XBOOLE_0, XBOOLE_1, XREAL_0, INTEGRA1, INTEGRA4, XXREAL_2, XXREAL_0,
RELAT_1, XCMPLX_1, ORDINAL1, XREAL_1, SEQ_4, SEQ_2, FINSEQ_1, FINSEQ_2,
RVSUM_1, FUNCT_1, FUNCT_2, PARTFUN1, VALUED_1, ZFMISC_1, TARSKI,
COMPLEX1, FINSEQ_3, XXREAL_1, SUBSET_1, VALUED_0, NAT_1, FCONT_2,
INTEGR20, FINSEQ_4, FINSEQ_5, INTEGRA3, ABSVALUE, INT_1, FUNCOP_1,
INTEGR22;
schemes FUNCT_2, FINSEQ_1, NAT_1, INTEGR20, BINOP_1;
begin :: 1. Preliminaries
theorem Th1:
for E be Real, q be FinSequence of REAL, S be FinSequence of REAL
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 E be Real;
defpred P[Nat] means
for q be FinSequence of REAL, S be FinSequence of REAL
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 REAL;
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
<*> REAL = S & <*> REAL = q;
hence thesis by RVSUM_1:72;
end;
A3: now
let i be Nat;
assume
A4: P[i];
now
let q be FinSequence of REAL, S be FinSequence of REAL;
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 A7,A8,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;
A12: i = len S0 & i = len q0 by A5,FINSEQ_1:59,NAT_1:11;
reconsider v=S.(i+1) as Real;
S = (S|i)^<* S/.len S *> by A5,FINSEQ_5:21; then
S = S0^<* v *> by A5,A10,FINSEQ_4:15; then
Sum S = Sum S0 + v by RVSUM_1:74;
hence Sum S = (Sum q)*E by A4,A6,A9,A11,A12;
end;
hence P[i+1];
end;
for i being Nat holds P[i] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
Lm1:
for xseq,yseq be FinSequence of REAL
st len xseq = len yseq + 1
& xseq | (len yseq) = yseq holds
ex v be Real st v = xseq.(len xseq) & Sum xseq = Sum yseq + v
proof
let xseq,yseq be FinSequence of REAL;
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
v = xseq/.(len xseq) by PARTFUN1:def 6; then
xseq = (xseq| (len yseq))^<* v *> by A1,FINSEQ_5:21;
hence thesis by A1,RVSUM_1:74;
end;
theorem Th2:
for xseq, 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 Real st v = xseq.i & yseq.i = |.v.|)
holds |.Sum xseq.| <= Sum yseq
proof
defpred P[Nat] means
for xseq, 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 Real st v = xseq.i & yseq.i = |.v.|)
holds |.Sum xseq.| <= Sum yseq;
A1: P[0]
proof
let xseq be FinSequence of REAL, 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 Real st v = xseq.i & yseq.i = |.v.|); then
<*>(REAL) = xseq; then
Sum xseq = 0 & <*>(REAL) = yseq by A2,RVSUM_1:72;
hence thesis by COMPLEX1:44,RVSUM_1:72;
end;
A3: now
let i be Nat;
assume
A4: P[i];
now
let xseq be FinSequence of REAL, 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 Real st v=xseq.i & yseq.i=|.v.|;
A6: for k be Element of NAT st k in dom xseq0 holds
ex v be Real st v=xseq0.k & yseq0.k=|.v.|
proof
let k be Element of NAT;
assume k in dom xseq0; then
A8: k in Seg i & k in dom xseq by RELAT_1:57; then
consider v be Real such that
A9: v=xseq.k & yseq.k=|.v.| by A5;
take v;
thus thesis by A8,A9,FUNCT_1:49;
end;
dom xseq = Seg(i+1) by A5,FINSEQ_1:def 3; then
consider w be Real 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 Real st v=xseq.(len xseq)
& Sum xseq = Sum xseq0 + v by A5,Lm1;
A15: |. Sum xseq0 + w.|<= |.Sum xseq0 .| + |. w .| by COMPLEX1:56;
len xseq0 = len yseq0 by A5,A13,FINSEQ_1:59,NAT_1:11; then
|. Sum xseq0 .| + |. w .| <= Sum yseq0 + yseq.(i+1)
by A4,A6,A10,A13,XREAL_1:6;
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 Th3:
for p,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 p, 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 Real 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 by XREAL_0:def 1;
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 Real 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 Real 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,Th2;
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 Real st v = p.j & u.j = |. v .| by A4;
hence uu.j <= qq.j by A1,A7;
end; then
Sum uu <= Sum qq by RVSUM_1:82;
hence thesis by A6,XXREAL_0:2;
end;
theorem Th4:
for n be Nat, a be object holds len (n |-> a) = n
proof
let n be Nat, a be object;
set x = n |-> a;
dom x = Seg len x by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:6,FUNCOP_1:13;
end;
theorem Th5:
for p be FinSequence, a be object holds
p = (len p) |-> a
iff (for k be object st k in dom p holds p.k = a)
proof
let p be FinSequence, a be object;
thus p = (len p) |-> a implies
for k be object st k in dom p holds p.k = a
proof
assume
A2: p = (len p) |-> a;
let k be object;
assume k in dom p; then
k in Seg len p by FINSEQ_1:def 3;
hence thesis by A2,FINSEQ_2:57;
end;
assume for k be object st k in dom p holds p.k = a; then
p = dom p --> a by FUNCOP_1:11;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th8:
for p be FinSequence of REAL,
i be Nat,
r be Real
st i in dom p & p.i = r
& for k be Nat st k in dom p & k <> i holds p.k = 0
holds Sum p = r
proof
defpred P[Nat] means
for p be FinSequence of REAL,
i be Nat,
r be Real
st len p = $1
& i in dom p & p.i = r
& (for k be Nat st k in dom p & k <> i holds p.k = 0)
holds Sum p = r;
A1: P[0]
proof
let p be FinSequence of REAL,
i be Nat,
r be Real;
assume that
A2: len p = 0 and
A3: i in dom p and
p.i = r and
for k be Nat st k in dom p & k <> i holds p.k = 0;
p = <*>REAL by A2;
hence thesis by A3;
end;
A4: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A5: P[n];
P[n+1]
proof
let p be FinSequence of REAL,
i be Nat,
r be Real;
assume that
A6: len p = n+1 and
A7: i in dom p and
A8: p.i = r and
A9: for k be Nat st k in dom p & k <> i holds p.k = 0;
consider q be FinSequence of REAL, a be Element of REAL such that
A10: p = q ^ <*a*> by A6,FINSEQ_2:19;
A11: len p = len q + 1 by A10,FINSEQ_2:16;
A12: 1 <= i <= n+1 by A6,A7,FINSEQ_3:25;
per cases;
suppose
A13: i <> n+1; then
1 <= i < n+1 by A12,XXREAL_0:1; then
A14: 1 <= i <= n by INT_1:7;
A15: q.i = r
proof
q = p | dom q by A10,FINSEQ_1:21;
hence thesis by A6,A8,A11,A14,FUNCT_1:47,FINSEQ_3:25;
end;
A17: for k be Nat st k in dom q & k <> i holds q.k = 0
proof
let k be Nat;
assume that
A18: k in dom q and
A19: k <> i;
A20: dom q c= dom p by A10,FINSEQ_1:26;
q.k = p.k by A10,A18,FINSEQ_1:def 7
.= 0 by A9,A18,A19,A20;
hence thesis;
end;
A21: 1 <= n+1 <= n+1 by XREAL_1:31;
a = p.(n+1) by A6,A10,A11,FINSEQ_1:42
.= 0 by A6,A9,A13,A21,FINSEQ_3:25; then
Sum p = Sum q + 0 by A10,RVSUM_1:74
.= r by A5,A6,A11,A14,A15,A17,FINSEQ_3:25;
hence thesis;
end;
suppose
A22: i = n+1;
for k be object st k in dom q holds q.k = 0
proof
let k be object;
assume
A23: k in dom q; then
reconsider k as Nat;
A24: 1 <= k <= n by A6,A11,A23,FINSEQ_3:25;
A25: dom q c= dom p by A10,FINSEQ_1:26;
A26: k+0 < n+1 by A24,XREAL_1:8;
q.k = p.k by A10,A23,FINSEQ_1:def 7
.= 0 by A9,A22,A23,A25,A26;
hence thesis;
end; then
A27: q = n |-> (0 qua Real) by A6,A11,Th5;
A28: a = r by A6,A8,A10,A11,A22,FINSEQ_1:42;
Sum p = Sum q + a by A10,RVSUM_1:74
.= 0 + r by A27,A28,RVSUM_1:81;
hence thesis;
end;
end;
hence thesis;
end;
A29: for k be Nat holds P[k] from NAT_1:sch 2(A1,A4);
let p be FinSequence of REAL,
i be Nat,
r be Real;
assume
A30: i in dom p & p.i = r
& for k be Nat st k in dom p & k <> i holds p.k = 0;
len p is Nat;
hence thesis by A29,A30;
end;
theorem Th9:
for p,q be FinSequence of REAL
st len p <= len q
& for i be Nat st i in dom q holds
(i <= len p implies q.i = p.i)
& (len p < i implies q.i = 0)
holds Sum q = Sum p
proof
let p,q be FinSequence of REAL;
assume that
A1: len p <= len q and
A2: for i be Nat st i in dom q holds
(i <= len p implies q.i = p.i)
& (len p < i implies q.i = 0);
len q - len p is Nat by A1,NAT_1:21; then
consider ix be Nat such that
A3: ix = len q - len p;
set x = ix |-> (0 qua Real);
A5: Sum x = 0 by RVSUM_1:81;
q = p ^ x
proof
A6: len x = ix by Th4; then
A7: len q = len p + len x by A3;
A8: dom q = Seg(len p + len x) by A3,A6,FINSEQ_1:def 3;
A9: for i be Nat st i in dom p holds q.i = p.i
proof
let i be Nat;
assume i in dom p; then
A10: 1 <= i <= len p by FINSEQ_3:25; then
1 <= i <= len q by A1,XXREAL_0:2; then
i in dom q by FINSEQ_3:25;
hence thesis by A2,A10;
end;
for i be Nat st i in dom x holds q.(len p + i) = x.i
proof
let i be Nat;
assume i in dom x; then
A11: i in Seg ix by FUNCOP_1:13; then
A12: x.i = 0 by FINSEQ_2:57;
consider j be Nat such that
A13: j = len p + i;
A14: i >= 1 by A11,FINSEQ_1:1; then
A15: len p < j by A13,NAT_1:19;
A16: 0+1 <= j by A13,A14,INT_1:7;
i <= len x by A6,A11,FINSEQ_1:1; then
j <= len q by A7,A13,XREAL_1:6; then
j in dom q by A16,FINSEQ_3:25;
hence thesis by A2,A12,A13,A15;
end;
hence thesis by A8,A9,FINSEQ_1:def 7;
end; then
Sum q = Sum p + Sum x by RVSUM_1:75
.= Sum p by A5;
hence thesis;
end;
theorem Th10:
for a,b,c,d be Real st b <= c holds [.a,b.] /\ [.c,d.] c= [.b,b.]
proof
let a,b,c,d be Real;
assume
A1: b <= c;
per cases;
suppose
A2: a <= b;
per cases;
suppose c <= d; then
b <= d by A1,XXREAL_0:2; then
[.a,b.] /\ [.b,d.] = [.b,b.] by A2,XXREAL_1:143;
hence [.a,b.] /\ [.c,d.] c= [.b,b.] by A1,XBOOLE_1:26,XXREAL_1:34;
end;
suppose d < c; then
[.c,d.] = {} by XXREAL_1:29;
hence [.a,b.] /\ [.c,d.] c= [.b,b.];
end;
end;
suppose b < a; then
[.a,b.] = {} by XXREAL_1:29;
hence [.a,b.] /\ [.c,d.] c= [.b,b.];
end;
end;
theorem Th11:
for a be Real, A be Subset of REAL,
rho be real-valued Function st A c= [.a,a.]
holds vol(A,rho) = 0
proof
let a be Real, A be Subset of REAL,
rho be real-valued Function;
assume A c= [.a,a.]; then
A c= {a} by XXREAL_1:17; then
per cases by ZFMISC_1:33;
suppose A = {};
hence vol(A,rho) = 0 by INTEGR22:def 1;
end;
suppose A = {a};
hence vol(A,rho)
= rho.(upper_bound {a}) - rho.(lower_bound {a}) by INTEGR22:def 1
.= rho.(upper_bound {a}) - rho.(upper_bound {a}) by SEQ_4:10
.= 0;
end;
end;
theorem Th12:
for s be non empty increasing FinSequence of REAL,
m be Nat
st m in dom s
holds s|m is non empty increasing FinSequence of REAL
proof
let s be non empty increasing FinSequence of REAL,
m be Nat;
assume a0: m in dom s; then
1 <= m <= len s by FINSEQ_3:25; then
len(s|m) = m by FINSEQ_1:59;
hence thesis by a0,FINSEQ_3:25;
end;
theorem Th13:
for s,t be non empty increasing FinSequence of REAL st s.(len s) < t.1
holds s^t is non empty increasing FinSequence of REAL
proof
let s,t be non empty increasing FinSequence of REAL;
assume
A1: s.(len s) < t.1;
set H = s^t;
A2: len H = len s + len t by FINSEQ_1:22;
for e1,e2 be ExtReal st e1 in dom H & e2 in dom H & e1 < e2
holds H.e1 < H.e2
proof
let e1,e2 be ExtReal;
assume
A3: e1 in dom H & e2 in dom H & e1 < e2; then
reconsider ie1 = e1,ie2 = e2 as Nat;
A5: 1 <= ie1 <= len s + len t
& 1 <= ie2 <= len s + len t by A2,A3,FINSEQ_3:25;
per cases;
suppose
A6: ie2 <= len s; then
A7: ie1 <= len s by A3,XXREAL_0:2;
A8: ie1 in dom s & ie2 in dom s by A5,A6,A7,FINSEQ_3:25; then
H.e1 = s.e1 & H.e2 = s.e2 by FINSEQ_1:def 7;
hence H.e1 < H.e2 by A3,A8,VALUED_0:def 13;
end;
suppose
A9: len s < ie2;
per cases;
suppose
A10: len s < ie1; then
a10: len s < ie2 by A3,XXREAL_0:2;
A11: not ie1 in dom s & not ie2 in dom s by A10,FINSEQ_3:25,a10; then
consider n1 being Nat such that
A12: n1 in dom t & ie1 = (len s) + n1 by A3,FINSEQ_1:25;
consider n2 being Nat such that
A13: n2 in dom t & ie2 = (len s) + n2 by A3,A11,FINSEQ_1:25;
A14: H.e1 = t.n1 by A12,FINSEQ_1:def 7;
A15: H.e2 = t.n2 by A13,FINSEQ_1:def 7;
ie1 - (len s) < ie2 -(len s) by A3,XREAL_1:14;
hence H.e1 < H.e2 by A12,A13,A14,A15,VALUED_0:def 13;
end;
suppose
A16: ie1 <= len s;
not ie2 in dom s by FINSEQ_3:25,A9; then
consider n2 being Nat such that
A17:n2 in dom t & ie2 = (len s) + n2 by A3,FINSEQ_1:25;
A18: 1<=n2 <= len t by A17,FINSEQ_3:25;
1 <= len t by A18,XXREAL_0:2; then
1 in dom t by FINSEQ_3:25; then
A19: t.1 <= t.n2 by A17,A18,VALUED_0:def 15;
A20: H.e2 = t.n2 by A17,FINSEQ_1:def 7;
A21: ie1 in dom s by A5,A16,FINSEQ_3:25; then
A22: H.e1 = s.ie1 by FINSEQ_1:def 7;
len s in Seg len s by FINSEQ_1:3; then
len s in dom s by FINSEQ_1:def 3; then
s.ie1 <= s.(len s) by A16,A21,VALUED_0:def 15; then
s.ie1 < t.1 by A1,XXREAL_0:2;
hence H.e1 < H.e2 by A19,A20,A22,XXREAL_0:2;
end;
end;
end;
hence thesis by VALUED_0:def 13;
end;
theorem Th14:
for s be non empty increasing FinSequence of REAL,
a be Real
st s.(len s) < a
holds s^<*a*> is non empty increasing FinSequence of REAL
proof
let s be non empty increasing FinSequence of REAL,
a be Real;
assume
A1: s.(len s) < a;
reconsider a0 = a as Element of REAL by XREAL_0:def 1;
reconsider t = <*a0*> as non empty increasing FinSequence of REAL;
s.(len s) < t.1 by A1;
hence thesis by Th13;
end;
theorem Th15:
for T be FinSequence of REAL, n,m be Nat
st n+1 < m <= len T holds
ex TM1 be FinSequence of REAL
st len TM1 = m-(n+1) & rng TM1 c= rng T
& for i be Nat st i in dom TM1 holds TM1.i = T.(i+n)
proof
let T be FinSequence of REAL, n,m be Nat;
assume
A1: n+1 < m <= len T;
deffunc F(Nat) = T.($1+n);
m-(n+1) in NAT by A1,INT_1:5; then
reconsider m1 = m-(n+1) as Nat;
consider p being FinSequence such that
A2: len p = m1
& for k being Nat st k in dom p holds p.k = F(k) from FINSEQ_1:sch 2;
A3: rng p c= rng T
proof
let x be object;
assume x in rng p; then
consider i be object such that
A4: i in dom p & x = p.i by FUNCT_1:def 3;
reconsider i as Nat by A4;
A6: p.i = T.(i+n) by A2,A4;
A7: 1 <= i <= m1 by A2,FINSEQ_3:25,A4;
A8: i + n <= m1 + n by A7,XREAL_1:6;
m - 1 <= m - 0 by XREAL_1:10; then
m - 1 <= len T by A1,XXREAL_0:2; then
A9: i + n <= len T by A8,XXREAL_0:2;
1 + 0 <= i + n by A7,XREAL_1:7; then
i+n in dom T by FINSEQ_3:25,A9;
hence thesis by A4,A6,FUNCT_1:3;
end; then
reconsider p as FinSequence of REAL by FINSEQ_1:def 4,XBOOLE_1:1;
take p;
thus len p = m-(n+1) by A2;
thus rng p c= rng T by A3;
let i be Nat;
assume i in dom p;
hence thesis by A2;
end;
theorem Th16:
for T be non empty increasing FinSequence of REAL, n,m be Nat
st n+1 < m <= len T holds
ex TM1 be non empty increasing FinSequence of REAL
st len TM1 = m-(n+1) & rng TM1 c= rng T
& for i be Nat st i in dom TM1 holds TM1.i = T.(i+n)
proof
let T be non empty increasing FinSequence of REAL, n,m be Nat;
assume
A1: n+1 < m <= len T; then
consider p be FinSequence of REAL such that
A2: len p = m-(n+1) & rng p c= rng T
& for i be Nat st i in dom p holds p.i = T.(i+n) by Th15;
m-(n+1) in NAT by A1,INT_1:5; then
reconsider m1 = m-(n+1) as Nat;
len p <> 0 by A1,A2; then
reconsider p as non empty FinSequence of REAL;
for e1,e2 be ExtReal st e1 in dom p & e2 in dom p & e1 < e2
holds p.e1 < p.e2
proof
let e1,e2 be ExtReal;
assume
A3: e1 in dom p & e2 in dom p & e1 < e2; then
reconsider ie1 = e1,ie2 = e2 as Nat;
A5: p.e1 = T.(ie1+n) by A2,A3;
A6: p.e2 = T.(ie2+n) by A2,A3;
A7: 1 <= ie1 <= m1 by A2,A3,FINSEQ_3:25;
A8: 1 <= ie2 <= m1 by A2,A3,FINSEQ_3:25;
A9: ie1 + n <= m1 + n by A7,XREAL_1:6;
m - 1 <= m - 0 by XREAL_1:10; then
A10: m - 1 <= len T by A1,XXREAL_0:2; then
A11: ie1+n <= len T by A9,XXREAL_0:2;
1 + 0 <= ie1 + n by A7,XREAL_1:7; then
A12: ie1+n in dom T by A11,FINSEQ_3:25;
A13: 1 + 0 <= ie2 + n by A8,XREAL_1:7;
ie2 + n <= m1 + n by A8,XREAL_1:6; then
ie2 + n <= len T by A10,XXREAL_0:2; then
A14: ie2 + n in dom T by FINSEQ_3:25,A13;
ie1 + n < ie2 + n by A3,XREAL_1:8;
hence thesis by A5,A6,A12,A14,VALUED_0:def 13;
end; then
reconsider p as non empty increasing FinSequence of REAL
by VALUED_0:def 13;
take p;
thus thesis by A2;
end;
theorem Th17:
for p be FinSequence of REAL, n,m be Nat
st n+1 < m <= len p holds
ex pM1 be FinSequence of REAL
st len pM1 = m-(n+1)-1 & rng pM1 c= rng p
& for i be Nat st i in dom pM1 holds pM1.i = p.(i+n+1)
proof
let p be FinSequence of REAL, n,m be Nat;
assume
A1: n+1 < m <= len p;
set n1 = n+1;
A2: n1 + 1 <= m by A1,NAT_1:13;
per cases;
suppose
A3: n1 + 1 = m;
set pM1 = <*>REAL;
take pM1;
thus len pM1 = m-(n+1)-1 by A3;
thus rng pM1 c= rng p;
thus for i be Nat st i in dom pM1 holds pM1.i = p.(i+n+1);
end;
suppose
n1 + 1 <> m; then
n1 + 1 < m by A2,XXREAL_0:1; then
consider TM1 be FinSequence of REAL such that
A4: len TM1 = m-(n1+1) & rng TM1 c= rng p
& for i be Nat st i in dom TM1 holds TM1.i = p.(i+n1)
by A1,Th15;
take TM1;
thus len TM1 = m-(n+1)-1 by A4;
thus rng TM1 c= rng p by A4;
let i be Nat;
assume i in dom TM1;
hence TM1.i = p.(i+n1) by A4
.= p.(i+n+1);
end;
end;
begin :: 2. Existence of Riemann-Stieltjes Integral for Continuous Functions
theorem Th18:
for A be non empty closed_interval Subset of REAL,
T be Division of A,
rho be real-valued Function,
B be non empty closed_interval Subset of REAL,
S0 be non empty increasing FinSequence of REAL,
ST be FinSequence of REAL
st B c= A & lower_bound B = lower_bound A
& ex S be Division of B
st S = S0
& len ST = len S
& for j be Nat st j in dom S holds
ex p be FinSequence of REAL
st ST.j = Sum p
& len p = len T
& for i be Nat st i in dom T
holds p.i = |. vol(divset(T,i) /\ divset(S,j), rho) .|
holds
ex H be Division of B, F be var_volume of rho,H
st Sum ST = Sum(F)
proof
let A be non empty closed_interval Subset of REAL,
T be Division of A,
rho be real-valued Function;
defpred P[Nat] means
for B be non empty closed_interval Subset of REAL,
S0 be non empty increasing FinSequence of REAL,
ST be FinSequence of REAL
st B c= A
& lower_bound B=lower_bound A
& len S0 = $1
& ex S be Division of B
st S = S0
& len ST = len S
& for j be Nat st j in dom S holds
ex p be FinSequence of REAL
st ST.j = Sum p
& len p = len T
& for i be Nat st i in dom T
holds p.i = |. vol(divset(T,i) /\ divset(S,j), rho) .|
holds
ex H be Division of B, F be var_volume of rho,H
st Sum ST = Sum(F);
A1: P[0];
A2: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A3: P[k];
let B be non empty closed_interval Subset of REAL,
S0 be non empty increasing FinSequence of REAL,
ST be FinSequence of REAL;
assume
A4: B c= A
& lower_bound B=lower_bound A
& len S0 = k+1
& ex S be Division of B
st S = S0
& len ST = len S
& for j be Nat st j in dom S holds
ex p be FinSequence of REAL
st ST.j = Sum p
& len p = len T
& for i be Nat st i in dom T holds
p.i = |. vol(divset(T,i) /\ divset(S,j), rho) .|; then
consider S be Division of B such that
A5: S = S0
& len ST = len S
& for j be Nat st j in dom S holds
ex p be FinSequence of REAL
st ST.j = Sum p
& len p = len T
& for i be Nat st i in dom T holds
p.i = |. vol(divset(T,i) /\ divset(S,j), rho) .|;
Z: dom ST = dom S by A5,FINSEQ_3:29;
per cases;
suppose
A6: k = 0;
set IDX = {i where i is Nat : i in dom T & T.i < upper_bound B};
IDX c= dom T
proof
let x be object;
assume x in IDX; then
ex i being Nat st x=i & i in dom T & T.i < upper_bound B;
hence thesis;
end; then
reconsider IDX as finite Subset of NAT by XBOOLE_1:1;
a: 1 <= len T by NAT_1:14; then
A7: 1 in dom T by FINSEQ_3:25;
ST = <*ST.1*> by A4,A6,FINSEQ_1:40; then
A8: Sum ST = ST.1 by RVSUM_1:73;
A10: 1 in dom S by A4,A5,A6,FINSEQ_3:25;
A11: S.1 = upper_bound B by A4,A5,A6,INTEGRA1:def 2;
per cases;
suppose
A12: IDX = {};
set F = the var_volume of rho,S;
take S,F;
F = <*F.1*> by A4,A5,A6,FINSEQ_1:40,INTEGR22:def 2; then
A13: Sum F = F.1 by RVSUM_1:73;
not 1 in IDX by A12; then
A14: upper_bound B <= T.1 by A7;
A15: F.1 = |. vol(divset(S,1), rho) .|
by A4,A5,A6,FINSEQ_3:25,INTEGR22:def 2;
consider p be FinSequence of REAL such that
A16: ST.1 = Sum p
& len p = len T
& for i be Nat st i in dom T
holds p.i = |. vol (divset(T,i) /\ divset(S,1),rho) .|
by A4,A5,A6,FINSEQ_3:25;
Z: dom p = dom T by A16,FINSEQ_3:29;
A18: p.1 = |. vol(divset(T,1) /\ divset(S,1), rho) .|
by FINSEQ_3:25,a,A16;
A19: divset(S,1) c= B by A4,A5,A6,FINSEQ_3:25,INTEGRA1:8;
A20: B = [. lower_bound B, upper_bound B .] by INTEGRA1:4;
A22: lower_bound divset(T,1) = lower_bound A
& upper_bound divset(T,1) = T.1 by INTEGRA1:def 4,A7;
[. lower_bound B, upper_bound B .]
c= [. lower_bound divset(T,1), upper_bound divset(T,1) .]
by A4,A14,A22,XXREAL_1:34; then
[. lower_bound B, upper_bound B .] c= divset(T,1) by INTEGRA1:4;
then
divset(S,1) c= divset(T,1) by A19,A20; then
A23: p.1 = |. vol(divset(S,1), rho) .| by A18,XBOOLE_1:28;
for i be Nat st i in dom p & i <> 1 holds p.i = 0
proof
let i be Nat;
assume
A24: i in dom p & i <> 1; then
A26: 1 <= i <= len p by FINSEQ_3:25; then
1 < i by A24,XXREAL_0:1; then
1+1 <= i by NAT_1:13; then
A27: 2-1 <= i-1 by XREAL_1:9; then
reconsider i1 = i-1 as Nat by INT_1:3,ORDINAL1:def 12;
i-1 <= len p - 0 by A26,XREAL_1:13; then
i1 in dom T by A16,A27,FINSEQ_3:25; then
A28: T.1 <= T.(i-1) by A7,A27,VALUED_0:def 15;
A29: lower_bound divset(T,i) = T.(i-1)
& upper_bound divset(T,i) = T.i
by Z,A24,INTEGRA1:def 4;
dom p = dom T by FINSEQ_3:29,A16; then
A30: p.i = |. vol(divset(T,i) /\ divset(S,1), rho) .| by A16,A24;
divset(T,i) /\ divset(S,1) c= divset(T,i) /\ B
by A10,INTEGRA1:8,XBOOLE_1:26; then
A31: divset(T,i) /\ divset(S,1)
c= [. lower_bound B, upper_bound B .]
/\ [. lower_bound divset(T,i), upper_bound divset(T,i) .]
by A20,INTEGRA1:4;
[. lower_bound B, upper_bound B .]
/\ [. lower_bound divset(T,i), upper_bound divset(T,i) .]
c= [.upper_bound B,upper_bound B.]
by A14,A28,A29,Th10,XXREAL_0:2; then
divset(T,i) /\ divset(S,1)
c= [.upper_bound B,upper_bound B.] by A31;
hence thesis by A30,COMPLEX1:44,Th11;
end;
hence Sum ST = Sum(F)
by A8,A13,A15,A16,a,FINSEQ_3:25,A23,Th8;
end;
suppose
A32: IDX <> {};
A33: sup IDX in IDX by A32,XXREAL_2:def 6; then
reconsider n = sup IDX as Nat;
A34: ex i be Nat
st n=i & i in dom T & T.i < upper_bound B by A33;
A35: 1 <= n <= len T by A34,FINSEQ_3:25;
n <> len T
proof
assume n = len T; then
upper_bound A < upper_bound B by A34,INTEGRA1:def 2;
hence contradiction by A4,XXREAL_2:59;
end; then
n < len T by A35,XXREAL_0:1; then
A37: 1 <= n+1 <= len T by NAT_1:11,NAT_1:13; then
A38: n+1 in dom T by FINSEQ_3:25;
A39: upper_bound B <= T.(n+1)
proof
assume T.(n+1) < upper_bound B; then
n+1 in IDX by A38;
hence contradiction by NAT_1:16,XXREAL_2:4;
end;
set H = (T|n)^ <* upper_bound B *>;
A41: len (T|n) = n by A35,FINSEQ_1:59;
len <* upper_bound B *> = 1 by FINSEQ_1:39; then
A42: len H = n+1 by A41,FINSEQ_1:22;
reconsider H as non empty FinSequence of REAL by FINSEQ_1:75;
for e1,e2 be ExtReal st
e1 in dom H & e2 in dom H & e1 < e2 holds H.e1 < H.e2
proof
let e1,e2 be ExtReal;
assume
A43: e1 in dom H & e2 in dom H & e1 < e2; then
reconsider i = e1, j = e2 as Nat;
A45: 1<=i <= n+1 & 1<=j <= n+1 by A42,A43,FINSEQ_3:25;
per cases;
suppose
A46: j = n+1; then
A47: H.e2 = upper_bound B by A41,FINSEQ_1:42;
A48: i <= n by A43,A46,NAT_1:13; then
A49: i in dom (T|n) by A41,A45,FINSEQ_3:25; then
A50: H.e1 = (T|n) .i by FINSEQ_1:def 7
.= T.i by A49,FUNCT_1:47;
i <= len T by A37,A43,A46,XXREAL_0:2; then
i in dom T by A45,FINSEQ_3:25; then
T.i <= T.n by A34,A48,VALUED_0:def 15;
hence H.e1 < H.e2 by A34,A47,A50,XXREAL_0:2;
end;
suppose
j <> n+1; then
j < n+1 by A45,XXREAL_0:1; then
A52: j <= n by NAT_1:13; then
A53: j in dom (T|n) by A41,A45,FINSEQ_3:25; then
A54: H.e2 = (T|n) .j by FINSEQ_1:def 7
.= T.j by A53,FUNCT_1:47;
A55: i <= n by A43,A52,XXREAL_0:2; then
A56: i in dom (T|n) by A41,A45,FINSEQ_3:25; then
A57: H.e1 = (T|n) .i by FINSEQ_1:def 7
.= T.i by A56,FUNCT_1:47;
i <= len T by A35,A55,XXREAL_0:2; then
A58: i in dom T by A45,FINSEQ_3:25;
j <= len T by A35,A52,XXREAL_0:2; then
j in dom T by A45,FINSEQ_3:25;
hence H.e1 < H.e2 by A43,A54,A57,A58,VALUED_0:def 13;
end;
end; then
reconsider H as non empty increasing FinSequence of REAL
by VALUED_0:def 13;
A59: B = [. lower_bound B, upper_bound B .] by INTEGRA1:4;
A60: A = [. lower_bound A, upper_bound A .] by INTEGRA1:4;
A61: H.(len H) = upper_bound B by A41,A42,FINSEQ_1:42;
A62: rng H = rng(T|n) \/ rng <* upper_bound B *> by FINSEQ_1:31;
A63: rng <* upper_bound B *> = { upper_bound B } by FINSEQ_1:39;
A64: rng(T|n) c= rng T by RELAT_1:70;
rng T c= A by INTEGRA1:def 2; then
A65: rng (T|n) c= A by A64;
lower_bound B <= upper_bound B by SEQ_4:11; then
upper_bound B in B by A59; then
{ upper_bound B } c= A by A4,ZFMISC_1:31; then
A66: rng H c= A by A62,A63,A65,XBOOLE_1:8;
for z be object st z in rng H holds z in B
proof
let z be object;
assume
A67: z in rng H; then
reconsider x = z as Real;
x in A by A66,A67; then
A68: ex r be Real
st x = r & lower_bound A <= r & r <= upper_bound A by A60;
consider i be object such that
A69: i in dom H & x = H.i by A67,FUNCT_1:def 3;
reconsider i as Nat by A69;
A70: 1 <= i <= len H by A69,FINSEQ_3:25;
1 <= len H <= len H by A70,XXREAL_0:2; then
len H in dom H by FINSEQ_3:25; then
x <= upper_bound B by A61,A69,A70,VALUED_0:def 15;
hence z in B by A4,A59,A68;
end; then
A71: rng H c= B;
reconsider H as Division of B by A61,A71,INTEGRA1:def 2;
set F = the var_volume of rho,H;
take H,F;
A72: len F = len H by INTEGR22:def 2;
ST = <*ST.1*> by A4,A6,FINSEQ_1:40; then
A73: Sum ST = ST.1 by RVSUM_1:73;
consider p be FinSequence of REAL such that
A74: ST.1 = Sum p
& len p = len T
& for i be Nat st i in dom T holds
p.i = |. vol (divset(T,i) /\ divset(S,1),rho) .|
by A4,A5,A6,FINSEQ_3:25;
for i be Nat st i in dom p holds
(i <= len F implies p.i = F.i)
& (len F < i implies p.i = 0)
proof
let i be Nat;
assume
A75: i in dom p;
dom p = dom T by A74,FINSEQ_3:29; then
A76: p.i = |. vol(divset(T,i) /\ divset(S,1), rho) .| by A74,A75;
A77: 1 <= i <= len T by A74,A75,FINSEQ_3:25;
A78: lower_bound divset(S,1) = lower_bound B
& upper_bound divset(S,1) = S.1 by A10,INTEGRA1:def 4;
A79: divset(S,1) = [.lower_bound B,upper_bound B.]
by A11,A78,INTEGRA1:4;
thus i <= len F implies p.i = F.i
proof
assume i <= len F; then
A80: 1 <= i <= len H by A75,FINSEQ_3:25,INTEGR22:def 2; then
A81: i in dom H by FINSEQ_3:25;
divset(T,i) /\ divset(S,1) = divset(H,i)
proof
per cases;
suppose
i <> n+1; then
i < n+1 by A42,A80,XXREAL_0:1; then
A82: i <= n by NAT_1:13; then
A83: i in dom (T|n) by A41,A80,FINSEQ_3:25; then
A84: H.i = (T|n) .i by FINSEQ_1:def 7
.= T.i by A83,FUNCT_1:47;
A85: i in dom T by A83,RELAT_1:57; then
T.i <= T.n by A34,A82,VALUED_0:def 15; then
A86: T.i <= upper_bound B by A34,XXREAL_0:2;
thus divset(T,i) /\ divset(S,1) = divset(H,i)
proof
per cases;
suppose
A87: i = 1; then
A88: lower_bound divset(T,i) = lower_bound A
& upper_bound divset(T,i) = T.i
by A85,INTEGRA1:def 4;
A89: lower_bound divset(H,i) = lower_bound B
& upper_bound divset(H,i) = H.i
by A81,A87,INTEGRA1:def 4;
A90: divset(T,i) =[.lower_bound B,T.i.]
by A4,A88,INTEGRA1:4;
divset(H,i) = [.lower_bound B, T.i .]
by A84,A89,INTEGRA1:4
.= divset(T,i) by A4,A88,INTEGRA1:4;
hence divset(T,i) /\ divset(S,1) = divset(H,i)
by A79,A86,A90,XBOOLE_1:28,XXREAL_1:34;
end;
suppose
A91: i <> 1; then
A92: lower_bound divset(T,i) = T.(i-1)
& upper_bound divset(T,i) = T.i
by A85,INTEGRA1:def 4;
A93: lower_bound divset(H,i) = H.(i-1)
& upper_bound divset(H,i) = H.i
by A81,A91,INTEGRA1:def 4;
1 < i by A77,A91,XXREAL_0:1; then
A94: 1-1 < i-1 by XREAL_1:14; then
reconsider i1 = i-1 as Nat by INT_1:3,ORDINAL1:def 12;
A95: 1 <= i1 by A94,NAT_1:14;
i1 <= n +1 -1 by A42,A80,XREAL_1:13; then
A96: i-1 in dom (T|n) by A41,A95,FINSEQ_3:25; then
H.(i-1) = (T|n) .(i-1) by FINSEQ_1:def 7
.= T.(i-1) by A96,FUNCT_1:47; then
A98: divset(H,i) = [.T.(i-1),T.i .]
by A84,A93,INTEGRA1:4;
A99: divset(T,i) = [.T.(i-1),T.i .] by A92,INTEGRA1:4;
i-1 in dom T by A96,RELAT_1:57; then
T.(i-1) in A by INTEGRA1:6; then
ex r be Real
st r= T.(i-1) & lower_bound A <=r & r <= upper_bound A
by A60;
hence divset(T,i) /\ divset(S,1) = divset(H,i)
by A4,A79,A86,A98,A99,XBOOLE_1:28,XXREAL_1:34;
end;
end;
end;
suppose
A100: i = n+1;
A101: 1 < i by A35,A100,NAT_1:16;
A102: lower_bound divset(T,i) = T.(i-1)
& upper_bound divset(T,i) = T.i
by A38,A100,A101,INTEGRA1:def 4;
A103: lower_bound divset(H,i) = H.(i-1)
& upper_bound divset(H,i) = H.i
by A81,A101,INTEGRA1:def 4;
reconsider i1 = i-1 as Nat by A100;
A104: i-1 in dom (T|n) by A35,A41,A100,FINSEQ_3:25; then
A105: H.(i-1) = (T|n).(i-1) by FINSEQ_1:def 7
.= T.(i-1) by A104,FUNCT_1:47;
T.(i-1) in A by A34,A100,INTEGRA1:6; then
A106: ex r be Real
st r= T.(i-1) & lower_bound A <=r & r <= upper_bound A
by A60;
thus divset(T,i) /\ divset(S,1)
= [.T.(i-1),T.i .] /\ [.lower_bound B,upper_bound B.]
by A79,A102,INTEGRA1:4
.= [.T.(i-1),upper_bound B .]
by A4,A39,A100,A106,XXREAL_1:143
.= [.H.(i-1),H.i.] by A41,A100,A105,FINSEQ_1:42
.= divset(H,i) by A103,INTEGRA1:4;
end;
end;
hence thesis by A76,A81,INTEGR22:def 2;
end;
thus len F < i implies p.i = 0
proof
assume
A107: len F < i; then
A108: len H < i by INTEGR22:def 2;
A109: 1 <= n+1 by NAT_1:11;
i in dom T by A75,A74,FINSEQ_3:29; then
lower_bound divset(T,i) = T.(i-1)
& upper_bound divset(T,i) = T.i
by A42,A72,A107,A109,INTEGRA1:def 4; then
A110: divset(T,i) = [.T.(i-1),T.i .] by INTEGRA1:4;
n+1 + 1 <= i by A42,A108,NAT_1:13; then
A111: n+1 +1 -1 <= i -1 by XREAL_1:9;
1 <= n+1 by NAT_1:11; then
A112: 1 <= i-1 by A111,XXREAL_0:2;
reconsider i1 = i-1 as Nat by A111,INT_1:3,ORDINAL1:def 12;
i-1 <= i-0 by XREAL_1:13; then
i-1 <= len T by A77,XXREAL_0:2; then
i1 in dom T by A112,FINSEQ_3:25; then
T.(n+1) <= T.i1 by A38,A111,VALUED_0:def 15; then
divset(T,i) /\ divset(S,1)
c= [.upper_bound B,upper_bound B.]
by A39,A79,A110,Th10,XXREAL_0:2;
hence p.i = 0 by A76,COMPLEX1:44,Th11;
end;
end;
hence Sum ST = Sum(F) by A37,A42,A72,A73,A74,Th9;
end;
end;
suppose
A114: k <> 0;
set S01 = S0 | k;
A115: B = [. lower_bound B, upper_bound B .] by INTEGRA1:4;
A116: A = [. lower_bound A, upper_bound A .] by INTEGRA1:4;
A117: k = len S01 by A4,FINSEQ_1:59,NAT_1:11;
dom S0 = Seg(k+1) by A4,FINSEQ_1:def 3; then
A118: Seg k c= dom S0 by FINSEQ_1:5,NAT_1:11;
reconsider S01 as non empty increasing FinSequence of REAL by A114;
A121: k in dom S0 by A114,A118,FINSEQ_1:3; then
consider B1,B2 be non empty closed_interval Subset of REAL such that
A122: B1 = [.lower_bound B, S0.k .] & B2 = [. S0.k, upper_bound B.]
& B = B1 \/ B2 by A5,INTEGRA1:32;
A123: B1 c= B by A122,XBOOLE_1:7; then
A124: B1 c= A by A4;
A125: B1 = [. lower_bound B1, upper_bound B1 .] by INTEGRA1:4; then
A126: upper_bound B1 = S.k by A5,A122,INTEGRA1:5;
A127: lower_bound B1 = lower_bound A by A4,A122,A125,INTEGRA1:5;
A128: rng S0 c= B by A5,INTEGRA1:def 2;
A129: rng S01 c= rng S0 by RELAT_1:70;
for y be object st y in rng S01 holds y in B1
proof
let y be object;
assume
A130: y in rng S01; then
y in B by A128,A129; then
y in [. lower_bound B, upper_bound B .] by INTEGRA1:4; then
consider y1 be Real such that
A131: y = y1 & lower_bound B <= y1 & y1 <= upper_bound B;
consider x be object such that
A132: x in dom S01 & y1 = S01.x by A130,A131,FUNCT_1:def 3;
reconsider x as Nat by A132;
A133: x in Seg k by A117,A132,FINSEQ_1:def 3; then
A134: x <= k by FINSEQ_1:1;
now
assume x <> k; then
x < k by A134,XXREAL_0:1;
hence S0.x <= S0.k by A118,A121,A133,VALUED_0:def 13;
end; then
y1 <= S0.k by A132,A133,FUNCT_1:49;
hence y in B1 by A122,A131;
end; then
A135: rng S01 c= B1;
A136: S01.k = S0.k by A114,FINSEQ_1:3,FUNCT_1:49;
A137: B1 = [. lower_bound B1, upper_bound B1 .] by INTEGRA1:4; then
S01.(len S01) = upper_bound B1 by A117,A122,A136,INTEGRA1:5; then
reconsider S1 = S01 as Division of B1 by A135,INTEGRA1:def 2;
reconsider ST1 = ST | k as FinSequence of REAL;
A138: len S1 = k by A4,FINSEQ_1:59,NAT_1:11;
A139: len ST1 = len S1 by A4,A138,FINSEQ_1:59,NAT_1:11;
for j be Nat st j in dom S1 holds
ex p be FinSequence of REAL st ST1.j = Sum p
& len p = len T
& for i be Nat st i in dom T
holds p.i = |. vol(divset(T,i) /\ divset(S1,j), rho) .|
proof
let j be Nat;
assume A140: j in dom S1; then
A141: j in Seg k & j in dom S0 by RELAT_1:57; then
consider p be FinSequence of REAL such that
A142: ST.j = Sum p
& len p = len T
& for i be Nat st i in dom T holds
p.i = |. vol(divset(T,i) /\ divset(S,j), rho) .| by A5;
A143: for i be Nat st i in dom T holds
p.i = |. vol(divset(T,i) /\ divset(S1,j), rho) .|
proof
let i be Nat;
assume
A144: i in dom T;
A145: divset(S,j)
= [. lower_bound divset(S,j), upper_bound divset(S,j) .]
& divset(S1,j)
= [. lower_bound divset(S1,j), upper_bound divset(S1,j) .]
by INTEGRA1:4;
divset(S,j) = divset(S1,j)
proof
per cases;
suppose
j = 1; then
A146: lower_bound(divset(S,j)) = lower_bound B
& upper_bound(divset(S,j)) = S.j
& lower_bound(divset(S1,j)) = lower_bound B1
& upper_bound(divset(S1,j)) = S1.j
by A5,A140,A141,INTEGRA1:def 4;
lower_bound B = lower_bound B1 by A122,A137,INTEGRA1:5;
hence divset(S,j) = divset(S1,j)
by A5,A140,A145,A146,FUNCT_1:47;
end;
suppose
A147: j<>1; then
A148: lower_bound(divset(S,j)) = S.(j-1)
& upper_bound(divset(S,j)) = S.j
& lower_bound(divset(S1,j)) = S1.(j-1)
& upper_bound(divset(S1,j)) = S1.j
by A5,A140,A141,INTEGRA1:def 4;
A149: 1 <= j by A141,FINSEQ_1:1; then
j-1 in NAT by INT_1:5; then
reconsider j1 = j-1 as Nat;
1 < j by A147,A149,XXREAL_0:1; then
S.j1 = S1.j1 by A5,A141,FINSEQ_3:12,FUNCT_1:49;
hence divset(S,j) = divset(S1,j)
by A5,A140,A145,A148,FUNCT_1:47;
end;
end;
hence p.i = |. vol (divset(T,i) /\ divset(S1,j),rho) .|
by A142,A144;
end;
take p;
thus thesis by A141,A142,A143,FUNCT_1:49;
end; then
consider H1 be Division of B1, F1 be var_volume of rho,H1 such that
A150: Sum ST1 = Sum(F1) by A3,A124,A127,A138,A139;
A151: 1 <= k + 1 <= len ST by A4,NAT_1:11;
ST = (ST|k)^<*ST/.(k+1)*> by A4,FINSEQ_5:21; then
A152: ST = ST1^<*ST.(k+1)*> by A151,FINSEQ_4:15;
dom ST = Seg (k+1) by A4,FINSEQ_1:def 3; then
consider p be FinSequence of REAL such that
A153: ST.(k+1) = Sum p
& len p = len T
& for i be Nat st i in dom T holds
p.i = |. vol(divset(T,i) /\ divset(S,(k+1)),rho) .|
by Z,A5,FINSEQ_1:4;
set JDX = {i where i is Nat :
i in dom T & upper_bound B <= T.i };
JDX c= dom T
proof
let x be object;
assume x in JDX; then
ex i being Nat st x = i & i in dom T & upper_bound B <= T.i;
hence thesis;
end; then
reconsider JDX as finite Subset of NAT by XBOOLE_1:1;
H: dom p = dom T by FINSEQ_3:29,A153;
A154: upper_bound B <= upper_bound A by A4,XXREAL_2:59;
A155: T.(len T) = upper_bound A by INTEGRA1:def 2;
A156: 1 <= len T by NAT_1:14; then
A157: 1 in dom T by FINSEQ_3:25;
reconsider m = min* JDX as Nat;
A159: S.(len S) = upper_bound B by INTEGRA1:def 2;
len T in dom T by A156,FINSEQ_3:25; then
len T in JDX by A154,A155; then
m in JDX by NAT_1:def 1; then
consider i being Nat such that
A160: m = i & i in dom T & upper_bound B <= T.i;
A161: 1 <= k by A114,NAT_1:14;
k <= k+1 by NAT_1:11; then
k in Seg (k+1) by A161; then
A162: k in dom S by A4,A5,FINSEQ_1:def 3; then
S.k in B by INTEGRA1:6; then
A163: ex r be Real
st r = S.k & lower_bound B <= r & r <= upper_bound B by A115;
A164: for i be Nat st m <= i & i in dom T
holds upper_bound B <= T.i
proof
let i be Nat;
assume m <= i & i in dom T; then
T.m <= T.i by A160,VALUED_0:def 15;
hence thesis by A160,XXREAL_0:2;
end;
k+1 in Seg (k+1) by FINSEQ_1:4; then
A167: k+1 in dom S by A4,A5,FINSEQ_1:def 3;
S.k < S.(k+1) by A162,A167,NAT_1:16,VALUED_0:def 13; then
A168: S.k < upper_bound B by A4,A5,INTEGRA1:def 2;
A169: divset(S,(k+1))
= [. lower_bound divset(S,(k+1)), upper_bound divset(S,(k+1)) .]
by INTEGRA1:4;
k+1 <> 1 by A114; then
A170: lower_bound(divset(S,k+1)) = S.(k+1-1)
& upper_bound(divset(S,k+1)) = S.(k+1) by A167,INTEGRA1:def 4;
A171: S.(k+1) = upper_bound B by A4,A5,INTEGRA1:def 2;
per cases;
suppose
A172: m = 1;
set H = H1 ^ <* upper_bound B *>;
A173: upper_bound B <= T.1 by A156,A164,A172,FINSEQ_3:25;
A175: len <* upper_bound B *> = 1 by FINSEQ_1:39; then
A176: len H = (len H1) + 1 by FINSEQ_1:22;
reconsider H as non empty FinSequence of REAL by FINSEQ_1:75;
for e1,e2 be ExtReal st e1 in dom H & e2 in dom H & e1 < e2
holds H.e1 < H.e2
proof
let e1,e2 be ExtReal;
assume
A177: e1 in dom H & e2 in dom H & e1 < e2; then
A178: e1 in Seg len H & e2 in Seg len H by FINSEQ_1:def 3;
reconsider i = e1, j = e2 as Nat by A177;
A179: 1<=i & i <= (len H1) + 1
& 1<=j & j <= (len H1) + 1 by A176,A178,FINSEQ_1:1;
per cases;
suppose
A180: j = (len H1) + 1; then
A181: H.e2 = upper_bound B by FINSEQ_1:42;
i <= len H1 by A177,A180,NAT_1:13; then
A182: i in dom H1 by A179,FINSEQ_3:25; then
A183: H.e1 = H1.i by FINSEQ_1:def 7;
H1.i in [.lower_bound B, S0.k .] by A122,A182,INTEGRA1:6; then
ex r be Real st r = H1.i & lower_bound B <= r & r <= S0.k;
hence H.e1 < H.e2 by A5,A168,A181,A183,XXREAL_0:2;
end;
suppose
j <> (len H1) + 1; then
j < (len H1) + 1 by A179,XXREAL_0:1; then
A184: j <= len H1 by NAT_1:13; then
A185: j in dom H1 by A179,FINSEQ_3:25; then
A186: H.e2 = H1 .j by FINSEQ_1:def 7;
i <= len H1 by A177,A184,XXREAL_0:2; then
A187: i in dom H1 by A179,FINSEQ_3:25; then
H.e1 = H1 .i by FINSEQ_1:def 7;
hence H.e1 < H.e2 by A177,A185,A186,A187,VALUED_0:def 13;
end;
end; then
reconsider H as non empty increasing FinSequence of REAL
by VALUED_0:def 13;
A188: H.(len H) = upper_bound B by A176,FINSEQ_1:42;
rng H1 c= B1 by INTEGRA1:def 2; then
A189: rng H1 c= B by A123;
A190: rng H = rng H1 \/ rng <* upper_bound B *>
by FINSEQ_1:31;
A191: rng <* upper_bound B *> = { upper_bound B } by FINSEQ_1:39;
lower_bound B <= upper_bound B by SEQ_4:11; then
upper_bound B in B by A115; then
rng <* upper_bound B *> c= B by A191,ZFMISC_1:31; then
reconsider H as Division of B
by A188,A189,A190,INTEGRA1:def 2,XBOOLE_1:8;
set F = F1 ^<* |. vol([.S.k,upper_bound B.], rho) .| *>;
reconsider F as FinSequence of REAL by FINSEQ_1:75;
A193: len F
= len F1 + len <* |. vol([.S.k,upper_bound B.],rho) .| *>
by FINSEQ_1:22
.= len H1 + len <* |. vol([.S.k,upper_bound B.],rho) .| *>
by INTEGR22:def 2
.= len H1 + 1 by FINSEQ_1:40
.= len H by A175,FINSEQ_1:22;
1 <= len H1 by NAT_1:14; then
A194: 1 in dom H1 by FINSEQ_3:25;
A195: len F1 = len H1 by INTEGR22:def 2; then
A196: dom F1 = dom H1 by FINSEQ_3:29;
for j be Nat st j in dom H holds
F.j = |. vol(divset(H,j),rho) .|
proof
let j be Nat;
A197: divset(H,j)
= [. lower_bound divset(H,j), upper_bound divset(H,j) .]
& divset(H1,j)
= [. lower_bound divset(H1,j), upper_bound divset(H1,j) .]
by INTEGRA1:4;
assume
A198: j in dom H; then
A199: 1 <= j <= len H by FINSEQ_3:25;
per cases;
suppose
A200: j = 1; then
A201: lower_bound divset(H,j) = lower_bound B
& upper_bound divset(H,j) = H.j by A198,INTEGRA1:def 4;
A203: lower_bound divset(H1,j) = lower_bound B1
& upper_bound divset(H1,j) = H1.j
by A194,A200,INTEGRA1:def 4;
A204: lower_bound B = lower_bound B1 by A122,A137,INTEGRA1:5;
thus F.j = F1.j by A196,A194,A200,FINSEQ_1:def 7
.= |. vol(divset(H1,j),rho) .|
by A200,A194,INTEGR22:def 2
.= |. vol(divset(H,j),rho) .|
by A197,A201,A200,A194,A203,A204,FINSEQ_1:def 7;
end;
suppose
A205: j <> 1;
per cases;
suppose
A206: j = len H; then
A207: j = len H1 + 1 by A175,FINSEQ_1:22;
A208: F.j = |. vol([.S.k,upper_bound B.],rho) .|
by A176,A195,A206,FINSEQ_1:42;
A209: lower_bound divset(H,j) = H.(j-1)
& upper_bound divset(H,j) = H.j
by A198,A205,INTEGRA1:def 4;
j-1 in NAT by A198,INT_1:5,FINSEQ_3:25; then
reconsider j1 = j-1 as Nat;
1 < j by A199,A205,XXREAL_0:1; then
1-1 < j1 by XREAL_1:14; then
A210: 1 <= j1 by NAT_1:14;
j-1 in dom H1 by A207,A210,FINSEQ_3:25; then
H.(j-1) = H1.(len H1) by A207,FINSEQ_1:def 7
.= S.k by A126,INTEGRA1:def 2;
hence F.j = |. vol(divset(H,j),rho) .|
by A197,A206,A208,A209,INTEGRA1:def 2;
end;
suppose
j <> len H; then
j < len H1 + 1 by A176,A199,XXREAL_0:1; then
L: j <= len H1 by NAT_1:13; then
A211: j in Seg len H1 by A199;
A212: j in dom H1 by A199,L,FINSEQ_3:25; then
A213: H.j = H1.j by FINSEQ_1:def 7;
j-1 in NAT by A198,FINSEQ_3:25,INT_1:5; then
reconsider j1 = j-1 as Nat;
1 < j by A199,A205,XXREAL_0:1; then
j-1 in Seg len H1 by A211,FINSEQ_3:12; then
j-1 in dom H1 by FINSEQ_1:def 3; then
A214: H.j1 = H1.j1 by FINSEQ_1:def 7;
A215: lower_bound divset(H,j) = H.(j-1)
& upper_bound divset(H,j) = H.j
by A198,A205,INTEGRA1:def 4;
thus F.j = F1.j by A196,A212,FINSEQ_1:def 7
.= |. vol(divset(H1,j),rho) .| by A212,INTEGR22:def 2
.= |. vol(divset(H,j),rho) .|
by A205,A212,A213,A214,A215,INTEGRA1:def 4;
end;
end;
end; then
reconsider F as var_volume of rho,H by A193,INTEGR22:def 2;
take H,F;
A217: p.1 = |. vol(divset(T,1) /\ divset(S,k+1),rho) .|
by A156,FINSEQ_3:25,A153;
A218: divset(S,k+1) c= B by A167,INTEGRA1:8;
A219: B = [. lower_bound B, upper_bound B .] by INTEGRA1:4;
A221: lower_bound divset(T,1) = lower_bound A
& upper_bound divset(T,1) = T.1 by INTEGRA1:def 4,A157;
[. lower_bound B, upper_bound B .]
c= [. lower_bound divset(T,1), upper_bound divset(T,1) .]
by A4,A173,A221,XXREAL_1:34; then
[. lower_bound B, upper_bound B .] c= divset(T,1)
by INTEGRA1:4; then
divset(S,k+1) c= divset(T,1) by A218,A219; then
A222: p.1 = |. vol(divset(S,k+1),rho) .| by A217,XBOOLE_1:28;
for i be Nat st i in dom p & i <> 1 holds p.i = 0
proof
let i be Nat;
assume
A223: i in dom p & i <> 1; then
A225: 1 <= i <= len p by FINSEQ_3:25; then
1 < i by A223,XXREAL_0:1; then
1+1 <= i by NAT_1:13; then
A226: 2-1 <= i-1 by XREAL_1:9; then
reconsider i1 = i-1 as Nat by INT_1:3,ORDINAL1:def 12;
i-1 <= len p - 0 by A225,XREAL_1:13; then
i1 in dom T by A226,FINSEQ_3:25,A153; then
A227: T.1 <= T.(i-1) by A157,A226,VALUED_0:def 15;
A228: lower_bound divset(T,i) = T.(i-1)
& upper_bound divset(T,i) = T.i by INTEGRA1:def 4,A223,H;
A229: p.i = |. vol(divset(T,i) /\ divset(S,k+1),rho) .|
by A153,A223,H;
divset(T,i) /\ divset(S,k+1)
c= divset(T,i) /\ B by A167,INTEGRA1:8,XBOOLE_1:26; then
A230: divset(T,i) /\ divset(S,k+1)
c= [. lower_bound B, upper_bound B .]
/\ [. lower_bound divset(T,i), upper_bound divset(T,i) .]
by A219,INTEGRA1:4;
[. lower_bound B, upper_bound B .]
/\ [. lower_bound divset(T,i), upper_bound divset(T,i) .]
c= [.upper_bound B,upper_bound B.]
by A173,A227,A228,Th10,XXREAL_0:2;
then divset(T,i) /\ divset(S,k+1)
c= [.upper_bound B,upper_bound B.] by A230;
hence thesis by A229,COMPLEX1:44,Th11;
end; then
A231: Sum p = |. vol(divset(S,k+1),rho) .|
by A153,A156,A222,Th8,FINSEQ_3:25
.= |. vol([.S.k,upper_bound B.],rho) .|
by A4,A5,A159,A170,INTEGRA1:4;
thus Sum ST = Sum(F1) + Sum p by A150,A152,A153,RVSUM_1:74
.= Sum(F) by A231,RVSUM_1:74;
end;
suppose
A232: m <> 1;
S: m in Seg len T by A160,FINSEQ_1:def 3;
A233: 1 <= m <= len T by A160,FINSEQ_3:25; then
1 < m by A232,XXREAL_0:1; then
a234: m - 1 in Seg len T by FINSEQ_3:12,S; then
A234: m-1 in dom T by FINSEQ_1:def 3; then
A235: 1 <= m-1 <= len T by FINSEQ_3:25;
reconsider m1 = m-1 as Nat by a234;
LL: m1 in dom T by a234,FINSEQ_1:def 3;
set IDX = {i where i is Nat : i in dom T & T.i <= S.k};
IDX c= dom T
proof
let x be object;
assume x in IDX; then
ex i being Nat st x = i & i in dom T & T.i <= S.k;
hence thesis;
end; then
reconsider IDX as finite Subset of NAT by XBOOLE_1:1;
per cases;
suppose
A237: IDX = {};
A238: for i be Nat st i in dom T holds S.k < T.i
proof
assume not for i be Nat st i in dom T holds S.k < T.i; then
consider i be Nat such that
A239: i in dom T & not S.k < T.i;
i in IDX by A239;
hence contradiction by A237;
end;
reconsider TM1 = T | m1
as non empty increasing FinSequence of REAL by Th12,LL;
A240: len TM1= m1 by A235,FINSEQ_1:59; then
a240: dom TM1 = Seg m1 by FINSEQ_1:def 3; then
A242: TM1.(len TM1) = T.m1 by FUNCT_1:49,A240,FINSEQ_3:25,A235;
A243: T.m1 < upper_bound B
proof
assume not T.m1 < upper_bound B; then
A245: m1 in JDX by A234;
m-1 < m-0 by XREAL_1:15;
hence contradiction by A245,NAT_1:def 1;
end; then
reconsider TM1B = TM1 ^ <* upper_bound B *>
as non empty increasing FinSequence of REAL by A242,Th14;
A246: H1.(len H1) = S.k by A126,INTEGRA1:def 2;
1 in Seg len TM1 by A235,A240; then
A248: TM1.1 = T.1 by A240,FUNCT_1:49;
1 in dom TM1 by A235,A240,FINSEQ_3:25; then
A249: TM1B.1 = T.1 by A248,FINSEQ_1:def 7;
reconsider H = H1 ^TM1B
as non empty increasing FinSequence of REAL
by A157,A238,A246,A249,Th13;
A250: rng TM1B = rng TM1 \/ rng <* upper_bound B *> by FINSEQ_1:31;
A251: rng <* upper_bound B *> = { upper_bound B } by FINSEQ_1:39;
A256: rng TM1 c= B
proof
let z be object;
assume
A252: z in rng TM1; then
reconsider x = z as Real;
x in rng T by A252,RELAT_1:70,TARSKI:def 3; then
x in A by INTEGRA1:def 2,TARSKI:def 3; then
A253: ex r be Real
st x = r & lower_bound A <= r & r <= upper_bound A by A116;
consider i be object such that
A254: i in dom TM1 & x =TM1.i by A252,FUNCT_1:def 3;
reconsider i as Nat by A254;
A255: 1 <= i <= len TM1 by FINSEQ_3:25,A254;
1 <= len TM1 by A255,XXREAL_0:2; then
len TM1 in dom TM1 by FINSEQ_3:25; then
TM1.i <= TM1.(len TM1) by A254,A255,VALUED_0:def 15; then
x <= upper_bound B by A242,A243,A254,XXREAL_0:2;
hence z in B by A4,A115,A253;
end;
lower_bound B <= upper_bound B by SEQ_4:11; then
upper_bound B in B by A115; then
{ upper_bound B } c= B by ZFMISC_1:31; then
A257: rng TM1B c= B by A250,A251,A256,XBOOLE_1:8;
rng H1 c= B1 by INTEGRA1:def 2; then
rng H1 c= B by A123; then
rng H1 \/ rng TM1B c= B by A257,XBOOLE_1:8; then
A258: rng H c= B by FINSEQ_1:31;
A259: len TM1B = len TM1 + len <* upper_bound B *> by FINSEQ_1:22
.= len TM1 + 1 by FINSEQ_1:40;
len TM1 + 1 in Seg(len TM1 + 1) by FINSEQ_1:4; then
A260: len TM1 + 1 in dom TM1B by A259,FINSEQ_1:def 3;
A261: len H = len H1 + (len TM1 + 1) by A259,FINSEQ_1:22;
X: 1 in Seg 1; then
A262: 1 in dom <* upper_bound B *> by FINSEQ_1:38;
H.(len H) = TM1B.(len TM1 + 1) by A260,A261,FINSEQ_1:def 7
.= (<* upper_bound B *>).1 by A262,FINSEQ_1:def 7
.= upper_bound B;
then
reconsider H as Division of B by A258,INTEGRA1:def 2;
set q = (p|m1) ^ <* |. vol([. T.m1,upper_bound B .], rho) .| *>;
rng q c= REAL; then
reconsider q as FinSequence of REAL by FINSEQ_1:def 4;
A263: len(p|m1) = m1 by A153,A235,FINSEQ_1:59;
A264: len q = len(p|m1)
+ len <* |. vol([. T.m1,upper_bound B .], rho) .| *>
by FINSEQ_1:22
.= m1+ 1 by A263,FINSEQ_1:40
.= m;
A265: 1 in dom <* |. vol([. T.m1,upper_bound B .], rho) .| *>
by FINSEQ_1:38,X;
A266: q.m = q.(m1+1)
.= (<* |. vol([. T.m1,upper_bound B .], rho) .| *>).1
by A263,A265,FINSEQ_1:def 7
.= |. vol([. T.m1,upper_bound B .], rho) .|;
A267: for i be Nat st 1 <= i & i <= m1 holds
q.i = |. vol(divset(T,i) /\ divset(S,(k+1)), rho) .|
proof
let i be Nat;
assume
A268: 1 <= i <= m1; then
A269: i in Seg m1; then
A270: i in dom (p|m1) by A263,FINSEQ_1:def 3;
C: i <= len T by A235,A268,XXREAL_0:2;
thus q.i = (p|m1).i by A270,FINSEQ_1:def 7
.= p.i by A269,FUNCT_1:49
.= |. vol(divset(T,i) /\ divset(S,(k+1)),rho) .|
by A153,C,FINSEQ_3:25,A268;
end;
reconsider F = F1^q as FinSequence of REAL;
A272: Sum F = Sum F1 + Sum q by RVSUM_1:75;
A273: len F = len F1 + len q by FINSEQ_1:22;
A274: len H = len H1 + m1 + 1 by A240,A261;
A275: 1 <= len H1 by NAT_1:14; then
A276: 1 in dom H1 by FINSEQ_3:25;
A277: len F1 = len H1 by INTEGR22:def 2; then
A278: dom F1 = dom H1 by FINSEQ_3:29;
m-1 <= m-0 by XREAL_1:15; then
1 <= m by A235,XXREAL_0:2; then
A279: m in dom q by A264,FINSEQ_3:25;
for j be Nat st j in dom H holds
F.j = |. vol (divset(H,j),rho) .|
proof
let j be Nat;
A280: divset(H,j)
= [. lower_bound divset(H,j), upper_bound divset(H,j) .]
& divset(H1,j)
= [. lower_bound divset(H1,j), upper_bound divset(H1,j) .]
by INTEGRA1:4;
assume
A281: j in dom H; then
A282: 1<=j <= len H by FINSEQ_3:25;
per cases;
suppose
A283: j = 1; then
A284: lower_bound divset(H,j) = lower_bound B
& upper_bound divset(H,j) = H.j by A281,INTEGRA1:def 4;
A285: j in dom H1 by A275,A283,FINSEQ_3:25; then
A286: lower_bound divset(H1,j) = lower_bound B1
& upper_bound divset(H1,j) = H1.j by A283,INTEGRA1:def 4;
A287: lower_bound B = lower_bound B1 by A122,A137,INTEGRA1:5;
thus F.j = F1.j by A278,A276,A283,FINSEQ_1:def 7
.= |. vol (divset(H1,j),rho) .| by A285,INTEGR22:def 2
.= |. vol (divset(H,j),rho) .|
by A280,A284,A285,A286,A287,FINSEQ_1:def 7;
end;
suppose
A288: j <> 1;
per cases;
suppose
A289: j = len H;
A290: F.j = |. vol([. T.m1,upper_bound B .],rho) .|
by A240,A261,A266,A277,A279,A289,FINSEQ_1:def 7;
A291: lower_bound divset(H,j) = H.(j-1)
& upper_bound divset(H,j) = H.j
by A281,A288,INTEGRA1:def 4;
j-1 in NAT by A281,INT_1:5,FINSEQ_3:25; then
reconsider j1 = j-1 as Nat;
m-1 < m-0 by XREAL_1:15; then
m1 in Seg m by A235; then
A292: m1 in dom TM1B by A240,A259,FINSEQ_1:def 3;
A293: m1 in dom TM1 by A240,A235,FINSEQ_3:25;
H.j1 = TM1B.m1 by A274,A289,A292,FINSEQ_1:def 7
.= TM1.m1 by A293,FINSEQ_1:def 7
.= T.m1 by a240,A240,FUNCT_1:49,A235,FINSEQ_3:25;
hence F.j = |. vol(divset(H,j),rho) .|
by A280,A289,A290,A291,INTEGRA1:def 2;
end;
suppose
j <> len H; then
A294: j < len H1 + m by A240,A261,A282,XXREAL_0:1;
per cases;
suppose
j > len H1; then
A295: j - len H1 > 0 by XREAL_1:50; then
j - len H1 in NAT by INT_1:3; then
reconsider j1 = j- len H1 as Nat;
A296: j1 < len H1 + m - len H1 by A294,XREAL_1:14; then
j1 + 1 <= m by NAT_1:13; then
A297: j1 + 1 - 1 <= m - 1 by XREAL_1:13;
A298: 1 <= j1 by A295,NAT_1:14; then
A299: j1 in Seg m by A296;
A300: j1 in dom q by A296,A264,FINSEQ_3:25,A298;
A301: j1 in Seg m1 by A297,A298; then
A302: j1 in dom TM1 by A240,FINSEQ_1:def 3;
A303: F.j = F.(len H1 + j1)
.= q.j1 by A277,A300,FINSEQ_1:def 7
.= |. vol(divset(T,j1) /\ divset(S,(k+1)),rho) .|
by A267,A297,A298;
A304: j1 in dom TM1B by A240,A259,A299,FINSEQ_1:def 3;
len TM1 in Seg len TM1 by FINSEQ_1:3; then
A305: m1 in dom TM1 by A240,FINSEQ_1:def 3;
A306: H.j = H.(len H1 + j1)
.= TM1B.j1 by A304,FINSEQ_1:def 7
.= TM1.j1 by A302,FINSEQ_1:def 7
.= T.j1 by A301,FUNCT_1:49;
A307: j1 in dom T by A302,RELAT_1:57;
m1 in dom T by A305,RELAT_1:57; then
T.j1 <= T.m1 by A297,A307,VALUED_0:def 15; then
A308: T.j1 <= upper_bound B by A243,XXREAL_0:2;
per cases;
suppose
A309: j1 <> 1; then
A310: lower_bound(divset(T,j1)) = T.(j1-1)
& upper_bound(divset(T,j1)) = T.j1
by A307,INTEGRA1:def 4;
1 < j1 by A298,A309,XXREAL_0:1; then
1+1 <= j1 by NAT_1:13; then
A311: 1+1-1 <= j1-1 by XREAL_1:9; then
j1-1 in NAT by INT_1:3; then
reconsider j11 = j1-1 as Nat;
A312: j11 <= m1-0 by A297,XREAL_1:13;
j11 <= len T by A235,A312,XXREAL_0:2; then
A313: lower_bound(divset(S,k+1))
<= lower_bound(divset(T,j1))
by A170,A238,A310,A311,FINSEQ_3:25;
A314: upper_bound(divset(T,j1))
<= upper_bound divset(S,(k+1))
by A4,A5,A159,A170,A307,A308,A309,INTEGRA1:def 4;
A315: divset(T,j1)
= [. lower_bound divset(T,j1),
upper_bound divset(T,j1) .] by INTEGRA1:4;
A316: divset(T,j1) /\ divset(S,(k+1))
= divset(T,j1)
by A169,A313,A314,A315,XBOOLE_1:28,XXREAL_1:34;
m-1 < m-0 by XREAL_1:15; then
1 <= j11 <= m by A311,A312,XXREAL_0:2; then
A317: j11 in dom TM1B
by A240,A259,FINSEQ_3:25;
A318: j11 in Seg m1 by A311,A312; then
A319: j11 in dom TM1 by A240,FINSEQ_1:def 3;
A320: H.(j-1) = H.(len H1 + j11)
.= TM1B.j11 by A317,FINSEQ_1:def 7
.= TM1.j11 by A319,FINSEQ_1:def 7
.= T.j11 by A318,FUNCT_1:49;
A321: upper_bound divset(H,j)
= T.j1 by A281,A288,A306,INTEGRA1:def 4
.= upper_bound divset(T,j1)
by A307,A309,INTEGRA1:def 4;
lower_bound divset(H,j)
= T.(j1-1) by A281,A288,A320,INTEGRA1:def 4
.= lower_bound divset(T,j1)
by A307,A309,INTEGRA1:def 4;
hence F.j = |. vol(divset(H,j), rho) .|
by A303,A315,A316,A321,INTEGRA1:4;
end;
suppose
A322: j1 = 1; then
A323: lower_bound(divset(T,j1)) = lower_bound A
& upper_bound(divset(T,j1)) = T.j1
by A307,INTEGRA1:def 4;
A324: divset(T,j1)
= [. lower_bound divset(T,j1),
upper_bound divset(T,j1) .] by INTEGRA1:4;
A325: upper_bound divset(H,j)
= T.j1 by A281,A288,A306,INTEGRA1:def 4
.= upper_bound(divset(T,j1))
by A307,A322,INTEGRA1:def 4;
A326: len H1 in dom H1 by A275,FINSEQ_3:25;
A327: lower_bound(divset(H,j))
= H.(len H1 + j1-1) by A281,A288,INTEGRA1:def 4
.= S.k by A246,A322,A326,FINSEQ_1:def 7;
divset(T,j1) /\ divset(S,k+1)
= [. S.k, upper_bound divset(T,j1) .]
by A4,A163,A169,A170,A171,A308,A323,A324,XXREAL_1:143
.= divset(H,j) by A325,A327,INTEGRA1:4;
hence F.j = |. vol(divset(H,j), rho) .| by A303;
end;
end;
suppose
B: j <= len H1; then
A328: j in Seg len H1 by A282;
A329: j in dom H1 by A282,B,FINSEQ_3:25; then
A330: H.j = H1.j by FINSEQ_1:def 7;
j-1 in NAT by A281,INT_1:5,FINSEQ_3:25; then
reconsider j1 = j-1 as Nat;
1 < j by A282,A288,XXREAL_0:1; then
j-1 in Seg len H1 by A328,FINSEQ_3:12; then
j-1 in dom H1 by FINSEQ_1:def 3; then
A331: H.j1 = H1.j1 by FINSEQ_1:def 7;
A332: lower_bound divset(H,j) = H.(j-1)
& upper_bound divset(H,j) = H.j
by A281,A288,INTEGRA1:def 4;
thus F.j = F1.j by A278,A329,FINSEQ_1:def 7
.= |. vol(divset(H1,j), rho) .|
by A329,INTEGR22:def 2
.= |. vol(divset(H,j), rho) .|
by A288,A329,A330,A331,A332,INTEGRA1:def 4;
end;
end;
end;
end; then
reconsider F as var_volume of rho,H
by A240,A261,A264,A273,A277,INTEGR22:def 2;
take H, F;
Z: dom p = dom T by FINSEQ_3:29,A153;
A333: for i be Nat st i in dom p holds
(i <= len q implies p.i = q.i)
& (len q < i implies p.i = 0)
proof
let i be Nat;
assume
A334: i in dom p; then
A335: 1 <= i <= len p by FINSEQ_3:25;
dom p = dom T by A153,FINSEQ_3:29; then
A336: p.i = |. vol(divset(T,i) /\ divset(S,(k+1)), rho) .|
by A153,A334;
thus i <= len q implies p.i = q.i
proof
assume
A337: i <= len q;
A338: divset(T,i)
= [. lower_bound divset(T,i), upper_bound divset(T,i) .]
by INTEGRA1:4;
per cases;
suppose
i <> m; then
i < m by A264,A337,XXREAL_0:1; then
i+1 <= m by NAT_1:13; then
i+1-1 <= m-1 by XREAL_1:13;
hence thesis by A267,A335,A336;
end;
suppose
A339: i = m;
m-1 < m-0 by XREAL_1:15; then
A341: lower_bound(divset(T,m)) = T.(m-1)
& upper_bound(divset(T,m)) = T.m
by A235,A160,INTEGRA1:def 4;
A342: lower_bound(divset(S,k+1))
< lower_bound(divset(T,m)) by A170,A234,A238,A341;
divset(T,i) /\ divset(S,(k+1))
= [. lower_bound divset(T,i), upper_bound divset(T,i) .]
/\ [. lower_bound divset(S,(k+1)),
upper_bound divset(S,(k+1)) .] by A338,INTEGRA1:4
.= [. T.m1, upper_bound B .]
by A4,A5,A159,A160,A170,A339,A341,A342,XXREAL_1:143;
hence thesis by A153,A266,A334,A339,Z;
end;
end;
A343: divset(T,i)
= [. lower_bound divset(T,i), upper_bound divset(T,i) .]
by INTEGRA1:4;
thus len q < i implies p.i = 0
proof
assume
A344: len q < i;
m-1 < m-0 by XREAL_1:15; then
A345: 1 < m by A235,XXREAL_0:2; then
A346: lower_bound(divset(T,i)) = T.(i-1)
& upper_bound(divset(T,i)) = T.i
by A264,A344,INTEGRA1:def 4,A334,Z;
m+1 <= i by A264,A344,NAT_1:13; then
A347: m+1-1 <= i-1 by XREAL_1:13; then
A348: 1 < i-1 by A345,XXREAL_0:2;
i-1 in NAT by A347,INT_1:3; then
reconsider i1 = i-1 as Nat;
len T - 1 < len T - 0 by XREAL_1:15; then
i1 <= len T by A153,A335,XREAL_1:15; then
A350: i1 in dom T by A348,FINSEQ_3:25;
divset(T,i) /\ divset(S,(k+1))
c= [.upper_bound(divset(S,k+1)),
upper_bound(divset(S,k+1)) .]
by A4,A5,A159,A164,A169,A170,A343,A346,A347,A350,Th10;
hence thesis by A336,COMPLEX1:44,Th11;
end;
end;
thus Sum ST = Sum(F1) + Sum p by A150,A152,A153,RVSUM_1:74
.= Sum(F)
by A272,A264,A153,A160,FINSEQ_3:25,A333,Th9;
end;
suppose
IDX <> {}; then
A351: sup IDX in IDX by XXREAL_2:def 6; then
reconsider n = sup IDX as Nat;
consider i be Nat such that
A352: n = i & i in dom T & T.i <= S.k by A351;
A353: 1 <= n <= len T by FINSEQ_3:25,A352;
n <> len T
proof
assume n = len T; then
A354: upper_bound A <= S.k by A352,INTEGRA1:def 2;
upper_bound A < upper_bound B by A168,A354,XXREAL_0:2;
hence contradiction by A4,XXREAL_2:59;
end; then
n < len T by A353,XXREAL_0:1; then
Z: 1 <= n+1 <= len T by NAT_1:11,13; then
A355: n+1 in dom T by FINSEQ_3:25;
A356: S.k < T.(n+1)
proof
assume T.(n+1) <= S.k; then
n+1 in IDX by A355;
hence contradiction by NAT_1:16,XXREAL_2:4;
end;
A357: for i be Nat st i in dom T & n < i holds S.k < T.i
proof
let i be Nat;
assume
A358: i in dom T & n < i; then
A359: n+1 <= i by NAT_1:13;
n+1 in dom T by Z,FINSEQ_3:25; then
T.(n+1) <= T.i by A358,A359,VALUED_0:def 15;
hence S.k < T.i by A356,XXREAL_0:2;
end;
A361: n < m
proof
assume m <= n; then
T.m <= T.n by A160,A352,VALUED_0:def 15; then
upper_bound B <= T.n by A160,XXREAL_0:2;
hence contradiction by A168,A352,XXREAL_0:2;
end;
A364: for i be Nat st i<=n & i in dom T holds T.i <= S.k
proof
let i be Nat;
assume
A365: i <= n & i in dom T;
assume
A366: not T.i <= S.k;
T.i <= T.n by A352,A365,VALUED_0:def 15;
hence contradiction by A352,A366,XXREAL_0:2;
end;
A368: for i be Nat st n<i & i < m & i in dom T
holds S.k < T.i & T.i < S.(k+1)
proof
let i be Nat;
assume
A369: n < i & i < m & i in dom T;
hence S.k < T.i by A357;
assume not T.i < S.(k+1); then
i in JDX by A4,A5,A159,A369;
hence contradiction by A369,NAT_1:def 1;
end;
A370: n+1 <= m by A361,NAT_1:13;
per cases;
suppose
A371: n+1 = m;
set H = H1 ^ <* upper_bound B *>;
H1.(len H1) = S.k by A126,INTEGRA1:def 2; then
reconsider H as non empty increasing FinSequence of REAL
by A168,Th14;
A372: len <* upper_bound B *> = 1 by FINSEQ_1:39; then
A373: len H = (len H1) + 1 by FINSEQ_1:22;
A374: H.(len H) = upper_bound B by A373,FINSEQ_1:42;
rng H1 c= B1 by INTEGRA1:def 2; then
A375: rng H1 c= B by A123;
A376: rng H = rng H1 \/ rng <* upper_bound B *> by FINSEQ_1:31;
A377: rng <* upper_bound B *> = { upper_bound B } by FINSEQ_1:39;
lower_bound B <= upper_bound B by SEQ_4:11; then
upper_bound B in B by A115; then
rng <* upper_bound B *> c= B by A377,ZFMISC_1:31; then
reconsider H as Division of B
by A374,A375,A376,INTEGRA1:def 2,XBOOLE_1:8;
set F = F1 ^ <* |. vol([. S.k, upper_bound B .], rho) .| *>;
reconsider F as FinSequence of REAL by FINSEQ_1:75;
A379: len F
= len F1 + len <* |. vol([.S.k,upper_bound B.], rho) .| *>
by FINSEQ_1:22
.= len H1 + len <* |. vol([.S.k,upper_bound B.], rho) .| *>
by INTEGR22:def 2
.= len H1 + 1 by FINSEQ_1:40
.= len H by A372,FINSEQ_1:22;
D: 1 <= len H1 by NAT_1:14; then
A380: 1 in dom H1 by FINSEQ_3:25;
A381: len F1 = len H1 by INTEGR22:def 2; then
A382: dom F1 = dom H1 by FINSEQ_3:29;
for j be Nat st j in dom H holds
F.j = |. vol(divset(H,j), rho) .|
proof
let j be Nat;
A383: divset(H,j)
= [. lower_bound divset(H,j), upper_bound divset(H,j) .]
& divset(H1,j)
= [. lower_bound divset(H1,j), upper_bound divset(H1,j) .]
by INTEGRA1:4;
assume
A384: j in dom H; then
A385: 1 <= j <= len H by FINSEQ_3:25;
per cases;
suppose
A386: j = 1; then
A387: lower_bound divset(H,j) = lower_bound B
& upper_bound divset(H,j) = H.j by A384,INTEGRA1:def 4;
A388: j in dom H1 by D,A386,FINSEQ_3:25;
A389: lower_bound divset(H1,j) = lower_bound B1
& upper_bound divset(H1,j) = H1.j
by INTEGRA1:def 4,A380,A386;
A390: lower_bound B = lower_bound B1
by A122,A137,INTEGRA1:5;
thus F.j = F1.j by A382,A388,FINSEQ_1:def 7
.= |. vol (divset(H1,j),rho) .| by A388,INTEGR22:def 2
.= |. vol (divset(H,j),rho) .|
by A383,A387,A388,A389,A390,FINSEQ_1:def 7;
end;
suppose
A391: j <> 1;
per cases;
suppose
A392: j = len H;
A393: F.j = |. vol([.S.k,upper_bound B.], rho) .|
by A373,A381,A392,FINSEQ_1:42;
A394: lower_bound divset(H,j) = H.(j-1)
& upper_bound divset(H,j) = H.j
by A384,A391,INTEGRA1:def 4;
j-1 in NAT by A384,INT_1:5,FINSEQ_3:25; then
reconsider j1 = j-1 as Nat;
1 < j by A385,A391,XXREAL_0:1; then
1-1 < j1 by XREAL_1:14; then
1 <= j1 by NAT_1:14; then
j1 in dom H1 by FINSEQ_3:25,A373,A392; then
H.(j-1) = H1.(len H1) by A373,A392,FINSEQ_1:def 7
.= S.k by A126,INTEGRA1:def 2;
hence F.j = |. vol (divset(H,j), rho) .|
by A383,A392,A393,A394,INTEGRA1:def 2;
end;
suppose
j <> len H; then
j < len H1 + 1 by A373,A385,XXREAL_0:1; then
K: j <= len H1 by NAT_1:13; then
A396: j in Seg len H1 by A385;
A397: j in dom H1 by FINSEQ_3:25,K,A385; then
A398: H.j = H1.j by FINSEQ_1:def 7;
j-1 in NAT by A384,FINSEQ_3:25,INT_1:5; then
reconsider j1 = j-1 as Nat;
1 < j by A385,A391,XXREAL_0:1; then
j-1 in Seg len H1 by A396,FINSEQ_3:12; then
j-1 in dom H1 by FINSEQ_1:def 3; then
A399: H.j1 = H1.j1 by FINSEQ_1:def 7;
A400: lower_bound divset(H,j) = H.(j-1)
& upper_bound divset(H,j) = H.j
by A384,A391,INTEGRA1:def 4;
thus F.j = F1.j by A382,A397,FINSEQ_1:def 7
.= |. vol(divset(H1,j), rho) .|
by A397,INTEGR22:def 2
.= |. vol(divset(H,j), rho) .|
by A391,A397,A398,A399,A400,INTEGRA1:def 4;
end;
end;
end; then
reconsider F as var_volume of rho,H by A379,INTEGR22:def 2;
take H, F;
A401: 1 < 1+n by A353,NAT_1:16;
A403: p.m = |. vol(divset(T,m) /\ divset(S,k+1), rho) .|
by A153,A160;
A405: lower_bound divset(T,m) = T.m1
& upper_bound divset(T,m) = T.m
by A160,A371,A401,INTEGRA1:def 4;
[. lower_bound divset(S,(k+1)),
upper_bound divset(S,(k+1)) .]
c= [. lower_bound divset(T,m),
upper_bound divset(T,m) .]
by A160,A170,A171,A352,A371,A405,XXREAL_1:34; then
divset(S,k+1) c= divset(T,m) by A169,INTEGRA1:4; then
A406: p.m = |. vol (divset(S,k+1), rho) .| by A403,XBOOLE_1:28;
for i be Nat st i in dom p & i <> m holds p.i = 0
proof
let i be Nat;
assume
A407: i in dom p & i <> m; then
A408: i in Seg len p by FINSEQ_1:def 3;
A409: 1 <= i <= len p by A407,FINSEQ_3:25;
per cases by A407,XXREAL_0:1;
suppose
A410: i < m;
A412: i in dom T by A153,A408,FINSEQ_1:def 3;
A413: upper_bound divset(T,i) = T.i
proof
per cases;
suppose
i = 1;
hence upper_bound divset(T,i) = T.i
by A412,INTEGRA1:def 4;
end;
suppose
i <> 1;
hence upper_bound divset(T,i) = T.i
by A412,INTEGRA1:def 4;
end;
end;
A414: i+1-1 <= n+1-1 by A371,A410,NAT_1:13;
A415: divset(T,i) /\ divset(S,k+1)
= [. lower_bound(divset(T,i)),
upper_bound(divset(T,i)) .]
/\ [. lower_bound(divset(S,k+1)),
upper_bound(divset(S,k+1)) .] by A169,INTEGRA1:4;
divset(T,i) /\ divset(S,k+1)
c= [. upper_bound(divset(T,i)), upper_bound(divset(T,i)) .]
by H,A170,A364,A407,A413,A414,A415,Th10; then
vol(divset(T,i) /\ divset(S,k+1),rho) = 0 by Th11;
hence thesis by A153,COMPLEX1:44,A412;
end;
suppose
A416: m < i; then
A417: 1 < i by A353,A371,NAT_1:16,XXREAL_0:2;
a418: i in dom T by A153,A408,FINSEQ_1:def 3; then
A419: lower_bound divset(T,i) = T.(i-1)
& upper_bound divset(T,i) = T.i
by A371,A401,A416,INTEGRA1:def 4;
m+1 <= i by A416,NAT_1:13; then
A420: m+1-1 <= i-1 by XREAL_1:9;
1+1 <= i by A417,NAT_1:13; then
A421: 2-1 <= i-1 by XREAL_1:9; then
reconsider i1 = i-1 as Nat by INT_1:3,ORDINAL1:def 12;
i-1 <= len p - 0 by A409,XREAL_1:13; then
i1 in dom T by A153,FINSEQ_3:25,A421; then
A422: T.m <= T.i1 by A160,A420,VALUED_0:def 15;
divset(T,i) /\ divset(S,k+1)
= [. lower_bound(divset(T,i)),
upper_bound(divset(T,i)) .]
/\ [. lower_bound(divset(S,k+1)),
upper_bound(divset(S,k+1)) .]
by A169,INTEGRA1:4; then
divset(T,i) /\ divset(S,k+1)
c= [. upper_bound(divset(S,k+1)),
upper_bound(divset(S,k+1)) .]
by A160,A170,A171,A419,A422,Th10,XXREAL_0:2; then
vol(divset(T,i) /\ divset(S,k+1), rho) = 0 by Th11;
hence thesis by A153,a418,COMPLEX1:44;
end;
end; then
A423: Sum p = |. vol(divset(S,k+1), rho) .|
by A160,H,A406,Th8
.= |. vol([.S.k,upper_bound B.], rho) .|
by A4,A5,A159,A170,INTEGRA1:4;
thus Sum ST = Sum(F1) + Sum p by A150,A152,A153,RVSUM_1:74
.= Sum(F) by A423,RVSUM_1:74;
end;
suppose
A424: n+1 <> m; then
A425: n+1 < m by A370,XXREAL_0:1;
m-(n+1) in NAT by A370,INT_1:5; then
reconsider mn1 = m-(n+1) as Nat;
m-n in NAT by A361,INT_1:5; then
reconsider mn = m-n as Nat;
A426: 0+1 <= mn1 by A425,NAT_1:13,XREAL_1:50;
m-n-1 <= mn-0 by XREAL_1:13; then
A427: 1 <= mn by A426,XXREAL_0:2;
consider TM1 be non empty increasing FinSequence of REAL
such that
A428: len TM1 = mn1 & rng TM1 c= rng T
& for i be Nat st i in dom TM1
holds TM1.i = T.(i+n) by A233,A425,Th16;
consider pM1 be FinSequence of REAL such that
A429: len pM1 = mn1-1 & rng pM1 c= rng p
& for i be Nat st i in dom pM1
holds pM1.i = p.(i+n+1) by A153,A233,A425,Th17;
reconsider m1 = m-1 as Nat by a234;
A430: TM1.(len TM1) = T.(mn1+n) by FINSEQ_3:25,A426,A428;
A431: T.(mn1+n) < upper_bound B
proof
assume
A432: not T.(mn1+n) < upper_bound B;
A433: (mn1+n) in JDX by A234,A432;
m-1 < m-0 by XREAL_1:15;
hence contradiction by A433,NAT_1:def 1;
end; then
reconsider TM1B = TM1 ^ <* upper_bound B *>
as non empty increasing FinSequence of REAL by A430,Th14;
A434: H1.(len H1) = S.k by A126,INTEGRA1:def 2;
KK: 1 in dom TM1 by A426,A428,FINSEQ_3:25;
A436: TM1.1 = T.(1+n) by A428,A426,FINSEQ_3:25;
A437: TM1B.1 = T.(1+n) by A436,FINSEQ_1:def 7,KK;
reconsider H = H1 ^TM1B
as non empty increasing FinSequence of REAL
by A356,A434,A437,Th13;
A438: rng TM1B = rng TM1 \/ rng <* upper_bound B *>
by FINSEQ_1:31;
A439: rng <* upper_bound B *> = { upper_bound B } by FINSEQ_1:39;
A444: rng TM1 c= B
proof
let z be object;
assume
A440: z in rng TM1; then
reconsider x = z as Real;
x in A by A428,A440,INTEGRA1:def 2,TARSKI:def 3; then
A441: ex r be Real
st x = r & lower_bound A <= r & r <= upper_bound A
by A116;
consider i be object such that
A442: i in dom TM1 & x = TM1.i by A440,FUNCT_1:def 3;
reconsider i as Nat by A442;
A443: 1 <= i <= len TM1 by A442,FINSEQ_3:25;
1 <= len TM1 <= len TM1 by A443,XXREAL_0:2; then
len TM1 in dom TM1 by FINSEQ_3:25; then
TM1.i <= TM1.(len TM1)
by A442,A443,VALUED_0:def 15; then
x <= upper_bound B by A430,A431,A442,XXREAL_0:2;
hence z in B by A4,A115,A441;
end;
lower_bound B <= upper_bound B by SEQ_4:11; then
upper_bound B in B by A115; then
{ upper_bound B } c= B by ZFMISC_1:31; then
A445: rng TM1B c= B by A438,A439,A444,XBOOLE_1:8;
rng H1 c= B1 by INTEGRA1:def 2; then
rng H1 c= B by A123; then
rng H1 \/ rng TM1B c= B by A445,XBOOLE_1:8; then
A446: rng H c= B by FINSEQ_1:31;
A447: len TM1B = len TM1 + len <* upper_bound B *> by FINSEQ_1:22
.= len TM1 + 1 by FINSEQ_1:40;
len TM1 + 1 in Seg(len TM1 + 1) by FINSEQ_1:4; then
A448: len TM1 + 1 in dom TM1B by A447,FINSEQ_1:def 3;
A449: len H = len H1 + (len TM1 + 1) by A447,FINSEQ_1:22;
G: 1 in Seg 1; then
A450: 1 in dom <* upper_bound B *> by FINSEQ_1:38;
H.(len H) = TM1B.(len TM1 + 1) by A448,A449,FINSEQ_1:def 7
.= (<* upper_bound B *>).1 by A450,FINSEQ_1:def 7
.= upper_bound B; then
reconsider H as Division of B by A446,INTEGRA1:def 2;
set q1 = <* |. vol([. S.k, T.(n+1) .], rho) .| *> ^ pM1;
set q = q1 ^ <* |. vol([. T.m1,upper_bound B .], rho) .| *>;
rng q1 c= REAL; then
reconsider q1 as FinSequence of REAL by FINSEQ_1:def 4;
rng q c= REAL; then
reconsider q as FinSequence of REAL by FINSEQ_1:def 4;
A451: len q1 = len(<* |. vol([. S.k, T.(n+1) .], rho) .| *>)
+ len pM1 by FINSEQ_1:22
.= 1 + (mn1-1) by A429,FINSEQ_1:40
.= mn1;
A452: len q = len q1
+ len <* |. vol([. T.m1, upper_bound B .], rho) .| *>
by FINSEQ_1:22
.= mn1+ 1 by A451,FINSEQ_1:40
.= mn;
A453: 1 in dom <* |. vol([. T.m1,upper_bound B .], rho) .| *>
by G,FINSEQ_1:38;
A454: q.(len q) = q.(mn1+1) by A452
.= ( <* |. vol([. T.m1,upper_bound B .], rho) .| *>).1
by A451,A453,FINSEQ_1:def 7
.= |. vol([. T.m1,upper_bound B .], rho) .|;
A455: 1 in dom <* |. vol([. S.k,T.(n+1) .], rho) .| *>
by FINSEQ_1:38,G;
1 in Seg mn1 by A426; then
1 in dom q1 by A451,FINSEQ_1:def 3; then
A456: q.1 = q1.1 by FINSEQ_1:def 7
.= (<* |. vol([. S.k,T.(n+1) .], rho) .| *>).1
by A455,FINSEQ_1:def 7
.= |. vol([. S.k,T.(n+1) .], rho) .|;
A457: for i be Nat st 2 <= i & i <= len q1 holds
q.i = |. vol(divset(T,n+i) /\ divset(S,(k+1)), rho) .|
proof
let i be Nat;
assume
A458: 2 <= i & i <= len q1; then
A459: 1 <= i by XXREAL_0:2; then
i in dom q1 by A458,FINSEQ_3:25; then
A460: q.i = q1.i by FINSEQ_1:def 7;
A461: 2-1 <= i-1 by A458,XREAL_1:9; then
A462: 1 <= i-1 & i-1 <= mn1-1 by A451,A458,XREAL_1:9;
i-1 in NAT by A461,INT_1:3; then
reconsider i1 = i-1 as Nat;
A463: len(<* |. vol([. S.k, T.(n+1) .], rho) .| *>) = 1
by FINSEQ_1:40;
A465: i1 in dom pM1 by FINSEQ_3:25,A429,A462;
A466: q1.i = q1.(1+i1)
.= pM1.i1 by A463,A465,FINSEQ_1:def 7
.= p.(i1+n+1) by FINSEQ_3:25,A429,A462
.= p.(i+n);
i <= i+n by NAT_1:11; then
A467: 1 <= i+n by A459,XXREAL_0:2;
i+n <= m-n-1+n by A451,A458,XREAL_1:6; then
i+n <= len T by A235,XXREAL_0:2;
hence thesis by A153,A460,A466,FINSEQ_3:25,A467;
end;
reconsider F = F1^q as FinSequence of REAL;
A468: len F = len F1 + len q by FINSEQ_1:22;
E: 1 <= len H1 by NAT_1:14; then
A469: 1 in dom H1 by FINSEQ_3:25;
A470: len F1 = len H1 by INTEGR22:def 2; then
A471: dom F1 = dom H1 by FINSEQ_3:29;
mn in Seg (mn) by A427; then
A472: mn in dom q by A452,FINSEQ_1:def 3;
1<= len q by NAT_1:14; then
A473: 1 in dom q by FINSEQ_3:25;
1 <= len TM1B by NAT_1:14; then
A474: 1 in dom TM1B by FINSEQ_3:25;
1 <= len TM1 by NAT_1:14; then
A475: 1 in dom TM1 by FINSEQ_3:25;
A476: H.(len H1 +1) = TM1B.1 by A474,FINSEQ_1:def 7
.= TM1.1 by A475,FINSEQ_1:def 7
.= T.(n+1) by A428,A426,FINSEQ_3:25;
for j be Nat st j in dom H holds
F.j = |. vol (divset(H,j),rho) .|
proof
let j be Nat;
A477: divset(H,j)
= [. lower_bound divset(H,j), upper_bound divset(H,j) .]
& divset(H1,j)
= [. lower_bound divset(H1,j), upper_bound divset(H1,j) .]
by INTEGRA1:4;
assume
A478: j in dom H; then
A479: 1 <= j <= len H by FINSEQ_3:25;
per cases;
suppose
A480: j = 1; then
A481: lower_bound divset(H,j) = lower_bound B
& upper_bound divset(H,j) = H.j by A478,INTEGRA1:def 4;
A482: j in dom H1 by E,A480,FINSEQ_3:25;
A483: lower_bound divset(H1,j) = lower_bound B1
& upper_bound divset(H1,j) = H1.j
by A469,A480,INTEGRA1:def 4;
A484: lower_bound B = lower_bound B1 by A122,A137,INTEGRA1:5;
thus F.j = F1.j by A471,A482,FINSEQ_1:def 7
.= |. vol(divset(H1,j), rho) .|
by A482,INTEGR22:def 2
.= |. vol(divset(H,j), rho) .|
by A477,A481,A482,A483,A484,FINSEQ_1:def 7;
end;
suppose
A485: j <> 1;
per cases;
suppose
A486: j = len H; then
A487: j = len H1 + mn1 + 1 by A428,A449;
A488: F.j = |. vol( [. T.m1,upper_bound B .], rho) .|
by A428,A449,A452,A454,A470,A472,A486,FINSEQ_1:def 7;
A489: lower_bound divset(H,j) = H.(j-1)
& upper_bound divset(H,j) = H.j
by A478,A485,INTEGRA1:def 4;
j-1 in NAT by A478,INT_1:5,FINSEQ_3:25; then
reconsider j1 = j-1 as Nat;
mn-1 < mn-0 by XREAL_1:15; then
mn1 in Seg mn by A426; then
A490: mn1 in dom TM1B by A428,A447,FINSEQ_1:def 3;
len TM1 in Seg len TM1 by FINSEQ_1:3; then
A491: mn1 in dom TM1 by A428,FINSEQ_1:def 3;
H.j1 = TM1B.mn1 by A487,A490,FINSEQ_1:def 7
.= T.m1 by A428,A430,A491,FINSEQ_1:def 7;
hence F.j = |. vol(divset(H,j), rho) .|
by A477,A486,A488,A489,INTEGRA1:def 2;
end;
suppose
j <> len H; then
A492: j < len H1 + mn1 + 1 by A428,A449,A479,XXREAL_0:1;
per cases;
suppose
j > len H1; then
A493: j - len H1 > 0 by XREAL_1:50; then
j- len H1 in NAT by INT_1:3; then
reconsider j1 = j - len H1 as Nat;
A494: j1 < len H1 + mn - len H1 by A492,XREAL_1:14; then
j1 + 1 <= mn by NAT_1:13; then
A495: j1 + 1 - 1 <= mn - 1 by XREAL_1:13;
A496: 1 <= j1 by A493,NAT_1:14; then
A497: j1 in Seg mn by A494; then
A498: j1 in dom q by A452,FINSEQ_1:def 3;
1 <= j1 <= mn1 by A493,A495,NAT_1:14; then
j1 in Seg mn1; then
A500: j1 in dom TM1 by A428,FINSEQ_1:def 3;
A501: j1 in dom TM1B by A428,A447,A497,FINSEQ_1:def 3;
A502: H.j = H.(len H1 + j1)
.= TM1B.j1 by A501,FINSEQ_1:def 7
.= TM1.j1 by A500,FINSEQ_1:def 7
.= T.(j1+n) by A428,A500;
A503: j1 +n <= mn1+n by A495,XREAL_1:6;
A504: 1 <= j1+n by A493,NAT_1:14;
j1+n <= len T by A235,A503,XXREAL_0:2; then
A505: j1+n in dom T by A504,FINSEQ_3:25; then
T.(j1+n) <= T.(mn1+n)
by A234,A503,VALUED_0:def 15; then
A506: T.(j1+n) <= upper_bound divset(S,(k+1))
by A4,A5,A159,A170,A431,XXREAL_0:2;
per cases;
suppose
A507: j1 = 1;
0 < len H1; then
1 + 0 < 1 + len H1 by XREAL_1:8; then
A508: lower_bound divset(H,j) = H.(j-1)
& upper_bound divset(H,j) = H.j
by A478,A507,INTEGRA1:def 4;
len H1 in Seg len H1 by FINSEQ_1:3; then
A509: len H1 in dom H1 by FINSEQ_1:def 3;
A510: F.j = F.(len H1 + 1) by A507
.= |. vol( [. S.k,T.(n+1) .], rho) .|
by A456,A470,A473,FINSEQ_1:def 7;
H.(len H1) = S.k by A434,A509,FINSEQ_1:def 7;
hence F.j = |. vol(divset(H,j), rho) .|
by A476,A507,A508,A510,INTEGRA1:4;
end;
suppose
j1 <> 1; then
A511: 1 < j1 by A496,XXREAL_0:1; then
A512: 1+1 <= j1 by NAT_1:13;
A513: F.j = F.(len H1 + j1)
.= q.j1 by A470,A498,FINSEQ_1:def 7
.= |. vol(divset(T,j1+n) /\ divset(S,(k+1)),rho) .|
by A451,A457,A495,A512;
A514: j1 + n <> 1 by A511,NAT_1:11; then
1 < j1+n by A504,XXREAL_0:1; then
1+1 <= j1+n by NAT_1:13; then
A515: 1+1 -1 <= j1+n -1 by XREAL_1:9; then
j1+n-1 in NAT by INT_1:3; then
reconsider j11=j1+n-1 as Nat;
2+(n-1) <= j1+(n-1) by A512,XREAL_1:6; then
n+1 <= j11; then
A516: n < j11 by NAT_1:16,XXREAL_0:2;
A517: j1 + (n-1) <= m-n-1 + (n-1) by A495,XREAL_1:6;
m1-1 <= m1-0 by XREAL_1:13; then
A518: j11 <= m1 by A517,XXREAL_0:2;
j11 <= len T by A235,A518,XXREAL_0:2; then
j11 in dom T by FINSEQ_3:25,A515; then
A519: S.k < T.j11 by A357,A516;
A520: lower_bound(divset(S,k+1))
<= lower_bound(divset(T,j1+n))
by A170,A505,A514,A519,INTEGRA1:def 4;
A521: upper_bound(divset(T,j1+n))
<= upper_bound divset(S,(k+1))
by A505,A506,A514,INTEGRA1:def 4;
A522: divset(T,j1+n)
= [. lower_bound divset(T,j1+n),
upper_bound divset(T,j1+n) .] by INTEGRA1:4;
A523: divset(T,j1+n) /\ divset(S,(k+1))
= divset(T,j1+n)
by A169,A520,A521,A522,XBOOLE_1:28,XXREAL_1:34;
j1-1 <= j1-0 by XREAL_1:13; then
A524: j11-n <= mn1 by A495,XXREAL_0:2;
A525: 2-1 <= j1-1 by A512,XREAL_1:9; then
j11-n in NAT by INT_1:3; then
reconsider j11n = j11-n as Nat;
j11n in Seg mn1 by A524,A525; then
A527: j11-n in dom TM1 by A428,FINSEQ_1:def 3;
mn-1 <= mn-0 by XREAL_1:13; then
1 <= j11-n & j11-n <= mn by A524,A525,XXREAL_0:2; then
j11n in Seg mn; then
A528: j11-n in dom TM1B by A428,A447,FINSEQ_1:def 3;
A529: H.(j-1) = H.(len H1 + (j11-n))
.= TM1B.(j11-n) by A528,FINSEQ_1:def 7
.= TM1.(j11-n) by A527,FINSEQ_1:def 7
.= T.(j1-1+n) by A428,A527;
A530: upper_bound divset(H,j)
= T.(j1+n) by A478,A485,A502,INTEGRA1:def 4
.= upper_bound divset(T,j1+n)
by A505,A514,INTEGRA1:def 4;
lower_bound divset(H,j)
= T.(j1+n-1) by A478,A485,A529,INTEGRA1:def 4
.= lower_bound divset(T,j1+n)
by A505,A514,INTEGRA1:def 4;
hence F.j = |. vol(divset(H,j),rho) .|
by A513,A522,A523,A530,INTEGRA1:4;
end;
end;
suppose
j <= len H1; then
A531: j in Seg len H1 by A479; then
A532: j in dom H1 by FINSEQ_1:def 3; then
A533: H.j =H1.j by FINSEQ_1:def 7;
j-1 in NAT by A478,INT_1:5,FINSEQ_3:25; then
reconsider j1 = j-1 as Nat;
1 < j by A479,A485,XXREAL_0:1; then
j-1 in Seg(len H1) by A531,FINSEQ_3:12; then
j-1 in dom H1 by FINSEQ_1:def 3; then
A534: H.j1 = H1.j1 by FINSEQ_1:def 7;
A535: lower_bound divset(H,j) = H.(j-1)
& upper_bound divset(H,j) = H.j
by A478,A485,INTEGRA1:def 4;
thus F.j = F1.j by A471,A532,FINSEQ_1:def 7
.= |. vol(divset(H1,j),rho) .|
by A532,INTEGR22:def 2
.= |. vol(divset(H,j),rho) .|
by A485,A532,A533,A534,A535,INTEGRA1:def 4;
end;
end;
end;
end; then
reconsider F as var_volume of rho,H
by A428,A449,A452,A468,A470,INTEGR22:def 2;
take H,F;
A536: for i be Nat st i in dom p holds
(i <= n implies p.i = 0)
& (i <= len q implies p.(n+i) = q.i)
& (len q + n < i implies p.i = 0)
proof
let i be Nat;
assume
A537: i in dom p; then
A538: 1<=i & i <= len p by FINSEQ_3:25;
F: dom p = dom T by A153,FINSEQ_3:29; then
A539: p.i = |. vol(divset(T,i) /\ divset(S,(k+1)),rho) .|
by A153,A537;
thus i <= n implies p.i = 0
proof
assume
A540: i <= n;
per cases;
suppose i = 1; then
A542: lower_bound(divset(T,i)) = lower_bound A
& upper_bound(divset(T,i)) = T.i
by INTEGRA1:def 4,F,A537;
divset(T,i) /\ divset(S,(k+1))
= [. lower_bound divset(T,i), upper_bound divset(T,i) .]
/\ [. lower_bound divset(S,(k+1)),
upper_bound divset(S,(k+1)) .] by A169,INTEGRA1:4;
then
divset(T,i) /\ divset(S,(k+1))
c= [.upper_bound divset(T,i),upper_bound divset(T,i) .]
by A170,A364,A537,A540,F,A542,Th10;
hence thesis by A539,COMPLEX1:44,Th11;
end;
suppose
A543: i <> 1; then
1 < i by A538,XXREAL_0:1; then
1+1 <= i by NAT_1:13; then
1+1-1 <= i-1 by XREAL_1:13; then
i-1 in NAT by INT_1:3; then
reconsider i1 = i-1 as Nat;
A544: lower_bound(divset(T,i)) = T.(i-1)
& upper_bound(divset(T,i)) = T.i
by A543,INTEGRA1:def 4,A537,F;
divset(T,i) /\ divset(S,(k+1))
= [. lower_bound divset(T,i), upper_bound divset(T,i) .]
/\ [. lower_bound divset(S,(k+1)),
upper_bound divset(S,(k+1)) .] by A169,INTEGRA1:4;
then
divset(T,i) /\ divset(S,(k+1))
c= [.upper_bound divset(T,i), upper_bound divset(T,i) .]
by A170,A364,A537,A540,A544,F,Th10;
hence thesis by A539,COMPLEX1:44,Th11;
end;
end;
thus i <= len q implies p.(n+i) = q.i
proof
assume
A545: i <= len q;
per cases;
suppose
A546: i = 1;
A547: divset(T,n+1) = [. lower_bound divset(T,n+1),
upper_bound divset(T,n+1) .]
by INTEGRA1:4;
n <> 0 by FINSEQ_3:25,A352; then
A548: n+1 <> 1;
A549: lower_bound(divset(T,n+1)) = T.(n+1-1)
& upper_bound(divset(T,n+1)) = T.(n+1)
by A548,A355,INTEGRA1:def 4;
n < n+1 & n+1 < m by A370,A424,NAT_1:16,XXREAL_0:1; then
A550: T.(n+1) < S.(k+1) by A355,A368;
divset(T,n+1) /\ divset(S,(k+1)) = [. S.k, T.(n+1) .]
by A169,A170,A352,A547,A549,A550,XXREAL_1:143;
hence p.(n+i) = q.i by A153,Z,A456,A546,FINSEQ_3:25;
end;
suppose
i <> 1; then
1 < i by A538,XXREAL_0:1; then
A551: 1+1 <= i by NAT_1:13;
per cases;
suppose
i <> mn; then
i < mn by A452,A545,XXREAL_0:1; then
i+1 <= mn by NAT_1:13; then
i+1-1 <= mn-1 by XREAL_1:9; then
A552: q.i
= |. vol(divset(T,n+i) /\ divset(S,(k+1)),rho) .|
by A451,A457,A551;
i+n <= m-n+n by A452,A545,XREAL_1:7; then
A553: i+n <= len T by A233,XXREAL_0:2;
1+0 <= i+n by A538,XREAL_1:7; then
n+i in Seg len T by A553; then
n+i in dom T by FINSEQ_1:def 3;
hence p.(n+i)=q.i by A153,A552;
end;
suppose
A554: i = mn;
1 <= n+1 by NAT_1:11; then
A556: lower_bound(divset(T,m)) = T.(m-1)
& upper_bound(divset(T,m)) = T.m
by A425,A160,INTEGRA1:def 4;
A557: m-1 < m-0 by XREAL_1:15;
n+1-1 < m-1 by A425,XREAL_1:14; then
A558: S.k < T.m1 < S.(k+1) by A234,A368,A557;
divset(T,m) /\ divset(S,(k+1))
= [.lower_bound(divset(T,m)),
upper_bound(divset(T,m)) .]
/\ [.lower_bound divset(S,(k+1)),
upper_bound divset(S,(k+1)).]
by A169,INTEGRA1:4
.= [. T.m1,upper_bound B .]
by A4,A5,A159,A160,A170,A556,A558,XXREAL_1:143;
hence p.(n+i) = q.i by A153,A160,A452,A454,A554;
end;
end;
end;
thus len q + n < i implies p.i = 0
proof
assume
A559: len q + n < i;
m-1 < m-0 by XREAL_1:15; then
A560: 1 < m by A235,XXREAL_0:2;
A561: lower_bound(divset(T,i)) = T.(i-1)
& upper_bound(divset(T,i)) = T.i
by A452,A559,A560,INTEGRA1:def 4,A537,F;
m+1 <= i by A452,A559,NAT_1:13; then
A562: m+1-1 <= i-1 by XREAL_1:13; then
A563: 1 < i-1 by A560,XXREAL_0:2;
i-1 in NAT by A562,INT_1:3; then
reconsider i1 = i-1 as Nat;
len T - 1 < len T - 0 by XREAL_1:15; then
A565: i1 in dom T by A563,FINSEQ_3:25,A153,A538,XREAL_1:13;
divset(T,i) /\ divset(S,(k+1))
= [. lower_bound divset(T,i), upper_bound divset(T,i) .]
/\ [. lower_bound divset(S,(k+1)),
upper_bound divset(S,(k+1)) .] by A169,INTEGRA1:4;
then
divset(T,i) /\ divset(S,(k+1))
c= [.upper_bound(divset(S,k+1)),
upper_bound(divset(S,k+1)) .]
by A4,A5,A159,A164,A170,A561,A562,A565,Th10;
hence thesis by A539,COMPLEX1:44,Th11;
end;
end;
len p - (len q + n) in NAT by A153,A233,A452,INT_1:5; then
reconsider L = len p - (len q + n) as Nat;
set s = (n |-> (0 qua Real)) ^ q ^ ( L |-> (0 qua Real));
reconsider nn = n, nL = L as Element of NAT by ORDINAL1:def 12;
reconsider z0 = (0 qua Real) as Element of REAL by XREAL_0:def 1;
A566: len(n |-> (0 qua Real)) = len(nn |-> z0)
.= n by FINSEQ_2:133;
A567: len(L |-> (0 qua Real)) = len(nL |-> z0)
.= L by FINSEQ_2:133;
A568: len s = len((n |-> (0 qua Real)) ^q)
+ len(L |-> (0 qua Real)) by FINSEQ_1:22
.= n + len q + L by A566,A567,FINSEQ_1:22
.= len p;
for j be Nat st 1 <= j & j <= len p holds p.j = s.j
proof
let j be Nat;
assume
A569: 1 <= j <= len p; then
A570: j in dom p by FINSEQ_3:25;
set sw = (n |-> (0 qua Real)) ^ q;
A571: len sw = n + len q by A566,FINSEQ_1:22;
per cases;
suppose
A572: j <= n; then
A573: p.j = 0 by A536,A570;
j <= n + len q by A572,NAT_1:12; then
j in Seg len(sw) by A569,A571; then
j in dom sw by FINSEQ_1:def 3; then
A574: s.j = sw.j by FINSEQ_1:def 7;
j in Seg len(n |-> (0 qua Real)) by A566,A569,A572; then
j in dom(n |-> (0 qua Real)) by FINSEQ_1:def 3; then
A575: sw.j = (n |-> (0 qua Real)).j by FINSEQ_1:def 7;
j in Seg n by A569,A572;
hence p.j = s.j by A573,A574,A575,FINSEQ_2:57;
end;
suppose
A576: n < j;
per cases;
suppose
A577: j <= len q + n;
j - n in NAT by A576,INT_1:5; then
reconsider jn = j-n as Nat;
A578: 0+1 <= jn by A576,NAT_1:13,XREAL_1:50;
A579: j - n <= len q + n - n by A577,XREAL_1:9; then
A580: jn in dom q by A578,FINSEQ_3:25;
len q <= len q + n by NAT_1:11; then
len q <= len p by A153,A233,A452,XXREAL_0:2; then
jn <= len p by A579,XXREAL_0:2; then
jn in dom p by FINSEQ_3:25,A578; then
A581: p.(n+jn)=q.jn by A536,A579;
A582: j in dom sw
by A569,A571,A577,FINSEQ_3:25;
s.j = sw.(n+jn) by A582,FINSEQ_1:def 7
.= q.jn by A566,A580,FINSEQ_1:def 7;
hence p.j = s.j by A581;
end;
suppose
A583: len q + n < j;
j - (len q + n) in NAT by A583,INT_1:5; then
reconsider j1 = j - (len q + n) as Nat;
A584: 0+1 <= j1 by A583,NAT_1:13,XREAL_1:50;
j - (len q + n) <= len p - (len q + n)
by A569,XREAL_1:9; then
A585: j1 in Seg L by A584; then
A586: j1 in dom(L |-> (0 qua Real))
by A567,FINSEQ_1:def 3;
s.j = s.(len sw + j1) by A571
.= ( L |-> (0 qua Real) ).j1 by A586,FINSEQ_1:def 7
.= 0 by A585,FINSEQ_2:57;
hence p.j = s.j by A536,A570,A583;
end;
end;
end; then
A587: p = s by A568;
A588: Sum p = Sum(( n |-> (0 qua Real)) ^ q)
+ Sum( L |-> (0 qua Real)) by A587,RVSUM_1:75
.= Sum(( n |-> (0 qua Real))) + Sum q
+ Sum(L |-> (0 qua Real)) by RVSUM_1:75
.= 0 + Sum q +Sum(L |-> (0 qua Real)) by RVSUM_1:81
.= 0 + Sum q by RVSUM_1:81;
thus Sum ST = Sum(F1) + Sum p by A150,A152,A153,RVSUM_1:74
.= Sum(F) by A588,RVSUM_1:75;
end;
end;
end;
end;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
Lm2:
for A be non empty closed_interval Subset of REAL,
rho be Function of A,REAL,
T,S be Division of A,
ST be FinSequence of REAL
st rho is bounded_variation
& len ST = len S
& for j be Nat st j in dom S holds
ex p be FinSequence of REAL
st ST.j = Sum p
& len p = len T
& for i be Nat st i in dom T holds
p.i = |. vol(divset(T,i) /\ divset(S,j),rho) .|
holds
ex H be Division of A, F be var_volume of rho,H
st Sum ST = Sum(F)
proof
let A be non empty closed_interval Subset of REAL,
rho be Function of A,REAL,
T,S be Division of A,
ST be FinSequence of REAL;
assume
A1: rho is bounded_variation
& len ST = len S
& for j be Nat st j in dom S holds
ex p be FinSequence of REAL
st ST.j = Sum p
& len p = len T
& for i be Nat st i in dom T
holds p.i = |. vol(divset(T,i) /\ divset(S,j),rho) .|;
A c= A & lower_bound A = lower_bound A;
hence thesis by A1,Th18;
end;
theorem Th19:
for A be non empty closed_interval Subset of REAL,
rho be Function of A,REAL,
T,S be Division of A
st rho is bounded_variation holds
ex ST be FinSequence of REAL
st len ST = len S
& Sum ST <= total_vd(rho)
& for j be Nat st j in dom S holds
ex p be FinSequence of REAL
st ST.j = Sum p
& len p = len T
& for i be Nat st i in dom T holds
p.i = |. vol(divset(T,i) /\ divset(S,j),rho) .|
proof
let A be non empty closed_interval Subset of REAL,
rho be Function of A,REAL,
T,S be Division of A;
assume
A1: rho is bounded_variation;
defpred P[Nat,object] means
ex p be FinSequence of REAL
st $2 = Sum p
& len p = len T
& for i be Nat st i in dom T
holds p.i = |. vol(divset(T,i) /\ divset(S,$1),rho) .|;
A2: for j be Nat st j in Seg len S holds
ex x be Element of REAL st P[j,x]
proof
let j be Nat;
assume j in Seg len S;
defpred Q[Nat,object] means
$2= |. vol (divset(T,$1) /\ divset(S,j),rho) .|;
A3: for i be Nat st i in Seg len T holds
ex y be Element of REAL st Q[i,y]
proof
let i be Nat;
assume i in Seg len T;
|. vol (divset(T,i) /\ divset(S,j),rho) .| in REAL
by XREAL_0:def 1;
hence thesis;
end;
consider p be FinSequence of REAL such that
A4: dom p = Seg len T
& for i be Nat st i in Seg len T
holds Q[i,p.i] from FINSEQ_1:sch 5(A3);
reconsider x = Sum p as Element of REAL by XREAL_0:def 1;
Z2: dom T = Seg len T by FINSEQ_1:def 3;
len p = len T by A4,FINSEQ_1:def 3; then
P[j,x] by A4,Z2;
hence ex x be Element of REAL st P[j,x];
end;
consider ST be FinSequence of REAL such that
A5: dom ST = Seg len S
& for j be Nat st j in Seg len S
holds P[j,ST.j] from FINSEQ_1:sch 5(A2);
take ST;
thus
A6: len ST = len S by A5,FINSEQ_1:def 3;
a6: dom ST = dom S by A5,FINSEQ_1:def 3; then
consider H be Division of A, F be var_volume of rho,H such that
A7: Sum ST = Sum(F) by A1,A5,A6,Lm2;
thus thesis by A1,A5,A7,INTEGR22:5,a6;
end;
theorem Th20:
for A be non empty closed_interval Subset of REAL,
rho be Function of A,REAL,
u be PartFunc of REAL,REAL
st rho is bounded_variation
& dom u = A
& u|A is uniformly_continuous
holds
for T being DivSequence of A, S be middle_volume_Sequence of rho,u,T
st delta T is convergent & lim delta T = 0
holds middle_sum(S) is convergent
proof
let A be non empty closed_interval Subset of REAL,
rho be Function of A,REAL,
u be PartFunc of REAL,REAL;
assume that
A1: rho is bounded_variation & dom u = A and
A2: u|A is uniformly_continuous;
thus
for T being DivSequence of A, S be middle_volume_Sequence of rho,u,T
st delta T is convergent & lim delta T = 0
holds middle_sum(S) is convergent
proof
let T being DivSequence of A, S be middle_volume_Sequence of rho,u,T;
assume
A4: delta T is convergent & lim delta T = 0;
defpred P[Element of NAT, set] means
ex p being 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 (u|divset((T.$1),i))
& ex z be Real
st z = (u|divset((T.$1),i)).(p.i)
& (S.$1).i = z * (vol (divset((T.$1),i),rho));
A5: 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 (u|divset((T.k),$1)) &
ex c be Real st c = (u|divset((T.k),$1)).($2) &
(S.k).$1 = c * (vol (divset((T.k),$1),rho));
A6: Seg len(T.k) = dom(T.k) by FINSEQ_1:def 3;
A7: 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 Real such that
A8: c in rng (u|divset((T.k),i)) &
(S.k).i = c * (vol(divset((T.k),i),rho)) by A1,INTEGR22:def 5;
consider x be object such that
A9: x in dom (u|divset(T.k,i)) &
c = (u|divset(T.k,i)).x by A8,FUNCT_1:def 3;
reconsider x as Element of REAL by A9;
take x;
thus thesis by A8,A9;
end;
consider p be FinSequence of REAL such that
A10: 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(A7);
take p;
len p = len (T.k) by A10,FINSEQ_1:def 3;
hence thesis by A6,A10,FINSEQ_1:def 11;
end;
consider Fn be sequence of (REAL)* such that
A11: for x be Element of NAT holds P[x, Fn.x] from FUNCT_2:sch 3(A5);
consider Fm be sequence of (REAL)* such that
A12: for x be Element of NAT holds P[x, Fm.x] from FUNCT_2:sch 3(A5);
set TVD = total_vd(rho);
A13: 0 <= TVD by A1,INTEGR22:6;
now
let p be Real;
set pp2= p/2;
set pv = pp2 / (TVD + 1);
assume
B13: p > 0; then
A14: 0 < pp2 & pp2 < p by XREAL_1:215,216; then
A15: 0 < pv by A13,XREAL_1:139; then
pv*(TVD) < pv *(TVD + 1) by XREAL_1:29,68; then
pv*(TVD) < pp2 by A13,XCMPLX_1:87; then
A16: pv*(TVD) < p by A14,XXREAL_0:2;
set p2v = pv/2;
consider sk be Real such that
A17: 0 < sk
& for x1,x2 be Real
st x1 in dom (u|A) & x2 in dom (u|A) & |. x1-x2 .| < sk
holds |.(u|A).x1-(u|A).x2 .| < p2v
by A2,A15,FCONT_2:def 1,XREAL_1:215;
consider m be Nat such that
A18: for i be Nat st m <= i holds |. (delta T).i - 0 .| < sk
by A4,A17,SEQ_2:def 7;
take m;
let n be Nat;
A19: n in NAT & m in NAT by ORDINAL1:def 12;
assume n >= m; then
|. (delta T).n - 0 .| < sk & |. (delta T).m - 0 .| < sk by A18; then
|. delta(T.n) .| < sk & |. delta(T.m) .| < sk by A19,INTEGRA3:def 2;
then
A20: delta(T.n) < sk & delta(T.m) < sk by ABSVALUE:def 1,INTEGRA3:9;
A21: (middle_sum(S)).n = Sum(S.n)
& (middle_sum(S)).m = Sum(S.m)
by INTEGR22:def 7;
consider p1 be FinSequence of REAL such that
A22: p1 = Fn.n & len p1 = len (T.n)
& for i be Nat st i in dom (T.n)
holds
p1.i in dom (u|divset(T.n,i))
& ex z be Real st z = (u|divset(T.n,i)).(p1.i)
& (S.n).i = z * (vol (divset(T.n,i),rho)) by A11,A19;
consider p2 be FinSequence of REAL such that
A23: p2 = Fm.m & len p2 = len (T.m)
& for i be Nat st i in dom (T.m) holds
p2.i in dom (u|divset(T.m,i))
& ex z be Real st z = (u|divset(T.m,i)).(p2.i)
& (S.m).i = z * (vol (divset(T.m,i),rho)) by A12,A19;
defpred H1[object,object,object] means
ex i,j being Nat, z be Real
st $1=i & $2=j & z = (u|divset(T.n,i)).(p1.i)
& $3 = (vol (divset(T.n,i) /\ divset(T.m,j),rho))* z;
A24: 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 REAL & H1[x,y,w]
proof
let x,y be object;
assume
A25: 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 A25,FINSEQ_1:def 3; then
consider z be Real such that
A26: z = (u|divset(T.n,i)).(p1.i)
& (S.n).i = z * (vol (divset(T.n,i),rho)) by A22;
(vol (divset(T.n,i) /\ divset(T.m,j),rho)) * z in REAL
by XREAL_0:def 1;
hence thesis by A26;
end;
consider Snm being Function of [: Seg len (T.n),Seg len (T.m) :],REAL
such that
A27: 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(A24);
A28: for i,j being Nat st i in Seg len (T.n) & j in Seg len (T.m)
holds
ex z be Real
st z = (u|divset(T.n,i)).(p1.i)
& Snm.(i,j) = (vol (divset(T.n,i) /\ divset(T.m,j),rho))* 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 Real
st i=i1 & j=j1 & z = (u|divset(T.n,i1)).(p1.i1)
& Snm.(i,j)= (vol (divset(T.n,i1) /\ divset(T.m,j1),rho))* z by A27;
hence thesis;
end;
defpred P1[Nat,object] means
ex r be FinSequence of REAL
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);
A29: 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
A30: k in Seg len (T.n);
deffunc G(set) = Snm.(k,$1);
consider r being FinSequence such that
A31: len r = len (T.m) and
A32: for j be Nat st j in dom r holds r.j = G(j) from FINSEQ_1:sch 2;
A33: dom r = Seg len (T.m) by A31,FINSEQ_1:def 3;
for j be Nat st j in dom r holds r.j in REAL
proof
let j be Nat;
assume
A34: j in dom r; then
[k,j] in [: Seg len (T.n), Seg len (T.m) :]
by A30,A33,ZFMISC_1:87; then
Snm.(k,j) in REAL by FUNCT_2:5;
hence thesis by A32,A34;
end; then reconsider r as FinSequence of REAL by FINSEQ_2:12;
take x = Sum r;
thus thesis by A32,A33;
end;
consider Xp be FinSequence such that
A35: 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(A29);
for i be Nat st i in dom Xp holds Xp.i in REAL
proof
let i be Nat;
assume i in dom Xp; then
ex r be FinSequence of REAL
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 A35;
hence thesis by XREAL_0:def 1;
end; then
reconsider Xp as FinSequence of REAL by FINSEQ_2:12;
A36: len Xp = len (T.n) by A35,FINSEQ_1:def 3;
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
A38: k in Seg len Xp & k in Seg len (T.n) by A36; then
A39: k in dom Xp & k in dom (T.n) by FINSEQ_1:def 3; then
consider z be Real such that
A40: z = (u|divset(T.n,k)).(p1.k)
& (S.n).k = z * (vol (divset(T.n,k),rho)) by A22;
consider r be FinSequence of REAL such that
A41: 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,A38;
defpred P11[Nat,set] means
$2 = vol (divset(T.n,k) /\ divset(T.m,$1),rho);
A42: 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;
vol(divset(T.n,k) /\ divset(T.m,i), rho) in REAL by XREAL_0:def 1;
hence thesis;
end;
consider vtntm be FinSequence of REAL such that
A43: 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(A42);
A44: dom vtntm = dom r
& for j be Nat st j in dom vtntm holds
vtntm.j=vol (divset(T.n,k) /\ divset(T.m,j),rho)
by A43,FINSEQ_1:def 3;
A45: len vtntm = len r & len (T.m) = len r
by A41,A43,FINSEQ_1:def 3; then
A46: Sum vtntm = vol(divset((T.n),k),rho)
by A39,A43,INTEGR22:1,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
A47: j in dom r; then
A48: ex w be Real
st w = (u|divset(T.n,k)).(p1.k)
& Snm.(k,j) = (vol(divset(T.n,k) /\ divset(T.m,j),rho)) * w
by A28,A38,A41;
take vtntm.j;
r.j = (vol(divset(T.n,k) /\ divset(T.m,j),rho)) * z
by A40,A41,A47,A48;
hence thesis by A44,A47;
end;
hence thesis by A40,A41,A45,A46,Th1;
end; then
A49: Xp = S.n by A1,A36,INTEGR22:def 5;
defpred P2[Nat,object] means
ex s be FinSequence of REAL
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);
A50: 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
A51: k in Seg len (T.m);
deffunc G(set)= Snm.($1,k);
consider s being FinSequence such that
A52: len s = len (T.n) and
A53: for i be Nat st i in dom s holds s.i = G(i) from FINSEQ_1:sch 2;
A54: dom s = Seg len (T.n) by A52,FINSEQ_1:def 3;
for i be Nat st i in dom s holds s.i in REAL
proof
let i be Nat;
assume
A55: i in dom s; then
[i,k] in [: Seg len (T.n), Seg len (T.m) :]
by A51,A54,ZFMISC_1:87; then
Snm.(i,k) in REAL by FUNCT_2:5;
hence thesis by A53,A55;
end; then
reconsider s as FinSequence of REAL by FINSEQ_2:12;
take x = Sum s;
thus thesis by A53,A54;
end;
consider Xq be FinSequence such that
A56: 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(A50);
for j be Nat st j in dom Xq holds Xq.j in REAL
proof
let j be Nat;
assume j in dom Xq; then
ex s be FinSequence of REAL
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 A56;
hence thesis by XREAL_0:def 1;
end; then
reconsider Xq as FinSequence of REAL by FINSEQ_2:12;
defpred H2[object,object,object] means
ex i,j being Nat, z be Real
st $1 = i & $2 = j & z = (u|divset(T.m,j)).(p2.j)
& $3 = (vol((divset(T.n,i) /\ divset(T.m,j)),rho)) * z;
A57: 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 REAL & H2[x,y,w]
proof
let x,y be object;
assume
A58: 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 A58,FINSEQ_1:def 3; then
consider z be Real such that
A59: z = (u|divset(T.m,j)).(p2.j)
& (S.m).j = z * (vol (divset(T.m,j),rho)) by A23;
(vol(divset(T.n,i) /\ divset(T.m,j),rho)) * z in REAL
by XREAL_0:def 1;
hence thesis by A59;
end;
consider Smn being Function of [: Seg len (T.n),Seg len (T.m) :], REAL
such that
A60: 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(A57);
A61: for i,j being Nat st i in Seg len(T.n) & j in Seg len(T.m) holds
ex z be Real st z = (u|divset(T.m,j)).(p2.j)
& Smn.(i,j) = (vol(divset(T.n,i) /\ divset(T.m,j),rho)) * 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 Real
st i = i1 & j = j1 & z = (u|divset(T.m,j1)).(p2.j1)
& Smn.(i,j) = (vol(divset(T.n,i1) /\ divset(T.m,j1),rho)) * z
by A60;
hence thesis;
end;
defpred P3[Nat,object] means
ex s be FinSequence of REAL
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);
A62: 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
A63: k in Seg len(T.m);
deffunc G(set)= Smn.($1,k);
consider s being FinSequence such that
A64: len s = len (T.n) and
A65: for i be Nat st i in dom s holds s.i = G(i) from FINSEQ_1:sch 2;
A66: dom s = Seg len (T.n) by A64,FINSEQ_1:def 3;
for i be Nat st i in dom s holds s.i in REAL
proof
let i be Nat;
assume
A67: i in dom s; then
[i,k] in [: Seg len (T.n), Seg len (T.m) :]
by A63,A66,ZFMISC_1:87; then
Smn.(i,k) in REAL by FUNCT_2:5;
hence thesis by A65,A67;
end; then
reconsider s as FinSequence of REAL by FINSEQ_2:12;
take x = Sum s;
thus thesis by A65,A66;
end;
consider Zq be FinSequence such that
A68: 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(A62);
for j be Nat st j in dom Zq holds Zq.j in REAL
proof
let j be Nat;
assume j in dom Zq; then
ex s be FinSequence of REAL
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 A68;
hence thesis by XREAL_0:def 1;
end; then
reconsider Zq as FinSequence of REAL by FINSEQ_2:12;
A69: len Zq = len(T.m) by A68,FINSEQ_1:def 3;
for k be Nat st 1 <= k & k <= len Zq holds Zq.k = (S.m).k
proof
let k be Nat;
assume
A71: 1 <= k <= len Zq; then
consider s be FinSequence of REAL such that
A72: 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 A68,FINSEQ_3:25;
A73: k in Seg len(T.m) by A69,A71;
A74: k in dom (T.m) by A69,A71,FINSEQ_3:25; then
consider z be Real such that
A75: z = (u|divset((T.m),k)).(p2.k)
& (S.m).k = z * (vol(divset((T.m),k),rho)) by A23;
defpred P11[Nat,set] means
$2 = vol(divset(T.n,$1) /\ divset(T.m,k),rho);
A76: 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;
vol(divset(T.n,i) /\ divset(T.m,k),rho) in REAL by XREAL_0:def 1;
hence thesis;
end;
consider vtntm be FinSequence of REAL such that
A77: 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(A76);
A78: dom vtntm = dom s & len vtntm = len s by A77,FINSEQ_1:def 3;
A79: for j be Nat st j in dom vtntm holds
vtntm.j = vol(divset(T.m,k) /\ divset(T.n,j),rho) by A77;
len s = len (T.n) by A72,FINSEQ_1:def 3; then
A80: Sum vtntm = vol (divset(T.m,k),rho)
by A74,A78,A79,INTEGR22:1,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
A81: j in dom s; then
A82: ex w be Real
st w = (u|divset((T.m),k)).(p2.k)
& Smn.(j,k) = (vol(divset(T.n,j) /\ divset(T.m,k),rho)) * w
by A61,A72,A73;
take vtntm.j;
s.j = (vol(divset(T.n,j) /\ divset(T.m,k),rho))* z
by A72,A75,A81,A82;
hence thesis by A77,A78,A81;
end;
hence thesis by A72,A75,A78,A80,Th1;
end; then
Zq = S.m by A1,A69,INTEGR22:def 5; then
A83: Sum(S.n) - Sum(S.m) = Sum Xq - Sum Zq by A35,A49,A56,INTEGR22:2;
set XZq = Xq - Zq;
A84: dom XZq = dom Xq /\ dom Zq by VALUED_1:12;
reconsider XZq = Xq - Zq as FinSequence of REAL;
len Xq = len Zq by A56,A68,FINSEQ_3:29; then
A86: Xq is Element of (len Xq)-tuples_on REAL
& Zq is Element of (len Xq)-tuples_on REAL by FINSEQ_2:92;
A87: for i,j be Nat, Snmij,Smnij be Real
st i in Seg len (T.n) & j in Seg len (T.m)
& Snmij = Snm.(i,j)
& Smnij = Smn.(i,j)
holds
|. Snmij - Smnij .|
<= |. vol(divset(T.n,i) /\ divset(T.m,j),rho) .| * pv
proof
let i,j be Nat, Snmij,Smnij be Real;
assume
A88: i in Seg len (T.n) & j in Seg len (T.m)
& Snmij = Snm.(i,j) & Smnij = Smn.(i,j); then
consider z1 be Real such that
A89: z1 = (u|divset(T.n,i)).(p1.i)
& Snm.(i,j) = (vol(divset(T.n,i) /\ divset(T.m,j),rho)) * z1
by A28;
consider z2 be Real such that
A90: z2 = (u|divset((T.m),j)).(p2.j)
& Smn.(i,j) = (vol(divset(T.n,i) /\ divset(T.m,j),rho)) * z2
by A61,A88;
A91: i in dom (T.n) & j in dom (T.m) by A88,FINSEQ_1:def 3; then
A92: p1.i in dom (u|divset(T.n,i))
& p2.j in dom (u|divset(T.m,j)) by A22,A23; then
p1.i in dom u /\ divset(T.n,i) & p2.j in dom u /\ divset(T.m,j)
by RELAT_1:61; then
A93: p1.i in dom u & p1.i in divset(T.n,i)
& p2.j in dom u & p2.j in divset(T.m,j) by XBOOLE_0:def 4;
A94: z1 = u.(p1.i) & z2 = u.(p2.j) by A89,A90,A92,FUNCT_1:47;
per cases;
suppose
divset(T.n,i) /\ divset(T.m,j) = {}; then
vol(divset(T.n,i) /\ divset(T.m,j),rho) = (0 qua Real)
by INTEGR22:def 1;
hence |. Snmij - Smnij .|
<= |. (vol (divset(T.n,i) /\ divset(T.m,j),rho)) .| * pv
by A88,A89,A90,COMPLEX1:44;
end;
suppose
divset(T.n,i) /\ divset(T.m,j) <> {}; then
consider t be object such that
A97: t in divset(T.n,i) /\ divset(T.m,j) by XBOOLE_0:def 1;
reconsider t as Real by A97;
A98: divset(T.m,j) c= A by A91,INTEGRA1:8;
A99: t in divset(T.n,i) & t in divset(T.m,j)
by A97,XBOOLE_0:def 4; then
|. (p1.i)-t .| < sk & |. t-(p2.j) .| < sk
by A20,A91,A93,INTEGR20:12; then
A100: |. u.(p1.i)-u.t .| < p2v
& |. u.t-u.(p2.j) .| < p2v by A1,A17,A93,A98,A99;
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
= (vol (DMN,rho)) * (u.(p1.i) - u.t)
+ (vol (DMN,rho)) * (u.t - u.(p2.j))
by A88,A89,A90,A94; then
A101: |. Snmij - Smnij .|
<= |. (vol (DMN,rho)) * (u.(p1.i) -u.t) .|
+ |. (vol (DMN,rho)) * (u.t - u.(p2.j)) .| by COMPLEX1:56;
A102: |. (vol (DMN,rho)) * (u.(p1.i) - u.t) .|
= |. vol (DMN,rho) .| * |. u.(p1.i) - u.t .|
& |. (vol (DMN,rho)) * (u.t - u.(p2.j)) .|
= |.vol (DMN,rho).| * |. u.t - u.(p2.j) .| by COMPLEX1:65;
0 <= |.vol (DMN,rho).| by COMPLEX1:46; then
|. (vol(DMN,rho)) * (u.(p1.i) - u.t) .| <= |.vol(DMN,rho).| * p2v
& |. (vol(DMN,rho)) * (u.t - u.(p2.j)) .| <= |.vol(DMN,rho).| * p2v
by A100,A102,XREAL_1:64; then
|. (vol (DMN,rho)) * (u.(p1.i) - u.t) .|
+ |. (vol (DMN,rho)) * (u.t - u.(p2.j)) .|
<= |.vol (DMN,rho).| * p2v + |.vol (DMN,rho).| * p2v by XREAL_1:7;
hence |. Snmij - Smnij .|
<= |. vol (divset(T.n,i) /\ divset(T.m,j),rho) .| * pv
by A101,XXREAL_0:2;
end;
end;
consider vtntm be FinSequence of REAL such that
A103: len vtntm = len(T.m)
& Sum vtntm <= total_vd(rho)
& for j be Nat st j in dom (T.m) holds
ex p be FinSequence of REAL
st vtntm.j = Sum p
& len p = len (T.n)
& for i be Nat st i in dom (T.n) holds
p.i = |. vol(divset(T.n,i) /\ divset(T.m,j),rho) .|
by A1,Th19;
reconsider PVD = pv * vtntm as FinSequence of REAL;
dom PVD = dom vtntm by VALUED_1:def 5; then
dom PVD = Seg len(T.m) by A103,FINSEQ_1:def 3; then
A104: len PVD = len (T.m) by FINSEQ_1:def 3;
A105: for j be Nat st j in Seg len (T.m) holds
ex pvtntm be FinSequence of REAL
st PVD.j = Sum pvtntm
& len (pvtntm) = len (T.n)
& for i be Nat st i in Seg len (T.n) holds
(pvtntm).i = pv * |. vol(divset(T.n,i) /\ divset(T.m,j),rho) .|
proof
let j be Nat;
assume j in Seg len (T.m); then
j in dom (T.m) by FINSEQ_1:def 3; then
consider v be FinSequence of REAL such that
A107: vtntm.j = Sum v
& len v = len (T.n)
& for i be Nat st i in dom (T.n) holds
v.i = |. vol(divset(T.n,i) /\ divset(T.m,j),rho) .| by A103;
reconsider pvtntm = pv * v as FinSequence of REAL;
take pvtntm;
thus PVD.j = pv * vtntm.j by VALUED_1:6
.= Sum pvtntm by A107,RVSUM_1:87;
dom pvtntm = dom v by VALUED_1:def 5; then
dom pvtntm = Seg len(T.n) by A107,FINSEQ_1:def 3;
hence len pvtntm = len(T.n) by FINSEQ_1:def 3;
let i be Nat;
assume i in Seg len (T.n); then
a108: i in dom (T.n) by FINSEQ_1:def 3;
thus (pvtntm).i = pv * v.i by VALUED_1:6
.= pv * |. vol(divset(T.n,i) /\ divset(T.m,j),rho) .|
by A107,a108;
end;
A109: Sum(PVD) = pv * Sum(vtntm) by RVSUM_1:87;
A110: pv * Sum(vtntm) <= pv * total_vd(rho)
by A13,B13,A103,XREAL_1:64;
A111: len XZq = len (T.m) by A56,A68,A84,FINSEQ_1:def 3;
for j be Nat st j in dom XZq holds |. XZq.j .| <= PVD.j
proof
let j be Nat;
assume
A112: j in dom XZq; then
A113: XZq.j = Xq.j - Zq.j by VALUED_1:13;
consider Xsq be FinSequence of REAL such that
A114: 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 A56,A68,A84,A112;
consider Zsq be FinSequence of REAL such that
A115: 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 A56,A68,A84,A112;
set XZsq = Xsq - Zsq;
A116: dom XZsq = dom Xsq /\ dom Zsq by VALUED_1:12;
reconsider XZsq as FinSequence of REAL;
A117: len XZsq = len (T.n) by A114,A115,A116,FINSEQ_1:def 3;
consider pvtntm be FinSequence of REAL such that
A118: PVD.j = Sum pvtntm
& len (pvtntm) = len (T.n)
& for i be Nat st i in Seg len (T.n) holds
(pvtntm).i = pv * |. vol(divset(T.n,i) /\ divset(T.m,j),rho) .|
by A105,A56,A68,A84,A112;
for i be Nat st i in dom XZsq holds |. XZsq.i .| <= (pvtntm).i
proof
let i be Nat;
assume
A119: i in dom XZsq; then
A120: XZsq.i = Xsq.i - Zsq.i by VALUED_1:13;
A121: (pvtntm).i
= pv * |. vol(divset(T.n,i) /\ divset(T.m,j),rho) .|
by A118,A114,A115,A116,A119;
Xsq.i = Snm.(i,j) & Zsq.i = Smn.(i,j)
by A114,A115,A116,A119;
hence |.XZsq.i.| <= pvtntm.i
by A56,A68,A84,A87,A112,A114,A115,A116,A119,A120,A121;
end; then
A122: |. Sum XZsq .| <= PVD.j by A117,A118,Th3;
len Xsq = len Zsq by A114,A115,FINSEQ_3:29; then
Xsq is Element of (len Xsq)-tuples_on REAL
& Zsq is Element of (len Xsq)-tuples_on REAL by FINSEQ_2:92;
hence thesis by A113,A114,A115,A122,RVSUM_1:90;
end; then
|. Sum XZq .| <= Sum PVD by A104,A111,Th3; then
A124: |. Sum XZq .| <= TVD * pv by A109,A110,XXREAL_0:2;
Sum (XZq) = ((middle_sum(S)).n) - ((middle_sum(S)).m)
by A21,A83,A86,RVSUM_1:90;
hence |.((middle_sum(S)).n) - ((middle_sum(S)).m).| < p
by A16,A124,XXREAL_0:2;
end;
hence middle_sum(S) is convergent by SEQ_4:41;
end;
end;
theorem Th21:
for A be non empty closed_interval Subset of REAL,
rho be Function of A,REAL,
u be PartFunc of REAL,REAL,
T0,T,T1 be DivSequence of A,
S0 be middle_volume_Sequence of rho,u,T0,
S be middle_volume_Sequence of rho,u,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 rho,u,T1
st for i be Nat holds S1.(2*i) = S0.i & S1.(2*i+1) = S.i
proof
let A be non empty closed_interval Subset of REAL,
rho be Function of A,REAL,
u be PartFunc of REAL,REAL,
T0,T,T1 be DivSequence of A,
S0 be middle_volume_Sequence of rho,u,T0,
S be middle_volume_Sequence of rho,u,T;
assume
A2: for k be Nat holds T1.(2*k) = T0.k & T1.(2*k+1) = T.k;
reconsider SS0 = S0, SS = S as sequence of (REAL)*;
deffunc F(Nat) = In(SS0.$1, (REAL)*);
deffunc G(Nat) = In(SS.$1, (REAL)*);
consider S1 being sequence of (REAL)* such that
A3: for n be Nat holds S1.(2*n) = F(n) & S1.(2*n+1) = G(n)
from INTEGR20:sch 1;
for i be Element of NAT holds S1.i is middle_volume of rho,u,T1.i
proof
let i be Element of NAT;
consider k be Nat such that
A4: i = 2*k or i = 2*k+1 by INTEGR20:14;
reconsider k as Element of NAT by ORDINAL1:def 12;
per cases by A4;
suppose
A5: i = 2*k; then
S1.i = In(SS0.k, (REAL)*) by A3
.= S0.k by FUNCT_2:5,SUBSET_1:def 8;
hence S1.i is middle_volume of rho,u,T1.i by A2,A5;
end;
suppose
A6: i = 2*k + 1; then
S1.i = In(SS.k, (REAL)*) by A3
.= S.k by FUNCT_2:5,SUBSET_1:def 8;
hence S1.i is middle_volume of rho,u,T1.i by A2,A6;
end;
end; then
reconsider S1 as middle_volume_Sequence of rho,u,T1 by INTEGR22:def 6;
take S1;
let i be Nat;
A7: i is Element of NAT by ORDINAL1:def 12;
A8: S1.(2*i) = In(SS0.i,(REAL)*) by A3
.= S0.i by A7,FUNCT_2:5,SUBSET_1:def 8;
S1.(2*i+1) = In(SS.i,(REAL)*) by A3
.= S.i by A7,FUNCT_2:5,SUBSET_1:def 8;
hence thesis by A8;
end;
theorem Th22:
for Sq0,Sq,Sq1 be Real_Sequence
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 Sq0,Sq,Sq1 be Real_Sequence;
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,SEQ_2:def 7;
consider k be Nat such that
A5: m = 2*k or m = 2*k+1 by INTEGR20:14;
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 by SEQ_2:def 6;
hence lim Sq0 = lim Sq1 by A3,SEQ_2: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,SEQ_2:def 7;
consider k be Nat such that
A9: m = 2*k or m = 2*k+1 by INTEGR20:14;
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 by SEQ_2:def 6;
hence lim Sq = lim Sq1 by SEQ_2:def 7,A7;
end;
theorem
for A be non empty closed_interval Subset of REAL,
rho be Function of A,REAL,
u be continuous PartFunc of REAL,REAL st
rho is bounded_variation & dom u = A
holds u is_RiemannStieltjes_integrable_with rho
proof
let A be non empty closed_interval Subset of REAL,
rho be Function of A,REAL,
u be continuous PartFunc of REAL,REAL;
assume
A1: rho is bounded_variation & dom u = A;
A2: u|A is uniformly_continuous by A1,FCONT_2:11;
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 rho,u,T0;
set I = lim middle_sum(S0);
for T being DivSequence of A,
S be middle_volume_Sequence of rho,u,T
st delta T is convergent & lim delta T = 0
holds middle_sum(S) is convergent & lim middle_sum(S) = I
proof
let T be DivSequence of A, S be middle_volume_Sequence of rho,u,T;
assume
A4: delta T is convergent & lim delta T = 0;
hence middle_sum(S) is convergent by A1,A2,Th20;
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 INTEGR20:15;
consider S1 be middle_volume_Sequence of rho,u,T1 such that
A6: for i be Nat holds S1.(2*i) = S0.i & S1.(2*i+1) = S.i
by A5,Th21;
delta T1 is convergent & lim delta T1 = 0 by A3,A4,A5,INTEGR20:16; then
A7: middle_sum(S1) is convergent by A1,A2,Th20;
A8: for i be Nat holds
(middle_sum(S1)).(2*i) = (middle_sum(S0)).i
& (middle_sum(S1)).(2*i+1) = (middle_sum(S)).i
proof
let i be Nat;
reconsider S1 as middle_volume_Sequence of rho,u,T1;
S1.(2*i) = S0.i & T1.(2*i) = T0.i
& S1.(2*i+1) = S.i & T1.(2*i+1) = T.i by A5,A6; then
(middle_sum(S1)).(2*i) = Sum(S0.i)
& (middle_sum(S1)).(2*i+1) = Sum(S.i)
by INTEGR22:def 7;
hence thesis by INTEGR22:def 7;
end;
lim middle_sum(S) = lim middle_sum(S1) by A7,A8,Th22;
hence lim middle_sum(S) = lim middle_sum(S0) by A7,A8,Th22;
end;
hence u is_RiemannStieltjes_integrable_with rho by INTEGR22:def 8;
end;