:: The Definition of Riemann Definite Integral and some Related Lemmas
:: by Noboru Endou and Artur Korni{\l}owicz
::
:: Received March 13, 1999
:: Copyright (c) 1999-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 FINSEQ_1, RCOMP_1, ORDINAL2, ARYTM_1, RELAT_1, FUNCT_1, PARTFUN1,
CARD_3, XBOOLE_0, FUNCT_3, ZFMISC_1, XXREAL_0, REAL_1, SUBSET_1,
FINSEQ_2, RFINSEQ, JORDAN3, SEQ_4, CARD_1, INTEGRA1, FUNCOP_1, VALUED_0,
NUMBERS, MEASURE7, ORDINAL4, XXREAL_1, XXREAL_2, NAT_1, ARYTM_3, TARSKI,
MEMBER_1, MEASURE5, FUNCT_7, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, NAT_D, RELAT_1, FUNCT_1,
RELSET_1, VALUED_0, MEMBERED, MEMBER_1, VALUED_1, SEQ_4, XXREAL_2,
COMSEQ_2, SEQ_2, RCOMP_1, FINSEQ_2, PARTFUN2, RFUNCT_1, RVSUM_1, RFINSEQ,
FINSEQ_6, PARTFUN1, FINSEQ_1, FUNCT_2, MEASURE5, MEASURE6;
constructors PARTFUN1, REAL_1, NAT_1, RCOMP_1, FINSOP_1, PARTFUN2, RFUNCT_1,
REALSET1, RFINSEQ, BINARITH, FINSEQ_5, SEQM_3, MEASURE6, FINSEQ_6,
BINOP_2, XXREAL_2, NAT_D, RVSUM_1, SEQ_4, RELSET_1, SEQ_2, MEMBER_1,
XXREAL_3, MEASURE5, COMSEQ_2, NUMBERS;
registrations SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0, NAT_1,
MEMBERED, FINSEQ_1, FINSEQ_2, SEQM_3, VALUED_0, VALUED_1, FINSET_1,
XXREAL_2, CARD_1, SEQ_2, RELSET_1, MEMBER_1, MEASURE5;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, XXREAL_2, FUNCT_2;
equalities XBOOLE_0, RVSUM_1;
expansions TARSKI, XBOOLE_0, XXREAL_2;
theorems TARSKI, RCOMP_1, FINSEQ_1, FINSEQ_2, SEQ_4, FUNCT_1, NAT_1, NAT_2,
SUBSET_1, PARTFUN1, RFUNCT_1, MEASURE6, RVSUM_1, PARTFUN2, ZFMISC_1,
FUNCT_3, FINSEQ_4, RFINSEQ, RELAT_1, FUNCT_2, XBOOLE_0, XBOOLE_1,
FUNCOP_1, XREAL_1, XXREAL_0, FINSOP_1, ORDINAL1, XXREAL_1, VALUED_1,
FINSEQ_3, XXREAL_2, SEQM_3, NAT_D, FINSEQ_6, MEMBER_1, MEMBERED, CARD_1,
MEASURE5, XREAL_0;
schemes FINSEQ_2, NAT_1, FUNCT_2, XFAMILY;
begin :: Definition of closed interval and its properties
reserve a,a1,b,b1,x,y for Real,
F,G,H for FinSequence of REAL,
i,j,k,n,m for Element of NAT,
I for Subset of REAL,
X for non empty set,
x1,R,s for set;
reserve A for non empty closed_interval Subset of REAL;
registration
cluster closed_interval -> compact for Subset of REAL;
coherence
proof let IT be Subset of REAL;
assume IT is closed_interval;
then ex a,b being Real st IT = [.a,b.] by MEASURE5:def 3;
hence thesis by RCOMP_1:6;
end;
end;
::$CT 2
theorem Th1:
A is bounded_below bounded_above
proof
A is real-bounded by RCOMP_1:10;
hence thesis;
end;
registration
cluster non empty closed_interval -> real-bounded for Subset of REAL;
coherence by Th1;
end;
reserve A, B for non empty closed_interval Subset of REAL;
theorem Th2:
A = [. lower_bound A, upper_bound A .]
proof
consider a,b being Real such that
A1: a <= b and
A2: A=[.a,b.] by MEASURE5:14;
A3: for y be Real st 0<y ex x be Real st x in A & b-y<x
proof
let y be Real;
assume
A4: 0<y;
take b;
b < b+y by A4,XREAL_1:29;
then b-y < b+y-y by XREAL_1:9;
hence thesis by A1,A2,XXREAL_1:1;
end;
A5: for x be Real st x in A holds x <= b
proof
let x be Real;
assume
A6: x in A;
A={y:a <= y & y <= b} by A2,RCOMP_1:def 1;
then ex y st x=y & a <= y & y <= b by A6;
hence thesis;
end;
A7: for x be Real st x in A holds a <= x
proof
let x be Real;
assume
A8: x in A;
A={y:a <= y & y <= b} by A2,RCOMP_1:def 1;
then ex y st x=y & a <= y & y <= b by A8;
hence thesis;
end;
for y be Real st 0<y ex x be Real st x in A & x<a + y
proof
let y be Real;
assume
A9: 0<y;
take a;
thus thesis by A1,A2,A9,XREAL_1:29,XXREAL_1:1;
end;
then a=lower_bound A by A7,SEQ_4:def 2;
hence thesis by A2,A5,A3,SEQ_4:def 1;
end;
theorem Th3:
for a1,a2,b1,b2 being Real holds A=[.a1,b1.] & A=[.a2,b2.]
implies a1=a2 & b1=b2
proof
let a1,a2,b1,b2 be Real;
assume that
A1: A=[.a1,b1.] and
A2: A=[.a2,b2.];
a1 <= b1 by A1,XXREAL_1:29;
hence thesis by A1,A2,XXREAL_1:66;
end;
begin :: Definition of division of closed interval and its properties
definition
::$CD
let A be non empty compact Subset of REAL;
mode Division of A -> non empty increasing FinSequence of REAL means
:Def1:
rng it c= A & it.(len it) = upper_bound A;
existence
proof
reconsider a = upper_bound A as Element of REAL by XREAL_0:def 1;
reconsider p = Seg 1 --> a as Function of Seg 1, REAL by FUNCOP_1:45;
A1: dom p = Seg 1 by FUNCOP_1:13;
rng p c= REAL;
then reconsider p as FinSequence of REAL by FINSEQ_1:def 4;
A2: 1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
for n,m being Nat st n in dom p & m in dom p & n<m holds p.n < p.m
proof
let n,m be Nat;
assume that
A3: n in dom p and
A4: m in dom p;
n = 1 by A1,A3,FINSEQ_1:2,TARSKI:def 1;
hence thesis by A1,A4,FINSEQ_1:2,TARSKI:def 1;
end;
then
A5: p is non empty increasing FinSequence of REAL by SEQM_3:def 1;
upper_bound A in A by RCOMP_1:14;
then for n being Nat st n in Seg 1 holds p.n in A by FUNCOP_1:7;
then p is FinSequence of A by A1,FINSEQ_2:12;
then
A6: rng p c= A by FINSEQ_1:def 4;
len p = 1 by A1,FINSEQ_1:def 3;
then p.(len p)=upper_bound A by A2,FUNCOP_1:7;
hence thesis by A6,A5;
end;
end;
definition
let A be non empty compact Subset of REAL;
func divs A -> set means
:Def2:
x1 in it iff x1 is Division of A;
existence
proof
defpred P[set] means $1 is Division of A;
consider R such that
A1: x1 in R iff x1 in bool [:NAT,REAL:] & P[x1] from XFAMILY:sch 1;
take R;
let x1;
thus x1 in R implies x1 is Division of A by A1;
assume x1 is Division of A;
then reconsider p = x1 as Division of A;
p c= [:NAT,REAL:];
hence thesis by A1;
end;
uniqueness
proof
let D1,D2 be set such that
A2: x1 in D1 iff x1 is Division of A and
A3: x1 in D2 iff x1 is Division of A;
now
let x1 be object;
thus x1 in D1 implies x1 in D2
proof
assume x1 in D1;
then x1 is Division of A by A2;
hence thesis by A3;
end;
assume x1 in D2;
then x1 is Division of A by A3;
hence x1 in D1 by A2;
end;
hence thesis by TARSKI:2;
end;
end;
registration
let A be non empty compact Subset of REAL;
cluster divs A -> non empty;
coherence
proof
the Division of A in divs A by Def2;
hence thesis;
end;
end;
registration
let A be non empty compact Subset of REAL;
cluster -> Function-like Relation-like for Element of divs A;
coherence by Def2;
end;
registration
let A be non empty compact Subset of REAL;
cluster -> real-valued FinSequence-like for Element of divs A;
coherence by Def2;
end;
reserve r for Real;
reserve D, D1, D2 for Division of A;
reserve f, g for Function of A,REAL;
theorem Th4:
i in dom D implies D.i in A
proof
assume i in dom D; then
A1: D.i in rng D by FUNCT_1:def 3;
rng D c= A by Def1;
hence thesis by A1;
end;
theorem Th5:
i in dom D & i<>1 implies i-1 in dom D & D.(i-1) in A & i-1 in NAT
proof
assume that
A1: i in dom D and
A2: i<>1;
consider j be Nat such that
A3: dom D = Seg j by FINSEQ_1:def 2;
i<>0 by A1,A3,FINSEQ_1:1; then
A4: i is non trivial by A2,NAT_2:def 1;
then consider l being Nat such that
A5: i=2+l by NAT_1:10,NAT_2:29;
reconsider l as Element of NAT by ORDINAL1:def 12;
i >= 2 by A4,NAT_2:29;
then
A6: 1+1-1 <= i-1 by XREAL_1:9;
i<=j by A1,A3,FINSEQ_1:1;
then
A7: i-1<=j-0 by XREAL_1:13;
A8: rng D c= A by Def1;
A9: l+1=i-(2-1) by A5;
then i-1 in dom D by A3,A6,A7,FINSEQ_1:1;
then D.(i-1) in rng D by FUNCT_1:def 3;
hence thesis by A3,A6,A7,A9,A8,FINSEQ_1:1;
end;
definition
let A be non empty closed_interval Subset of REAL;
let D be Division of A;
let i be Nat;
assume
A1: i in dom D;
func divset(D,i) -> non empty closed_interval Subset of REAL means
:Def3:
lower_bound it = lower_bound A & upper_bound it = D.i if i=1
otherwise lower_bound it = D.(i-1) & upper_bound it = D.i;
existence
proof
hereby
assume i=1;
thus ex IT being non empty closed_interval Subset of REAL
st lower_bound IT =
lower_bound A & upper_bound IT = D.i
proof
consider I such that
A2: I=[.lower_bound A,D.i .];
D.i in A by A1,Th4;
then lower_bound A <= D.i by SEQ_4:def 2;
then
A3: I is non empty closed_interval Subset of REAL by A2,MEASURE5:14;
then
A4: I = [.lower_bound I,upper_bound I.] by Th2;
then
A5: upper_bound I = D.i by A2,A3,Th3;
lower_bound I = lower_bound A by A2,A3,A4,Th3;
hence thesis by A3,A5;
end;
end;
assume that
A6: i<>1;
thus ex IT being non empty closed_interval Subset of REAL
st lower_bound IT = D.(i-1
) & upper_bound IT = D.i
proof
reconsider j=i-1 as Element of NAT by A1,A6,Th5;
A7: i+-1< i+(1+-1) by XREAL_1:6;
consider a1,b1 such that
A8: a1=D.(i-1) and
A9: b1=D.i;
consider I such that
A10: I=[.a1,b1.];
i-1 in dom D by A1,A6,Th5;
then D.j < D.i by A1,A7,SEQM_3:def 1;
then
A11: I is non empty closed_interval Subset of REAL by A8,A9,A10,MEASURE5:14;
then
A12: I=[.lower_bound I,upper_bound I.] by Th2;
then
A13: upper_bound I=D.i by A9,A10,A11,Th3;
lower_bound I=D.(i-1) by A8,A10,A11,A12,Th3;
hence thesis by A11,A13;
end;
end;
uniqueness
proof
let A1,A2 be non empty closed_interval Subset of REAL;
hereby
consider b such that
A14: b=D.i;
assume that
i=1 and
A15: lower_bound A1 =lower_bound A and
A16: upper_bound A1 = D.i and
A17: lower_bound A2 =lower_bound A and
A18: upper_bound A2 = D.i;
A1=[. lower_bound A, b .] by A15,A16,A14,Th2;
hence A1=A2 by A17,A18,A14,Th2;
end;
assume that
i<>1 and
A19: lower_bound A1 = D.(i-1) and
A20: upper_bound A1 = D.i and
A21: lower_bound A2 = D.(i-1) and
A22: upper_bound A2 = D.i;
consider a,b such that
A23: a=D.(i-1) and
A24: b=D.i;
A1=[.a,b.] by A19,A20,A23,A24,Th2;
hence thesis by A21,A22,A23,A24,Th2;
end;
correctness;
end;
theorem Th6:
i in dom D implies divset(D,i) c= A
proof
assume
A1: i in dom D;
now
per cases;
suppose
A2: i=1;
lower_bound A in A by RCOMP_1:14;
then
A3: lower_bound A in [.lower_bound A,upper_bound A.] by Th2;
A4: lower_bound divset(D,i) = lower_bound A by A1,A2,Def3;
consider b such that
A5: b=D.i;
upper_bound divset(D,i) = b by A1,A2,A5,Def3;
then
A6: divset(D,i)=[. lower_bound A,b .] by A4,Th2;
b in A by A1,A5,Th4;
then b in [.lower_bound A,upper_bound A.] by Th2;
then [. lower_bound A,b .] c= [.lower_bound A,upper_bound A.]
by A3,XXREAL_2:def 12;
hence thesis by A6,Th2;
end;
suppose
A7: i<>1;
set b=D.i;
b in A by A1,Th4; then
A8: b in [.lower_bound A,upper_bound A.] by Th2;
set a=D.(i-1);
D.(i-1) in A by A1,A7,Th5;
then a in [.lower_bound A,upper_bound A.] by Th2; then
A9: [.a,b.] c= [.lower_bound A,upper_bound A.] by A8,XXREAL_2:def 12;
A10: upper_bound divset(D,i) = b by A1,A7,Def3;
lower_bound divset(D,i) = a by A1,A7,Def3;
then divset(D,i)=[.a,b.] by A10,Th2;
hence thesis by A9,Th2;
end;
end;
hence thesis;
end;
definition
let A be Subset of REAL;
func vol(A) -> Real equals
upper_bound A - lower_bound A;
correctness;
end;
theorem
for A be real-bounded non empty Subset of REAL holds 0 <= vol(A)
by SEQ_4:11,XREAL_1:48;
begin :: Definitions of integrability and related topics
definition
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of A,REAL;
let D be Division of A;
func upper_volume(f,D) -> FinSequence of REAL means
:Def5:
len it = len D &
for i be Nat st i in dom D holds it.i=(upper_bound rng (f|divset(D,i)))*vol
divset(D,i);
existence
proof
deffunc F(Nat)=
In(upper_bound (rng (f|divset(D,$1)))*vol(divset(D,$1)),REAL);
consider IT being FinSequence of REAL such that
A1: len IT = len D & for i be Nat st i in dom IT holds IT.i=F(i) from
FINSEQ_2:sch 1;
take IT;
thus len IT = len D by A1;
let i be Nat;
A2: F(i)=
upper_bound (rng (f|divset(D,i)))*vol(divset(D,i));
assume i in dom D;
then i in dom IT by A1,FINSEQ_3:29;
hence thesis by A1,A2;
end;
uniqueness
proof
let s1,s2 be FinSequence of REAL such that
A3: len s1 = len D and
A4: for i be Nat st i in dom D holds s1.i=(upper_bound (rng (f|divset(
D, i))))*vol(divset(D,i)) and
A5: len s2 = len D and
A6: for i be Nat st i in dom D holds s2.i=(upper_bound (rng (f|divset(
D, i))))*vol(divset(D,i));
A7: dom s1 = dom D by A3,FINSEQ_3:29;
for i being Nat st i in dom s1 holds s1.i=s2.i
proof
let i be Nat;
assume
A8: i in dom s1;
then s1.i=(upper_bound (rng (f|divset(D,i))))*vol(divset(D,i)) by A4,A7;
hence thesis by A6,A7,A8;
end;
hence thesis by A3,A5,FINSEQ_2:9;
end;
func lower_volume(f,D) -> FinSequence of REAL means
:Def6:
len it = len D &
for i be Nat st i in dom D holds it.i=(lower_bound rng (f|divset(D,i)))*vol
divset(D,i);
existence
proof
deffunc F(Nat)=
In((lower_bound (rng (f|divset(D,$1))))*vol(divset(D,$1)),REAL);
consider IT being FinSequence of REAL such that
A9: len IT = len D & for i be Nat st i in dom IT holds IT.i=F(i) from
FINSEQ_2:sch 1;
take IT;
thus len IT = len D by A9;
let i be Nat;
A10: In((lower_bound (rng (f|divset(D,i))))*vol(divset(D,i)),REAL)
= (lower_bound (rng (f|divset(D,i))))*vol(divset(D,i));
assume i in dom D;
then i in dom IT by A9,FINSEQ_3:29;
hence thesis by A9,A10;
end;
uniqueness
proof
let s1,s2 be FinSequence of REAL such that
A11: len s1 = len D and
A12: for i be Nat st i in dom D holds s1.i=(lower_bound (rng (f|divset
(D,i))))*vol(divset(D,i)) and
A13: len s2 = len D and
A14: for i be Nat st i in dom D holds s2.i=(lower_bound (rng (f|divset
(D,i))))*vol(divset(D,i));
A15: dom s1 = dom D by A11,FINSEQ_3:29;
for i being Nat st i in dom s1 holds s1.i=s2.i
proof
let i be Nat;
assume
A16: i in dom s1;
then s1.i=(lower_bound (rng (f|divset(D,i))))*vol(divset(D,i)) by A12,A15
;
hence thesis by A14,A15,A16;
end;
hence thesis by A11,A13,FINSEQ_2:9;
end;
end;
definition
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of A,REAL;
let D be Division of A;
func upper_sum(f,D) -> Real equals
Sum(upper_volume(f,D));
correctness;
func lower_sum(f,D) -> Real equals
Sum(lower_volume(f,D));
correctness;
end;
definition
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of A,REAL;
set S = divs A;
func upper_sum_set(f) -> Function of divs A,REAL means
:Def9:
for D be Division of A holds it.D=upper_sum(f,D);
existence
proof
defpred P[Element of S,set] means
ex D being Division of A st D = $1 & $2 = upper_sum(f,D);
A1: for x being Element of S ex y being Element of REAL st P[x,y]
proof let x be Element of S;
reconsider x as Division of A by Def2;
take upper_sum(f,x);
thus thesis;
end;
consider g being Function of S,REAL such that
A2: for x being Element of S holds P[x,g.x] from FUNCT_2:sch 3(A1);
take g;
let D be Division of A;
reconsider D1 = D as Element of S by Def2;
P[D1,g.D1] by A2;
hence thesis;
end;
uniqueness
proof
let g1,g2 be Function of S,REAL such that
A3: for D be Division of A holds g1.D = upper_sum(f,D) and
A4: for D be Division of A holds g2.D = upper_sum(f,D);
let a be Element of S;
reconsider d = a as Division of A by Def2;
thus g1.a = upper_sum(f,d) by A3
.= g2.a by A4;
end;
func lower_sum_set(f) -> Function of divs A,REAL means
:Def10:
for D be Division of A holds it.D=lower_sum(f,D);
existence
proof
defpred P[Element of S,set] means ex D being Division of A st D = $1 & $2
= lower_sum(f,D);
A5: for x being Element of S ex y being Element of REAL st P[x,y]
proof let x be Element of S;
reconsider x as Division of A by Def2;
take lower_sum(f,x);
thus thesis;
end;
consider g being Function of S,REAL such that
A6: for x being Element of S holds P[x,g.x] from FUNCT_2:sch 3(A5);
take g;
let D be Division of A;
reconsider D1 = D as Element of S by Def2;
P[D1,g.D1] by A6;
hence thesis;
end;
uniqueness
proof
let g1,g2 be Function of S,REAL such that
A7: for D be Division of A holds g1.D = lower_sum(f,D) and
A8: for D be Division of A holds g2.D = lower_sum(f,D);
let a be Element of S;
reconsider d = a as Division of A by Def2;
thus g1.a = lower_sum(f,d) by A7
.= g2.a by A8;
end;
end;
definition
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of A,REAL;
attr f is upper_integrable means
rng upper_sum_set(f) is bounded_below;
attr f is lower_integrable means
rng lower_sum_set(f) is bounded_above;
end;
definition
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of A,REAL;
func upper_integral(f) -> Real equals
lower_bound rng upper_sum_set(f);
correctness;
end;
definition
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of A,REAL;
func lower_integral(f) -> Real equals
upper_bound rng lower_sum_set(f);
coherence;
end;
definition
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of A,REAL;
attr f is integrable means
f is upper_integrable lower_integrable &
upper_integral(f) = lower_integral(f);
end;
definition
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of A,REAL;
func integral(f) -> Real equals
upper_integral(f);
coherence;
end;
begin :: Real function's properties
theorem Th8:
for f,g be PartFunc of X,REAL holds rng(f+g) c= rng f ++ rng g
proof
let f,g be PartFunc of X,REAL;
let y be object;
assume y in rng(f+g);
then consider x1 being object such that
A1: x1 in dom(f+g) and
A2: y=(f+g).x1 by FUNCT_1:def 3;
A3: dom(f+g)=dom f /\ dom g by VALUED_1:def 1;
then x1 in dom f by A1,XBOOLE_0:def 4; then
A4: f.x1 in rng f by FUNCT_1:def 3;
x1 in dom g by A1,A3,XBOOLE_0:def 4;
then
A5: g.x1 in rng g by FUNCT_1:def 3;
(f+g).x1=f.x1+g.x1 by A1,VALUED_1:def 1;
hence thesis by A2,A4,A5,MEMBER_1:46;
end;
theorem Th9:
for f be real-valued Function holds f is bounded_below implies
rng f is bounded_below
proof
let f be real-valued Function;
set X = dom f;
AA: f|X = f;
assume f is bounded_below;
then consider a be Real such that
A1: for x1 being object st x1 in X /\ dom f holds a <= f.x1 by AA,RFUNCT_1:71;
a is LowerBound of rng f
proof
let y be ExtReal;
assume y in rng f;
then ex s being object st s in dom f & y = f.s by FUNCT_1:def 3;
hence thesis by A1;
end;
hence thesis;
end;
theorem
for f be real-valued Function st rng f is bounded_below holds
f is bounded_below
proof
let f be real-valued Function;
set X = dom f;
assume rng f is bounded_below;
then consider a be Real such that
A1: a is LowerBound of rng f;
AA: f|X = f;
for x1 being object st x1 in X /\ dom f holds a <= f.x1
proof
let x1 be object;
assume x1 in X /\ dom f;
then f.x1 in rng f by FUNCT_1:def 3;
hence thesis by A1,XXREAL_2:def 2;
end;
hence thesis by AA,RFUNCT_1:71;
end;
theorem Th11:
for f be real-valued Function st f is bounded_above holds
rng f is bounded_above
proof
let f be real-valued Function;
set X = dom f;
AA: f|X = f;
assume f is bounded_above;
then consider a be Real such that
A1: for x1 being object st x1 in X /\ dom f holds f.x1 <= a by AA,RFUNCT_1:70;
a is UpperBound of rng f
proof
let y be ExtReal;
assume y in rng f;
then ex s being object st s in dom f & y = f.s by FUNCT_1:def 3;
hence thesis by A1;
end;
hence thesis;
end;
theorem
for f be real-valued Function st rng f is bounded_above holds
f is bounded_above
proof
let f be real-valued Function;
set X = dom f;
assume rng f is bounded_above;
then consider a be Real such that
A1: a is UpperBound of rng f;
AA: f|X = f;
for x1 being object st x1 in X /\ dom f holds f.x1 <= a
proof
let x1 be object;
assume x1 in X /\ dom f;
then f.x1 in rng f by FUNCT_1:def 3;
hence thesis by A1,XXREAL_2:def 1;
end;
hence thesis by AA,RFUNCT_1:70;
end;
theorem
for f be real-valued Function holds f is bounded implies
rng f is real-bounded by Th11,Th9;
begin :: Characteristic function's properties
theorem Th14:
for A be non empty set holds chi(A,A)|A is constant
proof
let A be non empty set;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
for x being Element of A st x in A /\ dom chi(A,A) holds chi(A,A)/.x=jj
proof
let x be Element of A;
assume x in A /\ dom chi(A,A); then
A1: x in dom chi(A,A) by XBOOLE_0:def 4;
chi(A,A).x=1 by FUNCT_3:def 3;
hence thesis by A1,PARTFUN1:def 6;
end;
hence thesis by PARTFUN2:35;
end;
theorem Th15:
for A be non empty Subset of X holds rng chi(A,A) = {1}
proof
let A be non empty Subset of X;
A1: chi(A,A)|A is constant by Th14;
dom chi(A,A) = A by FUNCT_3:def 3; then
A2: A = A /\ dom chi(A,A);
A3: dom chi(A,A) = A by FUNCT_3:def 3;
ex x being Element of X st x in dom chi(A,A) & chi(A,A).x=1
proof
consider x being Element of X such that
A4: x in dom chi(A,A) by A3,SUBSET_1:4;
take x;
thus thesis by A4,FUNCT_3:def 3;
end;
then
A5: 1 in rng chi(A,A) by FUNCT_1:def 3;
A meets dom chi(A,A) by A2;
then ex y being Element of REAL st rng (chi(A,A)|A)={y} by A1,PARTFUN2:37;
hence thesis by A5,TARSKI:def 1;
end;
theorem Th16:
for A be non empty Subset of X, B be set holds B meets dom chi(A
,A) implies rng (chi(A,A)|B) = {1}
proof
let A be non empty Subset of X;
let B be set;
A1: dom (chi(A,A)|B) = B /\ dom (chi(A,A)) by RELAT_1:61;
rng (chi(A,A)|B) c= rng (chi(A,A)) by RELAT_1:70;
then
A2: rng (chi(A,A)|B) c= {1} by Th15;
assume B /\ dom (chi(A,A)) <> {};
then rng (chi(A,A)|B) <> {} by A1,RELAT_1:42;
hence thesis by A2,ZFMISC_1:33;
end;
theorem Th17:
i in dom D implies vol(divset(D,i))=lower_volume(chi(A,A),D).i
proof
A1: dom (chi(A,A)) = A by FUNCT_3:def 3;
assume
A2: i in dom D;
then
A3: lower_volume(chi(A,A),D).i= (lower_bound (rng (chi(A,A)|divset(D,i))))*
vol(divset(D,i)) by Def6;
divset(D,i) c= A by A2,Th6;
then divset(D,i) c= divset(D,i) /\ dom (chi(A,A)) by A1,XBOOLE_1:19;
then divset(D,i) /\ dom (chi(A,A)) <> {};
then divset(D,i) meets dom (chi(A,A));
then
A4: rng (chi(A,A)|divset(D,i)) = {1} by Th16;
A5: rng chi(A,A) = {1} by Th15;
then lower_bound rng (chi(A,A)) = 1 by SEQ_4:9;
hence thesis by A3,A5,A4;
end;
theorem Th18:
i in dom D implies vol(divset(D,i))=upper_volume(chi(A,A),D).i
proof
A1: dom (chi(A,A)) = A by FUNCT_3:def 3;
assume
A2: i in dom D; then
A3: upper_volume(chi(A,A),D).i= (upper_bound (rng (chi(A,A)|divset(D,i))))*
vol(divset(D,i)) by Def5;
divset(D,i) c= A by A2,Th6;
then divset(D,i) c= divset(D,i) /\ dom (chi(A,A)) by A1,XBOOLE_1:19;
then divset(D,i) /\ dom (chi(A,A)) <> {};
then divset(D,i) meets dom (chi(A,A));
then
A4: rng (chi(A,A)|divset(D,i)) = {1} by Th16;
A5: rng chi(A,A) = {1} by Th15;
then upper_bound rng (chi(A,A)) = 1 by SEQ_4:9;
hence thesis by A3,A5,A4;
end;
theorem
len F = len G & len F = len H & (for k st k in dom F holds H.k = F/.k
+ G/.k) implies Sum(H) = Sum(F) + Sum(G)
proof
assume that
A1: len F = len G and
A2: len F = len H and
A3: for k st k in dom F holds H.k = F/.k + G/.k;
A4: F is Element of (len F)-tuples_on REAL by FINSEQ_2:92;
A5: G is Element of (len F)-tuples_on REAL by A1,FINSEQ_2:92;
then F+G is Element of (len F)-tuples_on REAL by A4,FINSEQ_2:120;
then
A6: len H = len (F+G) by A2,CARD_1:def 7;
then
A7: dom H = Seg len(F+G) by FINSEQ_1:def 3;
A8: for k st k in dom F holds H.k = F.k + G.k
proof
let k;
assume
A9: k in dom F;
then k in Seg(len G) by A1,FINSEQ_1:def 3;
then k in dom G by FINSEQ_1:def 3;
then
A10: G/.k = G.k by PARTFUN1:def 6;
F/.k = F.k by A9,PARTFUN1:def 6;
hence thesis by A3,A9,A10;
end;
for k being Nat st k in dom H holds H.k = (F+G).k
proof
let k be Nat;
assume
A11: k in dom H;
then k in dom F by A2,A6,A7,FINSEQ_1:def 3;
then
A12: H.k=F.k+G.k by A8;
k in dom(F+G) by A7,A11,FINSEQ_1:def 3;
hence thesis by A12,VALUED_1:def 1;
end;
then Sum H=Sum(F+G) by A6,FINSEQ_2:9
.=Sum F+Sum G by A4,A5,RVSUM_1:89;
hence thesis;
end;
theorem Th20:
len F = len G & len F = len H & (for k st k in dom F holds H.k =
F/.k - G/.k) implies Sum(H) = Sum(F) - Sum(G)
proof
assume that
A1: len F = len G and
A2: len F = len H and
A3: for k st k in dom F holds H.k = F/.k - G/.k;
A4: F is Element of (len F)-tuples_on REAL by FINSEQ_2:92;
A5: G is Element of (len F)-tuples_on REAL by A1,FINSEQ_2:92;
then
A6: F-G is Element of (len F)-tuples_on REAL by A4,FINSEQ_2:120;
then
A7: len H = len (F-G) by A2,CARD_1:def 7;
then
A8: dom H = Seg len (F-G) by FINSEQ_1:def 3;
A9: for k st k in dom F holds H.k = F.k - G.k
proof
let k;
assume
A10: k in dom F;
then k in Seg(len G) by A1,FINSEQ_1:def 3;
then k in dom G by FINSEQ_1:def 3;
then
A11: G/.k = G.k by PARTFUN1:def 6;
F/.k = F.k by A10,PARTFUN1:def 6;
hence thesis by A3,A10,A11;
end;
for k being Nat st k in dom H holds H.k = (F-G).k
proof
let k be Nat;
assume
A12: k in dom H;
then k in Seg(len F) by A6,A8,CARD_1:def 7;
then k in dom F by FINSEQ_1:def 3;
then
A13: H.k=F.k-G.k by A9;
k in dom(F-G) by A8,A12,FINSEQ_1:def 3;
hence thesis by A13,VALUED_1:13;
end;
then Sum H=Sum(F-G) by A7,FINSEQ_2:9
.=Sum F-Sum G by A4,A5,RVSUM_1:90;
hence thesis;
end;
theorem Th21:
Sum(lower_volume(chi(A,A),D))=vol(A)
proof
deffunc F(Nat)=In(vol(divset(D,$1)),REAL);
consider p being FinSequence of REAL such that
A1: len p = len D & for i be Nat st i in dom p holds p.i = F(i) from
FINSEQ_2:sch 1;
A2: dom p = Seg len D by A1,FINSEQ_1:def 3;
A3: for i st i in Seg(len D) holds p.i = upper_bound divset(D,i) -
lower_bound divset(D,i)
proof
let i;
A4: In(vol(divset(D,i)),REAL) = vol(divset(D,i));
assume i in Seg(len D);
hence thesis by A1,A2,A4;
end;
len D - 1 in NAT
proof
ex j being Nat st len D = 1 + j by NAT_1:10,14;
hence thesis by ORDINAL1:def 12;
end;
then reconsider k = len D - 1 as Element of NAT;
deffunc G(Nat)=In(lower_bound divset(D,$1+1),REAL);
deffunc F(Nat)=In(upper_bound divset(D,$1),REAL);
consider s1 being FinSequence of REAL such that
A5: len s1 = k & for i be Nat st i in dom s1 holds s1.i = F(i) from
FINSEQ_2:sch 1;
consider s2 being FinSequence of REAL such that
A6: len s2 = k & for i be Nat st i in dom s2 holds s2.i = G(i) from
FINSEQ_2:sch 1;
A7: dom s2 = Seg k by A6,FINSEQ_1:def 3;
reconsider ub=upper_bound A, lb=lower_bound A as Element of REAL
by XREAL_0:def 1;
len (s1^<*upper_bound A*>) = len (<*lower_bound A*>^s2) & len (s1^<*
upper_bound A*>) = len p & for i st i in dom (s1^<*upper_bound A*>) holds p.i=(
s1^<*ub*>)/.i - (<*lb*>^s2)/.i
proof
dom(<*upper_bound A*>)=Seg 1 by FINSEQ_1:def 8;
then len(<*upper_bound A*>)=1 by FINSEQ_1:def 3;
then
A8: len(s1^<*upper_bound A*>)=k+1 by A5,FINSEQ_1:22;
dom(<*lower_bound A*>)=Seg 1 by FINSEQ_1:def 8;
then len(<*lower_bound A*>)=1 by FINSEQ_1:def 3;
hence
A9: len (s1^<*upper_bound A*>) = len (<*lower_bound A*>^s2) by A6,A8,
FINSEQ_1:22;
thus len (s1^<*upper_bound A*>) = len p by A1,A8;
let i;
A10: In(upper_bound divset(D,i),REAL) = upper_bound divset(D,i);
A11: In(lower_bound divset(D,i),REAL) = lower_bound divset(D,i);
assume
A12: i in dom (s1^<*upper_bound A*>);
then
A13: (s1^<*ub*>)/.i=(s1^<*ub*>).i by PARTFUN1:def 6;
i in Seg(len (s1^<*upper_bound A*>)) by A12,FINSEQ_1:def 3;
then i in dom (<*lower_bound A*>^s2) by A9,FINSEQ_1:def 3;
then
A14: (<*lb*>^s2)/.i=(<*lower_bound A*>^s2).i by PARTFUN1:def 6;
A15: len D = 1 or len D is non trivial by NAT_2:def 1;
now
per cases by A15,NAT_2:29;
suppose
A16: len D = 1;
then
A17: i in Seg 1 by A8,A12,FINSEQ_1:def 3;
then
A18: i = 1 by FINSEQ_1:2,TARSKI:def 1;
s1={} by A5,A16;
then s1^<*upper_bound A*> = <*upper_bound A*> by FINSEQ_1:34;
then
A19: (s1^<*ub*>)/.i=upper_bound A by A13,A18;
A20: i in dom D by A16,A17,FINSEQ_1:def 3;
s2={} by A6,A16;
then <*lower_bound A*>^s2 = <*lower_bound A*> by FINSEQ_1:34;
then
A21: (<*lb*>^s2)/.i=lower_bound A by A14,A18;
D.i=upper_bound A by A16,A18,Def1;
then
A22: upper_bound divset(D,i)=upper_bound A by A18,A20,Def3;
p.i=upper_bound divset(D,i)-lower_bound divset(D,i) by A3,A16,A17;
hence thesis by A18,A20,A19,A21,A22,Def3;
end;
suppose
A23: len D >= 2;
1 = 2 - 1;
then
A24: k>=1 by A23,XREAL_1:9;
now
per cases;
suppose
A25: i=1; then
A26: i in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then i in dom <*lower_bound A*> by FINSEQ_1:def 8;
then (<*lower_bound A*>^s2).i=<*lower_bound A*>.i by FINSEQ_1:def 7
;
then
A27: (<*lower_bound A*>^s2).i = lower_bound A by A25;
Seg 1 c= Seg k by A24,FINSEQ_1:5;
then i in Seg k by A26;
then
A28: i in dom s1 by A5,FINSEQ_1:def 3;
then (s1^<*upper_bound A*>).i=s1.i by FINSEQ_1:def 7;
then
A29: (s1^<*ub*>).i=upper_bound divset(D,i) by A5,A28,A10;
A30: i in Seg 2 by A25,FINSEQ_1:2,TARSKI:def 2;
A31: Seg 2 c= Seg len D by A23,FINSEQ_1:5;
then i in Seg(len D) by A30;
then
A32: i in dom D by FINSEQ_1:def 3;
p.i=upper_bound divset(D,i)-lower_bound divset(D,i) by A3,A31,A30;
hence thesis by A13,A14,A25,A32,A29,A27,Def3;
end;
suppose
A33: i=len D;
then i-len s1 in Seg 1 by A5,FINSEQ_1:2,TARSKI:def 1;
then
A34: i-len s1 in dom <*upper_bound A*> by FINSEQ_1:def 8;
i=i-len s1 + len s1;
then
(s1^<*upper_bound A*>).i=<*upper_bound A*>.(i-len s1) by A34,
FINSEQ_1:def 7;
then
A35: (s1^<*ub*>)/.i=upper_bound A by A5,A13,A33;
A36: i<>1 by A23,A33;
i in Seg(len D) by A33,FINSEQ_1:3;
then
A37: i in dom D by FINSEQ_1:def 3;
p.i=upper_bound divset(D,i)-lower_bound divset(D,i) by A3,A33,
FINSEQ_1:3;
then p.i=upper_bound divset(D,i)-D.(i-1) by A37,A36,Def3;
then
A38: p.i=D.i-D.(i-1) by A37,A36,Def3;
A39: i-len <*lower_bound A*> = i-1 by FINSEQ_1:40;
i-1<>0 by A23,A33;
then
A40: i-1 in Seg k by A33,FINSEQ_1:3;
then
A41: i-len <*lower_bound A*> in dom s2 by A6,A39,FINSEQ_1:def 3;
len <*lower_bound A*> + (i - len <* lower_bound A*>) = i;
then
A42: (<*lb*>^s2).i = s2.(i-1) by A41,A39,FINSEQ_1:def 7;
reconsider i1=i-1 as Nat by A40;
(<*lb*>^s2).i = G(i1) by A6,A39,A41,A42
.= lower_bound divset(D,i);
then (<*lower_bound A*>^s2).i = D.(i-1) by A37,A36,Def3;
hence thesis by A14,A33,A35,A38,Def1;
end;
suppose
A43: i<>1 & i<>len D;
len s1+len <*upper_bound A*> = k+1 by A5,FINSEQ_1:39;
then
A44: i in Seg(len D) by A12,FINSEQ_1:def 7;
A45: i in dom s1 & i in Seg k & i-1 in Seg k & i-1+1=i & i-len<*
lower_bound A*> in dom s2
proof
i <> 0 by A44,FINSEQ_1:1;
then i is non trivial by A43,NAT_2:def 1;
then i >= 1+1 by NAT_2:29;
then
A46: i-1 >= 1 by XREAL_1:19;
A47: 1 <= i by A44,FINSEQ_1:1;
i <= len D by A44,FINSEQ_1:1;
then
A48: i < k + 1 by A43,XXREAL_0:1;
then
A49: i <= k by NAT_1:13;
then i in Seg(len s1) by A5,A47,FINSEQ_1:1;
hence i in dom s1 by FINSEQ_1:def 3;
thus i in Seg k by A47,A49,FINSEQ_1:1;
i <= k by A48,NAT_1:13;
then i-1 <= k-1 by XREAL_1:9;
then
A50: i-1+0 <= k-1+1 by XREAL_1:7;
ex j being Nat st i = 1 + j by A47,NAT_1:10;
hence i-1 in Seg k by A46,A50,FINSEQ_1:1;
then
A51: i-len<*lower_bound A*> in Seg(len s2) by A6,FINSEQ_1:39;
thus i-1+1=i;
thus thesis by A51,FINSEQ_1:def 3;
end;
then
A52: i-len<*lower_bound A*> in Seg(len s2) by FINSEQ_1:def 3;
then i-len<*lower_bound A*> <= len s2 by FINSEQ_1:1;
then
A53: i <= len<*lower_bound A*>+len s2 by XREAL_1:20;
1 <= i-len<*lower_bound A*> by A52,FINSEQ_1:1;
then len<*lower_bound A*>+1 <= i by XREAL_1:19;
then (<*lower_bound A*>^s2).i = s2.(i-len<*lower_bound A*>) by A53,
FINSEQ_1:23;
then (<*lower_bound A*>^s2).i=s2.(i-1) by FINSEQ_1:39;
then
A54: (<*lower_bound A*>^s2).i= lower_bound divset(D,i)
by A6,A7,A45,A11;
(s1^<*upper_bound A*>).i = s1.i by A45,FINSEQ_1:def 7;
then (s1^<*upper_bound A*>).i = upper_bound divset(D,i)
by A5,A45,A10;
hence thesis by A3,A13,A14,A44,A54;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then Sum p = Sum(s1^<*ub*>)-Sum(<*lb*>^s2) by Th20;
then Sum p=Sum s1 + upper_bound A -Sum(<*lb*>^s2) by RVSUM_1:74;
then
A55: Sum p=Sum s1 + upper_bound A - (lower_bound A + Sum s2) by RVSUM_1:76;
A56: dom s1 = Seg k by A5,FINSEQ_1:def 3;
A57: for i st i in Seg k holds upper_bound divset(D,i) =lower_bound divset(D
,i+1)
proof
let i;
A58: 1+0 <= i+1 by XREAL_1:7;
assume
A59: i in Seg k;
then i <= k by FINSEQ_1:1;
then i+1 <= k+1 by XREAL_1:7;
then i+1 in Seg(len D) by A58,FINSEQ_1:1;
then
A60: i+1 in dom D by FINSEQ_1:def 3;
k + 1 = len D;
then k <= len D by NAT_1:11;
then Seg k c= Seg len D by FINSEQ_1:5;
then i in Seg (len D) by A59;
then
A61: i in dom D by FINSEQ_1:def 3;
A62: i+1-1=i;
now
per cases;
suppose
A63: i=1;
then upper_bound divset(D,i) = D.i by A61,Def3;
hence thesis by A60,A62,A63,Def3;
end;
suppose
A64: i<>1;
i >= 1 by A59,FINSEQ_1:1;
then i+1>=1+1 by XREAL_1:6;
then
A65: i+1 <> 1;
upper_bound divset(D,i) = D.i by A61,A64,Def3;
hence thesis by A60,A62,A65,Def3;
end;
end;
hence thesis;
end;
for i being Nat st i in dom s1 holds s1.i = s2.i
proof
let i be Nat;
A66: In(upper_bound divset(D,i),REAL) = upper_bound divset(D,i);
A67: In(lower_bound divset(D,i+1),REAL) = lower_bound divset(D,i+1);
assume
A68: i in dom s1;
then s1.i = upper_bound divset(D,i) by A5,A66;
then s1.i= lower_bound divset(D,i+1) by A57,A56,A68;
hence thesis by A6,A7,A56,A68,A67;
end;
then
A69: s1=s2 by A5,A6,FINSEQ_2:9;
A70: len lower_volume(chi(A,A),D) = len D by Def6;
then
A71: dom lower_volume(chi(A,A),D) = Seg len D by FINSEQ_1:def 3;
for i being Nat st i in dom lower_volume(chi(A,A),D) holds
lower_volume(chi(A,A),D).i = p.i
proof
let i be Nat;
A72: In(vol(divset(D,i)),REAL) = vol(divset(D,i));
assume
A73: i in dom lower_volume(chi(A,A),D);
then i in dom D by A70,FINSEQ_3:29;
then lower_volume(chi(A,A),D).i=vol(divset(D,i)) by Th17;
hence thesis by A1,A2,A71,A73,A72;
end;
hence thesis by A1,A69,A55,A70,FINSEQ_2:9;
end;
theorem Th22:
Sum(upper_volume(chi(A,A),D))=vol(A)
proof
A1: for i be Nat st 1 <= i & i <= len(lower_volume(chi(A,A),D)) holds
lower_volume(chi(A,A),D).i=upper_volume(chi(A,A),D).i
proof
let i be Nat;
assume that
A2: 1 <= i and
A3: i <= len(lower_volume(chi(A,A),D));
i <= len D by A3,Def6;
then
A4: i in dom D by A2,FINSEQ_3:25;
then lower_volume(chi(A,A),D).i=vol(divset(D,i)) by Th17
.=upper_volume(chi(A,A),D).i by A4,Th18;
hence thesis;
end;
len (lower_volume(chi(A,A),D)) = len D by Def6
.= len (upper_volume(chi(A,A),D)) by Def5;
then lower_volume(chi(A,A),D)=upper_volume(chi(A,A),D) by A1,FINSEQ_1:14;
hence thesis by Th21;
end;
begin :: Some properties of Darboux sum
registration
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of A,REAL;
let D be Division of A;
cluster upper_volume(f,D) -> non empty;
coherence
proof
len upper_volume(f,D) = len D by Def5;
hence thesis;
end;
cluster lower_volume(f,D) -> non empty;
coherence
proof
len lower_volume(f,D) = len D by Def6;
hence thesis;
end;
end;
theorem Th23:
f|A is bounded_below implies
(lower_bound rng f)*vol(A) <= lower_sum(f,D)
proof
assume
A1: f|A is bounded_below;
A2: for i st i in dom D holds (lower_bound rng f)*vol(divset(D,i)) <= (
lower_bound rng (f|divset(D,i)))*vol(divset(D,i))
proof
let i;
A3: rng(f|divset(D,i)) c= rng f by RELAT_1:70;
A4: 0 <= vol(divset(D,i)) by SEQ_4:11,XREAL_1:48;
A5: dom f = A by FUNCT_2:def 1;
assume i in dom D;
then dom (f|divset(D,i)) = divset(D,i) by A5,Th6,RELAT_1:62;
then
A6: rng(f|divset(D,i)) is non empty Subset of REAL by RELAT_1:42;
rng f is bounded_below by A1,Th9;
hence thesis by A3,A6,A4,SEQ_4:47,XREAL_1:64;
end;
A7: for i st i in dom D holds (lower_bound rng f)*(lower_volume(chi(A,A),D)
.i) <= (lower_bound rng (f|divset(D,i)))*vol(divset(D,i))
proof
let i;
assume
A8: i in dom D;
then
(lower_bound rng f)*vol(divset(D,i)) <= (lower_bound rng (f|divset(D,
i)))*vol(divset(D,i)) by A2;
hence thesis by A8,Th17;
end;
Sum((lower_bound rng f)*lower_volume(chi(A,A),D)) <=Sum(lower_volume(f,
D))
proof
len (lower_volume(chi(A,A),D)) = len ((lower_bound rng f)*
lower_volume(chi(A,A),D)) by FINSEQ_2:33;
then
A9: len ((lower_bound rng f)*lower_volume(chi(A,A),D))=len D by Def6;
deffunc G(Nat)=
In((lower_bound rng (f|divset(D,$1)))*vol(divset(D,$1)),REAL);
deffunc F(set)=
In((lower_bound rng f)*(lower_volume(chi(A,A),D).$1),REAL);
consider p being FinSequence of REAL such that
A10: len p = len D & for i be Nat st i in dom p holds p.i=F(i) from
FINSEQ_2:sch 1;
A11: dom p = Seg len D by A10,FINSEQ_1:def 3;
for i be Nat st 1 <= i & i <= len p holds p.i=((lower_bound rng f)*
lower_volume(chi(A,A),D)).i
proof
let i be Nat;
assume that
A12: 1 <= i and
A13: i <= len p;
i in Seg(len D) by A10,A12,A13,FINSEQ_1:1;
then p.i=F(i) by A10,A11;
hence thesis by RVSUM_1:44;
end;
then
A14: p=(lower_bound rng f)*lower_volume(chi(A,A),D) by A10,A9,FINSEQ_1:14;
reconsider p as Element of (len D)-tuples_on REAL by A10,FINSEQ_2:92;
consider q being FinSequence of REAL such that
A15: len q = len D & for i be Nat st i in dom q holds q.i=G(i) from
FINSEQ_2:sch 1;
A16: for i be Nat st i in dom q
holds q.i=(lower_bound rng (f|divset(D,i)))*vol(divset(D,i))
proof let i be Nat;
assume i in dom q;
then q.i = G(i) by A15;
hence thesis;
end;
A17: dom q = dom D by A15,FINSEQ_3:29;
then
A18: q=lower_volume(f,D) by A15,Def6,A16;
reconsider q as Element of (len D)-tuples_on REAL by A15,FINSEQ_2:92;
now
let i be Nat;
assume
A19: i in Seg (len D);
then
A20: p.i=F(i) by A10,A11;
A21: i in dom D by A19,FINSEQ_1:def 3;
then
q.i=G(i) by A15,A17;
hence p.i <= q.i by A7,A20,A21;
end;
hence thesis by A18,A14,RVSUM_1:82;
end;
then
(lower_bound rng f)*Sum(lower_volume(chi(A,A),D)) <=Sum(lower_volume(f,
D)) by RVSUM_1:87;
hence thesis by Th21;
end;
theorem
f|A is bounded_above & i in dom D implies (upper_bound rng f)*vol(
divset(D,i)) >= (upper_bound rng (f|divset(D,i)))*vol(divset(D,i))
proof
A1: dom f = A by FUNCT_2:def 1;
assume f|A is bounded_above;
then
A2: rng f is bounded_above by Th11;
assume i in dom D;
then dom (f|divset(D,i)) = divset(D,i) by A1,Th6,RELAT_1:62;
then
A3: rng(f|divset(D,i)) is non empty Subset of REAL by RELAT_1:42;
A4: 0 <= vol(divset(D,i)) by SEQ_4:11,XREAL_1:48;
rng(f|divset(D,i)) c= rng f by RELAT_1:70;
hence thesis by A3,A2,A4,SEQ_4:48,XREAL_1:64;
end;
theorem Th25:
f|A is bounded_above implies
upper_sum(f,D) <= (upper_bound rng f)*vol(A)
proof
assume
A1: f|A is bounded_above;
A2: for i st i in Seg(len D) holds (upper_bound rng f)*vol(divset(D,i)) >= (
upper_bound rng (f|divset(D,i)))*vol(divset(D,i))
proof
let i;
A3: rng(f|divset(D,i)) c= rng f by RELAT_1:70;
A4: 0 <= vol(divset(D,i)) by SEQ_4:11,XREAL_1:48;
assume i in Seg(len D); then
A5: i in dom D by FINSEQ_1:def 3;
dom f = A by FUNCT_2:def 1;
then dom (f|divset(D,i)) = divset(D,i) by A5,Th6,RELAT_1:62;
then
A6: rng(f|divset(D,i)) is non empty Subset of REAL by RELAT_1:42;
rng f is bounded_above by A1,Th11;
hence thesis by A3,A6,A4,SEQ_4:48,XREAL_1:64;
end;
A7: for i st i in Seg(len D) holds (upper_bound rng f)*(upper_volume(chi(A,
A),D).i) >= (upper_bound rng (f|divset(D,i)))*vol(divset(D,i))
proof
let i;
assume
A8: i in Seg(len D); then
A9: i in dom D by FINSEQ_1:def 3;
(upper_bound rng f)*vol(divset(D,i)) >= (upper_bound rng (f|divset(D,
i)))*vol(divset(D,i)) by A2,A8;
hence thesis by A9,Th18;
end;
Sum((upper_bound rng f)*upper_volume(chi(A,A),D)) >=Sum(upper_volume(f,
D))
proof
len (upper_volume(chi(A,A),D)) = len ((upper_bound rng f)*
upper_volume(chi(A,A),D)) by FINSEQ_2:33;
then
A10: len ((upper_bound rng f)*upper_volume(chi(A,A),D))=len D by Def5;
deffunc G(Nat)=
In((upper_bound rng (f|divset(D,$1)))*vol(divset(D,$1)),REAL);
deffunc
F(set)=In((upper_bound rng f)*(upper_volume(chi(A,A),D).$1),REAL);
consider p being FinSequence of REAL such that
A11: len p = len D & for i be Nat st i in dom p holds p.i=F(i) from
FINSEQ_2:sch 1;
A12: dom p = Seg len D by A11,FINSEQ_1:def 3;
for i be Nat st 1 <= i & i <= len p holds p.i=((upper_bound rng f)*
upper_volume(chi(A,A),D)).i
proof
let i be Nat;
assume that
A13: 1 <= i and
A14: i <= len p;
i in Seg(len D) by A11,A13,A14,FINSEQ_1:1;
then p.i=F(i) by A11,A12;
hence thesis by RVSUM_1:44;
end;
then
A15: p=(upper_bound rng f)*upper_volume(chi(A,A),D) by A11,A10,FINSEQ_1:14;
reconsider p as Element of (len D)-tuples_on REAL by A11,FINSEQ_2:92;
consider q being FinSequence of REAL such that
A16: len q = len D & for i be Nat st i in dom q holds q.i=G(i) from
FINSEQ_2:sch 1;
A17: for i be Nat st i in dom q holds q.i=
(upper_bound rng (f|divset(D,i)))*vol(divset(D,i))
proof let i be Nat;
assume i in dom q;
then q.i=G(i) by A16;
hence thesis;
end;
A18: dom q = dom D by A16,FINSEQ_3:29;
then
A19: q=upper_volume(f,D) by A16,Def5,A17;
reconsider q as Element of (len D)-tuples_on REAL by A16,FINSEQ_2:92;
now
let i be Nat;
assume
A20: i in Seg (len D);
then i in dom D by FINSEQ_1:def 3;
then
A21: q.i=G(i) by A16,A18;
p.i=F(i) by A11,A12,A20;
hence q.i <= p.i by A7,A20,A21;
end;
hence thesis by A19,A15,RVSUM_1:82;
end;
then
(upper_bound rng f)*Sum(upper_volume(chi(A,A),D))>= Sum(upper_volume(f,
D)) by RVSUM_1:87;
hence thesis by Th22;
end;
theorem Th26:
f|A is bounded implies lower_sum(f,D) <= upper_sum(f,D)
proof
deffunc F(Nat)=
In((lower_bound rng (f|divset(D,$1)))*vol(divset(D,$1)),REAL);
consider p being FinSequence of REAL such that
A1: len p = len D & for i be Nat st i in dom p holds p.i=F(i) from
FINSEQ_2:sch 1;
A2: for i be Nat st i in dom p holds p.i=
(lower_bound rng (f|divset(D,i)))*vol(divset(D,i))
proof let i be Nat;
assume i in dom p;
then p.i= F(i) by A1;
hence thesis;
end;
assume
A3: f|A is bounded;
then
A4: rng f is bounded_above by Th11;
A5: dom p = dom D by A1,FINSEQ_3:29;
reconsider p as Element of (len D)-tuples_on REAL by A1,FINSEQ_2:92;
deffunc G(Nat)=
In((upper_bound rng (f|divset(D,$1)))*vol(divset(D,$1)),REAL);
consider q being FinSequence of REAL such that
A6: len q = len D & for i be Nat st i in dom q holds q.i=G(i) from
FINSEQ_2:sch 1;
A7: for i be Nat st i in dom q holds q.i=
(upper_bound rng (f|divset(D,i)))*vol(divset(D,i))
proof let i be Nat;
assume i in dom q;
then q.i=G(i) by A6;
hence thesis;
end;
A8: dom q = dom D by A6,FINSEQ_3:29;
then len q = len D by FINSEQ_3:29;
then
A9: q=upper_volume(f,D) by A7,Def5,A8;
reconsider q as Element of (len D)-tuples_on REAL by A6,FINSEQ_2:92;
A10: rng f is bounded_below by A3,Th9;
for i be Nat st i in Seg(len D) holds p.i <= q.i
proof
let i be Nat;
A11: dom f = A by FUNCT_2:def 1;
assume
A12: i in Seg(len D);
then
A13: i in dom D by FINSEQ_1:def 3;
i in dom D by A12,FINSEQ_1:def 3;
then dom (f|divset(D,i)) = divset(D,i) by A11,Th6,RELAT_1:62;
then
A14: rng(f|divset(D,i)) is non empty Subset of REAL by RELAT_1:42;
A15: 0 <= vol(divset(D,i)) by SEQ_4:11,XREAL_1:48;
A16: rng (f|divset(D,i)) is bounded_above by A4,RELAT_1:70,XXREAL_2:43;
rng (f|divset(D,i)) is bounded_below by A10,RELAT_1:70,XXREAL_2:44;
then
lower_bound (rng(f|divset(D,i)))*vol(divset(D,i)) <= upper_bound (rng
(f|divset(D,i)))*vol(divset(D,i)) by A16,A14,A15,SEQ_4:11,XREAL_1:64;
then
p.i <= upper_bound (rng(f|divset(D,i)))*vol(divset(D,i))
by A5,A13,A2;
hence thesis by A8,A13,A7;
end;
then Sum p <= Sum q by RVSUM_1:82;
hence thesis by A1,A5,A9,Def6,A2;
end;
definition
let D1, D2 be FinSequence;
pred D1 <= D2 means
len D1 <= len D2 & rng D1 c= rng D2;
reflexivity;
end;
notation
let D1, D2 be FinSequence;
synonym D2 >= D1 for D1 <= D2;
end;
theorem
len D1 = 1 implies D1 <= D2
proof
A1: D2.(len D2) = upper_bound A by Def1;
assume
A2: len D1 = 1;
then D1.1 = upper_bound A by Def1;
then D1=<*upper_bound A*> by A2,FINSEQ_1:40;
then
A3: rng D1 = {upper_bound A} by FINSEQ_1:38;
A4: len D2 in Seg(len D2) by FINSEQ_1:3;
hence len D1 <= len D2 by A2,FINSEQ_1:1;
len D2 in dom D2 by A4,FINSEQ_1:def 3;
then upper_bound A in rng D2 by A1,FUNCT_1:def 3;
then rng D1 is Subset of rng D2 by A3,SUBSET_1:41;
hence thesis;
end;
theorem Th28:
f|A is bounded_above & len D1 = 1 implies
upper_sum(f,D1) >= upper_sum(f,D2)
proof
assume that
A1: f|A is bounded_above and
A2: len D1=1;
1 in Seg(len D1) by A2,FINSEQ_1:3; then
A3: 1 in dom D1 by FINSEQ_1:def 3; then
A4: lower_bound divset(D1,1)=lower_bound A by Def3;
A5: divset(D1,1)=[.lower_bound divset(D1,1),upper_bound divset(D1,1).] by Th2;
upper_bound divset(D1,1)=D1.1 by A3,Def3
.=upper_bound A by A2,Def1; then
A6: divset(D1,1)=A by A4,A5,Th2;
A7: upper_volume(f,D1).1=(upper_bound (rng(f|divset(D1,1))))*vol(divset(D1,
1)) by A3,Def5;
reconsider ubv =
(upper_bound (rng (f|divset(D1,1))))*vol(divset(D1,1)) as Element of REAL
by XREAL_0:def 1;
len upper_volume(f,D1) = 1 by A2,Def5;
then upper_sum(f,D1)=Sum <*ubv*> by A7,FINSEQ_1:40
.=(upper_bound (rng(f|A)))*vol(A) by A6,FINSOP_1:11
.=(upper_bound (rng f))*vol(A);
hence thesis by A1,Th25;
end;
theorem Th29:
f|A is bounded_below & len D1 = 1 implies
lower_sum(f,D1) <= lower_sum(f,D2)
proof
assume that
A1: f|A is bounded_below and
A2: len D1=1;
1 in Seg(len D1) by A2,FINSEQ_1:3; then
A3: 1 in dom D1 by FINSEQ_1:def 3; then
A4: lower_bound divset(D1,1)=lower_bound A by Def3;
upper_bound divset(D1,1)=D1.1 by A3,Def3
.=upper_bound A by A2,Def1;
then divset(D1,1)=[.lower_bound A,upper_bound A.] by A4,Th2; then
A5: divset(D1,1)=A by Th2;
A6: lower_volume(f,D1).1=(lower_bound (rng(f|divset(D1,1))))*vol(divset(D1,
1)) by A3,Def6;
reconsider lbv =(lower_bound (rng (f|divset(D1,1))))*vol(divset( D1,1))
as Element of REAL by XREAL_0:def 1;
len lower_volume(f,D1) = 1 by A2,Def6;
then lower_sum(f,D1)=Sum <*lbv*> by A6,FINSEQ_1:40
.=(lower_bound (rng(f|A)))*vol(A) by A5,FINSOP_1:11
.=(lower_bound (rng f))*vol(A);
hence thesis by A1,Th23;
end;
theorem
i in dom D implies ex A1,A2 be non empty closed_interval Subset of REAL
st A1=[.lower_bound A,D.i .] & A2=[. D.i,upper_bound A.] & A=A1 \/ A2
proof
assume i in dom D; then
A1: D.i in rng D by FUNCT_1:def 3;
rng D c= A by Def1;
then D.i in A by A1;
then D.i in [.lower_bound A,upper_bound A.] by Th2;
then D.i in {a: lower_bound A <= a & a <= upper_bound A} by RCOMP_1:def 1;
then
A2: ex a st a=D.i & lower_bound A <= a & a <= upper_bound A;
then reconsider
A1 =[.lower_bound A,D.i .] as non empty closed_interval Subset of REAL
by MEASURE5:14;
reconsider A2 = [. D.i,upper_bound A.]
as non empty closed_interval Subset of REAL by A2,MEASURE5:14;
take A1, A2;
A1 \/ A2 = [.lower_bound A,upper_bound A.] by A2,XXREAL_1:174
.= A by Th2;
hence thesis;
end;
theorem Th31:
i in dom D1 & D1 <= D2 implies ex j st j in dom D2 & D1.i=D2.j
proof
assume i in dom D1; then
A1: D1.i in rng D1 by FUNCT_1:def 3;
assume D1 <= D2;
then rng D1 c= rng D2;
then consider x1 being object such that
A2: x1 in dom D2 and
A3: D1.i=D2.x1 by A1,FUNCT_1:def 3;
reconsider x1 as Element of NAT by A2;
take x1;
thus thesis by A2,A3;
end;
definition
let A, D1, D2;
let i be Nat;
assume
A1: D1 <= D2;
func indx(D2,D1,i) -> Element of NAT means
:Def18:
it in dom D2 & D1.i=D2.it
if i in dom D1 otherwise it = 0;
existence by A1,Th31;
uniqueness
proof
let m,n be Element of NAT;
hereby
assume that
i in dom D1 and
A2: m in dom D2 and
A3: D1.i=D2.m and
A4: n in dom D2 and
A5: D1.i=D2.n;
assume
A6: m <> n;
now
per cases by A6,XXREAL_0:1;
suppose
m < n;
hence contradiction by A2,A3,A4,A5,SEQM_3:def 1;
end;
suppose
n < m;
hence contradiction by A2,A3,A4,A5,SEQM_3:def 1;
end;
end;
hence contradiction;
end;
assume that
not i in dom D1 and
A7: m=0 and
A8: n=0;
thus thesis by A7,A8;
end;
correctness;
end;
theorem Th32:
for p be increasing FinSequence of REAL, n be Element of NAT
holds n <= len p implies p/^n is increasing FinSequence of REAL
proof
let p be increasing FinSequence of REAL;
let n be Element of NAT;
assume
A1: n <= len p;
for i,j being Nat
st i in dom (p/^n) & j in dom (p/^n) & i< j holds (p/^n).i < (p
/^n).j
proof
let i,j be Nat;
assume that
A2: i in dom(p/^n) and
A3: j in dom(p/^n) and
A4: i<j;
A5: i+n<j+n by A4,XREAL_1:6;
A6: j in Seg(len (p/^n)) by A3,FINSEQ_1:def 3;
then 1 <= j by FINSEQ_1:1;
then
A7: 1+n <= j+n by XREAL_1:6;
j <= len (p/^n) by A6,FINSEQ_1:1;
then j <= len p - n by A1,RFINSEQ:def 1;
then
A8: j+n <= len p by XREAL_1:19;
1 <= 1+n by NAT_1:11;
then 1 <= j+n by A7,XXREAL_0:2;
then j+n in Seg(len p) by A8,FINSEQ_1:1;
then
A9: j+n in dom p by FINSEQ_1:def 3;
A10: i in Seg(len (p/^n)) by A2,FINSEQ_1:def 3;
then 1 <= i by FINSEQ_1:1;
then
A11: 1+n <= i+n by XREAL_1:6;
i <= len (p/^n) by A10,FINSEQ_1:1;
then i <= len p - n by A1,RFINSEQ:def 1;
then
A12: i+n <= len p by XREAL_1:19;
1 <= 1+n by NAT_1:11;
then 1 <= i+n by A11,XXREAL_0:2;
then i+n in Seg(len p) by A12,FINSEQ_1:1;
then
A13: i+n in dom p by FINSEQ_1:def 3;
A14: (p/^n).j=p.(j+n) by A1,A3,RFINSEQ:def 1;
(p/^n).i=p.(i+n) by A1,A2,RFINSEQ:def 1;
hence thesis by A14,A13,A9,A5,SEQM_3:def 1;
end;
hence thesis by SEQM_3:def 1;
end;
theorem Th33:
for p be increasing FinSequence of REAL, i,j be Element of NAT
holds j in dom p & i <= j implies mid(p,i,j) is increasing FinSequence of REAL
proof
let p be increasing FinSequence of REAL;
let i,j be Element of NAT;
assume that
A1: j in dom p and
A2: i <= j;
j in Seg(len p) by A1,FINSEQ_1:def 3;
then j <= len p by FINSEQ_1:1;
then i <= len p by A2,XXREAL_0:2;
then p/^(i-'1) is increasing FinSequence of REAL by Th32,NAT_D:44;
then
A3: (p/^(i-'1))|Seg(j-'i+1) is increasing FinSequence of REAL by FINSEQ_1:18;
mid(p,i,j)=(p/^(i-'1))|(j-'i+1) by A2,FINSEQ_6:def 3;
hence thesis by A3,FINSEQ_1:def 16;
end;
Lm1:
for f being FinSequence holds
i in dom f & j in dom f & i<=j implies len mid(f,i,j) = j-i+1
proof
let D be FinSequence;
assume that
A1: i in dom D and
A2: j in dom D and
A3: i<=j;
j in Seg(len D) by A2,FINSEQ_1:def 3;
then j <= len D by FINSEQ_1:1;
then i <= len D by A3,XXREAL_0:2;
then i-'1 <= len D by NAT_D:44;
then
A4: len (D/^(i-'1)) = len D - (i-'1) by RFINSEQ:def 1;
reconsider D1=D/^(i-'1) as FinSequence;
reconsider k=j-'i+1 as Element of NAT;
i in Seg(len D) by A1,FINSEQ_1:def 3;
then 1 <= i by FINSEQ_1:1;
then j-(i-'1)=j-(i-1) by XREAL_1:233; then
A5: j-(i-'1)=j-i+1;
j in Seg(len D) by A2,FINSEQ_1:def 3;
then j <= len D by FINSEQ_1:1;
then j-(i-'1) <= len D-(i-'1) by XREAL_1:9; then
A6: j-'i+1 <= len (D/^(i-'1)) by A3,A4,A5,XREAL_1:233;
mid(D,i,j) = (D/^(i-'1))|(j-'i+1) by A3,FINSEQ_6:def 3
.=D1|Seg k by FINSEQ_1:def 16;
then len mid(D,i,j) = j-'i+1 by A6,FINSEQ_1:17;
hence thesis by A3,XREAL_1:233;
end;
theorem Th34:
i in dom D & j in dom D & i<=j implies
ex B be non empty closed_interval Subset of REAL st
lower_bound B = mid(D,i,j).1 & upper_bound B = mid(D,i,j).(len mid(D,i,j)) &
mid(D,i,j) is Division of B
proof
assume that
A1: i in dom D and
A2: j in dom D and
A3: i<=j;
j in Seg(len D) by A2,FINSEQ_1:def 3;
then j <= len D by FINSEQ_1:1;
then i <= len D by A3,XXREAL_0:2;
then i-'1 <= len D by NAT_D:44; then
A4: len (D/^(i-'1)) = len D - (i-'1) by RFINSEQ:def 1;
reconsider D1=D/^(i-'1) as FinSequence of REAL;
reconsider k=j-'i+1 as Element of NAT;
i in Seg(len D) by A1,FINSEQ_1:def 3;
then 1 <= i by FINSEQ_1:1;
then j-(i-'1)=j-(i-1) by XREAL_1:233;
then
A5: j-(i-'1)=j-i+1;
j in Seg(len D) by A2,FINSEQ_1:def 3;
then j <= len D by FINSEQ_1:1;
then j-(i-'1) <= len D-(i-'1) by XREAL_1:9;
then
A6: j-'i+1 <= len (D/^(i-'1)) by A3,A4,A5,XREAL_1:233;
A7: mid(D,i,j) = (D/^(i-'1))|(j-'i+1) by A3,FINSEQ_6:def 3
.=D1|Seg k by FINSEQ_1:def 16;
then 0<len mid(D,i,j) by A6,FINSEQ_1:17;
then reconsider M=mid(D,i,j) as
non empty increasing FinSequence of REAL by A2,A3,Th33;
j-'i+1 >= 0 + 1 by XREAL_1:6;
then
A8: 1 <= len M by A6,A7,FINSEQ_1:17;
then len M in Seg(len M) by FINSEQ_1:1;
then
A9: len M in dom M by FINSEQ_1:def 3;
1 in Seg(len M) by A8,FINSEQ_1:1;
then
A10: 1 in dom M by FINSEQ_1:def 3;
then M.1 <= M.(len M) by A8,A9,SEQ_4:137;
then reconsider B=[. M.1,M.(len M) .]
as non empty closed_interval Subset of REAL by MEASURE5:14;
A11: B=[.lower_bound B,upper_bound B.] by Th2; then
A12: lower_bound B = M.1 by Th3;
A13: M.(len M)=upper_bound B by A11,Th3;
for x being Element of REAL st x in rng M holds x in B
proof
let x be Element of REAL;
assume x in rng M;
then consider i such that
A14: i in dom M and
A15: x=M.i by PARTFUN1:3;
A16: i in Seg(len M) by A14,FINSEQ_1:def 3;
then i <= len M by FINSEQ_1:1;
then
A17: M.i <= M.(len M) by A9,A14,SEQ_4:137;
1 <= i by A16,FINSEQ_1:1;
then M.1 <= M.i by A10,A14,SEQ_4:137;
then M.i in {a: M.1 <= a & a <= M.(len M)} by A17;
hence thesis by A15,RCOMP_1:def 1;
end;
then rng M c= B;
then M is Division of B by A13,Def1;
hence thesis by A12,A13;
end;
theorem Th35:
i in dom D & j in dom D & i<=j & D.i>=lower_bound B & D.j=
upper_bound B implies mid(D,i,j) is Division of B
proof
assume that
A1: i in dom D and
A2: j in dom D and
A3: i<=j and
A4: D.i>=lower_bound B and
A5: D.j=upper_bound B;
A6: j-i+1+i-1=j;
i in Seg(len D) by A1,FINSEQ_1:def 3; then
A7: 1 <= i by FINSEQ_1:1;
0<=j-i by A3,XREAL_1:48; then
A8: 0+1<=j-i+1 by XREAL_1:6;
j in Seg(len D) by A2,FINSEQ_1:def 3; then
A9: j<=len D by FINSEQ_1:1;
consider A1 be non empty closed_interval Subset of REAL such that
A10: lower_bound A1=mid(D,i,j).1 and
A11: upper_bound A1=mid(D,i,j).(len mid(D,i,j)) and
A12: mid(D,i,j) is Division of A1 by A1,A2,A3,Th34;
A13: len mid(D,i,j)=j-i+1 by A1,A2,A3,Lm1;
A14: 1+i-1 = i;
for x being Element of REAL st x in A1 holds x in B
proof
let x be Element of REAL;
assume x in A1;
then x in [.lower_bound A1,upper_bound A1.] by Th2;
then x in {a: lower_bound A1 <= a & a <= upper_bound A1} by RCOMP_1:def 1;
then
A15: ex a st x=a & lower_bound A1 <= a & a <= upper_bound A1;
then D.i <= x by A3,A10,A7,A9,A8,A14,FINSEQ_6:122;
then
A16: lower_bound B <= x by A4,XXREAL_0:2;
x <= upper_bound B by A3,A5,A11,A13,A7,A9,A8,A6,A15,FINSEQ_6:122;
then x in {a: lower_bound B <= a & a <= upper_bound B} by A16;
then x in [.lower_bound B,upper_bound B.] by RCOMP_1:def 1;
hence thesis by Th2;
end; then
A17: A1 c= B;
rng mid(D,i,j) c= A1 by A12,Def1;
then
A18: rng mid(D,i,j) c= B by A17;
mid(D,i,j).(len mid(D,i,j))=D.j by A3,A13,A7,A9,A8,A6,FINSEQ_6:122;
hence thesis by A5,A12,A18,Def1;
end;
definition
let p be FinSequence of REAL;
func PartSums(p) -> FinSequence of REAL means
:Def19:
len it = len p & for i be Nat st i in dom p holds it.i=Sum(p|i);
existence
proof
deffunc F(Nat)= In(Sum(p|$1),REAL);
consider IT being FinSequence of REAL such that
A1: len IT = len p & for i be Nat st i in dom IT holds IT.i=F(i) from
FINSEQ_2:sch 1;
take IT;
thus len IT = len p by A1;
let i be Nat;
assume i in dom p;
then i in dom IT by A1,FINSEQ_3:29;
then IT.i=F(i) by A1;
hence thesis;
end;
uniqueness
proof
let p1,p2 be FinSequence of REAL such that
A2: len p1=len p and
A3: for i be Nat st i in dom p holds p1.i=Sum(p|i) and
A4: len p2=len p and
A5: for i be Nat st i in dom p holds p2.i=Sum(p|i);
for i be Nat st 1 <= i & i <= len p1 holds p1.i=p2.i
proof
let i be Nat;
assume that
A6: 1 <= i and
A7: i <= len p1;
A8: i in dom p by A2,A6,A7,FINSEQ_3:25;
then p1.i=Sum(p|i) by A3;
hence thesis by A5,A8;
end;
hence thesis by A2,A4,FINSEQ_1:14;
end;
end;
theorem Th36:
D1 <= D2 & f|A is bounded_above implies for i be non zero
Element of NAT holds (i in dom D1 implies Sum(upper_volume(f,D1)|i) >= Sum(
upper_volume(f,D2)|indx(D2,D1,i)))
proof
assume that
A1: D1 <= D2 and
A2: f|A is bounded_above;
for i be non zero Nat holds i in dom D1 implies Sum(upper_volume(f,D1)|
i) >= Sum(upper_volume(f,D2)|indx(D2,D1,i))
proof
defpred P[Nat] means $1 in dom D1 implies Sum(upper_volume(f,D1)|$1) >=
Sum(upper_volume(f,D2)|indx(D2,D1,$1));
A3: P[1]
proof
reconsider g=f|divset(D1,1) as PartFunc of divset(D1,1),REAL by
PARTFUN1:10;
set B=divset(D1,1);
set DD1=mid(D1,1,1);
A4: dom g = dom f /\ divset(D1,1) by RELAT_1:61;
assume
A5: 1 in dom D1;
then
A6: D1.1 = upper_bound B by Def3;
then
A7: D2.indx(D2,D1,1) = upper_bound B by A1,A5,Def18;
D1.1 >= lower_bound B by A6,SEQ_4:11;
then reconsider DD1 as Division of B by A5,A6,Th35;
1 in Seg(len D1) by A5,FINSEQ_1:def 3;
then
A8: 1 <= len D1 by FINSEQ_1:1;
then
A9: len mid(D1,1,1)=1-'1+1 by FINSEQ_6:118;
A10: len upper_volume(g,DD1)=len DD1 by Def5
.= 1 by A9,XREAL_1:235;
A11: len mid(D1,1,1)=1 by A9,XREAL_1:235;
then
A12: len mid(D1,1,1)=len (D1|1);
for k be Nat st 1 <= k & k <= len mid(D1,1,1) holds
mid(D1,1,1).k=(D1|1).k
proof
let k be Nat;
assume that
A13: 1 <= k and
A14: k <= len mid(D1,1,1);
k in Seg(len(D1|1)) by A12,A13,A14,FINSEQ_1:1;
then k in dom (D1|1) by FINSEQ_1:def 3;
then k in dom (D1|Seg 1) by FINSEQ_1:def 16;
then
A15: (D1|Seg 1).k = D1.k by FUNCT_1:47;
A16: k = 1 by A11,A13,A14,XXREAL_0:1;
then mid(D1,1,1).k = D1.(1+1-1) by A8,FINSEQ_6:118;
hence thesis by A16,A15,FINSEQ_1:def 16;
end;
then
A17: mid(D1,1,1)=D1|1 by A12,FINSEQ_1:14;
A18: for i be Nat st 1 <= i & i <= len upper_volume(g,DD1) holds
upper_volume(g,DD1).i=(upper_volume(f,D1)|1).i
proof
let i be Nat;
assume that
A19: 1 <= i and
A20: i <= len upper_volume(g,DD1);
A21: 1 in Seg 1 by FINSEQ_1:3;
dom(D1|Seg 1) = dom D1 /\ Seg 1 by RELAT_1:61;
then
A22: 1 in dom(D1|Seg 1) by A5,A21,XBOOLE_0:def 4;
dom(upper_volume(f,D1))=Seg(len upper_volume(f,D1)) by FINSEQ_1:def 3
.=Seg(len D1) by Def5;
then
A23: dom(upper_volume(f,D1)|Seg 1) =Seg(len D1) /\ Seg 1 by RELAT_1:61
.=Seg 1 by A8,FINSEQ_1:7;
len DD1 = 1 by A9,XREAL_1:235;
then
A24: 1 in dom DD1 by A21,FINSEQ_1:def 3;
A25: (upper_volume(f,D1)|1).i=(upper_volume(f,D1)|Seg 1).i by
FINSEQ_1:def 16
.=(upper_volume(f,D1)|Seg 1).1 by A10,A19,A20,XXREAL_0:1
.=upper_volume(f,D1).1 by A23,FINSEQ_1:3,FUNCT_1:47
.=(upper_bound (rng(f|divset(D1,1))))*vol(divset(D1,1)) by A5,Def5;
A26: divset(D1,1)=[.lower_bound divset(D1,1),upper_bound divset(D1,1)
.] by Th2
.=[.lower_bound A,upper_bound divset(D1,1).] by A5,Def3
.=[.lower_bound A,D1.1 .] by A5,Def3;
A27: upper_volume(g,DD1).i = upper_volume(g,DD1).1 by A10,A19,A20,XXREAL_0:1
.= (upper_bound (rng (g|divset(DD1,1))))*vol(divset(DD1,1)) by A24
,Def5;
divset(DD1,1)=[.lower_bound divset(DD1,1), upper_bound divset(DD1
,1).] by Th2
.=[.lower_bound B,upper_bound divset(DD1,1).] by A24,Def3
.=[.lower_bound B,DD1.1 .] by A24,Def3
.=[.lower_bound A,(D1|1).1 .] by A5,A17,Def3
.=[.lower_bound A,(D1|Seg 1).1 .] by FINSEQ_1:def 16
.=[.lower_bound A,D1.1 .] by A22,FUNCT_1:47;
hence thesis by A27,A26,A25;
end;
A28: g|divset(D1,1) is bounded_above
proof
consider a be Real such that
A29: for x being object st x in A /\ dom f holds f.x <= a
by A2,RFUNCT_1:70;
for x being object st x in divset(D1,1) /\ dom g holds g.x <= a
proof
let x be object;
A30: dom g c= dom f by RELAT_1:60;
assume x in divset(D1,1) /\ dom g;
then
A31: x in dom g by XBOOLE_0:def 4;
A32: A /\ dom f = dom f by XBOOLE_1:28;
then x in A /\ dom f by A31,A30;
then reconsider x as Element of A;
f.x <= a by A29,A31,A32,A30;
hence thesis by A31,FUNCT_1:47;
end;
hence thesis by RFUNCT_1:70;
end;
A33: rng D2 c= A by Def1;
A34: indx(D2,D1,1) in dom D2 by A1,A5,Def18;
then
A35: indx(D2,D1,1) in Seg(len D2) by FINSEQ_1:def 3;
then
A36: 1 <= indx(D2,D1,1) by FINSEQ_1:1;
A37: indx(D2,D1,1) <= len D2 by A35,FINSEQ_1:1;
then 1 <= len D2 by A36,XXREAL_0:2;
then 1 in Seg(len D2) by FINSEQ_1:1;
then
A38: 1 in dom D2 by FINSEQ_1:def 3;
then D2.1 in rng D2 by FUNCT_1:def 3;
then D2.1 in A by A33;
then D2.1 in [.lower_bound A,upper_bound A.] by Th2;
then D2.1 in {a: lower_bound A <= a & a <= upper_bound A} by
RCOMP_1:def 1;
then ex a st D2.1=a & lower_bound A <= a & a <= upper_bound A;
then D2.1 >= lower_bound B by A5,Def3;
then reconsider
DD2=mid(D2,1,indx(D2,D1,1)) as Division of B by A34,A36,A38,A7,Th35;
indx(D2,D1,1) in dom D2 by A1,A5,Def18;
then
A39: indx(D2,D1,1) in Seg(len D2) by FINSEQ_1:def 3;
then
A40: 1 <= indx(D2,D1,1) by FINSEQ_1:1;
A41: indx(D2,D1,1) <= len D2 by A39,FINSEQ_1:1;
then
A42: 1 <= len D2 by A40,XXREAL_0:2;
then len mid(D2,1,indx(D2,D1,1))=indx(D2,D1,1)-'1+1 by A40,A41,
FINSEQ_6:118;
then
A43: len mid(D2,1,indx(D2,D1,1))=indx(D2,D1,1)-1+1 by A40,XREAL_1:233;
then
A44: len mid(D2,1,indx(D2,D1,1))=len (D2|indx(D2,D1,1)) by A41,FINSEQ_1:59;
A45: for k be Nat st 1 <= k & k <= len mid(D2,1,indx(D2,D1,1)) holds mid
(D2,1,indx(D2,D1,1)).k=(D2|indx(D2,D1,1)).k
proof
let k be Nat;
assume that
A46: 1 <= k and
A47: k <= len mid(D2,1,indx(D2,D1,1));
k in Seg len (D2|indx(D2,D1,1)) by A44,A46,A47,FINSEQ_1:1;
then k in dom (D2|indx(D2,D1,1)) by FINSEQ_1:def 3;
then k in dom (D2|Seg indx(D2,D1,1)) by FINSEQ_1:def 16;
then
A48: (D2|Seg indx(D2,D1,1)).k=D2.k by FUNCT_1:47;
mid(D2,1,indx(D2,D1,1)).k=D2.(k+1-'1) by A40,A41,A42,A46,A47,
FINSEQ_6:118;
then mid(D2,1,indx(D2,D1,1)).k=D2.(k+1-1) by NAT_1:11,XREAL_1:233;
hence thesis by A48,FINSEQ_1:def 16;
end;
then
A49: mid(D2,1,indx(D2,D1,1))=D2|indx(D2,D1,1) by A44,FINSEQ_1:14;
A50: for i be Nat st 1 <= i & i <= len upper_volume(g,DD2) holds
upper_volume(g,DD2).i = (upper_volume(f,D2)|indx(D2,D1,1)).i
proof
let i be Nat;
assume that
A51: 1 <= i and
A52: i <= len upper_volume(g,DD2);
A53: i <= len DD2 by A52,Def5;
then
A54: i in Seg(len DD2) by A51,FINSEQ_1:1;
then
A55: i in dom DD2 by FINSEQ_1:def 3;
divset(DD2,i)=divset(D2,i)
proof
Seg indx(D2,D1,1) c= Seg(len D2) by A41,FINSEQ_1:5;
then i in Seg(len D2) by A43,A54;
then
A56: i in dom D2 by FINSEQ_1:def 3;
now
per cases;
suppose
A57: i=1;
then
A58: 1 in dom (D2|Seg indx(D2,D1,1)) by A49,A55,FINSEQ_1:def 16;
then 1 in dom D2 /\ Seg indx(D2,D1,1) by RELAT_1:61;
then
A59: 1 in dom D2 by XBOOLE_0:def 4;
A60: divset(D2,i)= [.lower_bound divset(D2,1),upper_bound
divset(D2,1).] by A57,Th2
.=[.lower_bound A,upper_bound divset(D2,1).] by A59,Def3
.=[.lower_bound A,D2.1 .] by A59,Def3;
divset (DD2,i)=[.lower_bound divset(DD2,1), upper_bound
divset(DD2,1).] by A57,Th2
.=[.lower_bound B,upper_bound divset(DD2,1).] by A55,A57,Def3
.=[.lower_bound B,DD2.1 .] by A55,A57,Def3
.=[.lower_bound B,(D2|indx(D2,D1,1)).1 .] by A45,A53,A57
.=[.lower_bound B,(D2|Seg indx(D2,D1,1)).1 .] by
FINSEQ_1:def 16
.=[.lower_bound B,D2.1 .] by A58,FUNCT_1:47
.=[.lower_bound A,D2.1 .] by A5,Def3;
hence thesis by A60;
end;
suppose
A61: i<>1;
A62: i-1 in dom(D2|Seg indx(D2,D1,1))
proof
i is non trivial by A51,A61,NAT_2:def 1;
then
A63: i>=1+1 by NAT_2:29;
then
A64: 1 <= i-1 by XREAL_1:19;
A65: ex j being Nat st i = 1 + j by A51,NAT_1:10;
A66: i-1<=indx(D2,D1,1)-0 by A43,A53,XREAL_1:13;
then i-1 <= len D2 by A37,XXREAL_0:2;
then i-1 in Seg(len D2) by A65,A64,FINSEQ_1:1;
then
A67: i-1 in dom D2 by FINSEQ_1:def 3;
i-1 >= 1 by A63,XREAL_1:19;
then i-1 in Seg indx(D2,D1,1) by A65,A66,FINSEQ_1:1;
then i-1 in dom D2 /\ Seg indx(D2,D1,1) by A67,XBOOLE_0:def 4;
hence thesis by RELAT_1:61;
end;
DD2.(i-1)=(D2|indx(D2,D1,1)).(i-1) by A44,A45,FINSEQ_1:14
.=(D2|Seg indx(D2,D1,1)).(i-1) by FINSEQ_1:def 16;
then
A68: DD2.(i-1)=D2.(i-1) by A62,FUNCT_1:47;
i <= len D2 by A43,A37,A53,XXREAL_0:2;
then i in Seg(len D2) by A51,FINSEQ_1:1;
then i in dom D2 by FINSEQ_1:def 3;
then i in dom D2 /\ Seg indx(D2,D1,1) by A43,A54,XBOOLE_0:def 4;
then
A69: i in dom(D2|Seg indx(D2,D1,1)) by RELAT_1:61;
DD2.i=(D2|indx(D2,D1,1)).i by A44,A45,FINSEQ_1:14
.=(D2|Seg indx(D2,D1,1)).i by FINSEQ_1:def 16;
then
A70: DD2.i=D2.i by A69,FUNCT_1:47;
A71: divset(D2,i)= [.lower_bound divset(D2,i),upper_bound
divset(D2,i).] by Th2
.=[. D2.(i-1),upper_bound divset(D2,i).] by A56,A61,Def3
.=[. D2.(i-1),D2.i .] by A56,A61,Def3;
divset(DD2,i)=[.lower_bound divset(DD2,i), upper_bound
divset(DD2,i).] by Th2
.=[. DD2.(i-1),upper_bound divset(DD2,i).] by A55,A61,Def3
.=[. D2.(i-1),D2.i .] by A55,A61,A68,A70,Def3;
hence thesis by A71;
end;
end;
hence thesis;
end;
then
A72: upper_volume(g,DD2).i =(upper_bound (rng (g|divset(D2,i))))*vol(
divset(D2,i)) by A55,Def5;
Seg indx(D2,D1,1) c= Seg(len D2) by A41,FINSEQ_1:5;
then i in Seg(len D2) by A43,A54;
then
A73: i in dom D2 by FINSEQ_1:def 3;
A74: i in dom DD2 by A54,FINSEQ_1:def 3;
A75: now
per cases;
suppose
A76: i=1;
then 1 in dom (D2|Seg indx(D2,D1,1)) by A49,A74,FINSEQ_1:def 16;
then 1 in dom D2 /\ Seg indx(D2,D1,1) by RELAT_1:61;
then
A77: 1 in dom D2 by XBOOLE_0:def 4;
then
A78: D2.1 <= D2.indx(D2,D1,1) by A34,A36,SEQ_4:137;
lower_bound divset(D2,i)=lower_bound A by A76,A77,Def3;
then
A79: lower_bound divset(D2,i)=lower_bound divset(D1,1) by A5,Def3;
upper_bound divset(D2,i)=D2.1 by A76,A77,Def3;
then upper_bound divset(D2,i) <= D1.1 by A1,A5,A78,Def18;
then
A80: upper_bound divset(D2,i) <= upper_bound divset(D1,1) by A5,Def3;
lower_bound divset(D1,1) <= upper_bound divset(D1,1) by SEQ_4:11;
hence lower_bound divset(D2,i)in [.lower_bound divset(D1,1),
upper_bound divset(D1,1).] by A79,XXREAL_1:1;
lower_bound divset(D2,i) <= upper_bound divset(D2,i) by SEQ_4:11;
then upper_bound divset(D2,i)in{r: lower_bound divset(D1,1)<=r &
r<= upper_bound divset(D1,1)} by A79,A80;
hence upper_bound divset(D2,i)in [.lower_bound divset(D1,1),
upper_bound divset(D1,1).] by RCOMP_1:def 1;
end;
suppose
A81: i<>1;
then i is non trivial by A51,NAT_2:def 1;
then i >= 1+1 by NAT_2:29;
then
A82: 1 <= i-1 by XREAL_1:19;
A83: ex j being Nat st i = 1 + j by A51,NAT_1:10;
A84: rng D2 c= A by Def1;
A85: lower_bound divset(D2,i)=D2.(i-1) by A73,A81,Def3;
A86: lower_bound divset(D1,1)=lower_bound A by A5,Def3;
A87: i-1 <= indx(D2,D1,1)-0 by A43,A53,XREAL_1:13;
then i-1 <= len D2 by A37,XXREAL_0:2;
then i-1 in Seg(len D2) by A83,A82,FINSEQ_1:1;
then
A88: i-1 in dom D2 by FINSEQ_1:def 3;
then D2.(i-1) in rng D2 by FUNCT_1:def 3;
then
A89: lower_bound divset(D2,i) >= lower_bound divset(D1,1) by A85,A86,A84
,SEQ_4:def 2;
A90: upper_bound divset(D1,1)=D1.1 by A5,Def3;
D2.(i-1)<= D2.indx(D2,D1,1) by A34,A87,A88,SEQ_4:137;
then lower_bound divset(D2,i) <= upper_bound divset(D1,1) by A1,A5
,A85,A90,Def18;
then lower_bound divset(D2,i)in{r: lower_bound divset(D1,1)<=r &
r<= upper_bound divset(D1,1)} by A89;
hence lower_bound divset(D2,i)in [.lower_bound divset(D1,1),
upper_bound divset(D1,1).] by RCOMP_1:def 1;
A91: upper_bound divset(D2,i)=D2.i by A73,A81,Def3;
D2.i in rng D2 by A73,FUNCT_1:def 3;
then
A92: upper_bound divset(D2,i) >= lower_bound divset(D1,1) by A91,A86,A84
,SEQ_4:def 2;
D2.i <= D2.indx(D2,D1,1) by A43,A34,A53,A73,SEQ_4:137;
then upper_bound divset(D2,i) <= upper_bound divset(D1,1) by A1,A5
,A91,A90,Def18;
then upper_bound divset(D2,i)in{r: lower_bound divset(D1,1)<=r &
r<= upper_bound divset(D1,1)} by A92;
hence upper_bound divset(D2,i)in [.lower_bound divset(D1,1),
upper_bound divset(D1,1).] by RCOMP_1:def 1;
end;
end;
A93: divset(D1,1)=[.lower_bound divset(D1,1),upper_bound divset(D1,1)
.] by Th2;
A94: Seg indx(D2,D1,1) c= Seg(len D2) by A41,FINSEQ_1:5;
then i in Seg(len D2) by A43,A54;
then
A95: i in dom D2 by FINSEQ_1:def 3;
divset(D2,i)=[.lower_bound divset(D2,i),upper_bound divset(D2,i)
.] by Th2;
then
A96: divset(D2,i) c= divset(D1,1) by A93,A75,XXREAL_2:def 12;
A97: dom (upper_volume(f,D2)|Seg indx(D2,D1,1)) =dom upper_volume(f,
D2) /\ Seg indx(D2,D1,1) by RELAT_1:61
.=Seg(len upper_volume(f,D2)) /\ Seg indx(D2,D1,1) by FINSEQ_1:def 3
.=Seg(len D2) /\ Seg indx(D2,D1,1) by Def5
.=Seg indx(D2,D1,1) by A94,XBOOLE_1:28;
(upper_volume(f,D2)|indx(D2,D1,1)).i =(upper_volume(f,D2)|Seg
indx(D2,D1,1)).i by FINSEQ_1:def 16
.=upper_volume(f,D2).i by A43,A54,A97,FUNCT_1:47
.=(upper_bound (rng (f|divset(D2,i))))*vol(divset(D2,i)) by A95,Def5;
hence thesis by A72,A96,FUNCT_1:51;
end;
len upper_volume(g,DD1) = len (upper_volume(f,D1)|1) by A10;
then
A98: upper_volume(g,DD1) = upper_volume(f,D1)|1 by A18,FINSEQ_1:14;
A99: indx(D2,D1,1) <= len upper_volume(f,D2) by A41,Def5;
len upper_volume(g,DD2)= indx(D2,D1,1) by A43,Def5;
then
A100: len upper_volume(g,DD2)=len(upper_volume(f,D2)|indx(D2,D1, 1)) by A99,
FINSEQ_1:59;
dom g = A /\ divset(D1,1) by A4,FUNCT_2:def 1;
then dom g = divset(D1,1) by A5,Th6,XBOOLE_1:28;
then g is total by PARTFUN1:def 2;
then upper_sum(g,DD1) >= upper_sum(g,DD2) by A11,A28,Th28;
hence thesis by A98,A100,A50,FINSEQ_1:14;
end;
A101: for k being non zero Nat st P[k] holds P[k+1]
proof
let k be non zero Nat;
assume
A102: k in dom D1 implies Sum(upper_volume(f,D1)|k) >= Sum(
upper_volume(f,D2)|indx(D2,D1,k));
assume
A103: k+1 in dom D1;
then
A104: k+1 in Seg(len D1) by FINSEQ_1:def 3;
then
A105: 1 <= k+1 by FINSEQ_1:1;
A106: k+1 <= len D1 by A104,FINSEQ_1:1;
now
per cases;
suppose
1=k+1;
hence thesis by A3,A103;
end;
suppose
A107: 1<>k+1;
set IDK =indx(D2,D1,k);
set IDK1=indx(D2,D1,k+1);
set K1D2=upper_volume(f,D2)|indx(D2,D1,k+1);
set KD1 =upper_volume(f,D1)|k;
set K1D1=upper_volume(f,D1)|(k+1);
set n=k+1;
A108: k+1 <= len upper_volume(f,D1) by A106,Def5;
then
A109: len K1D1=k+1 by FINSEQ_1:59;
then consider p1,q1 being FinSequence of REAL such that
A110: len p1=k and
A111: len q1=1 and
A112: K1D1=p1^q1 by FINSEQ_2:23;
A113: k <= k+1 by NAT_1:11;
then
A114: k <= len D1 by A106,XXREAL_0:2;
then
A115: k <= len upper_volume(f,D1) by Def5;
then
A116: len p1 = len KD1 by A110,FINSEQ_1:59;
for i be Nat st 1 <= i & i <= len p1 holds p1.i=KD1.i
proof
let i be Nat;
assume that
A117: 1 <= i and
A118: i <= len p1;
A119: i in Seg(len p1) by A117,A118,FINSEQ_1:1;
then
A120: i in dom KD1 by A116,FINSEQ_1:def 3;
then
A121: i in dom (upper_volume(f,D1)|Seg k) by FINSEQ_1:def 16;
k <= k+1 by NAT_1:11;
then
A122: Seg k c= Seg(k+1) by FINSEQ_1:5;
A123: dom K1D1 =Seg(len K1D1) by FINSEQ_1:def 3
.= Seg(k+1) by A108,FINSEQ_1:59;
dom KD1=Seg(len KD1) by FINSEQ_1:def 3
.= Seg k by A115,FINSEQ_1:59;
then i in dom K1D1 by A120,A122,A123;
then
A124: i in dom (upper_volume(f,D1)|Seg(k+1)) by FINSEQ_1:def 16;
A125: K1D1.i = (upper_volume(f,D1)|Seg (k+1)).i by FINSEQ_1:def 16
.= upper_volume(f,D1).i by A124,FUNCT_1:47;
A126: KD1.i = (upper_volume(f,D1)|Seg k).i by FINSEQ_1:def 16
.= upper_volume(f,D1).i by A121,FUNCT_1:47;
i in dom p1 by A119,FINSEQ_1:def 3;
hence thesis by A112,A126,A125,FINSEQ_1:def 7;
end;
then
A127: p1=KD1 by A116,FINSEQ_1:14;
A128: indx(D2,D1,k+1) in dom D2 by A1,A103,Def18;
then
A129: indx(D2,D1,k+1) in Seg(len D2) by FINSEQ_1:def 3;
then
A130: 1 <= indx(D2,D1,k+1) by FINSEQ_1:1;
n is non trivial by A107,NAT_2:def 1;
then n >= 2 by NAT_2:29;
then k >= (1+1)-1 by XREAL_1:20;
then
A131: k in Seg(len D1) by A114,FINSEQ_1:1;
then
A132: k in dom D1 by FINSEQ_1:def 3;
then
A133: indx(D2,D1,k) in dom D2 by A1,Def18;
A134: indx(D2,D1,k) < indx(D2,D1,k+1)
proof
k < k+1 by NAT_1:13;
then
A135: D1.k < D1.(k+1) by A103,A132,SEQM_3:def 1;
assume indx(D2,D1,k) >= indx(D2,D1,k+1);
then
A136: D2.indx(D2,D1,k) >= D2.indx(D2,D1,k+1) by A133,A128,SEQ_4:137;
D1.k=D2.indx(D2,D1,k) by A1,A132,Def18;
hence contradiction by A1,A103,A136,A135,Def18;
end;
A137: indx(D2,D1,k+1) >= indx(D2,D1,k)
proof
assume indx(D2,D1,k+1) < indx(D2,D1,k);
then
A138: D2.indx(D2,D1,k+1) < D2.indx(D2,D1,k) by A133,A128,SEQM_3:def 1;
D1.(k+1) = D2.indx(D2,D1,k+1) by A1,A103,Def18;
then D1.(k+1) < D1.k by A1,A132,A138,Def18;
hence contradiction by A103,A132,NAT_1:11,SEQ_4:137;
end;
then consider ID being Nat such that
A139: indx(D2,D1,k+1) = indx(D2,D1,k) + ID by NAT_1:10;
reconsider ID as Element of NAT by ORDINAL1:def 12;
A140: len upper_volume(f,D2) = len D2 by Def5;
then
A141: indx(D2,D1,k+1) <= len upper_volume(f,D2) by A129,FINSEQ_1:1;
then len K1D2=IDK + (IDK1-IDK) by FINSEQ_1:59;
then consider p2,q2 being FinSequence of REAL such that
A142: len p2=IDK and
A143: len q2=IDK1-IDK and
A144: K1D2=p2^q2 by A139,FINSEQ_2:23;
indx(D2,D1,k) in dom D2 by A1,A132,Def18;
then
A145: indx(D2,D1,k)in Seg(len upper_volume(f,D2)) by A140,FINSEQ_1:def 3;
then
A146: 1<=indx(D2,D1,k) by FINSEQ_1:1;
set KD2 =upper_volume(f,D2)|indx(D2,D1,k);
A147: Sum K1D2=Sum p2+Sum q2 by A144,RVSUM_1:75;
A148: indx(D2,D1,k)<=len upper_volume(f, D2) by A145,FINSEQ_1:1;
then
A149: len p2 = len KD2 by A142,FINSEQ_1:59;
for i be Nat st 1 <= i & i <= len p2 holds p2.i=KD2.i
proof
let i be Nat;
assume that
A150: 1 <= i and
A151: i <= len p2;
A152: i in Seg(len p2) by A150,A151,FINSEQ_1:1;
then
A153: i in dom KD2 by A149,FINSEQ_1:def 3;
then
A154: i in dom (upper_volume(f,D2)|Seg indx(D2,D1,k)) by FINSEQ_1:def 16;
A155: dom K1D2 = Seg(len K1D2) by FINSEQ_1:def 3
.= Seg indx(D2,D1,k+1) by A141,FINSEQ_1:59;
A156: Seg indx(D2,D1,k) c= Seg indx(D2,D1,k+1) by A137,FINSEQ_1:5;
dom KD2 =Seg(len KD2) by FINSEQ_1:def 3
.= Seg indx(D2,D1,k) by A148,FINSEQ_1:59;
then i in dom K1D2 by A153,A156,A155;
then
A157: i in dom (upper_volume(f,D2)|Seg indx(D2,D1,k+ 1)) by
FINSEQ_1:def 16;
A158: K1D2.i=(upper_volume(f,D2)|Seg indx(D2,D1,k+1)).i by
FINSEQ_1:def 16
.=upper_volume(f,D2).i by A157,FUNCT_1:47;
A159: KD2.i=(upper_volume(f,D2)|Seg indx(D2,D1,k)).i by FINSEQ_1:def 16
.= upper_volume(f,D2).i by A154,FUNCT_1:47;
i in dom p2 by A152,FINSEQ_1:def 3;
hence thesis by A144,A159,A158,FINSEQ_1:def 7;
end;
then
A160: p2=KD2 by A149,FINSEQ_1:14;
A161: indx(D2,D1,k+1) <= len D2 by A129,FINSEQ_1:1;
A162: ID = indx(D2,D1,k+1) - indx(D2,D1,k) by A139;
A163: Sum q1 >= Sum q2
proof
set MD2 = mid(D2,indx(D2,D1,k)+1,indx(D2,D1,k+1));
set MD1 = mid(D1,k+1,k+1);
set DD1 = divset(D1,k+1);
set g = f|DD1;
A164: 1 <= indx(D2,D1,k)+1 by NAT_1:11;
reconsider g as PartFunc of DD1,REAL by PARTFUN1:10;
(k+1)-1=k;
then
A165: lower_bound DD1=D1.k by A103,A107,Def3;
D2.indx(D2,D1,k+1)=D1.(k+1) by A1,A103,Def18;
then
A166: D2.indx(D2,D1,k+1) = upper_bound DD1 by A103,A107,Def3;
A167: indx(D2,D1,k)+1 <= indx(D2,D1,k+1) by A134,NAT_1:13;
then
A168: indx(D2,D1,k)+1 <= len D2 by A161,XXREAL_0:2;
then indx(D2,D1,k)+1 in Seg(len D2) by A164,FINSEQ_1:1;
then
A169: indx(D2,D1,k)+1 in dom D2 by FINSEQ_1:def 3;
then D2.(indx(D2,D1,k)+1)>=D2.indx(D2,D1,k) by A133,NAT_1:11
,SEQ_4:137;
then D2.(indx(D2,D1,k)+1) >= lower_bound DD1 by A1,A132,A165,Def18;
then reconsider MD2 as Division of DD1 by A128,A167,A169,A166,Th35;
A170: indx(D2,D1,k+1)-'(indx(D2,D1,k)+1)+1 =indx(D2,D1,k+1)-(indx(
D2,D1,k)+1)+1 by A167,XREAL_1:233
.=indx(D2,D1,k+1)-indx(D2,D1,k);
A171: for n be Nat st 1 <= n & n <= len q2 holds q2.n=upper_volume
(g,MD2).n
proof
A172: dom K1D2 = Seg(len K1D2) by FINSEQ_1:def 3
.= Seg indx(D2,D1,k+1) by A141,FINSEQ_1:59;
then
A173: dom K1D2 c= Seg(len D2) by A161,FINSEQ_1:5;
then
A174: dom K1D2 c= dom D2 by FINSEQ_1:def 3;
A175: len mid(D2,indx(D2,D1,k)+1,indx(D2,D1,k+1)) =ID by A130,A161,A139
,A167,A168,A164,A170,FINSEQ_6:118;
let n be Nat;
assume that
A176: 1 <= n and
A177: n <= len q2;
n in Seg(len q2) by A176,A177,FINSEQ_1:1;
then
A178: n in dom q2 by FINSEQ_1:def 3;
then
A179: indx(D2,D1,k)+n in dom K1D2 by A142,A144,FINSEQ_1:28;
then
A180: indx(D2,D1,k)+n in dom (upper_volume(f,D2) |Seg indx(D2,D1
,k +1)) by FINSEQ_1:def 16;
A181: q2.n=K1D2.(indx(D2,D1,k)+n) by A142,A144,A178,FINSEQ_1:def 7
.=(upper_volume(f,D2)|Seg indx(D2,D1,k+1)).(indx(D2,D1,k)+n)
by FINSEQ_1:def 16
.=upper_volume(f,D2).(indx(D2,D1,k)+n) by A180,FUNCT_1:47
.=(upper_bound(rng(f|divset(D2,indx(D2,D1,k)+n))))* vol(
divset(D2,indx(D2,D1,k)+n)) by A179,A174,Def5;
indx(D2,D1,k)+n in Seg len D2 by A179,A173;
then
A182: indx(D2,D1,k)+n in dom D2 by FINSEQ_1:def 3;
indx(D2,D1,k)+n <= indx(D2,D1,k+1) by A172,A179,FINSEQ_1:1;
then
A183: n <= ID by A162,XREAL_1:19;
then n in Seg ID by A176,FINSEQ_1:1;
then
A184: n in dom MD2 by A175,FINSEQ_1:def 3;
n in Seg(len mid(D2,indx(D2,D1,k)+1,indx( D2, D1,k+1))) by A176
,A183,A175,FINSEQ_1:1; then
A185: n
in dom mid(D2,indx(D2,D1,k)+1,indx( D2, D1,k+1)) by FINSEQ_1:def 3;
A186: 1 <=indx(D2,D1,k)+n by A172,A179,FINSEQ_1:1;
A187: divset(MD2,n)=divset(D2,indx(D2,D1,k)+n) & divset(D2,indx(
D2,D1,k)+n) c= divset(D1,k+1)
proof
now
per cases;
suppose
A188: n=1;
then
A189: indx(D2,D1,k)+1<=len D2 by A179,A173,FINSEQ_1:1;
A190: 1<=indx(D2,D1,k)+1 by A172,A179,A188,FINSEQ_1:1;
A191: upper_bound divset(MD2,1)= mid(D2,indx(D2,D1,k)+1,
indx(D2,D1,k+1)).1 by A184,A188,Def3
.= D2.(1+indx(D2,D1,k)) by A130,A161,A190,A189,
FINSEQ_6:118;
A192: indx(D2,D1,k)+1 <> 1 by A146,NAT_1:13;
A193: (k+1)-1=k;
A194: lower_bound divset(MD2,1)=lower_bound divset(D1,k+1)
by A184,A188,Def3
.= D1.k by A103,A107,A193,Def3;
A195: divset(D2,indx(D2,D1,k)+n)= [.lower_bound divset(D2,
indx(D2,D1,k)+1),upper_bound divset(D2, indx(D2,D1,k)+1).] by A188,Th2
.=[.D2.(indx(D2,D1,k)+1-1),upper_bound divset(D2,indx(
D2,D1,k)+1).] by A169,A192,Def3
.=[.D2.indx(D2,D1,k),D2.(indx(D2,D1,k)+1).] by A169,A192
,Def3
.=[.D1.k,D2.(indx(D2,D1,k)+1).] by A1,A132,Def18;
hence
divset(MD2,n)=divset(D2,indx(D2,D1,k)+n) by A188,A194,A191
,Th2;
divset(MD2,n)=[.D1.k,D2.(indx( D2,D1,k)+1).] by A188,A194
,A191,Th2;
hence thesis by A184,A195,Th6;
end;
suppose
A196: n<>1;
A197: indx(D2,D1,k)+n <> 1
proof
assume indx(D2,D1,k)+n = 1;
then indx(D2,D1,k)=1-n;
then n+1 <= 1 by A146,XREAL_1:19;
then n <= 1-1 by XREAL_1:19;
hence contradiction by A176,NAT_1:3;
end;
A198: divset(D2,indx(D2,D1,k)+n) =[.lower_bound divset(D2,
indx(D2,D1,k)+n), upper_bound divset(D2,indx(D2,D1,k)+n).] by Th2
.=[.D2.(indx(D2,D1,k)+n-1),upper_bound divset(D2,indx(
D2,D1,k)+n).] by A182,A197,Def3
.=[. D2.(indx(D2,D1,k)+n-1),D2.(indx(D2,D1,k)+n) .] by
A182,A197,Def3;
n<=n+1 by NAT_1:12;
then n-1 <= n by XREAL_1:20;
then
A199: n-1<=len MD2 by A183,A175,XXREAL_0:2;
consider n1 being Nat such that
A200: n=1+n1 by A176,NAT_1:10;
n is non trivial by A176,A196,NAT_2:def 1;
then n >= 1+1 by NAT_2:29;
then
A201: 1<=n-1 by XREAL_1:19;
A202: indx(D2,D1,k)+1 <= indx(D2,D1,k+1) by A134,NAT_1:13;
reconsider n1 as Element of NAT by ORDINAL1:def 12;
A203: n1+(indx(D2,D1,k)+1)-'1=indx(D2,D1,k)+n-1 by A186,A200,
XREAL_1:233;
A204: n +(indx(D2,D1,k)+1)-'1=n+indx(D2,D1,k)+1-1 by NAT_1:11
,XREAL_1:233
.=indx(D2,D1,k)+n;
A205: lower_bound divset(MD2,n)=MD2.(n-1) by A184,A196,Def3
.=D2.(indx(D2,D1,k)+n-1) by A130,A161,A168,A164,A202,A200
,A203,A201,A199,FINSEQ_6:118;
A206: upper_bound divset(MD2,n)=MD2.n by A184,A196,Def3
.=D2.(indx(D2,D1,k)+n) by A130,A161,A168,A164,A176,A183,
A175,A202,A204,FINSEQ_6:118;
hence divset(MD2,n)=divset(D2,indx(D2,D1,k)+n) by A205,A198
,Th2;
divset(MD2,n)= [. D2.(indx(D2,D1,k)+n-1),D2.(indx(D2
,D1,k)+n) .] by A205,A206,Th2;
hence thesis by A184,A198,Th6;
end;
end;
hence thesis;
end;
then g|divset(MD2,n) =f|divset(D2,indx(D2,D1,k)+n) by FUNCT_1:51;
hence thesis by A185,A181,A187,Def5;
end;
(k+1)-1=k;
then
A207: lower_bound DD1=D1.k by A103,A107,Def3;
D1.(k+1) = upper_bound DD1 by A103,A107,Def3;
then reconsider MD1 as Division of DD1 by A103,A113,A132,A207,Th35,
SEQ_4:137;
A208: g|divset(D1,k+1) is bounded_above
proof
consider a be Real such that
A209: for x being object st x in A /\ dom f holds f.x <= a by A2,
RFUNCT_1:70;
for x being object st x in divset(D1,k+1) /\ dom g holds g.x
<= a
proof
let x be object;
A210: dom g c= dom f by RELAT_1:60;
assume x in divset(D1,k+1) /\ dom g;
then
A211: x in dom g by XBOOLE_0:def 4;
A212: A /\ dom f = dom f by XBOOLE_1:28;
then x in A /\ dom f by A211,A210;
then reconsider x as Element of A;
f.x <= a by A209,A211,A212,A210;
hence thesis by A211,FUNCT_1:47;
end;
hence thesis by RFUNCT_1:70;
end;
len MD1 = (k+1) -'(k+1) + 1 by A105,A106,FINSEQ_6:118;
then
A213: len MD1 = ((k+1)-(k+1)) +1 by XREAL_1:233;
then
A214: dom q1 = dom MD1 by A111,FINSEQ_3:29;
A215: for n be Nat st 1 <= n & n <= len q1 holds q1.n=upper_volume
(g,MD1).n
proof
k+1 in Seg(len K1D1) by A109,FINSEQ_1:4;
then k+1 in dom K1D1 by FINSEQ_1:def 3;
then
A216: k+1 in dom (upper_volume(f,D1)|Seg(k+1)) by FINSEQ_1:def 16;
A217: MD1.1 =D1.(k+1) by A105,A106,FINSEQ_6:118;
1 in Seg(len MD1) by A213,FINSEQ_1:3;
then
A218: 1 in dom MD1 by FINSEQ_1:def 3;
divset(MD1,1)=[.lower_bound divset(MD1,1), upper_bound
divset(MD1,1).] by Th2;
then
A219: divset(MD1,1)=[.lower_bound DD1,upper_bound divset(MD1,1)
.] by A218,Def3
.=[.lower_bound DD1,D1.(k+1).] by A218,A217,Def3;
(k+1)-1=k;
then
A220: lower_bound DD1 = D1.k by A103,A107,Def3;
let n be Nat;
assume that
A221: 1 <= n and
A222: n <= len q1;
A223: n = 1 by A111,A221,A222,XXREAL_0:1;
n in Seg(len q1) by A221,A222,FINSEQ_1:1;
then
A224: n in dom q1 by FINSEQ_1:def 3;
upper_bound DD1 = D1.(k+1) by A103,A107,Def3;
then divset(D1,k+1)=[. D1.k,D1.(k+1).] by A220,Th2;
then
A225: upper_volume(g,MD1).n =(upper_bound(rng(g|divset(D1,k+1)))
)*vol(divset(D1,k+1)) by A214,A223,A224,A219,A220,Def5;
K1D1.(k+1)=(upper_volume(f,D1)|Seg(k+1)).(k+1) by FINSEQ_1:def 16
.=upper_volume(f,D1).(k+1) by A216,FUNCT_1:47;
then q1.n = upper_volume(f,D1).(k+1) by A110,A112,A223,A224,
FINSEQ_1:def 7
.=(upper_bound(rng(f|divset(D1,k+1))))*vol(divset(D1,k+1))
by A103,Def5;
hence thesis by A225;
end;
len q1 = len(upper_volume(g,MD1)) by A111,A213,Def5;
then
A226: q1=upper_volume(g,MD1) by A215,FINSEQ_1:14;
dom g = dom f /\ divset(D1,k+1) by RELAT_1:61;
then dom g = A /\ divset(D1,k+1) by FUNCT_2:def 1;
then dom g = divset(D1,k+1) by A103,Th6,XBOOLE_1:28;
then
A227: g is total by PARTFUN1:def 2;
len MD1 = (k+1) -'(k+1) + 1 by A105,A106,FINSEQ_6:118;
then len MD1 = (k+1) - (k+1) + 1 by XREAL_1:233;
then
A228: upper_sum(g,MD1) >= upper_sum(g,MD2) by A208,A227,Th28;
len(upper_volume(g,MD2))= len mid(D2,indx(D2,D1,k)+1,indx(D2
,D1,k+1)) by Def5
.=indx(D2,D1,k+1)-indx(D2,D1,k) by A130,A161,A167,A168,A164,A170,
FINSEQ_6:118;
hence thesis by A143,A226,A171,A228,FINSEQ_1:14;
end;
Sum K1D1=Sum p1+Sum q1 by A112,RVSUM_1:75;
then Sum q1 = Sum K1D1 - Sum p1;
then Sum K1D1 >= Sum q2 + Sum p1 by A163,XREAL_1:19;
then Sum K1D1 - Sum q2 >= Sum p1 by XREAL_1:19;
then Sum K1D1 - Sum q2 >= Sum p2 by A102,A131,A127,A160,
FINSEQ_1:def 3,XXREAL_0:2;
hence thesis by A147,XREAL_1:19;
end;
end;
hence thesis;
end;
thus for k being non zero Nat holds P[k] from NAT_1:sch 10(A3, A101);
end;
hence thesis;
end;
theorem Th37:
D1 <= D2 & f|A is bounded_below implies for i be non zero
Element of NAT holds (i in dom D1 implies
Sum(lower_volume(f,D1)|i) <= Sum(lower_volume(f,D2)|indx(D2,D1,i)))
proof
assume that
A1: D1 <= D2 and
A2: f|A is bounded_below;
for i be non zero Nat holds i in dom D1 implies Sum(lower_volume(f,D1)|
i) <= Sum(lower_volume(f,D2)|indx(D2,D1,i))
proof
defpred P[Nat] means $1 in dom D1 implies Sum(lower_volume(f,D1)|$1) <=
Sum(lower_volume(f,D2)|indx(D2,D1,$1));
A3: P[1]
proof
set g=f|divset(D1,1);
set B=divset(D1,1);
set DD2=mid(D2,1,indx(D2,D1,1));
set DD1=mid(D1,1,1);
reconsider g as PartFunc of divset(D1,1),REAL by PARTFUN1:10;
A4: dom g = dom f /\ divset(D1,1) by RELAT_1:61;
assume
A5: 1 in dom D1;
then
A6: D1.1 = upper_bound B by Def3;
then
A7: D2.indx(D2,D1,1) = upper_bound B by A1,A5,Def18;
lower_bound B <= upper_bound B by SEQ_4:11;
then reconsider DD1 as Division of B by A5,A6,Th35;
1 in Seg(len D1) by A5,FINSEQ_1:def 3;
then
A8: 1 <= len D1 by FINSEQ_1:1;
then
A9: len mid(D1,1,1)=1-'1+1 by FINSEQ_6:118;
A10: len lower_volume(g,DD1)=len DD1 by Def6
.= 1 by A9,XREAL_1:235;
A11: len mid(D1,1,1)=1 by A9,XREAL_1:235;
then
A12: len mid(D1,1,1)=len (D1|1);
for k be Nat st 1 <= k & k <= len mid(D1,1,1) holds mid(D1,1,1).k=(
D1|1).k
proof
let k be Nat;
assume that
A13: 1 <= k and
A14: k <= len mid(D1,1,1);
k in Seg(len(D1|1)) by A12,A13,A14,FINSEQ_1:1;
then k in dom (D1|1) by FINSEQ_1:def 3;
then k in dom (D1|Seg 1) by FINSEQ_1:def 16;
then
A15: (D1|Seg 1).k = D1.k by FUNCT_1:47;
A16: k = 1 by A11,A13,A14,XXREAL_0:1;
then mid(D1,1,1).k = D1.(1+1-1) by A8,FINSEQ_6:118;
hence thesis by A16,A15,FINSEQ_1:def 16;
end;
then
A17: mid(D1,1,1)=D1|1 by A12,FINSEQ_1:14;
A18: for i be Nat st 1 <= i & i <= len lower_volume(g,DD1) holds
lower_volume(g,DD1).i=(lower_volume(f,D1)|1).i
proof
let i be Nat;
assume that
A19: 1 <= i and
A20: i <= len lower_volume(g,DD1);
A21: 1 in Seg 1 by FINSEQ_1:3;
dom(D1|Seg 1) = dom D1 /\ Seg 1 by RELAT_1:61;
then
A22: 1 in dom(D1|Seg 1) by A5,A21,XBOOLE_0:def 4;
dom(lower_volume(f,D1))=Seg(len lower_volume(f,D1)) by FINSEQ_1:def 3
.=Seg(len D1) by Def6;
then
A23: dom(lower_volume(f,D1)|Seg 1) =Seg(len D1) /\ Seg 1 by RELAT_1:61
.=Seg 1 by A8,FINSEQ_1:7;
len DD1 = 1 by A9,XREAL_1:235;
then
A24: 1 in dom DD1 by A21,FINSEQ_1:def 3;
A25: (lower_volume(f,D1)|1).i=(lower_volume(f,D1)|Seg 1).i by
FINSEQ_1:def 16
.=(lower_volume(f,D1)|Seg 1).1 by A10,A19,A20,XXREAL_0:1
.=lower_volume(f,D1).1 by A23,FINSEQ_1:3,FUNCT_1:47
.=(lower_bound (rng(f|divset(D1,1))))*vol(divset(D1,1)) by A5,Def6;
A26: divset(D1,1)=[.lower_bound divset(D1,1),upper_bound divset(D1,1)
.] by Th2
.=[.lower_bound A,upper_bound divset(D1,1).] by A5,Def3
.=[.lower_bound A,D1.1 .] by A5,Def3;
A27: lower_volume(g,DD1).i = lower_volume(g,DD1).1 by A10,A19,A20,XXREAL_0:1
.= (lower_bound (rng (g|divset(DD1,1))))*vol(divset(DD1,1)) by A24
,Def6;
divset(DD1,1)=[.lower_bound divset(DD1,1),upper_bound divset(DD1,
1).] by Th2
.=[.lower_bound B,upper_bound divset(DD1,1).] by A24,Def3
.=[.lower_bound B,DD1.1 .] by A24,Def3
.=[.lower_bound A,(D1|1).1 .] by A5,A17,Def3
.=[.lower_bound A,(D1|Seg 1).1 .] by FINSEQ_1:def 16
.=[.lower_bound A,D1.1 .] by A22,FUNCT_1:47;
hence thesis by A27,A26,A25;
end;
A28: g|divset(D1,1) is bounded_below
proof
consider a be Real such that
A29: for x being object st x in A /\ dom f holds a <= f.x
by A2,RFUNCT_1:71;
for x being object st x in divset(D1,1) /\ dom g holds a <= g.x
proof
let x be object;
A30: dom g c= dom f by RELAT_1:60;
assume x in divset(D1,1) /\ dom g; then
A31: x in dom g by XBOOLE_0:def 4;
A32: A /\ dom f = dom f by XBOOLE_1:28;
then reconsider x as Element of A by A31,A30,XBOOLE_0:def 4;
a <= f.x by A29,A31,A32,A30;
hence thesis by A31,FUNCT_1:47;
end;
hence thesis by RFUNCT_1:71;
end;
A33: rng D2 c= A by Def1;
A34: indx(D2,D1,1) in dom D2 by A1,A5,Def18;
then
A35: indx(D2,D1,1) in Seg(len D2) by FINSEQ_1:def 3;
then
A36: 1 <= indx(D2,D1,1) by FINSEQ_1:1;
A37: indx(D2,D1,1) <= len D2 by A35,FINSEQ_1:1;
then 1 <= len D2 by A36,XXREAL_0:2;
then 1 in Seg(len D2) by FINSEQ_1:1;
then
A38: 1 in dom D2 by FINSEQ_1:def 3;
then D2.1 in rng D2 by FUNCT_1:def 3;
then D2.1 in A by A33;
then D2.1 in [.lower_bound A,upper_bound A.] by Th2;
then D2.1 in {a: lower_bound A <= a & a <= upper_bound A} by
RCOMP_1:def 1;
then ex a st D2.1=a & lower_bound A <= a & a <= upper_bound A;
then D2.1 >= lower_bound B by A5,Def3;
then reconsider DD2 as Division of B by A34,A36,A38,A7,Th35;
indx(D2,D1,1) in dom D2 by A1,A5,Def18;
then
A39: indx(D2,D1,1) in Seg(len D2) by FINSEQ_1:def 3;
then
A40: 1 <= indx(D2,D1,1) by FINSEQ_1:1;
A41: indx(D2,D1,1) <= len D2 by A39,FINSEQ_1:1;
then
A42: 1 <= len D2 by A40,XXREAL_0:2;
then len mid(D2,1,indx(D2,D1,1))=indx(D2,D1,1)-'1+1 by A40,A41,
FINSEQ_6:118;
then
A43: len mid(D2,1,indx(D2,D1,1))=indx(D2,D1,1)-1+1 by A40,XREAL_1:233;
then
A44: len mid(D2,1,indx(D2,D1,1))=len(D2|indx(D2,D1,1)) by A41,FINSEQ_1:59;
A45: for k be Nat st 1 <= k & k <= len mid(D2,1,indx(D2,D1,1)) holds mid
(D2,1,indx(D2,D1,1)).k=(D2|indx(D2,D1,1)).k
proof
let k be Nat;
assume that
A46: 1 <= k and
A47: k <= len mid(D2,1,indx(D2,D1,1));
k in Seg len (D2|indx(D2,D1,1)) by A44,A46,A47,FINSEQ_1:1;
then k in dom (D2|indx(D2,D1,1)) by FINSEQ_1:def 3;
then k in dom (D2|Seg indx(D2,D1,1)) by FINSEQ_1:def 16;
then
A48: (D2|Seg indx(D2,D1,1)).k=D2.k by FUNCT_1:47;
mid(D2,1,indx(D2,D1,1)).k=D2.(k+1-'1) by A40,A41,A42,A46,A47,
FINSEQ_6:118;
then mid(D2,1,indx(D2,D1,1)).k=D2.(k+1-1) by NAT_1:11,XREAL_1:233;
hence thesis by A48,FINSEQ_1:def 16;
end;
then
A49: mid(D2,1,indx(D2,D1,1))=D2|indx(D2,D1,1) by A44,FINSEQ_1:14;
A50: for i be Nat st 1 <= i & i <= len lower_volume(g,DD2) holds
lower_volume(g,DD2).i = (lower_volume(f,D2)|indx(D2,D1,1)).i
proof
let i be Nat;
assume that
A51: 1 <= i and
A52: i <= len lower_volume(g,DD2);
A53: i <= len DD2 by A52,Def6;
then
A54: i in Seg(len DD2) by A51,FINSEQ_1:1;
then
A55: i in dom DD2 by FINSEQ_1:def 3;
divset(DD2,i)=divset(D2,i)
proof
Seg indx(D2,D1,1) c= Seg(len D2) by A41,FINSEQ_1:5;
then i in Seg(len D2) by A43,A54;
then
A56: i in dom D2 by FINSEQ_1:def 3;
now
per cases;
suppose
A57: i=1;
then
A58: 1 in dom (D2|Seg indx(D2,D1,1)) by A49,A55,FINSEQ_1:def 16;
then 1 in dom D2 /\ Seg indx(D2,D1,1) by RELAT_1:61;
then
A59: 1 in dom D2 by XBOOLE_0:def 4;
A60: divset(D2,i)=[.lower_bound divset(D2,1), upper_bound
divset(D2,1).] by A57,Th2
.=[.lower_bound A,upper_bound divset(D2,1).] by A59,Def3
.=[.lower_bound A,D2.1 .] by A59,Def3;
divset (DD2,i)=[.lower_bound divset(DD2,1), upper_bound
divset(DD2,1).] by A57,Th2
.=[.lower_bound B,upper_bound divset(DD2,1).] by A55,A57,Def3
.=[.lower_bound B,DD2.1 .] by A55,A57,Def3
.=[.lower_bound B,(D2|indx(D2,D1,1)).1 .] by A45,A53,A57
.=[.lower_bound B,(D2|Seg indx(D2,D1,1)).1 .] by
FINSEQ_1:def 16
.=[.lower_bound B,D2.1 .] by A58,FUNCT_1:47
.=[.lower_bound A,D2.1 .] by A5,Def3;
hence thesis by A60;
end;
suppose
A61: i<>1;
A62: i-1 in dom(D2|Seg indx(D2,D1,1))
proof
i is non trivial by A51,A61,NAT_2:def 1;
then
A63: i >= 1+1 by NAT_2:29;
then
A64: 1 <= i-1 by XREAL_1:19;
A65: ex j being Nat st i = 1 + j by A51,NAT_1:10;
A66: i-1 <= indx(D2,D1,1)-0 by A43,A53,XREAL_1:13;
then i-1 <= len D2 by A37,XXREAL_0:2;
then i-1 in Seg(len D2) by A65,A64,FINSEQ_1:1;
then
A67: i-1 in dom D2 by FINSEQ_1:def 3;
i-1 >= 1 by A63,XREAL_1:19;
then i-1 in Seg indx(D2,D1,1) by A65,A66,FINSEQ_1:1;
then i-1 in dom D2 /\ Seg indx(D2,D1,1) by A67,XBOOLE_0:def 4;
hence thesis by RELAT_1:61;
end;
DD2.(i-1)=(D2|indx(D2,D1,1)).(i-1) by A44,A45,FINSEQ_1:14
.=(D2|Seg indx(D2,D1,1)).(i-1) by FINSEQ_1:def 16;
then
A68: DD2.(i-1)=D2.(i-1) by A62,FUNCT_1:47;
i <= len D2 by A43,A37,A53,XXREAL_0:2;
then i in Seg(len D2) by A51,FINSEQ_1:1;
then i in dom D2 by FINSEQ_1:def 3;
then i in dom D2 /\ Seg indx(D2,D1,1) by A43,A54,XBOOLE_0:def 4;
then
A69: i in dom(D2|Seg indx(D2,D1,1)) by RELAT_1:61;
DD2.i=(D2|indx(D2,D1,1)).i by A44,A45,FINSEQ_1:14
.=(D2|Seg indx(D2,D1,1)).i by FINSEQ_1:def 16;
then
A70: DD2.i=D2.i by A69,FUNCT_1:47;
A71: divset(D2,i)=[.lower_bound divset(D2,i), upper_bound
divset(D2,i).] by Th2
.=[. D2.(i-1),upper_bound divset(D2,i).] by A56,A61,Def3
.=[. D2.(i-1),D2.i .] by A56,A61,Def3;
divset(DD2,i)=[.lower_bound divset(DD2,i), upper_bound
divset(DD2,i).] by Th2
.=[. DD2.(i-1),upper_bound divset(DD2,i).] by A55,A61,Def3
.=[. D2.(i-1),D2.i .] by A55,A61,A68,A70,Def3;
hence thesis by A71;
end;
end;
hence thesis;
end;
then
A72: lower_volume(g,DD2).i =(lower_bound (rng (g|divset(D2,i))))*vol(
divset(D2,i)) by A55,Def6;
Seg indx(D2,D1,1) c= Seg(len D2) by A41,FINSEQ_1:5;
then i in Seg(len D2) by A43,A54;
then
A73: i in dom D2 by FINSEQ_1:def 3;
A74: i in dom DD2 by A54,FINSEQ_1:def 3;
A75: now
per cases;
suppose
A76: i=1;
then 1 in dom (D2|Seg indx(D2,D1,1)) by A49,A74,FINSEQ_1:def 16;
then 1 in dom D2 /\ Seg indx(D2,D1,1) by RELAT_1:61;
then
A77: 1 in dom D2 by XBOOLE_0:def 4;
then D2.1 <= D2.indx(D2,D1,1) by A34,A36,SEQ_4:137;
then
A78: D2.1 <= D1.1 by A1,A5,Def18;
lower_bound divset(D2,i)=lower_bound A by A76,A77,Def3;
then
A79: lower_bound divset(D2,i)=lower_bound divset(D1,1) by A5,Def3;
upper_bound divset(D2,i)=D2.1 by A76,A77,Def3;
then
A80: upper_bound divset(D2,i) <= upper_bound divset(D1,1)
by A5,A78,Def3;
lower_bound divset(D1,1) <= upper_bound divset(D1,1 ) by SEQ_4:11;
hence lower_bound divset(D2,i)in [.lower_bound divset(D1,1),
upper_bound divset(D1,1).] by A79,XXREAL_1:1;
lower_bound divset(D2,i) <= upper_bound divset(D2,i) by SEQ_4:11;
then upper_bound divset(D2,i)in{r: lower_bound divset(D1,1)<=r &
r<= upper_bound divset(D1,1)} by A79,A80;
hence upper_bound divset(D2,i)in [.lower_bound divset(D1,1),
upper_bound divset(D1,1).] by RCOMP_1:def 1;
end;
suppose
A81: i<>1;
then i is non trivial by A51,NAT_2:def 1;
then i >= 1+1 by NAT_2:29;
then
A82: 1 <= i-1 by XREAL_1:19;
A83: ex j being Nat st i = 1 + j by A51,NAT_1:10;
A84: rng D2 c= A by Def1;
A85: lower_bound divset(D2,i)=D2.(i-1) by A73,A81,Def3;
A86: lower_bound divset(D1,1)=lower_bound A by A5,Def3;
A87: i-1 <= indx(D2,D1,1)-0 by A43,A53,XREAL_1:13;
then i-1 <= len D2 by A37,XXREAL_0:2;
then i-1 in Seg(len D2) by A83,A82,FINSEQ_1:1;
then
A88: i-1 in dom D2 by FINSEQ_1:def 3;
then D2.(i-1) in rng D2 by FUNCT_1:def 3;
then
A89: lower_bound divset(D2,i) >= lower_bound divset(D1,1) by A85,A86,A84
,SEQ_4:def 2;
A90: upper_bound divset(D1,1)=D1.1 by A5,Def3;
D2.(i-1)<= D2.indx(D2,D1,1) by A34,A87,A88,SEQ_4:137;
then lower_bound divset(D2,i) <= upper_bound divset(D1,1) by A1,A5
,A85,A90,Def18;
then lower_bound divset(D2,i)in{r: lower_bound divset(D1,1)<=r &
r<= upper_bound divset(D1,1)} by A89;
hence lower_bound divset(D2,i)in [.lower_bound divset(D1,1),
upper_bound divset(D1,1).] by RCOMP_1:def 1;
A91: upper_bound divset(D2,i)=D2.i by A73,A81,Def3;
D2.i in rng D2 by A73,FUNCT_1:def 3;
then
A92: upper_bound divset(D2,i) >= lower_bound divset(D1,1) by A91,A86,A84
,SEQ_4:def 2;
D2.i <= D2.indx(D2,D1,1) by A43,A34,A53,A73,SEQ_4:137;
then upper_bound divset(D2,i) <= upper_bound divset(D1,1) by A1,A5
,A91,A90,Def18;
then upper_bound divset(D2,i)in{r: lower_bound divset(D1,1)<=r &
r<= upper_bound divset(D1,1)} by A92;
hence upper_bound divset(D2,i)in [.lower_bound divset(D1,1),
upper_bound divset(D1,1).] by RCOMP_1:def 1;
end;
end;
A93: divset(D1,1)=[.lower_bound divset(D1,1),upper_bound divset(D1,1)
.] by Th2;
A94: Seg indx(D2,D1,1) c= Seg(len D2) by A41,FINSEQ_1:5;
then i in Seg(len D2) by A43,A54;
then
A95: i in dom D2 by FINSEQ_1:def 3;
divset(D2,i)=[.lower_bound divset(D2,i),upper_bound divset(D2,i)
.] by Th2;
then
A96: divset(D2,i) c= divset(D1,1) by A93,A75,XXREAL_2:def 12;
A97: dom (lower_volume(f,D2)|Seg indx(D2,D1,1)) =dom lower_volume(f,
D2) /\ Seg indx(D2,D1,1) by RELAT_1:61
.=Seg(len lower_volume(f,D2)) /\ Seg indx(D2,D1,1) by FINSEQ_1:def 3
.=Seg(len D2) /\ Seg indx(D2,D1,1) by Def6
.=Seg indx(D2,D1,1) by A94,XBOOLE_1:28;
(lower_volume(f,D2)|indx(D2,D1,1)).i =(lower_volume(f,D2)|Seg
indx(D2,D1,1)).i by FINSEQ_1:def 16
.=lower_volume(f,D2).i by A43,A54,A97,FUNCT_1:47
.=(lower_bound (rng (f|divset(D2,i))))*vol(divset(D2,i)) by A95,Def6;
hence thesis by A72,A96,FUNCT_1:51;
end;
len lower_volume(g,DD1) = len (lower_volume(f,D1)|1) by A10;
then
A98: lower_volume(g,DD1) = lower_volume(f,D1)|1 by A18,FINSEQ_1:14;
A99: indx(D2,D1,1) <= len lower_volume(f,D2) by A41,Def6;
len lower_volume(g,DD2)= indx(D2,D1,1) by A43,Def6;
then
A100: len lower_volume(g,DD2)=len(lower_volume(f,D2)|indx(D2,D1, 1)) by A99,
FINSEQ_1:59;
dom g = A /\ divset(D1,1) by A4,FUNCT_2:def 1;
then dom g = divset(D1,1) by A5,Th6,XBOOLE_1:28;
then g is total by PARTFUN1:def 2;
then lower_sum(g,DD1) <= lower_sum(g,DD2) by A11,A28,Th29;
hence thesis by A98,A100,A50,FINSEQ_1:14;
end;
A101: for k being non zero Nat st P[k] holds P[k+1]
proof
let k be non zero Nat;
assume
A102: k in dom D1 implies Sum(lower_volume(f,D1)|k) <= Sum(
lower_volume(f,D2)|indx(D2,D1,k));
assume
A103: k+1 in dom D1;
then
A104: k+1 in Seg(len D1) by FINSEQ_1:def 3;
then
A105: 1 <= k+1 by FINSEQ_1:1;
A106: k+1 <= len D1 by A104,FINSEQ_1:1;
now
per cases;
suppose
1=k+1;
hence thesis by A3,A103;
end;
suppose
A107: 1<>k+1;
set IDK =indx(D2,D1,k);
set IDK1=indx(D2,D1,k+1);
set K1D2=lower_volume(f,D2)|indx(D2,D1,k+1);
set KD1 =lower_volume(f,D1)|k;
set K1D1=lower_volume(f,D1)|(k+1);
set n=k+1;
A108: k+1 <= len lower_volume(f,D1) by A106,Def6;
then
A109: len K1D1=k+1 by FINSEQ_1:59;
then consider p1,q1 being FinSequence of REAL such that
A110: len p1=k and
A111: len q1=1 and
A112: K1D1=p1^q1 by FINSEQ_2:23;
A113: k <= k+1 by NAT_1:11;
then
A114: k <= len D1 by A106,XXREAL_0:2;
then
A115: k <= len lower_volume(f,D1) by Def6;
then
A116: len p1 = len KD1 by A110,FINSEQ_1:59;
for i be Nat st 1 <= i & i <= len p1 holds p1.i=KD1.i
proof
let i be Nat;
assume that
A117: 1 <= i and
A118: i <= len p1;
A119: i in Seg(len p1) by A117,A118,FINSEQ_1:1;
then
A120: i in dom KD1 by A116,FINSEQ_1:def 3;
then
A121: i in dom (lower_volume(f,D1)|Seg k) by FINSEQ_1:def 16;
k <= k+1 by NAT_1:11;
then
A122: Seg k c= Seg(k+1) by FINSEQ_1:5;
A123: dom K1D1 =Seg(len K1D1) by FINSEQ_1:def 3
.= Seg(k+1) by A108,FINSEQ_1:59;
dom KD1=Seg(len KD1) by FINSEQ_1:def 3
.= Seg k by A115,FINSEQ_1:59;
then i in dom K1D1 by A120,A122,A123;
then
A124: i in dom (lower_volume(f,D1)|Seg(k+1)) by FINSEQ_1:def 16;
A125: K1D1.i = (lower_volume(f,D1)|Seg (k+1)).i by FINSEQ_1:def 16
.= lower_volume(f,D1).i by A124,FUNCT_1:47;
A126: KD1.i = (lower_volume(f,D1)|Seg k).i by FINSEQ_1:def 16
.= lower_volume(f,D1).i by A121,FUNCT_1:47;
i in dom p1 by A119,FINSEQ_1:def 3;
hence thesis by A112,A126,A125,FINSEQ_1:def 7;
end;
then
A127: p1=KD1 by A116,FINSEQ_1:14;
A128: indx(D2,D1,k+1) in dom D2 by A1,A103,Def18;
then
A129: indx(D2,D1,k+1) in Seg(len D2) by FINSEQ_1:def 3;
then
A130: 1 <= indx(D2,D1,k+1) by FINSEQ_1:1;
n is non trivial by A107,NAT_2:def 1;
then n >= 2 by NAT_2:29;
then k >= (1+1)-1 by XREAL_1:20;
then
A131: k in Seg(len D1) by A114,FINSEQ_1:1;
then
A132: k in dom D1 by FINSEQ_1:def 3;
then
A133: indx(D2,D1,k) in dom D2 by A1,Def18;
A134: indx(D2,D1,k) < indx(D2,D1,k+1)
proof
k < k+1 by NAT_1:13;
then
A135: D1.k < D1.(k+1) by A103,A132,SEQM_3:def 1;
assume indx(D2,D1,k) >= indx(D2,D1,k+1);
then
A136: D2.indx(D2,D1,k) >= D2.indx(D2,D1,k+1) by A133,A128,SEQ_4:137;
D1.k=D2.indx(D2,D1,k) by A1,A132,Def18;
hence contradiction by A1,A103,A136,A135,Def18;
end;
A137: indx(D2,D1,k+1) >= indx(D2,D1,k)
proof
assume indx(D2,D1,k+1) < indx(D2,D1,k); then
A138: D2.indx(D2,D1,k+1) < D2.indx(D2,D1,k) by A133,A128,SEQM_3:def 1;
D1.(k+1) = D2.indx(D2,D1,k+1) by A1,A103,Def18;
then D1.(k+1) < D1.k by A1,A132,A138,Def18;
hence contradiction by A103,A132,NAT_1:11,SEQ_4:137;
end;
then consider ID being Nat such that
A139: indx(D2,D1,k+1) = indx(D2,D1,k) + ID by NAT_1:10;
reconsider ID as Element of NAT by ORDINAL1:def 12;
A140: len lower_volume(f,D2) = len D2 by Def6;
then
A141: indx(D2,D1,k+1) <= len lower_volume(f,D2) by A129,FINSEQ_1:1;
then len K1D2=IDK + (IDK1-IDK) by FINSEQ_1:59;
then consider p2,q2 being FinSequence of REAL such that
A142: len p2=IDK and
A143: len q2=IDK1-IDK and
A144: K1D2=p2^q2 by A139,FINSEQ_2:23;
A145: indx(D2,D1,k+1) <= len D2 by A129,FINSEQ_1:1;
indx(D2,D1,k) in dom D2 by A1,A132,Def18;
then
A146: indx(D2,D1,k) in Seg(len D2) by FINSEQ_1:def 3;
then
A147: 1<=indx(D2,D1,k) by FINSEQ_1:1;
A148: Sum q1 <= Sum q2
proof
set MD2 = mid(D2,indx(D2,D1,k)+1,indx(D2,D1,k+1));
set MD1 = mid(D1,k+1,k+1);
set DD1 = divset(D1,k+1);
set g = f|DD1;
A149: 1 <= indx(D2,D1,k)+1 by NAT_1:11;
reconsider g as PartFunc of DD1,REAL by PARTFUN1:10;
(k+1)-1=k;
then
A150: lower_bound DD1=D1.k by A103,A107,Def3;
dom g = dom f /\ divset(D1,k+1) by RELAT_1:61;
then dom g = A /\ divset(D1,k+1) by FUNCT_2:def 1;
then dom g = divset(D1,k+1) by A103,Th6,XBOOLE_1:28;
then
A151: g is total by PARTFUN1:def 2;
A152: upper_bound divset(D1,k+1)=D1.(k+1) by A103,A107,Def3;
A153: D2.indx(D2,D1,k+1)=D1.(k+1) by A1,A103,Def18;
A154: indx(D2,D1,k)+1 <= indx(D2,D1,k+1) by A134,NAT_1:13;
then
A155: indx(D2,D1,k)+1 <= len D2 by A145,XXREAL_0:2;
then indx(D2,D1,k)+1 in Seg(len D2) by A149,FINSEQ_1:1;
then
A156: indx(D2,D1,k)+1 in dom D2 by FINSEQ_1:def 3;
then D2.(indx(D2,D1,k)+1)>=D2.indx(D2,D1,k)by A133,NAT_1:11
,SEQ_4:137;
then
D2.(indx(D2,D1,k)+1) >= lower_bound DD1 by A1,A132,A150,Def18;
then reconsider
MD2 as Division of DD1 by A128,A154,A156,A153,A152,Th35;
A157: indx(D2,D1,k+1)-'(indx(D2,D1,k)+1)+1 =indx(D2,D1,k+1)-(indx(
D2,D1,k)+1)+1 by A154,XREAL_1:233
.=indx(D2,D1,k+1)-indx(D2,D1,k);
A158: for n be Nat st 1 <= n & n <= len q2 holds q2.n=lower_volume
(g,MD2).n
proof
let n be Nat;
assume that
A159: 1 <= n and
A160: n <= len q2;
n in Seg(len q2) by A159,A160,FINSEQ_1:1;
then
A161: n in dom q2 by FINSEQ_1:def 3;
then
A162: indx(D2,D1,k)+n in dom K1D2 by A142,A144,FINSEQ_1:28;
then
A163: indx(D2,D1,k)+n in dom (lower_volume(f,D2) |Seg indx(D2,D1
,k +1)) by FINSEQ_1:def 16;
A164: len mid(D2,indx(D2,D1,k)+1,indx(D2,D1,k+1)) =ID by A130,A145,A139
,A154,A155,A149,A157,FINSEQ_6:118;
A165: dom K1D2 = Seg(len K1D2) by FINSEQ_1:def 3
.= Seg indx(D2,D1,k+1) by A141,FINSEQ_1:59;
then indx(D2,D1,k)+n <= indx(D2,D1,k+1) by A162,FINSEQ_1:1;
then
A166: n <= indx(D2,D1,k+1)-indx(D2,D1,k) by XREAL_1:19;
then n in Seg(len mid(D2,indx(D2,D1,k)+1,indx( D2,D1,k+1))) by
A139,A159,A164,FINSEQ_1:1;
then
A167: n in dom MD2 by FINSEQ_1:def 3;
A168: Seg indx(D2,D1,k+1) c= Seg(len D2) by A145,FINSEQ_1:5;
then indx(D2,D1,k)+n in Seg(len D2) by A165,A162;
then
A169: indx(D2,D1,k)+n in dom D2 by FINSEQ_1:def 3;
A170: q2.n=K1D2.(indx(D2,D1,k)+n) by A142,A144,A161,FINSEQ_1:def 7
.=(lower_volume(f,D2)|Seg indx(D2,D1,k+1)).(indx(D2,D1,k)+n)
by FINSEQ_1:def 16
.=lower_volume(f,D2).(indx(D2,D1,k)+n) by A163,FUNCT_1:47
.=(lower_bound(rng(f|divset(D2,indx(D2,D1,k)+n))))* vol(
divset(D2,indx(D2,D1,k)+n)) by A169,Def6;
A171: 1 <=indx(D2,D1,k)+n by A165,A162,FINSEQ_1:1;
A172: divset(MD2,n)=divset(D2,indx(D2,D1,k)+n) & divset(D2,indx(
D2,D1,k)+n) c= divset(D1,k+1)
proof
now
per cases;
suppose
A173: n=1;
then
A174: 1<=indx(D2,D1,k)+1 by A165,A162,FINSEQ_1:1;
A175: indx(D2,D1,k)+1<=len D2 by A165,A162,A168,A173,FINSEQ_1:1;
A176: upper_bound divset(MD2,1)= mid(D2,indx(D2,D1,k)+1,
indx(D2,D1,k+1)).1 by A167,A173,Def3
.= D2.(1+indx(D2,D1,k)) by A130,A145,A174,A175,
FINSEQ_6:118;
A177: indx(D2,D1,k)+1 <> 1 by A147,NAT_1:13;
A178: (k+1)-1=k;
A179: lower_bound divset(MD2,1)=lower_bound divset(D1,k+1)
by A167,A173,Def3
.= D1.k by A103,A107,A178,Def3;
A180: divset(D2,indx(D2,D1,k)+n)= [.lower_bound divset(D2,
indx(D2,D1,k)+1), upper_bound divset(D2,indx(D2,D1,k)+1).] by A173,Th2
.=[.D2.(indx(D2,D1,k)+1-1),upper_bound divset(D2,indx(
D2,D1,k)+1).] by A156,A177,Def3
.=[.D2.indx(D2,D1,k),D2.(indx(D2,D1,k)+1).] by A156,A177
,Def3
.=[.D1.k,D2.(indx(D2,D1,k)+1).] by A1,A132,Def18;
hence
divset(MD2,n)=divset(D2,indx(D2,D1,k)+n) by A173,A179,A176
,Th2;
divset(MD2,n)=[.D1.k,D2.(indx( D2,D1,k)+1).] by A173,A179
,A176,Th2;
hence thesis by A167,A180,Th6;
end;
suppose
A181: n<>1;
A182: indx(D2,D1,k)+n <> 1
proof
assume indx(D2,D1,k)+n = 1;
then indx(D2,D1,k)=1-n;
then n+1 <= 1 by A147,XREAL_1:19;
then n <= 1-1 by XREAL_1:19;
hence contradiction by A159,NAT_1:3;
end;
A183: divset(D2,indx(D2,D1,k)+n) =[.lower_bound divset(D2,
indx(D2,D1,k)+n), upper_bound divset(D2,indx(D2,D1,k)+n).] by Th2
.=[.D2.(indx(D2,D1,k)+n-1),upper_bound divset(D2,indx(
D2,D1,k)+n).] by A169,A182,Def3
.=[. D2.(indx(D2,D1,k)+n-1),D2.(indx(D2,D1,k)+n) .] by
A169,A182,Def3;
n<=n+1 by NAT_1:12;
then n-1 <= n by XREAL_1:20;
then
A184: n-1<=len MD2 by A139,A166,A164,XXREAL_0:2;
A185: indx(D2,D1,k)+1 <= indx(D2,D1,k+1) by A134,NAT_1:13;
n is non trivial by A159,A181,NAT_2:def 1;
then n >= 1+1 by NAT_2:29;
then
A186: 1<=n-1 by XREAL_1:19;
consider n1 being Nat such that
A187: n=1+n1 by A159,NAT_1:10;
reconsider n1 as Element of NAT by ORDINAL1:def 12;
A188: n1+(indx(D2,D1,k)+1)-'1=indx(D2,D1,k)+n-1 by A171,A187,
XREAL_1:233;
A189: n+(indx(D2,D1,k)+1)-'1=n+indx(D2,D1,k)+1-1 by NAT_1:11
,XREAL_1:233
.=indx(D2,D1,k)+n;
A190: lower_bound divset(MD2,n)=MD2.(n-1) by A167,A181,Def3
.=D2.(indx(D2,D1,k)+n-1) by A130,A145,A155,A149,A185,A187
,A188,A186,A184,FINSEQ_6:118;
A191: upper_bound divset(MD2,n)=MD2.n by A167,A181,Def3
.=D2.(indx(D2,D1,k)+n) by A130,A145,A139,A155,A149,A159
,A166,A164,A185,A189,FINSEQ_6:118;
hence divset(MD2,n)=divset(D2,indx(D2,D1,k)+n) by A190,A183
,Th2;
divset(MD2,n)= [. D2.(indx(D2,D1,k)+n-1),D2.(indx(D2
,D1,k)+n) .] by A190,A191,Th2;
hence thesis by A167,A183,Th6;
end;
end;
hence thesis;
end;
then g|divset(MD2,n) =f|divset(D2,indx(D2,D1,k)+n) by FUNCT_1:51;
hence thesis by A167,A170,A172,Def6;
end;
(k+1)-1=k;
then
A192: lower_bound DD1=D1.k by A103,A107,Def3;
D1.(k+1) = upper_bound DD1 by A103,A107,Def3;
then reconsider MD1 as Division of DD1 by A103,A113,A132,A192,Th35,
SEQ_4:137;
A193: g|divset(D1,k+1) is bounded_below
proof
consider a be Real such that
A194: for x being object st x in A /\ dom f holds a <= f.x by A2,
RFUNCT_1:71;
for x being object st x in divset(D1,k+1) /\ dom g holds a <=
g.x
proof
let x be object;
A195: dom g c= dom f by RELAT_1:60;
assume x in divset(D1,k+1) /\ dom g; then
A196: x in dom g by XBOOLE_0:def 4;
A197: A /\ dom f = dom f by XBOOLE_1:28;
then reconsider x as Element of A by A196,A195,XBOOLE_0:def 4;
a <= f.x by A194,A196,A197,A195;
hence thesis by A196,FUNCT_1:47;
end;
hence thesis by RFUNCT_1:71;
end;
len MD1 = (k+1) -'(k+1) + 1 by A105,A106,FINSEQ_6:118;
then
A198: len MD1 = (k+1) - (k+1) + 1 by XREAL_1:233;
A199: for n be Nat st 1 <= n & n <= len q1 holds q1.n=lower_volume
(g,MD1).n
proof
k+1 in Seg(len K1D1) by A109,FINSEQ_1:4;
then k+1 in dom K1D1 by FINSEQ_1:def 3;
then
A200: k+1 in dom (lower_volume(f,D1)|Seg(k+1)) by FINSEQ_1:def 16;
A201: K1D1.(k+1)=(lower_volume(f,D1)|Seg(k+1)).(k+1) by FINSEQ_1:def 16
.=lower_volume(f,D1).(k+1) by A200,FUNCT_1:47;
A202: MD1.1 =D1.(k+1) by A105,A106,FINSEQ_6:118;
1 in Seg 1 by FINSEQ_1:3;
then
A203: 1 in dom MD1 by A198,FINSEQ_1:def 3;
then
A204: upper_bound divset( MD1,1) = MD1.1 by Def3;
let n be Nat;
assume that
A205: 1 <= n and
A206: n <= len q1;
A207: n = 1 by A111,A205,A206,XXREAL_0:1;
lower_bound divset(MD1,1) = lower_bound DD1 by A203,Def3;
then
A208: divset(MD1,1)=[.lower_bound DD1,D1.(k+1).] by A204,A202,Th2;
(k+1)-1=k;
then
A209: lower_bound DD1 = D1.k by A103,A107,Def3;
upper_bound DD1 = D1.(k+1) by A103,A107,Def3;
then
A210: divset(D1,k+1)=[. D1.k,D1.(k+1).] by A209,Th2;
A211: n in Seg(len q1) by A205,A206,FINSEQ_1:1;
then n in dom MD1 by A111,A198,FINSEQ_1:def 3;
then
A212: lower_volume(g,MD1).n =(lower_bound(rng(g|divset(D1,k+1)))
)*vol(divset(D1,k+1)) by A207,A208,A209,A210,Def6;
n in dom q1 by A211,FINSEQ_1:def 3;
then q1.n = lower_volume(f,D1).(k+1) by A110,A112,A207,A201,
FINSEQ_1:def 7
.=(lower_bound(rng(f|divset(D1,k+1))))*vol(divset(D1,k+1))
by A103,Def6;
hence thesis by A212;
end;
len q1 = len(lower_volume(g,MD1)) by A111,A198,Def6;
then
A213: q1=lower_volume(g,MD1) by A199,FINSEQ_1:14;
len MD1 = (k+1) -'(k+1) + 1 by A105,A106,FINSEQ_6:118;
then len MD1 = (k+1) - (k+1) + 1 by XREAL_1:233;
then
A214: lower_sum(g,MD1) <= lower_sum(g,MD2) by A193,A151,Th29;
len(lower_volume(g,MD2))= len mid(D2,indx(D2,D1,k)+1,indx(D2
,D1,k+1)) by Def6
.=indx(D2,D1,k+1)-indx(D2,D1,k) by A130,A145,A154,A155,A149,A157,
FINSEQ_6:118;
hence thesis by A143,A213,A158,A214,FINSEQ_1:14;
end;
set KD2 =lower_volume(f,D2)|indx(D2,D1,k);
A215: Sum K1D2=Sum p2+Sum q2 by A144,RVSUM_1:75;
A216: indx(D2,D1,k)<=len lower_volume(f, D2) by A140,A146,FINSEQ_1:1;
then
A217: len p2 = len KD2 by A142,FINSEQ_1:59;
for i be Nat st 1 <= i & i <= len p2 holds p2.i=KD2.i
proof
let i be Nat;
assume that
A218: 1 <= i and
A219: i <= len p2;
A220: i in Seg(len p2) by A218,A219,FINSEQ_1:1;
then
A221: i in dom KD2 by A217,FINSEQ_1:def 3;
then
A222: i in dom (lower_volume(f,D2)|Seg indx(D2,D1,k)) by FINSEQ_1:def 16;
A223: dom K1D2 = Seg(len K1D2) by FINSEQ_1:def 3
.= Seg indx(D2,D1,k+1) by A141,FINSEQ_1:59;
A224: Seg indx(D2,D1,k) c= Seg indx(D2,D1,k+1) by A137,FINSEQ_1:5;
dom KD2 =Seg(len KD2) by FINSEQ_1:def 3
.= Seg indx(D2,D1,k) by A216,FINSEQ_1:59;
then i in dom K1D2 by A221,A224,A223;
then
A225: i in dom (lower_volume(f,D2)|Seg indx(D2,D1,k+ 1)) by
FINSEQ_1:def 16;
A226: K1D2.i=(lower_volume(f,D2)|Seg indx(D2,D1,k+1)).i by
FINSEQ_1:def 16
.=lower_volume(f,D2).i by A225,FUNCT_1:47;
A227: KD2.i=(lower_volume(f,D2)|Seg indx(D2,D1,k)).i by FINSEQ_1:def 16
.= lower_volume(f,D2).i by A222,FUNCT_1:47;
i in dom p2 by A220,FINSEQ_1:def 3;
hence thesis by A144,A227,A226,FINSEQ_1:def 7;
end;
then
A228: p2=KD2 by A217,FINSEQ_1:14;
Sum K1D1=Sum p1+Sum q1 by A112,RVSUM_1:75;
then Sum q1 = Sum K1D1 - Sum p1;
then Sum K1D1 <= Sum q2 + Sum p1 by A148,XREAL_1:20;
then Sum K1D1 - Sum q2 <= Sum p1 by XREAL_1:20;
then Sum K1D1 - Sum q2 <= Sum p2 by A102,A131,A127,A228,
FINSEQ_1:def 3,XXREAL_0:2;
hence thesis by A215,XREAL_1:20;
end;
end;
hence thesis;
end;
thus for n being non zero Nat holds P[n] from NAT_1:sch 10(A3, A101);
end;
hence thesis;
end;
theorem Th38:
D1 <= D2 & i in dom D1 & f|A is bounded_above implies (PartSums(
upper_volume(f,D1))).i >= (PartSums(upper_volume(f,D2))).indx(D2,D1,i)
proof
assume that
A1: D1 <= D2 and
A2: i in dom D1 and
A3: f|A is bounded_above;
A4: len upper_volume(f,D2)=len D2 by Def5;
i in Seg(len D1) by A2,FINSEQ_1:def 3;
then i in Seg(len upper_volume(f,D1)) by Def5;
then i in dom upper_volume(f,D1) by FINSEQ_1:def 3;
then
A5: (PartSums(upper_volume(f,D1))).i=Sum(upper_volume(f,D1)|i) by Def19;
indx(D2,D1,i) in dom D2 by A1,A2,Def18;
then indx(D2,D1,i) in Seg(len upper_volume(f,D2)) by A4,FINSEQ_1:def 3;
then
A6: indx(D2,D1,i) in dom upper_volume(f,D2) by FINSEQ_1:def 3;
i in Seg(len D1) by A2,FINSEQ_1:def 3;
then i is non zero Element of NAT by FINSEQ_1:1;
then
(PartSums(upper_volume(f,D1))).i >= Sum(upper_volume(f,D2)|indx(D2,D1,i
)) by A1,A2,A3,A5,Th36;
hence thesis by A6,Def19;
end;
theorem Th39:
D1 <= D2 & i in dom D1 & f|A is bounded_below implies (PartSums(
lower_volume(f,D1))).i <= (PartSums(lower_volume(f,D2))).indx(D2,D1,i)
proof
assume that
A1: D1 <= D2 and
A2: i in dom D1 and
A3: f|A is bounded_below;
A4: len lower_volume(f,D2)=len D2 by Def6;
i in Seg(len D1) by A2,FINSEQ_1:def 3;
then i in Seg(len lower_volume(f,D1)) by Def6;
then i in dom lower_volume(f,D1) by FINSEQ_1:def 3;
then
A5: (PartSums(lower_volume(f,D1))).i=Sum(lower_volume(f,D1)|i) by Def19;
indx(D2,D1,i) in dom D2 by A1,A2,Def18;
then indx(D2,D1,i) in Seg(len lower_volume(f,D2)) by A4,FINSEQ_1:def 3;
then
A6: indx(D2,D1,i) in dom lower_volume(f,D2) by FINSEQ_1:def 3;
i in Seg(len D1) by A2,FINSEQ_1:def 3;
then i is non zero Element of NAT by FINSEQ_1:1;
then
(PartSums(lower_volume(f,D1))).i <= Sum(lower_volume(f,D2)|indx(D2,D1,i
)) by A1,A2,A3,A5,Th37;
hence thesis by A6,Def19;
end;
theorem Th40:
(PartSums(upper_volume(f,D))).(len D) = upper_sum(f,D)
proof
len upper_volume(f,D) = len D by Def5;
then len D in Seg(len upper_volume(f,D)) by FINSEQ_1:3;
then len D in dom upper_volume(f,D) by FINSEQ_1:def 3;
then
A1: (PartSums(upper_volume(f,D))).(len D) = Sum(upper_volume(f,D)|(len D ))
by Def19;
dom upper_volume(f,D)=Seg len upper_volume(f,D) by FINSEQ_1:def 3;
then dom upper_volume(f,D)=Seg len D by Def5;
then upper_volume(f,D)|(Seg len D) = upper_volume(f,D);
hence thesis by A1,FINSEQ_1:def 16;
end;
theorem Th41:
(PartSums(lower_volume(f,D))).(len D) = lower_sum(f,D)
proof
len lower_volume(f,D) = len D by Def6;
then len D in Seg(len lower_volume(f,D)) by FINSEQ_1:3;
then len D in dom lower_volume(f,D) by FINSEQ_1:def 3;
then
A1: (PartSums(lower_volume(f,D))).(len D) = Sum(lower_volume(f,D)|(len D ))
by Def19;
dom lower_volume(f,D)=Seg len lower_volume(f,D) by FINSEQ_1:def 3;
then dom lower_volume(f,D)=Seg len D by Def6;
then lower_volume(f,D)|(Seg len D) = lower_volume(f,D);
hence thesis by A1,FINSEQ_1:def 16;
end;
theorem Th42:
D1 <= D2 implies indx(D2,D1,len D1) = len D2
proof
len D1 in Seg(len D1) by FINSEQ_1:3;
then
A1: len D1 in dom D1 by FINSEQ_1:def 3;
assume
A2: D1 <= D2;
then D1.(len D1)=D2.indx(D2,D1,len D1) by A1,Def18;
then
A3: D2.indx(D2,D1,len D1)=upper_bound A by Def1;
len D2 in Seg(len D2) by FINSEQ_1:3;
then
A4: len D2 in dom D2 by FINSEQ_1:def 3;
assume
A5: indx(D2,D1,len D1) <> len D2;
A6: indx(D2,D1,len D1) in dom D2 by A2,A1,Def18;
then indx(D2,D1,len D1) in Seg(len D2) by FINSEQ_1:def 3;
then indx(D2,D1,len D1) <= len D2 by FINSEQ_1:1;
then indx(D2,D1,len D1) < len D2 by A5,XXREAL_0:1;
then D2.indx(D2,D1,len D1) < D2.(len D2) by A4,A6,SEQM_3:def 1;
hence contradiction by A3,Def1;
end;
theorem Th43:
D1 <= D2 & f|A is bounded_above implies upper_sum(f,D2) <=
upper_sum(f,D1)
proof
assume that
A1: D1 <= D2 and
A2: f|A is bounded_above;
len D1 in Seg(len D1) by FINSEQ_1:3;
then len D1 in dom D1 by FINSEQ_1:def 3;
then
(PartSums(upper_volume(f,D1))).(len D1) >= (PartSums(upper_volume(f,D2))
).indx(D2,D1,len D1) by A1,A2,Th38;
then
upper_sum(f,D1) >= (PartSums(upper_volume(f,D2))).indx(D2,D1,len D1) by Th40;
then upper_sum(f,D1) >= (PartSums(upper_volume(f,D2))).(len D2) by A1,Th42;
hence thesis by Th40;
end;
theorem Th44:
D1 <= D2 & f|A is bounded_below implies lower_sum(f,D2) >=
lower_sum(f,D1)
proof
assume that
A1: D1 <= D2 and
A2: f|A is bounded_below;
len D1 in Seg(len D1) by FINSEQ_1:3;
then len D1 in dom D1 by FINSEQ_1:def 3;
then
(PartSums(lower_volume(f,D1))).(len D1) <= (PartSums(lower_volume(f,D2))
).indx(D2,D1,len D1) by A1,A2,Th39;
then
lower_sum(f,D1) <= (PartSums(lower_volume(f,D2))).indx(D2,D1,len D1) by Th41;
then lower_sum(f,D1) <= (PartSums(lower_volume(f,D2))).(len D2) by A1,Th42;
hence thesis by Th41;
end;
theorem Th45:
ex D be Division of A st D1 <= D & D2 <= D
proof
consider D3 being FinSequence of REAL such that
A1: rng D3 = rng(D1^D2) and
A2: len D3 = card rng(D1^D2) and
A3: D3 is increasing by SEQ_4:140;
reconsider D3 as non empty increasing FinSequence of REAL by A1,A3;
A4: rng D2 c= A by Def1;
rng D1 c= A by Def1;
then rng D1 \/ rng D2 c= A by A4,XBOOLE_1:8;
then
A5: rng D3 c= A by A1,FINSEQ_1:31;
D3.(len D3) = upper_bound A
proof
assume
A6: D3.(len D3) <> upper_bound A;
now
per cases by A6,XXREAL_0:1;
suppose
A7: D3.(len D3) > upper_bound A;
len D3 in Seg(len D3) by FINSEQ_1:3;
then len D3 in dom D3 by FINSEQ_1:def 3;
then D3.(len D3) in rng D3 by FUNCT_1:def 3;
then D3.(len D3) in A by A5;
then D3.(len D3) in [.lower_bound A,upper_bound A.] by Th2;
then
D3.(len D3) in {r:lower_bound A <= r & r <= upper_bound A} by RCOMP_1:def 1;
then ex a st a=D3.(len D3) & lower_bound A <= a & a <= upper_bound
A;
hence contradiction by A7;
end;
suppose
A8: D3.(len D3) < upper_bound A;
A9: rng D1 c= rng (D1^D2) by FINSEQ_1:29;
len D1 in Seg(len D1) by FINSEQ_1:3;
then
A10: len D1 in dom D1 by FINSEQ_1:def 3;
len D3 in Seg(len D3) by FINSEQ_1:3;
then
A11: len D3 in dom D3 by FINSEQ_1:def 3;
D1.(len D1) = upper_bound A by Def1;
then upper_bound A in rng D1 by A10,FUNCT_1:def 3;
then consider k being Nat such that
A12: k in dom D3 and
A13: D3.k = upper_bound A by A1,A9,FINSEQ_2:10;
k in Seg(len D3) by A12,FINSEQ_1:def 3;
then k <= len D3 by FINSEQ_1:1;
hence contradiction by A8,A11,A12,A13,SEQ_4:137;
end;
end;
hence thesis;
end;
then reconsider D3 as Division of A by A5,Def1;
len D2 = card(rng D2) by FINSEQ_4:62;
then
A14: len D2 <= len D3 by A2,FINSEQ_1:30,NAT_1:43;
take D3;
A15: rng D1 c= rng (D1^D2) by FINSEQ_1:29;
A16: rng D2 c= rng (D1^D2) by FINSEQ_1:30;
len D1 = card(rng D1) by FINSEQ_4:62;
then len D1 <= len D3 by A2,FINSEQ_1:29,NAT_1:43;
hence thesis by A1,A15,A16,A14;
end;
theorem Th46:
f|A is bounded implies lower_sum(f,D1) <= upper_sum(f,D2)
proof
consider D such that
A1: D1 <= D and
A2: D2 <= D by Th45;
assume
A3: f|A is bounded;
then
A4: lower_sum(f,D) <= upper_sum(f,D) by Th26;
upper_sum(f,D) <= upper_sum(f,D2) by A3,A2,Th43;
then
A5: lower_sum(f,D) <= upper_sum(f,D2) by A4,XXREAL_0:2;
lower_sum(f,D1) <= lower_sum(f,D) by A3,A1,Th44;
hence thesis by A5,XXREAL_0:2;
end;
begin :: Additivity of integral
theorem Th47:
f|A is bounded implies upper_integral(f) >= lower_integral(f)
proof
assume
A1: f|A is bounded;
A2: for b be Real st b in rng upper_sum_set(f) holds lower_integral(f
) <= b
proof
let b be Real;
assume b in rng upper_sum_set(f);
then consider D1 being Element of divs A such that
D1 in dom upper_sum_set(f) and
A3: b=(upper_sum_set(f)).D1 by PARTFUN1:3;
reconsider D1 as Division of A by Def2;
A4: for a being Real st a in rng lower_sum_set(f) holds a <=
upper_sum(f,D1)
proof
let a be Real;
assume a in rng lower_sum_set(f);
then consider D2 being Element of divs A such that
D2 in dom lower_sum_set(f) and
A5: a=(lower_sum_set(f)).D2 by PARTFUN1:3;
reconsider D2 as Division of A by Def2;
a=lower_sum(f,D2) by A5,Def10;
hence thesis by A1,Th46;
end;
b=upper_sum(f,D1) by A3,Def9;
hence thesis by A4,SEQ_4:45;
end;
thus thesis by A2,SEQ_4:43;
end;
theorem Th48:
for X,Y be Subset of REAL holds (--X)++(--Y)=--(X++Y)
proof
let X,Y be Subset of REAL;
for z be object st z in --(X++Y) holds z in (--X)++(--Y)
proof
let z be object;
assume A1: z in --(X++Y);
reconsider XY = X++Y as Subset of REAL by MEMBERED:3;
z in -- XY by A1;
then consider x be Real such that
A2: x in XY and
A3: z=-x by MEASURE6:72;
consider a,b be Real such that
A4: a in X and
A5: b in Y and
A6: x=a+b by A2,MEASURE6:21;
A7: -a in --X by A4,MEMBER_1:11;
A8: -b in --Y by A5,MEMBER_1:11;
z = -a+-b by A3,A6;
hence thesis by A7,A8,MEMBER_1:46;
end; then
A9: --(X++Y) c= (--X)++(--Y);
for z be object st z in (--X)++(--Y) holds z in --(X++Y)
proof
let z be object;
assume A10: z in --(X)++(--Y);
consider x,y being Real such that
A11: x in --X and
A12: y in --Y and
A13: z=x+y by A10,MEASURE6:21;
consider b be Real such that
A14: b in Y and
A15: y=-b by A12,MEASURE6:72;
reconsider X as Subset of REAL;
consider a be Real such that
A16: a in X and
A17: x=-a by A11,MEASURE6:72;
A18: a+b in X++Y by A16,A14,MEMBER_1:46;
z=-(a+b) by A13,A17,A15;
hence thesis by A18,MEMBER_1:11;
end;
then (--X)++(--Y) c= --(X++Y);
hence thesis by A9;
end;
theorem Th49:
for X,Y being Subset of REAL st X is bounded_above & Y is
bounded_above holds X++Y is bounded_above
proof
let X,Y be Subset of REAL;
assume that
A1: X is bounded_above and
A2: Y is bounded_above;
A3: (--Y) is bounded_below by A2,MEASURE6:41;
(--X) is bounded_below by A1,MEASURE6:41;
then
A4: (--X)++(--Y) is bounded_below by A3,SEQ_4:124;
reconsider XY = X++Y as Subset of REAL by MEMBERED:3;
--XY is bounded_below by Th48,A4;
hence thesis by MEASURE6:41;
end;
theorem Th50:
for X,Y be non empty Subset of REAL st
X is bounded_above & Y is bounded_above holds
upper_bound(X++Y) = upper_bound X + upper_bound Y
proof
let X,Y be non empty Subset of REAL;
assume that
A1: X is bounded_above and
A2: Y is bounded_above;
A3: (--Y) is bounded_below by A2,MEASURE6:41;
A4: (--X) is bounded_below by A1,MEASURE6:41;
then lower_bound(--X++--Y) = lower_bound(--X)+lower_bound(--Y)
by A3,SEQ_4:125; then
A5: lower_bound(--X++--Y) = -upper_bound(----X)+lower_bound(--Y)
by A4,MEASURE6:43
.= -upper_bound X + -upper_bound(----Y) by A3,MEASURE6:43
.= -(upper_bound X + upper_bound Y);
A6: (--X)++(--Y)=--(X++Y) by Th48;
then A7: --(X++Y) is bounded_below by A4,A3,SEQ_4:124;
reconsider XY = X++Y as Subset of REAL by MEMBERED:3;
- upper_bound(-- --XY)= - (upper_bound X + upper_bound Y)
by A6,A5,A7,MEASURE6:43; then
upper_bound XY = upper_bound X + upper_bound Y;
hence thesis;
end;
theorem Th51:
i in dom D & f|A is bounded_above & g|A is bounded_above implies
upper_volume(f+g,D).i <= upper_volume(f,D).i + upper_volume(g,D).i
proof
assume
A1: i in dom D;
dom(f+g) = A /\ A by FUNCT_2:def 1;
then dom((f+g)|divset(D,i)) = divset(D,i) by A1,Th6,RELAT_1:62;
then
A2: rng((f+g)|divset(D,i)) is non empty by RELAT_1:42;
(f+g)|divset(D,i)=f|divset(D,i) + g|divset(D,i) by RFUNCT_1:44;
then
A3: rng((f+g)|divset(D,i))c=rng(f|divset(D,i))++rng(g|divset(D,i)) by Th8;
assume f|A is bounded_above;
then rng f is bounded_above by Th11; then
A4: rng(f|divset(D,i)) is bounded_above by RELAT_1:70,XXREAL_2:43;
dom g = A by FUNCT_2:def 1;
then dom (g|divset(D,i)) = divset(D,i) by A1,Th6,RELAT_1:62;
then
A5: rng(g|divset(D,i)) is non empty by RELAT_1:42;
A6: 0 <= vol(divset(D,i)) by SEQ_4:11,XREAL_1:48;
assume g|A is bounded_above;
then rng g is bounded_above by Th11;
then
A7: rng(g|divset(D,i)) is bounded_above by RELAT_1:70,XXREAL_2:43;
then
A8: rng(f|divset(D,i))++rng(g|divset(D,i)) is bounded_above by A4,Th49;
dom f = A by FUNCT_2:def 1;
then dom (f|divset(D,i)) = divset(D,i) by A1,Th6,RELAT_1:62;
then rng(f|divset(D,i)) is non empty by RELAT_1:42;
then upper_bound(rng(f|divset(D,i))++rng(g|divset(D,i))) =
upper_bound rng(f|divset(D,i)) + upper_bound rng(g|divset(D,i))
by A4,A7,A5,Th50;
then
upper_bound rng((f+g)|divset(D,i))*vol(divset(D,i)) <= (upper_bound rng
(f|divset(D,i)) + upper_bound rng(g|divset(D,i)))*vol(divset(D,i)) by A8,A2
,A6,A3,SEQ_4:48,XREAL_1:64;
then
upper_volume(f+g,D).i <= upper_bound rng(f|divset(D,i))*vol(divset(D,i)
)+ upper_bound rng(g|divset(D,i))*vol(divset(D,i)) by A1,Def5;
then
upper_volume(f+g,D).i <= upper_volume(f,D).i+ upper_bound rng(g|divset(
D,i))*vol(divset(D,i)) by A1,Def5;
hence thesis by A1,Def5;
end;
theorem Th52:
i in dom D & f|A is bounded_below & g|A is bounded_below implies
lower_volume(f,D).i + lower_volume(g,D).i <= lower_volume(f+g,D).i
proof
assume that
A1: i in dom D and
A2: f|A is bounded_below and
A3: g|A is bounded_below;
A4: 0 <= vol(divset(D,i)) by SEQ_4:11,XREAL_1:48;
dom(f+g) = A /\ A by FUNCT_2:def 1;
then dom((f+g)|divset(D,i)) = divset(D,i) by A1,Th6,RELAT_1:62;
then
A5: rng((f+g)|divset(D,i)) is non empty by RELAT_1:42;
rng g is bounded_below by A3,Th9;
then
A6: rng(g|divset(D,i)) is bounded_below by RELAT_1:70,XXREAL_2:44;
dom g = A by FUNCT_2:def 1;
then dom (g|divset(D,i)) = divset(D,i) by A1,Th6,RELAT_1:62;
then
A7: rng(g|divset(D,i)) is non empty by RELAT_1:42;
(f+g)|divset(D,i)=f|divset(D,i) + g|divset(D,i) by RFUNCT_1:44;
then
A8: rng((f+g)|divset(D,i))c=rng(f|divset(D,i))++rng(g|divset(D,i)) by Th8;
rng f is bounded_below by A2,Th9;
then
A9: rng(f|divset(D,i)) is bounded_below by RELAT_1:70,XXREAL_2:44;
then
A10: rng (f|divset(D,i))++rng(g|divset(D,i)) is bounded_below by A6,SEQ_4:124;
dom f = A by FUNCT_2:def 1;
then dom (f|divset(D,i)) = divset(D,i) by A1,Th6,RELAT_1:62;
then rng(f|divset(D,i)) is non empty by RELAT_1:42;
then lower_bound(rng(f|divset(D,i))++rng(g|divset(D,i))) =
lower_bound rng(f|divset(D,i)) + lower_bound rng(g|divset(D,i))
by A9,A6,A7,SEQ_4:125; then
lower_bound rng((f+g)|divset(D,i))*vol(divset(D,i)) >= (lower_bound rng
(f|divset(D,i)) + lower_bound rng(g|divset(D,i)))*vol(divset(D,i)) by A10,A5
,A4,A8,SEQ_4:47,XREAL_1:64;
then
lower_volume(f+g,D).i >= lower_bound rng(f|divset(D,i))*vol(divset(D,i)
)+ lower_bound rng(g|divset(D,i))*vol(divset(D,i)) by A1,Def6;
then
lower_volume(f+g,D).i >= lower_volume(f,D).i+ lower_bound rng(g|divset(
D,i))*vol(divset(D,i)) by A1,Def6;
hence thesis by A1,Def6;
end;
theorem Th53:
f|A is bounded_above & g|A is bounded_above implies upper_sum(f+
g,D) <= upper_sum(f,D) + upper_sum(g,D)
proof
assume that
A1: f|A is bounded_above and
A2: g|A is bounded_above;
set H=upper_volume(f+g,D);
set G=upper_volume(g,D);
set F=upper_volume(f,D);
len G = len D by Def5;
then
A3: G is Element of (len D)-tuples_on REAL by FINSEQ_2:92;
len F = len D by Def5;
then
A4: F is Element of (len D)-tuples_on REAL by FINSEQ_2:92;
A5: for j be Nat st j in Seg(len D) holds H.j <= (F+G).j
proof
let j be Nat;
assume j in Seg(len D);
then j in dom D by FINSEQ_1:def 3;
then
upper_volume(f+g,D).j <= upper_volume(f,D).j + upper_volume(g,D).j by A1,A2
,Th51;
hence thesis by A4,A3,RVSUM_1:11;
end;
len H = len D by Def5;
then
A6: H is Element of (len D)-tuples_on REAL by FINSEQ_2:92;
F+G is Element of (len D)-tuples_on REAL by A4,A3,FINSEQ_2:120;
then Sum H <= Sum(F+G) by A6,A5,RVSUM_1:82;
hence thesis by A4,A3,RVSUM_1:89;
end;
theorem Th54:
f|A is bounded_below & g|A is bounded_below implies lower_sum(f,
D) + lower_sum(g,D) <= lower_sum(f+g,D)
proof
assume that
A1: f|A is bounded_below and
A2: g|A is bounded_below;
set H=lower_volume(f+g,D);
set G=lower_volume(g,D);
set F=lower_volume(f,D);
len G = len D by Def6;
then
A3: G is Element of (len D)-tuples_on REAL by FINSEQ_2:92;
len F = len D by Def6;
then
A4: F is Element of (len D)-tuples_on REAL by FINSEQ_2:92;
A5: for j be Nat st j in Seg(len D) holds (F+G).j <= H.j
proof
let j be Nat;
assume j in Seg(len D);
then j in dom D by FINSEQ_1:def 3;
then
lower_volume(f,D).j + lower_volume(g,D).j <= lower_volume(f+g,D).j by A1,A2
,Th52;
hence thesis by A4,A3,RVSUM_1:11;
end;
len H = len D by Def6;
then
A6: H is Element of (len D)-tuples_on REAL by FINSEQ_2:92;
F+G is Element of (len D)-tuples_on REAL by A4,A3,FINSEQ_2:120;
then Sum(F+G) <= Sum H by A6,A5,RVSUM_1:82;
hence thesis by A4,A3,RVSUM_1:89;
end;
theorem
f|A is bounded & g|A is bounded & f is integrable & g is integrable
implies f+g is integrable & integral(f+g)=integral(f)+integral(g)
proof
assume that
A1: f|A is bounded and
A2: g|A is bounded and
A3: f is integrable and
A4: g is integrable;
A5: lower_integral(f)+lower_integral(g) =upper_integral(f) +
lower_integral(g) by A3
.=integral(f) + integral(g) by A4;
A6: (f+g)|(A /\ A) is bounded by A1,A2,RFUNCT_1:83;
for D be object st D in divs A /\ dom(lower_sum_set(f+g)) holds (
lower_sum_set(f+g)).D <= (upper_bound rng f)*vol(A) + (upper_bound rng g)*vol(A
)
proof
let D be object;
assume
D in divs A /\ dom(lower_sum_set(f+g));
then reconsider D as Division of A by Def2;
(lower_sum_set(f+g)).D = lower_sum((f+g),D) by Def10;
then
A7: (lower_sum_set(f+g)).D <= upper_sum((f+g),D) by A6,Th26;
upper_sum(f,D) <= (upper_bound rng f)*vol(A) by A1,Th25;
then
A8: upper_sum(f,D)+upper_sum(g,D) <= (upper_bound rng f)*vol(A)+upper_sum
(g,D ) by XREAL_1:6;
upper_sum(g,D) <= (upper_bound rng g)*vol(A) by A2,Th25;
then
A9: (upper_bound rng f)*vol(A)+upper_sum(g,D)<= (upper_bound rng f)*vol(A
)+( upper_bound rng g)*vol(A) by XREAL_1:6;
upper_sum((f+g),D) <= upper_sum(f,D)+upper_sum(g,D) by A1,A2,Th53;
then (lower_sum_set(f+g)).D <= upper_sum(f,D)+upper_sum(g,D) by A7,
XXREAL_0:2;
then (lower_sum_set(f+g)).D <= (upper_bound rng f)*vol(A)+upper_sum(g,D )
by A8,XXREAL_0:2;
hence thesis by A9,XXREAL_0:2;
end;
then (lower_sum_set(f+g))|divs A is bounded_above by RFUNCT_1:70;
then
A10: rng lower_sum_set(f+g) is bounded_above by Th11;
then
A11: f+g is lower_integrable;
for D be object st D in divs A /\ dom(upper_sum_set(f+g)) holds (
lower_bound rng f)*vol(A) + (lower_bound rng g)*vol(A) <= (upper_sum_set(f+g)).
D
proof
let D be object;
assume
D in divs A /\ dom(upper_sum_set(f+g));
then reconsider D as Division of A by Def2;
(upper_sum_set(f+g)).D = upper_sum((f+g),D) by Def9;
then
A12: lower_sum((f+g),D) <= (upper_sum_set(f+g)).D by A6,Th26;
(lower_bound rng f)*vol(A) <= lower_sum(f,D) by A1,Th23;
then
A13: (lower_bound rng f)*vol(A)+lower_sum(g,D) <= lower_sum(f,D)+lower_sum
(g,D) by XREAL_1:6;
(lower_bound rng g)*vol(A) <= lower_sum(g,D) by A2,Th23;
then
A14: (lower_bound rng f)*vol(A)+(lower_bound rng g)*vol(A)<= (lower_bound
rng f )*vol(A)+lower_sum(g,D) by XREAL_1:6;
lower_sum(f,D)+lower_sum(g,D) <= lower_sum((f+g),D) by A1,A2,Th54;
then lower_sum(f,D)+lower_sum(g,D) <= (upper_sum_set(f+g)).D by A12,
XXREAL_0:2;
then (lower_bound rng f)*vol(A)+lower_sum(g,D) <= (upper_sum_set(f+g)).D
by A13,XXREAL_0:2;
hence thesis by A14,XXREAL_0:2;
end;
then (upper_sum_set(f+g))|divs A is bounded_below by RFUNCT_1:71;
then
A15: rng upper_sum_set(f+g) is bounded_below by Th9;
A16: for D st D in divs A /\ dom upper_sum_set(f+g) holds (upper_sum_set f).
D + (upper_sum_set g).D >= upper_integral(f+g)
proof
let D;
upper_sum(f,D)+upper_sum(g,D) >= upper_sum((f+g),D) by A1,A2,Th53;
then
A17: (upper_sum_set f).D+upper_sum(g,D) >= upper_sum((f+g),D) by Def9;
assume D in divs A /\ dom upper_sum_set(f+g);
then
D in dom(upper_sum_set(f+g)) by XBOOLE_0:def 4;
then (upper_sum_set(f+g)).D in rng upper_sum_set(f+g) by FUNCT_1:def 3;
then
A18: (upper_sum_set(f+g)).D >= upper_integral(f+g) by A15,SEQ_4:def 2;
(upper_sum_set f).D+(upper_sum_set g).D >= upper_sum((f+g),D) by A17,Def9;
then (upper_sum_set f).D+(upper_sum_set g).D>=(upper_sum_set(f+g)).D by
Def9;
hence thesis by A18,XXREAL_0:2;
end;
A19: dom upper_sum_set(f+g) = divs A by FUNCT_2:def 1;
A20: for a1 be Real st a1 in rng upper_sum_set(f) holds a1 >=
upper_integral(f+g) - upper_integral(g)
proof
let a1 be Real;
assume a1 in rng upper_sum_set(f);
then consider D1 be Element of divs A such that
D1 in dom upper_sum_set(f) and
A21: a1=(upper_sum_set(f)).D1 by PARTFUN1:3;
reconsider D1 as Division of A by Def2;
A22: a1=upper_sum(f,D1) by A21,Def9;
for a2 being Real st a2 in rng upper_sum_set(g) holds a2 >=
upper_integral(f+g) - a1
proof
let a2 be Real;
assume a2 in rng upper_sum_set(g);
then consider D2 be Element of divs A such that
D2 in dom upper_sum_set(g) and
A23: a2=(upper_sum_set(g)).D2 by PARTFUN1:3;
reconsider D2 as Division of A by Def2;
consider D such that
A24: D1 <= D and
A25: D2 <= D by Th45;
A26: D in divs A by Def2;
(upper_sum_set(g)).D = upper_sum(g,D) by Def9;
then
A27: (upper_sum_set(g)).D <= upper_sum(g,D2) by A2,A25,Th43;
(upper_sum_set(f)).D = upper_sum(f,D) by Def9;
then (upper_sum_set(f)).D <= upper_sum(f,D1) by A1,A24,Th43;
then
A28: (upper_sum_set f).D + (upper_sum_set g).D <= upper_sum(f,D1) +
upper_sum(g,D2) by A27,XREAL_1:7;
(upper_sum_set f).D + (upper_sum_set g).D >= upper_integral(f+g) by A19
,A16,A26;
then
A29: upper_sum(f,D1)+upper_sum(g,D2) >= upper_integral(f+g) by A28,XXREAL_0:2;
a2=upper_sum(g,D2) by A23,Def9;
hence thesis by A22,A29,XREAL_1:20;
end;
then lower_bound rng upper_sum_set(g) >= upper_integral(f+g) - a1 by
SEQ_4:43;
then a1+lower_bound rng upper_sum_set(g) >= upper_integral(f+g) by
XREAL_1:20;
hence thesis by XREAL_1:20;
end;
upper_integral(f) >= upper_integral(f+g) - upper_integral(g) by A20,SEQ_4:43;
then
A30: integral(f)+upper_integral(g)>=upper_integral(f+g) by XREAL_1:20;
A31: for D st D in divs A /\ dom lower_sum_set(f+g) holds (lower_sum_set f).
D + (lower_sum_set g).D <= lower_integral(f+g)
proof
let D;
lower_sum(f,D)+lower_sum(g,D) <= lower_sum((f+g),D) by A1,A2,Th54;
then
A32: (lower_sum_set f).D+lower_sum(g,D) <= lower_sum((f+g),D) by Def10;
assume D in divs A /\ dom lower_sum_set(f+g);
then
D in dom(lower_sum_set(f+g)) by XBOOLE_0:def 4;
then (lower_sum_set(f+g)).D in rng lower_sum_set(f+g) by FUNCT_1:def 3;
then
A33: (lower_sum_set(f+g)).D <= lower_integral(f+g) by A10,SEQ_4:def 1;
(lower_sum_set f).D+(lower_sum_set g).D <= lower_sum((f+g),D) by A32,Def10;
then (lower_sum_set f).D+(lower_sum_set g).D<=(lower_sum_set(f+g)).D by
Def10;
hence thesis by A33,XXREAL_0:2;
end;
A34: dom lower_sum_set(f+g) = divs A by FUNCT_2:def 1;
A35: for a1 be Real st a1 in rng lower_sum_set(f) holds a1 <=
lower_integral(f+g) - lower_integral(g)
proof
let a1 be Real;
assume a1 in rng lower_sum_set(f);
then consider D1 be Element of divs A such that
D1 in dom lower_sum_set(f) and
A36: a1=(lower_sum_set(f)).D1 by PARTFUN1:3;
reconsider D1 as Division of A by Def2;
A37: a1=lower_sum(f,D1) by A36,Def10;
for a2 be Real st a2 in rng lower_sum_set(g) holds a2 <=
lower_integral(f+g) - a1
proof
let a2 be Real;
assume a2 in rng lower_sum_set(g);
then consider D2 be Element of divs A such that
D2 in dom lower_sum_set(g) and
A38: a2=(lower_sum_set(g)).D2 by PARTFUN1:3;
reconsider D2 as Division of A by Def2;
consider D such that
A39: D1 <= D and
A40: D2 <= D by Th45;
A41: D in divs A by Def2;
(lower_sum_set(g)).D = lower_sum(g,D) by Def10;
then
A42: (lower_sum_set(g)).D >= lower_sum(g,D2) by A2,A40,Th44;
(lower_sum_set(f)).D = lower_sum(f,D) by Def10;
then (lower_sum_set(f)).D >= lower_sum(f,D1) by A1,A39,Th44;
then
A43: (lower_sum_set f).D + (lower_sum_set g).D >= lower_sum(f,D1) +
lower_sum(g,D2) by A42,XREAL_1:7;
(lower_sum_set f).D + (lower_sum_set g).D <= lower_integral(f+g)
by A34,A31,A41;
then
A44: lower_sum(f,D1)+lower_sum(g,D2) <= lower_integral(f+g) by A43,XXREAL_0:2;
a2=lower_sum(g,D2) by A38,Def10;
hence thesis by A37,A44,XREAL_1:19;
end;
then upper_bound rng lower_sum_set(g)<= lower_integral(f+g) - a1 by
SEQ_4:45;
then a1+upper_bound rng lower_sum_set(g) <= lower_integral(f+g) by
XREAL_1:19;
hence thesis by XREAL_1:19;
end;
upper_bound rng lower_sum_set(f)<= lower_integral(f+g)-lower_integral(
g) by A35,SEQ_4:45;
then
A45: lower_integral(f) + lower_integral(g) <= lower_integral(f+g) by XREAL_1:19
;
A46: upper_integral(f+g)>=lower_integral(f+g) by A6,Th47;
then integral(f)+integral(g) <= upper_integral(f+g) by A45,A5,XXREAL_0:2;
then upper_integral(f+g)=integral(f) + integral(g) by A30,XXREAL_0:1;
then
A47: upper_integral(f+g) = lower_integral(f+g) by A45,A46,A5,XXREAL_0:1;
f+g is upper_integrable by A15;
hence thesis by A11,A45,A5,A30,A47,XXREAL_0:1;
end;
theorem
for f being FinSequence holds
i in dom f & j in dom f & i<=j implies len mid(f,i,j) = j-i+1 by Lm1;