:: The Linearity of Riemann Integral on Functions from $\mathbbbR$ into Real
:: {B}anach Space
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received October 7, 2013
:: Copyright (c) 2013-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies PRE_TOPC, NORMSP_1, FUNCT_1, ARYTM_1, NAT_1, SUBSET_1, NUMBERS,
CARD_1, XXREAL_0, REAL_1, ARYTM_3, RELAT_1, ORDINAL2, SEQ_2, LOPBAN_1,
STRUCT_0, COMPLEX1, VALUED_1, SUPINF_2, XBOOLE_0, INTEGRA1, INTEGRA2,
FINSEQ_1, TARSKI, INTEGRA5, INTEGR15, INTEGRA4, MEASURE7, CARD_3,
XXREAL_1, PARTFUN1, SEQ_4, XXREAL_2, MEASURE5, FUNCT_3, ORDINAL4,
RFINSEQ;
notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1,
ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2,
NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, VALUED_0, COMPLEX1,
XXREAL_2, FINSEQ_1, FINSEQ_2, SEQ_2, RFUNCT_1, RVSUM_1, RFINSEQ, SEQ_4,
RCOMP_1, MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3, INTEGRA4, INTEGRA5,
STRUCT_0, PRE_TOPC, RLVECT_1, VFUNCT_1, NORMSP_0, NORMSP_1, LOPBAN_1,
INTEGR15, INTEGR18, NFCONT_3, INTEGR19;
constructors ABIAN, SEQ_2, RELSET_1, SEQ_4, VFUNCT_1, PDIFF_1, RLSUB_1,
FCONT_1, NFCONT_1, INTEGRA3, INTEGRA4, NDIFF_3, INTEGR18, RVSUM_1,
INTEGR19, INTEGR15, COMSEQ_2, VALUED_2, BINOM, FDIFF_1, NFCONT_2, C0SP2,
ORDEQ_01, RFINSEQ, RFUNCT_1, RFINSEQ2, SQUARE_1, PDIFF_7, NDIFF_5,
INTEGR20, NEWTON;
registrations STRUCT_0, NAT_1, XXREAL_0, NUMBERS, XBOOLE_0, FUNCT_2, XREAL_0,
MEMBERED, NORMSP_1, RELAT_1, RELSET_1, INTEGRA1, ORDINAL1, NFCONT_3,
XXREAL_2, RLVECT_1, VALUED_0, FINSEQ_1, FINSET_1, MEASURE5, SEQM_3,
INT_1, CARD_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions INTEGR19, TARSKI;
equalities ALGSTR_0, FINSEQ_1, INTEGRA5, INTEGRA1, INTEGRA3, INTEGR15,
INTEGR18, XCMPLX_0;
expansions INTEGRA5, INTEGRA4, INTEGR18, NORMSP_1, INTEGR19, TARSKI;
theorems TARSKI, ABSVALUE, RLVECT_1, NORMSP_0, SEQ_2, PARTFUN1, PARTFUN2,
FUNCT_1, NAT_1, FUNCT_2, NORMSP_1, XREAL_1, LOPBAN_1, XXREAL_0, XREAL_0,
ORDINAL1, RELAT_1, NFCONT_3, VFUNCT_1, XBOOLE_0, FINSEQ_1, COMSEQ_2,
SEQM_3, INTEGR15, INTEGRA2, XXREAL_1, COMPLEX1, XBOOLE_1, INTEGR19,
INTEGRA4, INTEGRA5, INTEGRA3, INTEGRA1, INTEGR18, INTEGRA6, FINSEQ_3,
FINSEQ_5, RFINSEQ, XXREAL_2, INTEGR20, SUBSET_1;
schemes FUNCT_2, FINSEQ_1;
begin :: Some Properties of Bounded Functions
reserve Z for RealNormSpace;
reserve a,b,c,d,e,r for Real;
reserve A,B for non empty closed_interval Subset of REAL;
Lm2:
a <= b & c in ['a,b'] & d in ['a,b']
implies ['min(c,d),max(c,d)'] c= ['a,b']
proof
assume A1:a<=b & c in ['a,b'] & d in ['a,b'];
then ['a,b'] = [.a,b.] by INTEGRA5:def 3;
then
A2: a <=c & d <=b & a <=d & c <= b by A1,XXREAL_1:1;
per cases;
suppose A3:c <= d; then
A4: c = min(c,d) & d = max(c,d) by XXREAL_0:def 9,def 10;
['c,b'] c= ['a,b'] & ['c,d'] c= ['c,b'] by A2,A3,INTEGR19:1;
hence ['min(c,d),max(c,d)'] c=['a,b'] by A4;
end;
suppose A6:not c <= d; then
A7: d = min(c,d) & c = max(c,d) by XXREAL_0:def 9,def 10;
['d,b'] c= ['a,b'] & ['d,c'] c= ['d,b'] by A2,A6,INTEGR19:1;
hence ['min(c,d),max(c,d)'] c=['a,b'] by A7;
end;
end;
Lm3:
for X,Y,Z be non empty set, f be PartFunc of X,Y
st Z c= dom f holds f|Z is Function of Z,Y
proof
let X,Y,Z be non empty set, f be PartFunc of X,Y;
rng f c= Y; then
f is Function of dom f,Y by FUNCT_2:2;
hence thesis by FUNCT_2:32;
end;
theorem Th1915:
for f be PartFunc of REAL,the carrier of Z st
f is bounded & A c= dom f holds f|A is bounded
proof
let f be PartFunc of REAL,the carrier of Z;
assume that
A1: f is bounded and
A2: A c= dom f;
consider r be Real such that
A3: for x be set st x in dom f holds ||. f/.x .|| <r by A1;
now let x be set;
assume x in dom(f|A); then
||. f/.x .|| <r & x in dom f /\ A by A3,A2,RELAT_1:61;
hence ||. (f|A)/.x .|| <r by PARTFUN2:16;
end;
hence f|A is bounded;
end;
theorem Th1915a:
for f be PartFunc of REAL,the carrier of Z
st f|A is bounded & B c= A & B c= dom (f|A)
holds f|B is bounded
proof
let f be PartFunc of REAL,the carrier of Z;
assume
A1: f|A is bounded & B c= A & B c= dom (f|A);
set g = f|A;
A4: g|B is bounded by Th1915,A1;
consider r be Real such that
A5: for x be set st x in dom (g|B) holds ||. (g|B)/.x .|| <r by A4;
g|B = f|B by A1,RELAT_1:74;
hence f|B is bounded by A5;
end;
theorem Th1915b:
for f be PartFunc of REAL,the carrier of Z
st a <= c & c <= d & d <= b & f| ['a,b'] is bounded & ['a,b'] c= dom f
holds f| ['c,d'] is bounded
proof
let f be PartFunc of REAL,the carrier of Z;
assume A1:a <= c & c <= d & d <= b &
f| ['a,b'] is bounded & ['a,b'] c= dom f;
A2:c <= b & a <= d by A1,XXREAL_0:2; then
A4:c in ['a,b'] & d in ['a,b'] by A1,INTEGR19:1;
reconsider A = ['a,b'], B = ['c,d']
as non empty closed_interval Subset of REAL;
c = min(c,d) & d = max(c,d) by A1,XXREAL_0:def 9,def 10; then
A5:B c= A by A2,A1,XXREAL_0:2,A4,Lm2;
then B c= dom(f|A) by A1,RELAT_1:62;
hence f| ['c,d'] is bounded by A1,A5,Th1915a;
end;
theorem Th1935:
for X,Y be set, f1,f2 be PartFunc of REAL,the carrier of Z
st f1|X is bounded & f2|Y is bounded
holds (f1+f2) | (X /\ Y) is bounded & (f1-f2) | (X /\ Y) is bounded
proof
let X,Y be set, f1,f2 be PartFunc of REAL,the carrier of Z;
assume A1: f1|X is bounded & f2|Y is bounded;
consider r1 be Real such that
A2: for x be set st x in dom (f1|X) holds ||. (f1|X)/.x .|| <r1 by A1;
consider r2 be Real such that
A3: for x be set st x in dom (f2|Y) holds ||. (f2|Y)/.x .|| <r2 by A1;
now let x be set;
assume A41: x in dom ((f1+f2) | (X /\ Y)); then
A4: x in dom (f1+f2) & x in (X /\ Y) by RELAT_1:57;
then x in (dom f1) /\ (dom f2) by VFUNCT_1:def 1; then
A5: x in dom f1 & x in dom f2 & x in X & x in Y by A41,XBOOLE_0:def 4; then
A6: x in dom(f2|Y) by RELAT_1:57;
((f1+f2) | (X /\ Y))/.x = (f1+f2)/.x by A4,PARTFUN2:17
.= f1/.x + f2/.x by A4,VFUNCT_1:def 1
.= (f1|X)/.x + f2/.x by A5,PARTFUN2:17
.= (f1|X)/.x + (f2|Y)/.x by A5,PARTFUN2:17; then
A7: ||. ((f1+f2) | (X /\ Y))/.x .||
<= ||.(f1|X)/.x .|| + ||.(f2|Y)/.x .|| by NORMSP_1:def 1;
||.(f1|X)/.x .|| < r1 by A2,A5,RELAT_1:57; then
||.(f1|X)/.x .|| + ||.(f2|Y)/.x .|| < r1+r2 by A3,A6,XREAL_1:8;
hence ||. ((f1+f2) | (X /\ Y))/.x .|| < r1+r2 by A7,XXREAL_0:2;
end;
hence (f1+f2) | (X /\ Y) is bounded;
take r1+r2;
let x be set;
assume
A8: x in dom ((f1-f2) | (X /\ Y)); then
A9: x in dom (f1-f2) & x in (X /\ Y) by RELAT_1:57;
then x in (dom f1) /\ (dom f2) by VFUNCT_1:def 2; then
A10: x in dom f1 & x in dom f2 & x in X & x in Y by A8,XBOOLE_0:def 4; then
A11:x in dom (f2|Y) by RELAT_1:57;
((f1-f2) | (X /\ Y))/.x = (f1-f2)/.x by A9,PARTFUN2:17
.= f1/.x - f2/.x by A9,VFUNCT_1:def 2
.= (f1|X)/.x - f2/.x by A10,PARTFUN2:17
.= (f1|X)/.x - (f2|Y)/.x by A10,PARTFUN2:17; then
A12: ||. ((f1-f2) | (X /\ Y))/.x .||
<= ||.(f1|X)/.x .|| + ||.(f2|Y)/.x .|| by NORMSP_1:3;
||.(f1|X)/.x .|| < r1 by A2,A10,RELAT_1:57;
then ||.(f1|X)/.x .|| + ||.(f2|Y)/.x .|| < r1+r2 by A11,A3,XREAL_1:8;
hence ||. ((f1-f2) | (X /\ Y))/.x .|| < r1+r2 by A12,XXREAL_0:2;
end;
theorem Th1935a:
for X be set, f be PartFunc of REAL,the carrier of Z
st f|X is bounded holds (r(#)f)|X is bounded
proof
let X be set, f be PartFunc of REAL,the carrier of Z;
assume f|X is bounded; then
consider s be Real such that
A2: for x be set st x in dom (f|X) holds ||. (f|X)/.x .|| <s;
reconsider p = |.r.|*|.s.|+1 as Real;
take p;
now let x be set;
assume A3: x in dom ((r(#)f)|X); then
A4: x in dom (r(#)f) /\ X by RELAT_1:61;
A5: x in X & x in dom (r(#)f) by A3,RELAT_1:57; then
A6: x in X & x in dom f by VFUNCT_1:def 4; then
A7: x in dom f /\ X by XBOOLE_0:def 4;
A8: ||. (f|X)/.x .|| <s by A2,A6,RELAT_1:57;
(r(#)f)/.x = r * (f/.x) by VFUNCT_1:def 4,A5; then
((r(#)f)|X)/.x = r * (f/.x) by A4,PARTFUN2:16; then
A11: ||. ( (r(#)f)|X )/.x .|| = ||. r * ((f|X)/.x) .|| by A7,PARTFUN2:16
.= |.r.| * ||. (f|X)/.x .|| by NORMSP_1:def 1;
0 <= |.r.| by COMPLEX1:46; then
|.r.| * s <= |.r.| * |.s.| & |.r.| * ||. (f|X)/.x .|| <= |.r.| * s
by A8,ABSVALUE:4,XREAL_1:64; then
|.r.| * ||. (f|X)/.x .|| <= |.r.| * |.s.| by XXREAL_0:2;
hence ||. ( (r(#)f)|X )/.x .|| <p by A11,XREAL_1:145;
end;
hence thesis;
end;
theorem Th1935b:
for X be set, f be PartFunc of REAL,the carrier of Z
st f|X is bounded holds (-f)|X is bounded
proof
let X be set, f be PartFunc of REAL,the carrier of Z;
assume f|X is bounded; then
consider s be Real such that
A2: for x be set st x in dom(f|X) holds ||. (f|X)/.x .|| <s;
now let x be set;
assume x in dom ((-f)|X); then
A4: x in dom (-(f|X)) by VFUNCT_1:29; then
x in dom (f|X) by VFUNCT_1:def 5; then
A5: ||. (f|X)/.x .|| <s by A2;
((-f)|X)/.x = (-(f|X))/.x by VFUNCT_1:29
.= -((f|X)/.x) by A4,VFUNCT_1:def 5;
hence ||. (-f)|X/.x .|| <s by A5,NORMSP_1:2;
end;
hence (-f)|X is bounded;
end;
theorem Th1914:
for f be Function of A,the carrier of Z holds
f is bounded iff ||.f.|| is bounded
proof
let f be Function of A,the carrier of Z;
hereby assume A1: f is bounded;
consider r be Real such that
A2: for x be set st x in dom f holds ||. f/.x .|| <r by A1;
now let x be set;
assume A3: x in dom ||. f .||; then
x in dom f by NORMSP_0:def 2; then
A4: ||. f/.x .|| <r by A2;
||. f/.x .|| = ||. f .||.x by A3,NORMSP_0:def 2;
hence |. ||. f .||.x .| <r by A4,ABSVALUE:def 1;
end;
hence ||.f.|| is bounded by COMSEQ_2:def 3;
end;
assume ||.f.|| is bounded; then
consider r be Real such that
B2: for x be set st x in dom ||. f .||
holds |. ||. f .||.x .| <r by COMSEQ_2:def 3;
now let x be set;
assume x in dom f; then
B3: x in dom ||. f .|| by NORMSP_0:def 2; then
B4: |. ||. f .||.x .| <r by B2;
||. f .||.x = ||. f/.x .|| by B3,NORMSP_0:def 2;
hence ||. f/.x .|| <r by B4,ABSVALUE:def 1;
end;
hence f is bounded;
end;
theorem Th1918:
for f be PartFunc of REAL,the carrier of Z st
A c= dom f holds ||.f|A.|| = (||.f.||) |A
proof
let f be PartFunc of REAL,the carrier of Z;
assume A1: A c= dom f; then
A2:dom (f|A) = A by RELAT_1:62;
A3:dom ((||.f.||) |A) = dom ||.f.|| /\ A by RELAT_1:61; then
A6:dom ((||.f.||) |A) = dom f /\ A by NORMSP_0:def 3; then
dom ((||.f.||) |A) = A by A1,XBOOLE_1:28; then
A4:dom ||. f|A .|| = dom ((||.f.||) |A) by A2,NORMSP_0:def 3;
now let x be object;
assume A5: x in dom ((||.f.||) |A); then
A9: x in dom (||.f.||) & x in dom f by A3,A6,XBOOLE_0:def 4; then
A11:f/.x = f.x by PARTFUN1:def 6
.= (f|A).x by FUNCT_1:49,A5
.= (f|A)/.x by A2,PARTFUN1:def 6,A5;
thus ((||.f.||) |A).x = (||.f.||).x by FUNCT_1:49,A5
.= ||. f/.x .|| by A9,NORMSP_0:def 3
.= (||. (f|A) .||) .x by A11,A4,A5,NORMSP_0:def 3;
end;
hence thesis by A4,FUNCT_1:2;
end;
theorem Th1919:
for g be PartFunc of REAL,the carrier of Z
st A c= dom g & g|A is bounded
holds (||.g.||) |A is bounded
proof
let g be PartFunc of REAL,the carrier of Z;
assume A1: A c= dom g & g|A is bounded; then
A2: ||. (g|A) .|| = (||.g.||) |A by Th1918;
reconsider h = g|A as Function of A,the carrier of Z by A1,Lm3;
h is bounded by A1;
hence thesis by A2,Th1914;
end;
begin :: Some Properties of Integral of Continuous Functions
reserve X,Y for RealBanachSpace;
reserve E for Point of Y;
theorem Th3:
for Y be RealNormSpace,
f be continuous PartFunc of REAL,the carrier of Y
st a <= b & ['a,b'] c= dom f holds ||.f.|| | ['a,b'] is bounded
proof
let Y be RealNormSpace, f be continuous PartFunc of REAL,the carrier of Y;
assume A1: a <= b & [' a,b '] c= dom f;
P11: f | ['a,b'] is continuous;
['a,b'] c= dom ||.f.|| by NORMSP_0:def 3,A1;
hence thesis by P11,A1,NFCONT_3:22,INTEGRA5:10;
end;
theorem Th1:
for Y be RealNormSpace, f be continuous PartFunc of REAL,the carrier of Y
st a <= b & ['a,b'] c= dom f holds f|['a,b'] is bounded
proof
let Y be RealNormSpace,
f be continuous PartFunc of REAL,the carrier of Y;
set h = ||.f.|| | ['a,b'];
set g = f|['a,b'];
assume A1: a <= b & ['a,b'] c= dom f;
then h is bounded by Th3; then
consider r be Real such that
P2: for y being set st y in dom h holds |. h.y .| < r by COMSEQ_2:def 3;
D1:dom ||.f.|| = dom f by NORMSP_0:def 3;
for y be set st y in dom g holds ||. g/.y .|| < r
proof
let y be set;
assume P3: y in dom g; then
P5: y in ['a,b'] by A1,RELAT_1:62; then
P6: y in dom h by A1,D1,RELAT_1:62;
P81:h.y = ||.f.||.y by P5,FUNCT_1:49
.= ||. f/.y .|| by NORMSP_0:def 2,D1,P5,A1;
f/.y = f.y by PARTFUN1:def 6,P5,A1
.= g.y by P5,FUNCT_1:49
.= g/.y by PARTFUN1:def 6,P3;
then |. h.y .| = ||. g/.y .|| by P81,ABSVALUE:def 1;
hence thesis by P2,P6;
end;
hence thesis;
end;
theorem Th4:
for Y be RealNormSpace,
f be continuous PartFunc of REAL,the carrier of Y
st a <= b & ['a,b'] c= dom f
holds ||.f.|| is_integrable_on ['a,b']
proof
let Y be RealNormSpace,
f be continuous PartFunc of REAL,the carrier of Y;
assume A1: a <= b & ['a,b'] c= dom f;
P11: f | [' a,b '] is continuous;
['a,b'] c= dom ||.f.|| by NORMSP_0:def 3,A1;
hence ||.f.|| is_integrable_on ['a,b'] by P11,A1,NFCONT_3:22,INTEGRA5:11;
end;
theorem Th1909:
for f be continuous PartFunc of REAL,the carrier of Y
st a <= c & c <= d & d <= b & ['a,b'] c= dom f
holds f is_integrable_on ['c,d']
proof
let f be continuous PartFunc of REAL,the carrier of Y;
assume
A1: a <= c & c <= d & d <= b & ['a,b'] c= dom f; then
A2:c <= b & a <= d by XXREAL_0:2; then
A4:c in ['a,b'] & d in ['a,b'] by A1,INTEGR19:1;
c = min(c,d) & d = max(c,d) by A1,XXREAL_0:def 9,def 10; then
['c,d'] c= ['a,b'] by A2,A1,XXREAL_0:2,A4,Lm2; then
['c,d'] c= dom f by A1;
hence f is_integrable_on ['c,d'] by A1,INTEGR20:19;
end;
theorem Th1947:
for f be PartFunc of REAL,the carrier of Y st a <= b & ['a,b'] c= dom f
holds integral(f,b,a) = - integral(f,a,b)
proof
let f be PartFunc of REAL,the carrier of Y;
assume A1: a<=b & ['a,b'] c= dom f; then
A2:['a,b'] = [.a,b.] by INTEGRA5:def 3;
integral(f,['a,b'])= integral(f,a,b) by A2,INTEGR18:16;
hence thesis by A2,A1,INTEGR18:18;
end;
Lm62:
for f be continuous PartFunc of REAL,the carrier of X
st a <= b & ['a,b'] c= dom f & c in ['a,b'] & b <> c holds
integral(f,a,b) = integral(f,a,c) + integral(f,c,b)
proof
let f be continuous PartFunc of REAL,the carrier of X;
assume that
A1: a <= b and
A2: ['a,b'] c= dom f and
A5: c in ['a,b'] and
A6: b <> c;
reconsider AB = ['a,b'], AC = ['a,c'], CB = ['c,b']
as non empty closed_interval Subset of REAL;
A7:['a,b'] = [.a,b.] by A1,INTEGRA5:def 3; then
A8:a <= c & c <= b by A5,XXREAL_1:1; then
A9: ['a,c'] = [.a,c.] & ['c,b'] = [.c,b.] by INTEGRA5:def 3; then
[.c,b.] = [.lower_bound [.c,b.], upper_bound [.c,b.].]
& [.a,c.] = [.lower_bound [.a,c.], upper_bound [.a,c.].]
& [.a,b.] = [.lower_bound [.a,b.], upper_bound [.a,b.].] by A7,INTEGRA1:4;
then
A11: upper_bound CB = b & lower_bound CB = c
& upper_bound AC = c & lower_bound AC = a
& upper_bound AB = b & lower_bound AB = a by A7,A9,INTEGRA1:5;
C1:
f is_integrable_on AB & f is_integrable_on AC
& f is_integrable_on CB by A1,A2,A8,Th1909;
consider FAB be Function of AB,the carrier of X such that
C3: FAB = f|AB & FAB is integrable by C1;
consider FAC be Function of AC,the carrier of X such that
C4: FAC = f|AC & FAC is integrable by C1;
consider FCB be Function of CB,the carrier of X such that
C5: FCB = f|CB & FCB is integrable by C1;
c < b by A6,A8,XXREAL_0:1;
then vol CB > 0 by A11,XREAL_1:50;
then consider PS2 being DivSequence of CB such that
A25: delta PS2 is convergent & lim delta PS2 = 0
& for n be Element of NAT holds
ex Tn being Division of CB st
Tn divide_into_equal n+1 & PS2.n =Tn by INTEGRA6:16;
A27:
for i be Element of NAT st 2 <= i holds
ex S2i be Division of CB st S2i = PS2.i & 2 <= len S2i
proof
let i be Element of NAT;
assume A22: 2 <= i;
consider Tn being Division of CB such that
A23: Tn divide_into_equal i+1 & PS2.i =Tn by A25;
take Tn;
thus Tn=PS2.i by A23;
i <= len Tn by NAT_1:11,A23;
hence 2 <= len Tn by A22,XXREAL_0:2;
end;
defpred Q[set,set] means
ex n be Nat, e being Division of ['c,b'] st
n = $1 & e = $2 & e = PS2.(n+2);
A28:for n be Element of NAT ex D being Element of divs CB st Q[n,D]
proof
let n be Element of NAT;
reconsider D = PS2.(n+2) as Element of divs CB by INTEGRA1:def 3;
take D;
thus thesis;
end;
consider S2 being sequence of divs CB such that
A29:for n be Element of NAT holds Q[n,S2.n] from FUNCT_2:sch 3(A28);
reconsider S2 as DivSequence of CB;
defpred P1[Element of NAT, set] means
ex S be Division of CB st S = S2.$1 & $2 = S/^1;
A30:
now let i be Element of NAT;
ex n being Nat,e being Division of CB st
n = i & e = S2.i & e = PS2.(n+2) by A29;
hence ex S2i be Division of CB st S2i=S2.i & 2 <= len S2i by A27,NAT_1:11;
end;
A31:
for i be Element of NAT ex T be Element of divs CB st P1[i,T]
proof
let i be Element of NAT;
consider S be Division of CB such that
A32: S=S2.i & 2 <= len S by A30;
set T=S/^1;
A34:1 <= len S by A32,XXREAL_0:2;
2-1 <= len S -1 by A32,XREAL_1:13;
then
A35: 1 <= len T by A34,RFINSEQ:def 1; then
reconsider T as non empty increasing FinSequence of REAL
by A32,INTEGRA1:34,XXREAL_0:2;
len T in dom T by A35,FINSEQ_3:25;
then T.(len T) =S.(len T+ 1) by A34,RFINSEQ:def 1;
then T.(len T) =S.(len S -1+ 1) by A34,RFINSEQ:def 1;
then
A36: T.(len T) = upper_bound CB by INTEGRA1:def 2;
rng S c= CB & rng T c= rng S by FINSEQ_5:33,INTEGRA1:def 2;
then rng T c= CB;
then T is Division of CB by A36,INTEGRA1:def 2;
then T is Element of divs CB by INTEGRA1:def 3;
hence thesis by A32;
end;
consider T2 be DivSequence of CB such that
A38:for i be Element of NAT holds P1[i,T2.i] from FUNCT_2:sch 3(A31);
A39:
for n be Element of NAT holds
ex D be Division of CB st
D = T2.n & for i be Element of NAT st i in dom D holds c < D.i
proof
let n be Element of NAT;
reconsider D=T2.n as Division of CB;
take D;
consider E be Division of CB such that
A40: E=S2.n & T2.n=E/^1 by A38;
A42:ex E1 be Division of CB st E1=S2.n & 2 <= len E1 by A30;
then
A43:2-1 <= len E -1 by A40,XREAL_1:13;
A44:1 <= len E by A40,A42,XXREAL_0:2;
then
A45:1 in dom E by FINSEQ_3:25;
then rng E c=CB & E.1 in rng E by FUNCT_1:def 3,INTEGRA1:def 2;
then
A46:c <= E.1 by A9,XXREAL_1:1;
2 in dom E by A40,A42,FINSEQ_3:25;
then
A47:E.1 < E.2 by A45,SEQM_3:def 1;
len D = len E -1 by A40,A44,RFINSEQ:def 1;
then
A48:1 in dom D by A43,FINSEQ_3:25;
then
A49:D.1 = E.(1+1) by A40,A44,RFINSEQ:def 1;
then
A50:c < D.1 by A46,A47,XXREAL_0:2;
now let i be Element of NAT;
assume
A51: i in dom D;
then
A52: 1 <=i by FINSEQ_3:25;
thus now assume i <> 1;
then 1 < i by A52,XXREAL_0:1;
then D.1 < D.i by A48,A51,SEQM_3:def 1;
hence c < D.i by A50,XXREAL_0:2;
end;
hence c < D.i by A49,A46,A47,XXREAL_0:2;
end;
hence thesis;
end;
consider T1 be DivSequence of AC such that
A53:delta T1 is convergent & lim delta T1 = 0 by INTEGRA4:11;
A54:
for n be Element of NAT holds
ex D be Division of CB st D = T2.n & 1 <= len D
proof
let n be Element of NAT;
reconsider D=T2.n as Division of CB;
take D;
consider E be Division of CB such that
A55: E=S2.n & T2.n=E/^1 by A38;
ex E1 be Division of CB st E1=S2.n & 2 <= len E1 by A30;
then 1 <= len E & 2-1 <= len E -1 by A55,XREAL_1:13,XXREAL_0:2;
hence thesis by A55,RFINSEQ:def 1;
end;
defpred P2[Element of NAT,set] means
ex S1 be Division of AC, S2 be Division of CB st
S1=T1.$1 & S2=T2.$1 & $2=S1^S2;
A61:
for i be Element of NAT ex T be Element of divs AB st P2[i,T]
proof
let i0 be Element of NAT;
reconsider S1=T1.i0 as Division of AC;
reconsider S2=T2.i0 as Division of CB;
set T=S1^S2;
ex D be Division of CB st D = T2.i0 & 1 <= len D by A54;
then len S2 in Seg len S2;
then
A62:len S2 in dom S2 by FINSEQ_1:def 3;
A63:rng S1 c= AC by INTEGRA1:def 2;
now let i,j be Nat;
assume that
A64: i in dom T & j in dom T and
A66: i < j;
A67: 1 <= i & i <= len T & 1 <= j & j <= len T by A64,FINSEQ_3:25;
then i <= len S1 + len S2 & j <= len S1 + len S2 by FINSEQ_1:22;
then
A71: i-len S1 <= len S2 & j-len S1 <= len S2 by XREAL_1:20;
A79: i - len S1 < j -len S1 by A66,XREAL_1:14;
A70: now assume A72: j > len S1; then
A73: T.j = S2.(j-len S1) by A67,FINSEQ_1:24;
A74: len S1 + 1 <=j by A72,NAT_1:13;
then consider m be Nat such that
A75: (len S1 + 1)+m=j by NAT_1:10;
1+m = j - len S1 by A75; then
A76: j - len S1 in dom S2 by A71,A74,XREAL_1:19,FINSEQ_3:25;
A77: now assume A80: i > len S1; then
A81: len S1 + 1 <=i by NAT_1:13;
then consider m be Nat such that
A82: (len S1 + 1)+m=i by NAT_1:10;
1+m = i - len S1 by A82; then
A83: i - len S1 in dom S2 by A71,A81,XREAL_1:19,FINSEQ_3:25;
T.i = S2.(i-len S1) by A67,A80,FINSEQ_1:24;
hence T.i < T.j by A73,A76,A79,A83,SEQM_3:def 1;
end;
now assume i <= len S1; then
A84: i in dom S1 by A67,FINSEQ_3:25;
then T.i = S1.i by FINSEQ_1:def 7;
then T.i in rng S1 by A84,FUNCT_1:def 3;
then
A85: T.i <= c by A9,A63,XXREAL_1:1;
ex DD be Division of CB st
DD = T2.i0
& for k be Element of NAT st k in dom DD holds c < DD.k by A39;
hence T.i < T.j by A73,A76,A85,XXREAL_0:2;
end;
hence T.i < T.j by A77;
end;
now assume A87: j <= len S1; then
i <= len S1 by A66,XXREAL_0:2; then
A88: j in dom S1 & i in dom S1 by A67,A87,FINSEQ_3:25; then
T.j = S1.j & T.i = S1.i by FINSEQ_1:def 7;
hence T.i < T.j by A66,A88,SEQM_3:def 1;
end;
hence T.i < T.j by A70;
end;
then
reconsider T as non empty increasing FinSequence of REAL by SEQM_3:def 1;
rng S2 c= CB by INTEGRA1:def 2;
then rng S1 \/ rng S2 c= AC \/ CB by A63,XBOOLE_1:13;
then rng S1 \/ rng S2 c= [.a,b.] by A8,A9,XXREAL_1:174;
then
A92:rng T c= AB by A7,FINSEQ_1:31;
T.(len T) = T.(len S1 + len S2) by FINSEQ_1:22
.= S2.(len S2) by A62,FINSEQ_1:def 7
.= upper_bound AB by A11,INTEGRA1:def 2;
then reconsider T as Division of AB by A92,INTEGRA1:def 2;
T is Element of divs AB by INTEGRA1:def 3;
hence thesis;
end;
consider T be DivSequence of AB such that
A93: for i be Element of NAT holds P2[i,T.i] from FUNCT_2:sch 3(A61);
reconsider T as DivSequence of AB;
reconsider T1 as DivSequence of AC;
reconsider T2 as DivSequence of CB;
set h1=FAB, g1=FAC, g2=FCB;
set F1=the middle_volume_Sequence of FAC,T1;
set F2=the middle_volume_Sequence of FCB,T2;
B57:
integral(f,c,b) = integral(f,CB)
& integral(f,a,c) = integral(f,AC) by A9,INTEGR18:16;
A17: CB c= AB & AC c= AB by A7,A8,A9,XXREAL_1:34; then
CB c= dom f & AC c= dom f by A2; then
A57:
integral(f,c,b) = integral FCB
& integral(f,a,c) = integral FAC by B57,C4,C5,INTEGR18:9;
A95:
for i,k be Element of NAT, S0 be Division of AC st
S0=T1.i & k in Seg len S0 holds divset(T.i,k) = divset(T1.i,k)
proof
let i,k be Element of NAT, S0 be Division of AC;
assume
A96: S0=T1.i;
reconsider S=T.i as Division of AB;
A97:divset(T1.i,k) =
[. lower_bound divset(T1.i,k),upper_bound divset(T1.i,k).] by INTEGRA1:4;
consider S1 be Division of AC, S2 be Division of CB such that
A98: S1=T1.i & S2=T2.i and
A99: T.i=S1^S2 by A93;
assume
A100: k in Seg len S0;
then
A101: k in dom S1 by A96,A98,FINSEQ_1:def 3; then
A102: k in dom S by A99,FINSEQ_3:22;
A103: divset(T.i,k) =
[.lower_bound divset(T.i,k),upper_bound divset(T.i,k).] by INTEGRA1:4;
A104:
now assume
A106: k <> 1;
1 <= k by A100,FINSEQ_1:1;
then 1 < k by A106,XXREAL_0:1;
then k-1 in Seg len S1 by A96,A98,A100,FINSEQ_3:12;
then
A109:k-1 in dom S1 by FINSEQ_1:def 3;
thus divset(T.i,k) =[. S.(k-1),upper_bound divset(T.i,k) .]
by A102,A103,A106,INTEGRA1:def 4
.=[. S.(k-1),S.k .] by A102,A106,INTEGRA1:def 4
.=[. S.(k-1),S1.k .] by A99,A101,FINSEQ_1:def 7
.=[. S1.(k-1),S1.k .] by A99,A109,FINSEQ_1:def 7
.=[. lower_bound divset(T1.i,k),S1.k .] by A98,A101,A106,INTEGRA1:def 4
.= divset(T1.i,k) by A98,A101,A97,A106,INTEGRA1:def 4;
end;
now assume
A110: k=1;
hence divset(T.i,k) =[. lower_boundAB,upper_bound divset(T.i,k) .]
by A102,A103,INTEGRA1:def 4
.=[. lower_boundAB,S.k .] by A102,A110,INTEGRA1:def 4
.=[. lower_boundAB,S1.k .] by A99,A101,FINSEQ_1:def 7
.=[. lower_bound divset(T1.i,k),S1.k .]
by A11,A98,A101,A110,INTEGRA1:def 4
.= divset(T1.i,k) by A98,A101,A97,A110,INTEGRA1:def 4;
end;
hence thesis by A104;
end;
A112:
for i,k be Element of NAT,
S01 be Division of AC, S02 be Division of CB
st S01=T1.i & S02=T2.i & k in Seg len S02
holds divset(T.i,(len S01 + k)) = divset(T2.i,k)
proof
let i,k be Element of NAT, S01 be Division of AC, S02 be Division of CB;
assume
A113: S01=T1.i & S02=T2.i;
reconsider S=T.i as Division of AB;
consider S1 be Division of AC, S2 be Division of CB such that
A115: S1=T1.i & S2=T2.i and
A117: T.i = S1^S2 by A93;
assume
A118: k in Seg len S02;
then
A119: k in dom S2 by A113,A115,FINSEQ_1:def 3;
then
A120: len S1 + k in dom S by A117,FINSEQ_1:28;
A121: divset(T2.i,k) =
[. lower_bound divset(T2.i,k), upper_bound divset(T2.i,k).] by INTEGRA1:4;
A122: divset(T.i,(len S1 + k)) =
[.lower_bound divset(T.i,(len S1 + k)), upper_bound divset
(T .i,(len S1 + k)).] by INTEGRA1:4;
A123:
now assume
A125: k <> 1;
A126:1 <=k by A118,FINSEQ_1:1;
then 1 < k by A125,XXREAL_0:1;
then k-1 in Seg len S2 by A113,A115,A118,FINSEQ_3:12;
then
A129:k-1 in dom S2 by FINSEQ_1:def 3;
A130:1+0 < k + len S1 by A126,XREAL_1:8;
hence divset(T.i,(len S1 + k)) =
[. S.(len S1 + k-1),upper_bound divset(T.i,len S1
+ k) .] by A120,A122,INTEGRA1:def 4
.=[. S.(len S1 + k-1),S.(len S1 + k) .] by A120,A130,INTEGRA1:def 4
.=[. S.(len S1 + (k-1)),S2.k .] by A117,A119,FINSEQ_1:def 7
.=[. S2.(k-1),S2.k .] by A117,A129,FINSEQ_1:def 7
.=[. lower_bound divset(T2.i,k), S2.k .]
by A115,A119,A125,INTEGRA1:def 4
.= divset(T2.i,k) by A115,A119,A121,A125,INTEGRA1:def 4;
end;
now
len S1 in Seg len S1 by FINSEQ_1:3;
then
A131:len S1 in dom S1 by FINSEQ_1:def 3;
assume
A132: k=1;
len S1 <> 0; then
A133:len S1 + k <> 1 by A132;
hence
divset(T.i,(len S1 + k)) =
[. S.(len S1 + k-1),upper_bound divset(T.i,len S1
+ k) .] by A120,A122,INTEGRA1:def 4
.=[. S1.(len S1),upper_bound divset(T.i,len S1 +k) .]
by A117,A132,A131,FINSEQ_1:def 7
.=[. upper_bound (AC), upper_bound divset(T.i,len S1 + k) .]
by INTEGRA1:def 2
.=[. lower_bound (CB), S.(len S1 + k) .] by A11,A120,A133,
INTEGRA1:def 4
.=[. lower_bound CB, S2.k .] by A117,A119,FINSEQ_1:def 7
.=[. lower_bound divset(T2.i,k), S2.1 .]
by A115,A119,A132,INTEGRA1:def 4
.= divset(T2.i,k) by A115,A119,A121,A132,INTEGRA1:def 4;
end;
hence thesis by A113,A115,A123;
end;
A134:
for i,k be Element of NAT, S0 be Division of CB
st S0=T2.i & k in Seg len S0 holds divset(T2.i,k) c= CB
proof
let i,k be Element of NAT, S0 be Division of CB;
assume A135: S0=T2.i & k in Seg len S0; then
k in dom S0 by FINSEQ_1:def 3;
hence thesis by A135,INTEGRA1:8;
end;
A139:
for i,k be Element of NAT, S0 be Division of AC
st S0=T1.i & k in Seg len S0 holds divset(T1.i,k) c= AC
proof
let i,k be Element of NAT, S0 be Division of AC;
assume A140: S0=T1.i & k in Seg len S0; then
k in dom S0 by FINSEQ_1:def 3;
hence thesis by A140,INTEGRA1:8;
end;
defpred P1[Nat,set] means
ex q,q1,q2 being FinSequence of (the carrier of X) st
q = $2 & q1 =F1.$1 & q2 =F2.$1 & q = q1^q2;
B12:
for k being Element of NAT
ex y being Element of (the carrier of X)* st P1[k, y]
proof
let k being Element of NAT;
reconsider p1= F1.k as FinSequence of (the carrier of X);
reconsider p2= F2.k as FinSequence of X;
p1^p2 in (the carrier of X)* by FINSEQ_1:def 11;
hence ex p being Element of (the carrier of X)* st P1[k, p];
end;
consider Sh1 being sequence of (the carrier of X)* such that
B22:for x being Element of NAT holds P1[x, Sh1.x] from FUNCT_2:sch 3(B12);
now let k be Element of NAT;
consider q,q1,q2 being FinSequence of the carrier of X such that
B221:q = Sh1.k & q1 =F1.k & q2 =F2.k & q = q1^q2 by B22;
consider S1 be Division of AC, S2 be Division of CB such that
U1: S1=T1.k & S2=T2.k & T.k=S1^S2 by A93;
X1: len (F1.k) = len (T1.k) & len (F2.k) = len (T2.k) by INTEGR18:def 1;
then
B226:len (Sh1.k) = len (T1.k) + len (T2.k) &
len (T.k) = len (T1.k) + len (T2.k) by U1,B221,FINSEQ_1:22;
for i be Nat st i in dom (T.k) holds
ex c be Point of X st c in rng (h1|divset((T.k),i)) &
(Sh1.k).i= (vol divset((T.k),i)) * c
proof
let i be Nat;
assume i in dom (T.k); then
per cases by U1,FINSEQ_1:25;
suppose VC1: i in dom S1; then
VC3: ex c be Point of X st
c in rng (g1|divset(T1.k,i)) &
(F1.k).i= (vol divset(T1.k,i)) * c by INTEGR18:def 1,U1;
VC41: i in dom (F1.k) by VC1,U1,X1,FINSEQ_3:29;
V1: i in Seg len S1 by VC1,FINSEQ_1:def 3;
V6: divset(T1.k,i) = divset(T.k,i) by V1,A95,U1;
divset(T1.k,i) c= AC by V1,U1,A139; then
V4: divset(T1.k,i) c= AB by A17;
(f|AC)|divset(T1.k,i) = f|divset(T1.k,i) by RELAT_1:74,V1,U1,A139;
then g1|divset(T1.k,i) = h1|divset(T.k,i) by C3,C4,V6,RELAT_1:74,V4;
hence thesis by VC3,VC41,B221,FINSEQ_1:def 7,V6;
end;
suppose ex n be Nat st n in dom S2 & i=len S1 + n;
then consider n be Nat such that
C20: n in dom S2 & i=len S1 + n;
VC3: i = len (F1.k) + n
& ex c be Point of X st
c in rng (g2|divset((T2.k),n)) &
(F2.k).n= (vol divset((T2.k),n)) * c by INTEGR18:def 1,U1,C20;
V1: n in dom (F2.k) & n in Seg len S2
by C20,U1,X1,FINSEQ_1:def 3,FINSEQ_3:29;
VC5: divset((T2.k),n) = divset((T.k),i) by C20,V1,A112,U1;
divset((T2.k),n) c= CB by V1,U1,A134; then
V4: divset((T2.k),n) c= AB by A17;
(f|CB) | divset(T2.k,n) = f| divset(T2.k,n) by RELAT_1:74,V1,U1,A134;
then g2|divset(T2.k,n) = h1|divset(T.k,i) by C3,C5,VC5,RELAT_1:74,V4;
hence thesis by VC3,V1,B221,FINSEQ_1:def 7,VC5;
end;
end;
hence Sh1.k is middle_volume of h1,T.k by B226,INTEGR18:def 1;
end;
then reconsider F=Sh1 as middle_volume_Sequence of h1,T by INTEGR18:def 3;
A164:
for i be Nat holds middle_sum(FAB,F.i) =
middle_sum(FAC,(F1.i)) + middle_sum(FCB,(F2.i))
proof
let i be Nat;
i is Element of NAT by ORDINAL1:def 12; then
ex q,q1,q2 being FinSequence of the carrier of X st
q = Sh1.i & q1 =F1.i & q2 =F2.i & q = q1^q2 by B22;
hence middle_sum(FAB,F.i)
= middle_sum(FAC,F1.i) + middle_sum(FCB,F2.i) by RLVECT_1:41;
end;
now let i be Nat;
thus (middle_sum(FAB,F)).i = middle_sum(FAB,F.i) by INTEGR18:def 4
.= middle_sum(FAC,F1.i) + middle_sum(FCB,F2.i) by A164
.= (middle_sum(FAC,F1)).i + middle_sum(FCB,F2.i) by INTEGR18:def 4
.= (middle_sum(FAC,F1)).i + (middle_sum(FCB,F2)).i by INTEGR18:def 4;
end;
then
A165:
middle_sum(FAB,F) = middle_sum(FAC,F1) + middle_sum(FCB,F2)
by NORMSP_1:def 2;
reconsider XAB = chi(AB,AB) as PartFunc of AB,REAL;
reconsider XAC = chi(AC,AC) as PartFunc of AC,REAL;
reconsider XCB = chi(CB,CB) as PartFunc of CB,REAL;
A168:
now let e be Real;
assume 0 < e;
then consider m be Nat such that
A169: for n be Nat st m <= n holds |.delta(PS2).n -0 .| < e
by A25,SEQ_2:def 7;
take m;
hereby let n be Nat;
assume m <=n;
then |.delta(PS2).(n+2) -0 .| < e by A169,NAT_1:12;
then
A171: |.delta(PS2.(n+2)) -0 .| < e by INTEGRA3:def 2;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
ex k being Nat, e1 being Division of CB st k = n1
& e1 =S2.n1 & e1 = PS2.(k+2) by A29;
hence |.delta(S2).n -0 .| < e by A171,INTEGRA3:def 2;
end;
end;
A172:
now let e be Real;
assume
A173: e > 0;
then consider m be Nat such that
A174: for n be Nat st m <=n holds
|. delta(S2).n - 0 .| < e/2 by A168,XREAL_1:215;
take m;
A175: e/2 < e by A173,XREAL_1:216;
let n be Nat;
X1: n in NAT by ORDINAL1:def 12;
assume m <=n; then
|. delta(S2).n - 0 .| < e/2 by A174;
then 0 <= delta(S2.n) & |.delta(S2.n).| < e/2 by X1,INTEGRA3:9,def 2;
then
A177: max rng upper_volume(XCB,S2.n) < e/2 by ABSVALUE:def 1;
reconsider S2n= S2.n as Division of CB;
A178:
for y be Real st y in rng upper_volume(XCB,T2.n) holds y < e
proof
reconsider D=T2.n as Division of CB;
let y be Real;
assume y in rng upper_volume(XCB,T2.n);
then consider x be object such that
A179: x in dom upper_volume(XCB,T2.n)
& y=(upper_volume(XCB,T2.n)).x by FUNCT_1:def 3;
reconsider i=x as Nat by A179;
A181:x in Seg len upper_volume(XCB,T2.n) by A179,FINSEQ_1:def 3;
X1: n in NAT by ORDINAL1:def 12;
then
consider E1 be Division of CB such that
A182: E1=S2.n & 2 <= len E1 by A30;
set i1=i+1;
consider E be Division of CB such that
A184: E=S2.n and
A185: T2.n=E/^1 by A38,X1;
A186:1 <= len E1 by A182,XXREAL_0:2;
then
A187:len D = len E -1 by A184,A185,A182,RFINSEQ:def 1;
A188:len (upper_volume(XCB,T2.n)) = len D by INTEGRA1:def 6;
then
A189:dom (upper_volume(XCB,T2.n)) = dom D by FINSEQ_3:29; then
A203:y=( upper_bound rng(XCB|divset(T2.n,i)) ) * vol divset(T2.n,i)
by A179,INTEGRA1:def 6;
A207:i in dom D by A181,A188,FINSEQ_1:def 3;
A196:1 in dom E & 2 in dom E by A184,A182,A186,FINSEQ_3:25; then
XX2: E.2 = upper_bound divset(S2.n,2)
& E.(2-1) = lower_bound divset(S2.n,2)
& lower_bound CB = lower_bound divset(S2.n,1)
& E.1 = upper_bound divset(S2.n,1) by A184,INTEGRA1:def 4;
XX6: vol divset(S2.n,1) = (upper_volume(XCB,S2.n)).1
& vol divset(S2.n,2) = (upper_volume(XCB,S2.n)).2
by A184,A196,INTEGRA1:20;
XX1: len upper_volume(XCB,S2.n) = len E
& len upper_volume(XCB,S2.n) = len D + 1 by A184,A187,INTEGRA1:def 6;
then 1 <= len upper_volume(XCB,S2.n) by NAT_1:11;
then
1 in dom upper_volume(XCB,S2.n)
& 2 in dom upper_volume(XCB,S2.n) by XX1,A184,A182,FINSEQ_3:25;
then (upper_volume(XCB,S2.n)).1 in rng upper_volume(XCB,S2.n)
& (upper_volume(XCB,S2.n)).2 in rng upper_volume(XCB,S2.n)
by FUNCT_1:def 3;
then (upper_volume(XCB,S2.n)).1 <= max rng upper_volume(XCB,S2.n)
& (upper_volume(XCB,S2.n)).2 <= max rng upper_volume(XCB,S2.n)
by XXREAL_2:def 8;
then
A191:vol divset(S2.n,1) < e/2
& vol divset(S2.n,2) < e/2 by XX6,A177,XXREAL_0:2;
XX4: divset(S2.n,2)
= [. lower_bound divset(S2.n,2), upper_bound divset(S2.n,2) .]
& divset(T2.n,i)
= [. lower_bound divset(T2.n,i), upper_bound divset(T2.n,i) .]
& divset(S2.n,i1)
= [. lower_bound divset(S2.n,i1),upper_bound divset(S2.n,i1) .]
by INTEGRA1:4;
XX5: D.i = E.(i+1) by A184,A185,A182,A186,A207,RFINSEQ:def 1;
A209:dom upper_volume(XCB,S2.n) = dom E by XX1,FINSEQ_3:29;
i1 in Seg len (upper_volume(XCB,S2.n)) by XX1,A181,A188,FINSEQ_1:60;
then
A205:i1 in dom upper_volume(XCB,S2.n) by FINSEQ_1:def 3;
A190:now
assume A192: i=1; then
XX3: lower_bound CB = lower_bound divset(T2.n,1)
& D.1 = upper_bound divset(T2.n,1) by A207,INTEGRA1:def 4;
y =vol divset(T2.n,1) by A179,A189,A192,INTEGRA1:20;
then y = vol divset(S2.n,2) + vol divset(S2.n,1)
by A192,XX3,XX5,XX2;
then y < (e/2)+(e/2) by A191,XREAL_1:8;
hence thesis;
end;
now assume A210: i <> 1; then
XX7: D.(i-1) = lower_bound divset(T2.n,i)
& D.i = upper_bound divset(T2.n,i) by A207,INTEGRA1:def 4;
B211: 1 <= i by A179,FINSEQ_3:25; then
reconsider i9 = i-1 as Nat;
A211: 1 < i by A210,B211,XXREAL_0:1;
then
i9 in Seg len D by A181,A188,FINSEQ_3:12;
then i9 in dom D by FINSEQ_1:def 3; then
XX9: D.(i-1) = E.(i9+1) by A184,A185,A182,A186,RFINSEQ:def 1;
1+1 < i+1 by A211,XREAL_1:8;
then i1 <> 1; then
E.(i1-1) = lower_bound divset(S2.n,i1)
& E.i1 = upper_bound divset(S2.n,i1) by A184,A205,A209,INTEGRA1:def 4;
then
y = (upper_volume(XCB,S2.n)).i1
by XX5,XX4,XX7,XX9,A203,A184,A205,A209,INTEGRA1:def 6;
then y in rng upper_volume(XCB,S2.n) by A205,FUNCT_1:def 3;
then y <= max rng upper_volume(XCB,S2.n) by XXREAL_2:def 8;
then y < e/2 by A177,XXREAL_0:2;
hence thesis by A175,XXREAL_0:2;
end;
hence thesis by A190;
end;
X1: n in NAT by ORDINAL1:def 12;
max rng upper_volume(XCB,T2.n) in rng upper_volume(XCB,T2.n)
by XXREAL_2:def 8;
then 0 <= delta(T2.n) & delta(T2.n) < e by A178,INTEGRA3:9;
then |.delta(T2.n).| < e by ABSVALUE:def 1;
hence |.delta(T2).n-0 .| < e by INTEGRA3:def 2,X1;
end;
then
A215: delta T2 is convergent by SEQ_2:def 6;
then lim delta T2 =0 by A172,SEQ_2:def 7;
then
A217: middle_sum(FCB,F2) is convergent
& lim middle_sum(FCB,F2) = integral FCB by A215,C5,INTEGR18:def 6;
A218:
now let e be Real;
assume A219: 0 < e;
then consider n1 be Nat such that
A220: for m be Nat st n1 <= m holds |.delta(T1).m -0 .| < e
by A53,SEQ_2:def 7;
consider n2 be Nat such that
A221: for m be Nat st n2 <= m holds |.delta(T2).m -0 .| < e by A172,A219;
reconsider n = max(n1,n2) as Nat by TARSKI:1;
take n;
let m be Nat;
assume
A222: n <=m;
X1: m in NAT by ORDINAL1:def 12;
n1 <= n & n2 <= n by XXREAL_0:25;
then n1 <= m & n2 <= m by A222,XXREAL_0:2;
then |.delta(T1).m -0 .| < e & |.delta(T2).m -0 .| < e by A220,A221;
then |.delta(T1.m) .| < e & |.delta(T2.m) .| < e by X1,INTEGRA3:def 2;
then
A224: max rng upper_volume(XCB,T2.m) < e
& max rng upper_volume(XAC,T1.m) < e by ABSVALUE:def 1,INTEGRA3:9;
A227: for r be Real st r in rng upper_volume(XAB,T.m) holds r < e
proof
reconsider Tm=T.m as Division of AB;
let y be Real;
assume y in rng upper_volume(XAB,T.m);
then consider x be object such that
A228:x in dom upper_volume(XAB,T.m)
& y = (upper_volume(XAB,T.m)).x by FUNCT_1:def 3;
reconsider i=x as Nat by A228;
A230:x in Seg len (upper_volume(XAB,T.m)) by A228,FINSEQ_1:def 3;
then
A231:1 <= i by FINSEQ_1:1;
A232:len(upper_volume(XAB,T.m)) =len Tm by INTEGRA1:def 6;
then
A233:i <= len Tm by A230,FINSEQ_1:1;
dom(upper_volume(XAB,T.m)) =dom Tm by A232,FINSEQ_3:29;
then
A234:y=(upper_bound rng(XAB|divset(T.m,i))) * vol divset(T.m,i)
by A228,INTEGRA1:def 6;
consider S1 be Division of AC, S2 be Division of CB such that
A235: S1=(T1.m) & S2=(T2.m) and
A237: T.m = S1^S2 by A93,X1;
A238:len Tm = len S1 + len S2 by A237,FINSEQ_1:22;
per cases;
suppose i <= len S1; then
A239: i in Seg len S1 by A231;
then
A240: i in dom S1 by FINSEQ_1:def 3;
len (upper_volume(XAC,T1.m)) = len S1 by A235,INTEGRA1:def 6; then
A241: dom upper_volume(XAC,T1.m) = dom S1 by FINSEQ_3:29;
A242: divset(T1.m,i) = divset(T.m,i) by X1,A95,A235,A239;
A243: divset(T1.m,i) c= AC by X1,A139,A235,A239;
then divset(T1.m,i) c= AB by A17;
then XAC|divset(T1.m,i) = XAB|divset(T.m,i) by A242,A243,INTEGRA6:4;
then y=(upper_volume(XAC,T1.m)).i by A234,A235,A240,A242,
INTEGRA1:def 6;
then y in rng upper_volume(XAC,T1.m) by A240,A241,FUNCT_1:def 3;
then y <= max rng upper_volume(XAC,T1.m) by XXREAL_2:def 8;
hence thesis by A224,XXREAL_0:2;
end;
suppose i > len S1; then
A244: len S1 + 1 <=i by NAT_1:13;
then consider k be Nat such that
A245: (len S1 + 1)+k=i by NAT_1:10;
set i1=1+k;
A246: i-len S1 <= len S2 by A238,A233,XREAL_1:20;
1+k = i - len S1 by A245;
then 1 <= 1+k by A244,XREAL_1:19;
then
A247: 1+k in Seg len S2 by A245,A246;
then
A248: 1+k in dom S2 by FINSEQ_1:def 3;
A249: divset(T2.m,i1) =divset(T.m,len S1 + i1) by X1,A112,A235,A247;
A250: divset(T2.m,i1) c= CB by X1,A134,A235,A247;
then divset(T2.m,i1) c= AB by A17;
then y=(upper_bound rng(XCB|divset(T2.m,i1))) * vol divset(T2.m,i1)
by A234,A245,A249,A250,INTEGRA6:4;
then
A251: y=(upper_volume(XCB,T2.m)).i1 by A235,A248,INTEGRA1:def 6;
len upper_volume(XCB,T2.m) = len S2 by A235,INTEGRA1:def 6;
then i1 in dom upper_volume(XCB,T2.m) by A247,FINSEQ_1:def 3;
then y in rng upper_volume(XCB,T2.m) by A251,FUNCT_1:def 3;
then y <= max rng upper_volume(XCB,T2.m) by XXREAL_2:def 8;
hence thesis by A224,XXREAL_0:2;
end;
end;
max rng upper_volume(XAB,T.m) in rng upper_volume(XAB,T.m)
by XXREAL_2:def 8;
then delta(T.m) < e by A227;
then |. delta(T.m) .| < e by INTEGRA3:9,ABSVALUE:def 1;
hence |.delta(T).m -0 .| < e by X1,INTEGRA3:def 2;
end;
then
A253: delta T is convergent by SEQ_2:def 6;
then
B255: lim delta(T)=0 by A218,SEQ_2:def 7;
A282: middle_sum(FAC,F1) is convergent
& lim middle_sum(FAC,F1) = integral FAC by A53,C4,INTEGR18:def 6;
integral(f,a,b) = integral(f,AB) by A7,INTEGR18:16
.= integral FAB by A2,C3,INTEGR18:9
.= lim middle_sum(FAB,F) by B255,A253,C3,INTEGR18:def 6;
hence integral(f,a,b) = integral(f,a,c) + integral(f,c,b)
by A57,A165,A282,A217,NORMSP_1:25;
end;
theorem Th1908:
for f be continuous PartFunc of REAL,the carrier of Y
st a <= b & ['a,b'] c= dom f & c in ['a,b'] holds
f is_integrable_on ['a,c'] & f is_integrable_on ['c,b']
& integral(f,a,b) = integral(f,a,c) + integral(f,c,b)
proof
let f be continuous PartFunc of REAL,the carrier of Y;
assume A1: a <= b & ['a,b'] c= dom f & c in ['a,b'];
then ['a,b'] = [.a,b.] by INTEGRA5:def 3; then
A3:a <= c & c <= b by A1,XXREAL_1:1;
hence f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] by A1,Th1909;
['c,b'] c= ['a,b'] by A3,INTEGR19:1; then
A5:['c,b'] c= dom f by A1;
per cases;
suppose A6: b = c; then
A7: ['c,b']= [.c,b.] by INTEGRA5:def 3; then
A91:integral(f,c,b) = integral(f,['c,b'] ) by INTEGR18:16;
['c,b']= [. lower_bound(['c,b']),upper_bound(['c,b']) .] by INTEGRA1:4;
then lower_bound(['c,b']) = c & upper_bound(['c,b']) = b by A7,INTEGRA1:5;
then vol(['c,b']) =0 by A6; then
integral(f,c,b) = 0.Y by A5,A91,INTEGR18:17;
hence thesis by A6;
end;
suppose b <> c;
hence thesis by A1,Lm62;
end;
end;
theorem
for f,g be continuous PartFunc of REAL,the carrier of Y
st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g
holds f+g is_integrable_on ['c,d'] & (f+g) | ['c,d'] is bounded
proof
let f,g be continuous PartFunc of REAL,the carrier of Y;
assume A1: a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g;
reconsider A = ['c,d'] as non empty closed_interval Subset of REAL;
A2:f is_integrable_on A & g is_integrable_on A by A1,Th1909;
A c= dom f & A c= dom g by A1,INTEGR19:2;
hence f+g is_integrable_on ['c,d'] by A2,INTEGR18:14;
a <= d by A1,XXREAL_0:2;
then f | ['a,b'] is bounded & g | ['a,b'] is bounded by A1,Th1,XXREAL_0:2;
then
A3:f| ['c,d'] is bounded & g| ['c,d'] is bounded by A1,Th1915b;
['c,d'] /\ ['c,d'] = ['c,d'];
hence (f + g) | ['c,d'] is bounded by A3,Th1935;
end;
theorem Th1911:
for f be continuous PartFunc of REAL,the carrier of Y
st a <= c & c <= d & d <= b & ['a,b'] c= dom f
holds r(#)f is_integrable_on ['c,d'] & (r(#)f) | ['c,d'] is bounded
proof
let f be continuous PartFunc of REAL,the carrier of Y;
assume A1: a <= c & c <= d & d <= b & ['a,b'] c= dom f;
reconsider A = ['c,d'] as non empty closed_interval Subset of REAL;
A2:f is_integrable_on A by A1,Th1909;
A c= dom f by A1,INTEGR19:2;
hence r(#)f is_integrable_on ['c,d'] by A2,INTEGR18:13;
a <= d by A1,XXREAL_0:2; then
f| ['a,b'] is bounded by A1,Th1,XXREAL_0:2;
then f| ['c,d'] is bounded by A1,Th1915b;
hence (r(#)f) | ['c,d'] is bounded by Th1935a;
end;
theorem
for f be continuous PartFunc of REAL,the carrier of Y
st a <= c & c <= d & d <= b & f is_integrable_on ['a,b']
& f| ['a,b'] is bounded & ['a,b'] c= dom f
holds -f is_integrable_on ['c,d'] & (-f) | ['c,d'] is bounded
proof
let f be continuous PartFunc of REAL,the carrier of Y;
assume A1: a <= c & c <= d & d <= b & f is_integrable_on ['a,b']
& f| ['a,b'] is bounded & ['a,b'] c= dom f;
-f = (-1)(#)f by VFUNCT_1:23;
hence -f is_integrable_on ['c,d'] by A1,Th1911;
f| ['c,d'] is bounded by A1,Th1915b;
hence (-f) | ['c,d'] is bounded by Th1935b;
end;
theorem
for f,g be continuous PartFunc of REAL,the carrier of Y
st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g
holds f-g is_integrable_on ['c,d'] & (f-g) | ['c,d'] is bounded
proof
let f,g be continuous PartFunc of REAL,the carrier of Y;
assume A1: a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g;
then a <= d by XXREAL_0:2;
then
A1X:f is_integrable_on ['a,b'] & g is_integrable_on ['a,b']
& f| ['a,b'] is bounded & g| ['a,b'] is bounded
by A1,Th1,INTEGR20:19,XXREAL_0:2;
reconsider A = ['c,d'] as non empty closed_interval Subset of REAL;
A2:f is_integrable_on A & g is_integrable_on A by A1,Th1909;
A c= dom f & A c= dom g by A1,INTEGR19:2;
hence f - g is_integrable_on ['c,d'] by A2,INTEGR18:15;
A3:f| ['c,d'] is bounded & g| ['c,d'] is bounded by A1,A1X,Th1915b;
['c,d'] /\ ['c,d'] = ['c,d'];
hence (f - g) | ['c,d'] is bounded by A3,Th1935;
end;
Lm8:
for h be Function of A,the carrier of Y, f be Function of A,REAL
st h is bounded & h is integrable & f = ||. h .|| & f is integrable
holds ||.integral h.|| <= integral f
proof
let h be Function of A,the carrier of Y, f be Function of A,REAL;
assume
A1: h is bounded & h is integrable & f = ||. h .|| & f is integrable;
then
A2: f is bounded by Th1914;
consider T be DivSequence of A such that
A3: delta T is convergent & lim delta T = 0 by INTEGRA4:11;
set S = the middle_volume_Sequence of h,T;
A4:dom f = dom h by A1,NORMSP_0:def 3;
defpred P[Element of NAT, set] means
ex p be FinSequence of REAL st
p = $2 & len p = len (T.$1)
& for i be Nat st i in dom (T.$1) holds
p.i in dom (h|divset(T.$1,i))
& ex z be Point of Y st
z = (h|divset(T.$1,i)).(p.i) & (S.$1).i = (vol divset(T.$1,i)) * z;
A5:for k be Element of NAT ex p be Element of (REAL)* st P[k,p]
proof
let k be Element of NAT;
defpred P1[Nat,set] means
$2 in dom (h|divset(T.k,$1))
& ex c be Point of Y st
c = (h|divset(T.k,$1)).$2
& (S.k).$1 = (vol divset(T.k,$1)) * c;
A6: Seg len (T.k) = dom (T.k) by FINSEQ_1:def 3;
A7: for i be Nat st i in Seg len (T.k) ex x be Element of REAL st P1[i,x]
proof
let i be Nat;
assume i in Seg len (T.k); then
i in dom (T.k) by FINSEQ_1:def 3; then
consider c be Point of Y such that
A8: c in rng (h|divset(T.k,i))
& (S.k).i = (vol divset(T.k,i)) * c by INTEGR18:def 1;
consider x be object such that
A9: x in dom (h|divset(T.k,i))
& c = (h|divset(T.k,i)).x by A8,FUNCT_1:def 3;
x in dom h & x in divset(T.k,i) by A9,RELAT_1:57; then
reconsider x as Element of REAL;
take x;
thus thesis by A8,A9;
end;
consider p be FinSequence of REAL such that
A10: dom p = Seg len (T.k)
& for i be Nat st i in Seg len (T.k)
holds P1[i,p.i] from FINSEQ_1:sch 5(A7);
take p;
len p = len (T.k) by A10,FINSEQ_1:def 3;
hence thesis by A10,A6,FINSEQ_1:def 11;
end;
consider F be sequence of (REAL)* such that
A11:for x be Element of NAT holds P[x, F.x] from FUNCT_2:sch 3(A5);
defpred P1[Element of NAT,set] means
ex q be middle_volume of f,T.$1
st q = $2
& for i be Nat st i in dom (T.$1)
ex z be Element of REAL
st (F.$1).i in dom (f|divset(T.$1,i))
& z = (f|divset(T.$1,i)).((F.$1).i)
& q.i = (vol divset(T.$1,i)) * z;
A12:for k be Element of NAT ex y be Element of (REAL)* st P1[k,y]
proof
let k be Element of NAT;
defpred P11[Nat,set] means
ex c be Element of REAL
st (F.k).$1 in dom (f|divset(T.k,$1))
& c = (f|divset(T.k,$1)).((F.k).$1)
& $2 = (vol divset(T.k,$1)) * c;
A13:Seg len (T.k) = dom (T.k) by FINSEQ_1:def 3;
A14:for i be Nat st i in Seg len (T.k) holds
ex x be Element of REAL st P11[i,x]
proof
let i be Nat;
assume i in Seg len (T.k); then
A15: i in dom (T.k) by FINSEQ_1:def 3;
consider p be FinSequence of REAL such that
A16: p = F.k & len p = len (T.k)
& for i be Nat st i in dom (T.k) holds
p.i in dom (h|divset(T.k,i))
& ex z be Point of Y st z = (h|divset(T.k,i)).(p.i)
& (S.k).i = (vol divset(T.k,i)) * z by A11;
p.i in dom (h|divset((T.k),i)) by A15,A16; then
A171:p.i in dom h & p.i in divset(T.k,i) by RELAT_1:57;
(vol divset(T.k,i)) * (f|divset(T.k,i)).(p.i) in REAL
& (f|divset(T.k,i)).(p.i) in REAL by XREAL_0:def 1;
hence thesis by A16,A171,A4,RELAT_1:57;
end;
consider q be FinSequence of REAL such that
A18: dom q = Seg len (T.k)
& for i be Nat st i in Seg len (T.k) holds P11[i,q.i]
from FINSEQ_1:sch 5(A14);
A19:len q = len (T.k) by A18,FINSEQ_1:def 3;
now let i be Nat;
assume i in dom (T.k); then
i in Seg len (T.k) by FINSEQ_1:def 3; then
ex c be Element of REAL st (F.k).i in dom (f|divset(T.k,i))
& c = (f|divset(T.k,i)).((F.k).i) & q.i = (vol divset(T.k,i)) * c by A18;
hence ex c be Element of REAL st c in rng (f|divset(T.k,i)) &
q.i = c*(vol divset(T.k,i)) by FUNCT_1:3;
end; then
reconsider q as middle_volume of f,T.k by A19,INTEGR15:def 1;
q is Element of (REAL)* by FINSEQ_1:def 11;
hence thesis by A13,A18;
end;
consider Sf be sequence of (REAL)* such that
A21:for x be Element of NAT holds P1[x, Sf.x] from FUNCT_2:sch 3(A12);
now let k be Element of NAT;
ex q be middle_volume of f,T.k st q = Sf.k
& for i be Nat st i in dom (T.k) holds
ex z be Element of REAL st
(F.k).i in dom (f|divset(T.k,i))
& z = (f|divset(T.k,i)).((F.k).i)
& q.i = (vol divset(T.k,i)) * z by A21;
hence Sf.k is middle_volume of f,T.k;
end; then
reconsider Sf as middle_volume_Sequence of f,T by INTEGR15:def 3;
A22: middle_sum(f,Sf) is convergent & lim (middle_sum(f,Sf)) = integral f
by A1,A2,A3,INTEGR15:9;
A23: middle_sum(h,S) is convergent & lim (middle_sum(h,S)) = integral h
by A1,A3,INTEGR18:def 6;
A24: for k be Element of NAT holds
||. (middle_sum(h,S)).k .|| <= (middle_sum(f,Sf)).k
proof
let k be Element of NAT;
A25:(middle_sum(f,Sf)).k = middle_sum(f,Sf.k) by INTEGR15:def 4;
A28:ex p be FinSequence of REAL st
p = F.k & len p = len (T.k)
& for i be Nat st i in dom (T.k) holds
p.i in dom (h|divset(T.k,i))
& ex z be Point of Y st z = (h|divset(T.k,i)).(p.i)
& (S.k).i = (vol divset(T.k,i)) * z by A11;
A29:ex q be middle_volume of f,T.k st
q = Sf.k
& for i be Nat st i in dom (T.k) holds
ex z be Element of REAL st
(F.k).i in dom (f|divset(T.k,i))
& z = (f|divset(T.k,i)).((F.k).i)
& q.i = (vol divset(T.k,i)) * z by A21;
A30:len (Sf.k) = len(T.k) by INTEGR15:def 1;
A31:len(S.k) = len(T.k) by INTEGR18:def 1;
now let i be Nat;
assume A32: i in dom (S.k); then
i in Seg len (T.k) by A31,FINSEQ_1:def 3; then
A34: i in dom (T.k) by FINSEQ_1:def 3; then
A36: (F.k).i in dom (h|divset(T.k,i)) by A28;
consider z be Point of Y such that
A37: z = (h|divset(T.k,i)).((F.k).i)
& (S.k).i = (vol divset(T.k,i)) *z by A28,A34;
A38: ex w be Element of REAL st
(F.k).i in dom (f|divset(T.k,i))
& w = (f|divset(T.k,i)).((F.k).i)
& (Sf.k).i = (vol divset(T.k,i)) * w by A29,A34;
(S.k).i = (S.k)/.i by A32,PARTFUN1:def 6; then
A41: ||. (S.k)/.i .||
= |.vol divset(T.k,i).| *||.z.|| by A37,NORMSP_1:def 1
.= (vol divset(T.k,i)) *||.z.|| by INTEGRA1:9,ABSVALUE:def 1;
A42: dom (h|divset(T.k,i)) c= dom h
& dom (f|divset(T.k,i)) c= dom f by RELAT_1:60;
A43: (h|divset(T.k,i)).((F.k).i) = h.((F.k).i) by A36,FUNCT_1:47;
(f|divset(T.k,i)).((F.k).i) = f.((F.k).i) by A38,FUNCT_1:47
.= ||. h/.((F.k).i) .|| by A42,A1,A38,NORMSP_0:def 2;
hence ||. (S.k)/.i .|| <= (Sf.k).i
by A41,A43,A38,A37,A42,A36,PARTFUN1:def 6;
end;
then ||. middle_sum(h,S.k) .|| <= Sum(Sf.k) by A30,A31,INTEGR20:10;
hence thesis by A25,INTEGR18:def 4;
end;
A45:
now let i be Nat;
XX: i in NAT by ORDINAL1:def 12;
||. middle_sum(h,S) .|| .i = ||. (middle_sum(h,S)).i .||
by NORMSP_0:def 4;
hence ||. middle_sum(h,S).|| .i <= (middle_sum(f,Sf)).i by A24,XX;
end;
||. middle_sum(h,S).|| is convergent by A1,A3,NORMSP_1:23;
then lim ||. middle_sum(h,S).|| <= lim middle_sum(f,Sf) by A45,A22,SEQ_2:18;
hence thesis by A22,A23,LOPBAN_1:41;
end;
theorem Th1920:
for f be PartFunc of REAL,the carrier of Y
st A c= dom f & f|A is bounded & f is_integrable_on A
& ||.f.|| is_integrable_on A
holds ||.integral(f,A).|| <= integral(||.f.||,A)
proof
let f be PartFunc of REAL,the carrier of Y;
assume A1: A c= dom f & f|A is bounded & f is_integrable_on A
& ||.f.|| is_integrable_on A;
set g = ||.f.||;
reconsider fA = f|A as Function of A,the carrier of Y by A1;
A2:integral(f,A) = integral fA by A1,INTEGR18:9;
A c= dom g by A1,NORMSP_0:def 2; then
reconsider gA = g|A as Function of A,REAL by Lm3;
A3:gA is integrable by A1;
fA is bounded & ||. fA .|| = g|A by Th1918,A1;
hence thesis by A2,A3,A1,Lm8;
end;
theorem Th1921:
for f be PartFunc of REAL,the carrier of Y
st a<=b & ['a,b'] c= dom f & f is_integrable_on ['a,b']
& ||.f.|| is_integrable_on ['a,b'] & f| ['a ,b'] is bounded
holds ||.integral(f,a,b).|| <= integral(||.f.||,a,b)
proof
let f be PartFunc of REAL,the carrier of Y;
assume A1: a<=b & ['a,b'] c= dom f & f is_integrable_on ['a,b']
& ||.f.|| is_integrable_on ['a,b'] & f| ['a ,b'] is bounded;
['a,b'] = [.a,b.] by A1,INTEGRA5:def 3; then
A3:integral(f,a,b) = integral(f,['a,b']) by INTEGR18:16;
integral(||.f.||,a,b) = integral (||.f.||,['a,b']) by A1,INTEGRA5:def 4;
hence thesis by Th1920,A1,A3;
end;
Lm10:
for f be continuous PartFunc of REAL,the carrier of Y
st a <= b & c <=d & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b']
holds f is_integrable_on ['c,d'] & ||.f.|| is_integrable_on ['c,d']
& ||.f.|| | ['c,d'] is bounded
& ||. integral(f,c,d) .|| <= integral(||.f.||,c,d)
proof
let f be continuous PartFunc of REAL,the carrier of Y;
assume that
A1: a <= b & c <= d and
A2: ['a,b'] c= dom f and
A4: c in ['a,b'] & d in ['a,b'];
A3:f is_integrable_on ['a,b'] & ||.f.|| is_integrable_on ['a,b']
& f| ['a,b'] is bounded by Th1,INTEGR20:19,Th4,A1,A2;
['a,b'] = [.a,b.] by A1,INTEGRA5:def 3; then
A5:a <= c & d <= b by A4,XXREAL_1:1; then
A6:f|['c,d'] is bounded by A1,A2,A3,Th1915b;
A7:['c,d'] c= dom f & f is_integrable_on ['c,d'] by A1,A2,A5,Th1909,INTEGR19:2;
A8:['a,b'] c= dom ||.f.|| by A2,NORMSP_0:def 2;
||.f.|| | ['a,b'] is bounded by Th3,A1,A2;
then ['c,d'] c= dom ||.f.|| & ||.f.|| is_integrable_on ['c,d']
by A1,A3,A5,A8,INTEGRA6:18;
hence thesis by A1,A7,Th1921,A6,Th1919;
end;
theorem Th1922:
for f be continuous PartFunc of REAL,the carrier of Y
st a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b']
holds ||.f.|| is_integrable_on ['min(c,d),max(c,d)']
& ||.f.|| | ['min(c,d),max(c,d)'] is bounded
& ||. integral(f,c,d) .|| <= integral(||.f.||,min(c,d),max(c,d))
proof
let f be continuous PartFunc of REAL,the carrier of Y;
assume A1: a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'];
per cases;
suppose A3: not c <= d; then
A5: d = min(c,d) & c = max(c,d) by XXREAL_0:def 9,def 10; then
['d,c'] c= dom f by A1,INTEGR19:3; then
integral(f,c,d) = -integral(f,d,c) by A3,Th1947; then
||. integral(f,c,d) .|| = ||.integral(f,d,c).|| by NORMSP_1:2;
hence thesis by A1,A3,A5,Lm10;
end;
suppose A6: c <= d; then
c = min(c,d) & d = max(c,d) by XXREAL_0:def 9,def 10;
hence thesis by A1,A6,Lm10;
end;
end;
Th1925a:
for f be continuous PartFunc of REAL,the carrier of Y
st a <= b & c <= d & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b']
holds integral(r(#)f,c,d) = r*integral(f,c,d)
proof
let f be continuous PartFunc of REAL,the carrier of Y;
assume A1: a <= b & c <= d & ['a,b'] c= dom f
& c in ['a,b'] & d in ['a,b']; then
['a,b'] = [.a,b.] by INTEGRA5:def 3; then
A2:a <= c & c <= b & a <= d & d <= b by A1,XXREAL_1:1;
reconsider A = ['c,d'] as non empty closed_interval Subset of REAL;
c = min(c,d) & d = max(c,d) by A1,XXREAL_0:def 9,def 10; then
['c,d'] c= ['a,b'] by A1,Lm2; then
A4:f is_integrable_on A & A c= dom f by A1,A2,Th1909;
integral(r(#)f,A) = integral(r(#)f,c,d)
& integral(f,A) = integral(f,c,d) by A1,INTEGR18:def 9;
hence integral(r(#)f,c,d) = r*integral(f,c,d) by A4,INTEGR18:13;
end;
theorem Th1925:
for f be continuous PartFunc of REAL,the carrier of Y
st a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b']
holds integral(r(#)f,c,d) = r*integral(f,c,d)
proof
let f be continuous PartFunc of REAL,the carrier of Y;
assume A1: a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'];
per cases;
suppose A2: not c <= d;
reconsider A = ['d,c'] as non empty closed_interval Subset of REAL;
d = min(c,d) & c = max(c,d) by A2,XXREAL_0:def 9,def 10; then
['d,c'] c= ['a,b'] by A1,Lm2; then
A7: A c= dom f by A1; then
A c= dom(r(#)f) by VFUNCT_1:def 4; then
A8: -integral(r(#)f,d,c) = integral(r(#)f,c,d)
& -integral(f,d,c) = integral(f,c,d) by A2,A7,Th1947;
integral(r(#)f,d,c) = r*integral(f,d,c) by A1,A2,Th1925a;
hence integral(r(#)f,c,d) = r*integral(f,c,d) by A8,RLVECT_1:25;
end;
suppose c <= d;
hence thesis by A1,Th1925a;
end;
end;
theorem
for f be continuous PartFunc of REAL,the carrier of Y
st a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b']
holds integral(-f,c,d) = -integral(f,c,d)
proof
let f be continuous PartFunc of REAL,the carrier of Y;
assume A1: a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'];
A2:-f = (-1)(#)f by VFUNCT_1:23;
(-1)*integral(f,c,d)=-integral(f,c,d) by RLVECT_1:16;
hence thesis by A1,A2,Th1925;
end;
theorem
for f be continuous PartFunc of REAL,the carrier of Y
st ( a<=b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b']
& for x be Real st x in ['min(c,d),max(c,d)']
holds ||. f/.x .|| <= e )
holds ||.integral(f,c,d).|| <= e * |.d-c.|
proof
let f be continuous PartFunc of REAL,the carrier of Y;
set A = ['min(c,d),max(c,d)'];
assume that
A1: a<=b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] and
A2: for x be Real st x in A holds ||. f/.x .|| <= e;
rng ||.f.|| c= REAL; then
A3: ||.f.|| is Function of dom ||.f.||,REAL by FUNCT_2:2;
B1:A c= ['a,b'] by A1,Lm2;
B2:dom ||.f.|| = dom f by NORMSP_0:def 2; then
A c= dom ||.f.|| by A1,B1;
then reconsider g =(||.f.||)| A as Function of A,REAL by A3,FUNCT_2:32;
A4:vol A = |.d-c.| by INTEGRA6:6;
A5: ||.f.|| is_integrable_on A & g|A is bounded
& ||.integral(f,c,d).|| <= integral(||.f.||,min(c,d),max(c,d)) by A1,Th1922;
consider h be Function of A,REAL such that
A6: rng h = {e} and
A7: h|A is bounded by INTEGRA4:5;
A8:now let x be Real;
assume
A9: x in A; then
g.x = ||.f.||.x by FUNCT_1:49;
then
A10:g.x = ||. f/.x .|| by A9,B2,A1,B1,NORMSP_0:def 2;
h.x in {e} by A6,A9,FUNCT_2:4;
then h.x =e by TARSKI:def 1;
hence g.x <= h.x by A2,A9,A10;
end;
min(c,d) <= c & c <= max(c,d) by XXREAL_0:17,25; then
A12: integral(||.f.||,min(c,d),max(c,d)) = integral(||.f.||,A)
by INTEGRA5:def 4,XXREAL_0:2;
h is integrable & integral h = e*vol A by A6,INTEGRA4:4;
then integral(||.f.||,min(c,d),max(c,d)) <= e * |.d-c.|
by A12,A7,A8,A5,A4,INTEGRA2:34;
hence thesis by A5,XXREAL_0:2;
end;
Th1928:
for f,g be continuous PartFunc of REAL,the carrier of Y
st a <= b & c <= d & ['a,b'] c= dom f & ['a,b'] c= dom g
& c in ['a,b'] & d in ['a,b']
holds
integral(f-g,c,d) = integral(f,c,d) - integral(g,c,d)
proof
let f,g be continuous PartFunc of REAL,the carrier of Y;
assume A1: a <= b & c <= d & ['a,b'] c= dom f & ['a,b'] c= dom g
& c in ['a,b'] & d in ['a,b'];
reconsider A = ['c,d'] as non empty closed_interval Subset of REAL;
['a,b'] = [.a,b.] by A1,INTEGRA5:def 3; then
a <= c & c <= b & a <= d & d <= b by A1,XXREAL_1:1; then
A4:f is_integrable_on A & g is_integrable_on A by A1,Th1909;
c = min(c,d) & d = max(c,d) by A1,XXREAL_0:def 9,def 10; then
['c,d'] c= ['a,b'] by A1,Lm2; then
A5:A c= dom f & A c= dom g by A1;
integral(f-g,A)=integral(f-g,c,d) & integral(f,A)=integral(f,c,d)
& integral(g,A)=integral(g,c,d) by A1,INTEGR18:def 9;
hence thesis by A5,A4,INTEGR18:15;
end;
theorem Th404:
for Y be RealNormSpace,
A be non empty closed_interval Subset of REAL,
f be Function of A,the carrier of Y,
E be Point of Y
st rng f = {E} holds f is integrable & integral f = (vol A) * E
proof
let Y be RealNormSpace;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,the carrier of Y;
let E be Point of Y;
assume AS1: rng f = {E};
reconsider I = (vol A) * E as Point of Y;
P1:for T being DivSequence of A,
S be middle_volume_Sequence of f,T st
delta T is convergent & lim delta T = 0 holds
middle_sum(f,S) is convergent & lim middle_sum(f,S) = I
proof
let T be DivSequence of A,
S be middle_volume_Sequence of f,T;
assume delta T is convergent & lim delta T = 0;
set s = middle_sum(f,S);
A1: for k being Nat holds s.k = I
proof
let k be Nat;
defpred P11[Nat,set] means $2 = vol divset(T.k,$1);
A14: for i be Nat st i in Seg len (T.k) holds
ex x be Element of REAL st P11[i,x]
proof
let i be Nat;
assume i in Seg len (T.k);
vol divset(T.k,i) in REAL by XREAL_0:def 1;
hence thesis;
end;
consider q be FinSequence of REAL such that
A18: dom q = Seg len (T.k)
& for i be Nat st i in Seg len (T.k) holds P11[i,q.i]
from FINSEQ_1:sch 5(A14);
B7: Sum q = vol A by INTEGR20:6,A18;
len q = len (T.k) by A18,FINSEQ_1:def 3; then
B8: len (S.k) = len q by INTEGR18:def 1;
B40: for i be Nat st i in dom (S.k) holds
ex r be Real st r =q.i & (S.k).i= r * E
proof
let i be Nat;
assume i in dom (S.k); then
i in Seg len (S.k) by FINSEQ_1:def 3; then
B44: i in Seg len (T.k) by INTEGR18:def 1; then
i in dom (T.k) by FINSEQ_1:def 3; then
consider c be Point of Y such that
B42: c in rng (f|divset(T.k,i))
& (S.k).i= (vol divset(T.k,i)) * c by INTEGR18:def 1;
c in rng f by B42,TARSKI:def 3,RELAT_1:70; then
B43: c = E by AS1,TARSKI:def 1;
q.i = vol divset(T.k,i) by A18,B44;
hence thesis by B42,B43;
end;
s.k = middle_sum(f,S.k) by INTEGR18:def 4;
hence thesis by B40,B7,B8,INTEGR20:7;
end;
A2: now let p be Real;
assume A3: 0<p;
reconsider k = 0 as Nat;
take k;
let n be Nat such that k<=n;
thus ||.s.n - I.|| < p by A3,NORMSP_1:6,A1;
end;
hence s is convergent;
hence thesis by A2,NORMSP_1:def 7;
end;
hence f is integrable;
hence integral f = (vol A) * E by P1,INTEGR18:def 6;
end;
theorem Th1929:
for f be PartFunc of REAL,the carrier of Y, E be Point of Y
st ( a <= b & ['a,b'] c= dom f
& for x be Real st x in ['a,b'] holds f/.x = E ) holds
f is_integrable_on ['a,b'] & integral(f,a,b) = (b-a)*E
proof
let f be PartFunc of REAL,the carrier of Y, E be Point of Y;
assume that
A1: a <= b and
A2: ['a,b'] c= dom f and
A3: for x be Real st x in ['a,b'] holds f/.x = E;
reconsider A=['a,b'] as non empty closed_interval Subset of REAL;
f is Function of dom f, rng f by FUNCT_2:1; then
f is Function of dom f,the carrier of Y by FUNCT_2:2; then
reconsider g=f|A as Function of A,the carrier of Y by A2,FUNCT_2:32;
A7:{E} c= rng g
proof
let x be object;
assume x in {E}; then
A5: x = E by TARSKI:def 1;
consider a being Element of A such that
A6: a in dom g by SUBSET_1:4;
f/.a = E by A3; then
f.a = E by A2,PARTFUN1:def 6; then
g.a = E by FUNCT_1:49;
hence thesis by A5,A6,FUNCT_1:3;
end;
rng g c= {E}
proof
let x be object;
assume x in rng g;
then consider a being Element of A such that
a in dom g and
A9: g.a=x by PARTFUN1:3;
f.a=x by A9,FUNCT_1:49; then
f/.a=x by A2,PARTFUN1:def 6; then
x = E by A3;
hence x in {E} by TARSKI:def 1;
end; then
A10:rng g = {E} by A7,XBOOLE_0:def 10;
hence f is_integrable_on ['a,b'] by Th404;
integral g = (vol A) * E by A10,Th404; then
integral(f,A) = (vol A) * E by A2,INTEGR18:def 8; then
integral(f,A) = (b-a)*E by A1,INTEGRA6:5;
hence integral(f,a,b) = (b-a)*E by A1,INTEGR18:def 9;
end;
theorem
for f be PartFunc of REAL,the carrier of Y
st a <= b & c in ['a,b'] & d in ['a,b'] & ['a,b'] c= dom f
& for x be Real st x in ['a,b'] holds f/.x = E
holds integral(f,c,d) = (d-c)*E
proof
let f be PartFunc of REAL,the carrier of Y;
assume that
A1: a <= b & c in ['a,b'] & d in ['a,b'] and
A3: ['a,b'] c= dom f & for x be Real st x in ['a,b'] holds f/.x = E;
per cases;
suppose A5: c <= d; then
c = min(c,d) & d = max(c,d) by XXREAL_0:def 9,def 10; then
['c,d'] c= ['a,b'] by A1,Lm2; then
['c,d'] c= dom f & for x be Real st x in ['c,d'] holds f/.x = E by A3;
hence integral(f,c,d) = (d-c)*E by A5,Th1929;
end;
suppose A8: not c <= d; then
d = min(c,d) & c = max(c,d) by XXREAL_0:def 9,def 10; then
['d,c'] c= ['a,b'] by A1,Lm2; then
A10:['d,c'] c= dom f & for x be Real st x in ['d,c'] holds f/.x = E by A3; then
integral(f,c,d) = -integral(f,d,c) by A8,Th1947; then
integral(f,c,d) = -(c-d)*E by A8,A10,Th1929; then
integral(f,c,d) = (-(c-d))*E by RLVECT_1:79;
hence integral(f,c,d) = (d-c)*E;
end;
end;
Th1931:
for f be continuous PartFunc of REAL,the carrier of Y st
a <= b & c <= d & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral(f,a,d) = integral(f,a,c) + integral(f,c,d)
proof
let f be continuous PartFunc of REAL,the carrier of Y;
assume A1: a <= b & c <= d & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'];
['a,b'] = [.a,b.] by A1,INTEGRA5:def 3; then
A2:a <= c & c <= b & a <= d & d <= b by A1,XXREAL_1:1; then
A3:['a,d'] c= ['a,b'] & c in ['a,d'] by A1,INTEGR19:1; then
['a,d'] c= dom f by A1;
hence integral(f,a,d) = integral(f,a,c) + integral(f,c,d) by A2,A3,Th1908;
end;
theorem
for f be continuous PartFunc of REAL,the carrier of Y
st a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral(f,a,d) = integral(f,a,c) + integral(f,c,d)
proof
let f be continuous PartFunc of REAL,the carrier of Y;
assume A1: a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'];
per cases;
suppose A2: not c <= d;
['a,b'] = [.a,b.] by A1,INTEGRA5:def 3; then
c <= b & a <= d by A1,XXREAL_1:1; then
A3: ['d,c'] c= dom f by A1,A2,INTEGR19:2;
integral(f,a,c) = integral(f,a,d) + integral(f,d,c) by A1,A2,Th1931; then
integral(f,a,c) - integral(f,d,c)
= integral(f,a,d) + (integral(f,d,c) - integral(f,d,c)) by RLVECT_1:28
.= integral(f,a,d) + 0.Y by RLVECT_1:15;
hence thesis by A3,A2,Th1947;
end;
suppose c <= d;
hence thesis by A1,Th1931;
end;
end;
theorem
for f,g be continuous PartFunc of REAL,the carrier of Y
st a <= b & ['a,b'] c= dom f & ['a,b'] c= dom g
& c in ['a,b'] & d in ['a,b']
holds integral(f-g,c,d) = integral(f,c,d) - integral(g,c,d)
proof
let f,g be continuous PartFunc of REAL,the carrier of Y;
assume A1: a <= b & ['a,b'] c= dom f & ['a,b'] c= dom g
& c in ['a,b'] & d in ['a,b'];
per cases;
suppose A2: not c <= d; then
d = min(c,d) & c = max(c,d) by XXREAL_0:def 9,def 10; then
['d,c'] c= ['a,b'] by A1,Lm2; then
A7: ['d,c'] c= dom f & ['d,c'] c= dom g by A1; then
['d,c'] c= dom f /\ dom g by XBOOLE_1:19; then
['d,c'] c= dom(f-g) by VFUNCT_1:def 2; then
A11:integral(f-g,c,d) = -integral(f-g,d,c)
& integral(f,c,d) = -integral(f,d,c)
& integral(g,c,d) = -integral(g,d,c) by A2,A7,Th1947;
integral(f-g,d,c) = integral(f,d,c) - integral(g,d,c)
by A1,A2,Th1928; then
integral(f-g,c,d) = integral(g,d,c) + integral(f,c,d) by A11,RLVECT_1:33;
hence thesis by A11;
end;
suppose c <= d;
hence thesis by A1,Th1928;
end;
end;