:: Relationship between the {R}iemann and {L}ebesgue Integrals
:: by Noboru Endou
::
:: Received September 30, 2021
:: Copyright (c) 2021-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 FUNCT_1, NUMBERS, SUBSET_1, SUPINF_2, ARYTM_3, CARD_1, RELAT_1,
TARSKI, ORDINAL2, XXREAL_0, NAT_1, XXREAL_2, ORDINAL1, XBOOLE_0,
FUNCOP_1, MEASURE5, SUPINF_1, REAL_1, PROB_1, MEASURE1, MEASURE7,
XCMPLX_0, XXREAL_1, ARYTM_1, CARD_3, FINSEQ_1, ORDINAL4, VALUED_0,
MESFUNC5, SEQ_2, NEWTON, COMPLEX1, SEQ_1, MEASURE3, REWRITE1, MEASUR12,
PARTFUN1, INTEGRA1, INTEGRA2, INTEGRA4, MEMBERED, MESFUNC8, INTEGRA5,
REALSET1, MESFUNC1, MEASURE6, SEQ_4, SEQFUNC, MESFUNC2, RFUNCT_3,
MESFUNC3, FINSEQ_2, PBOOLE, MESFUN10, MESFUN14, FUNCT_3, FDIFF_1, POWER,
VALUED_1, MEASURE2, LPSPACE1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, SEQ_1, FUNCOP_1, FUNCT_1,
RELSET_1, PARTFUN1, VALUED_1, FINSEQ_1, FINSEQ_2, RVSUM_1, SEQ_2, SEQ_4,
VALUED_0, FUNCT_2, XXREAL_2, XXREAL_1, XXREAL_0, MEMBERED, MEASURE3,
XXREAL_3, XCMPLX_0, EXTREAL1, COMPLEX1, XREAL_0, NUMBERS, MEASURE2,
SUPINF_1, RFUNCT_3, RINFSUP2, SUPINF_2, NAT_1, RCOMP_1, MEASURE1,
MEASURE5, MESFUNC1, MESFUNC2, MESFUNC3, MESFUNC6, MESFUNC5, MESFUNC8,
MESFUN10, PROB_1, NAT_D, PROB_3, NEWTON, MEASUR12, INTEGRA1, INTEGRA2,
POWER, RFUNCT_1, FDIFF_1, INTEGRA3, INTEGRA4, INTEGRA5, SEQFUNC,
LPSPACE1;
constructors SUPINF_1, MEASURE6, EXTREAL1, PROB_3, RVSUM_1, FINSEQOP,
MEASUR11, SEQ_4, NEWTON, COMSEQ_2, MEASUR12, INTEGRA2, INTEGRA4,
INTEGRA5, NAT_D, MESFUNC6, MESFUNC2, SEQFUNC, MESFUNC3, MESFUNC8,
MESFUN10, RINFSUP2, INTEGRA3, FDIFF_1, LPSPACE1, PROB_4;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0,
MEMBERED, MEASURE1, VALUED_0, XXREAL_2, RELSET_1, MEASURE5, NAT_1,
FINSEQ_1, RELAT_1, FINSET_1, XXREAL_0, CARD_1, XXREAL_1, ZFMISC_1,
FUNCOP_1, XXREAL_3, MEASURE3, MEASUR12, INTEGRA1, PARTFUN1, SEQ_4,
NEWTON, SEQM_3, MESFUNC8;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
expansions TARSKI;
theorems TARSKI, SUPINF_2, MEASURE1, FUNCT_1, MEASURE5, ZFMISC_1, FUNCT_2,
NAT_1, XBOOLE_0, XBOOLE_1, FUNCOP_1, XXREAL_0, ORDINAL1, XXREAL_2,
XXREAL_3, MEASURE7, XXREAL_1, MESFUNC5, MESFUNC9, RINFSUP2, XREAL_1,
MEASUR10, XREAL_0, VALUED_0, FINSEQ_1, PARTFUN1, FINSEQ_3, EXTREAL1,
MESFUNC3, RVSUM_1, RELAT_1, FINSEQ_2, PROB_2, XCMPLX_1, SERIES_1, NEWTON,
NUMBERS, MEASURE3, MEASUR12, MESFUNC6, MESFUNC1, INTEGRA5, INTEGRA1,
INTEGRA4, EUCLID_7, NAT_D, RFUNCT_1, SEQ_4, MESFUNC2, MESFUNC4, MESFUN11,
SUBSET_1, VALUED_1, MESFUN10, MESFUNC8, PREPOWER, PEPIN, SEQ_2, ABSVALUE,
XCMPLX_0, INTEGRA3, FDIFF_1, POWER, SEQ_1, RELSET_1, MESFUN13, MEASURE2,
LPSPACE1, INTEGRA2, FINSUB_1, MESFUN12, MESFUNC7, FUNCT_3, RFUNCT_3;
schemes FUNCT_2, NAT_1, SEQ_1, FINSEQ_1, PARTFUN1;
begin :: Preliminaries
Lm1:
for a1,b1 be Real, a2,b2 be R_eal st
a1=a2 & b1=b2 holds a1-b1 = a2-b2
proof
let a1,b1 be Real, a2, b2 be R_eal;
assume A1: a1=a2 & b1=b2;
a2-b2 = a2+(-b2) by XXREAL_3:def 4; then
a2-b2 = a2+(-b1) by A1,XXREAL_3:def 3; then
a2-b2 = a1+(-b1) by A1,XXREAL_3:def 2;
hence thesis;
end;
theorem Th1:
for X be non empty set, f be PartFunc of X,ExtREAL holds
rng max+f c= rng f \/ {0} & rng max-f c= rng (-f) \/ {0}
proof
let X be non empty set, f be PartFunc of X,ExtREAL;
now let y be object;
assume y in rng max+f; then
consider x be Element of X such that
A1: x in dom max+f & y = (max+f).x by PARTFUN1:3;
A2: x in dom f by A1,MESFUNC2:def 2;
A3: y = max(f.x,0) by A1,MESFUNC2:def 2;
per cases by A3,XXREAL_0:16;
suppose y = f.x; then
y in rng f by A2,FUNCT_1:3;
hence y in rng f \/ {0} by XBOOLE_0:def 3;
end;
suppose y = 0; then
y in {0} by TARSKI:def 1;
hence y in rng f \/ {0} by XBOOLE_0:def 3;
end;
end;
hence rng max+f c= rng f \/ {0};
now let y be object;
assume y in rng max-f; then
consider x be Element of X such that
A4: x in dom max-f & y = (max-f).x by PARTFUN1:3;
x in dom f by A4,MESFUNC2:def 3; then
A5: x in dom(-f) by MESFUNC1:def 7;
y = max(-(f.x),0) by A4,MESFUNC2:def 3; then
per cases by XXREAL_0:16;
suppose y = -(f.x); then
y = (-f).x by A5,MESFUNC1:def 7; then
y in rng (-f) by A5,FUNCT_1:3;
hence y in rng (-f) \/ {0} by XBOOLE_0:def 3;
end;
suppose y = 0; then
y in {0} by TARSKI:def 1;
hence y in rng (-f) \/ {0} by XBOOLE_0:def 3;
end;
end;
hence rng max-f c= rng (-f) \/ {0};
end;
theorem Th2:
for X be non empty set, f be PartFunc of X,ExtREAL st f is real-valued
holds -f is real-valued & max+f is real-valued & max-f is real-valued
proof
let X be non empty set, f be PartFunc of X,ExtREAL;
assume f is real-valued; then
A1: rng f c= REAL by VALUED_0:def 3;
now let y be object;
assume y in rng(-f); then
consider x be Element of X such that
A2: x in dom(-f) & y = (-f).x by PARTFUN1:3;
x in dom f by A2,MESFUNC1:def 7; then
A3: f.x in REAL by A1,FUNCT_1:3;
y = -(f.x) by A2,MESFUNC1:def 7;
hence y in REAL by A3,XREAL_0:def 1;
end; then
A4: rng(-f) c= REAL;
hence -f is real-valued by VALUED_0:def 3;
A5: rng f \/ {0} c= REAL by A1,XBOOLE_1:8;
rng max+f c= rng f \/ {0} by Th1; then
rng max+f c= REAL by A5;
hence max+f is real-valued by VALUED_0:def 3;
A6: rng(-f) \/ {0} c= REAL by A4,XBOOLE_1:8;
rng max-f c= rng(-f) \/ {0} by Th1; then
rng max-f c= REAL by A6;
hence max-f is real-valued by VALUED_0:def 3;
end;
theorem Th3:
for X be non empty set, f be PartFunc of X,ExtREAL st
f is without-infty without+infty holds f is PartFunc of X,REAL
proof
let X be non empty set, f be PartFunc of X,ExtREAL;
assume f is without-infty without+infty; then
not -infty in rng f & not +infty in rng f by MESFUNC5:def 3,def 4; then
rng f c= REAL by XXREAL_0:14;
hence f is PartFunc of X,REAL by RELSET_1:6;
end;
theorem Th4:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL st f is_simple_func_in S holds
max+f is_simple_func_in S & max-f is_simple_func_in S
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL;
assume A1: f is_simple_func_in S; then
A2: f is real-valued by MESFUNC2:def 4;
consider F be Finite_Sep_Sequence of S such that
A3: dom f = union rng F and
A4: for n be Nat, x,y be Element of X st n in dom F & x in F.n & y in F.n
holds f.x = f.y by A1,MESFUNC2:def 4;
A5: dom max+f = union rng F by A3,MESFUNC2:def 2;
for n be Nat, x,y be Element of X st n in dom F & x in F.n & y in F.n
holds (max+f).x = (max+f).y
proof
let n be Nat, x,y be Element of X;
assume that
A6: n in dom F and
A7: x in F.n and
A8: y in F.n;
F.n in rng F by A6,FUNCT_1:3; then
x in dom max+f & y in dom max+f by A5,A7,A8,TARSKI:def 4; then
(max+f).x = max(f.x,0) & (max+f).y = max(f.y,0) by MESFUNC2:def 2;
hence (max+f).x = (max+f).y by A4,A6,A7,A8;
end;
hence max+f is_simple_func_in S by A2,A5,Th2,MESFUNC2:def 4;
A9: dom max-f = union rng F by A3,MESFUNC2:def 3;
for n be Nat, x,y be Element of X st n in dom F & x in F.n & y in F.n
holds (max-f).x = (max-f).y
proof
let n be Nat, x,y be Element of X;
assume that
A10: n in dom F and
A11: x in F.n and
A12: y in F.n;
F.n in rng F by A10,FUNCT_1:3; then
x in dom max-f & y in dom max-f by A9,A11,A12,TARSKI:def 4; then
(max-f).x = max(-(f.x),0) & (max-f).y = max(-(f.y),0) by MESFUNC2:def 3;
hence (max-f).x = (max-f).y by A4,A10,A11,A12;
end;
hence max-f is_simple_func_in S by A2,A9,Th2,MESFUNC2:def 4;
end;
theorem Th5:
for a,b be Real st a <= b
holds B-Meas.([.a,b.]) = b-a & B-Meas.([.a,b.[) = b-a
& B-Meas.(].a,b.]) = b-a & B-Meas.(].a,b.[) = b-a
& L-Meas.([.a,b.]) = b-a & L-Meas.([.a,b.[) = b-a
& L-Meas.(].a,b.]) = b-a & L-Meas.(].a,b.[) = b-a
proof
let a,b be Real;
assume
A1: a <= b;
reconsider a1=a, b1=b as R_eal by XXREAL_0:def 1;
B-Meas.([.a,b.]) = diameter [.a,b.] & L-Meas.([.a,b.]) = diameter [.a,b.]
by MEASUR12:71,76; then
A2: B-Meas.([.a,b.]) = b1-a1 & L-Meas.([.a,b.]) = b1-a1 by A1,MEASURE5:6;
A3: B-Meas.([.a,b.[) = diameter [.a1,b1.[
& B-Meas.(].a,b.]) = diameter ].a1,b1.]
& B-Meas.(].a,b.[) = diameter ].a1,b1.[
& L-Meas.([.a,b.[) = diameter [.a1,b1.[
& L-Meas.(].a,b.]) = diameter ].a1,b1.]
& L-Meas.(].a,b.[) = diameter ].a1,b1.[ by MEASUR12:71,76;
now assume a <> b; then
a1 < b1 by A1,XXREAL_0:1; then
B-Meas.([.a,b.[) = b1-a1 & B-Meas.(].a,b.]) = b1-a1
& B-Meas.(].a,b.[) = b1-a1
& L-Meas.([.a,b.[) = b1-a1 & L-Meas.(].a,b.]) = b1-a1
& L-Meas.(].a,b.[) = b1-a1 by A3,MEASURE5:5,7,8;
hence B-Meas.([.a,b.[) = b-a & B-Meas.(].a,b.]) = b-a
& B-Meas.(].a,b.[) = b-a
& L-Meas.([.a,b.[) = b-a & L-Meas.(].a,b.]) = b-a
& L-Meas.(].a,b.[) = b-a by Lm1;
end;
hence thesis by A2,A3,Lm1,MEASURE5:5,7,8;
end;
theorem
for a,b be Real st a > b
holds B-Meas.([.a,b.]) = 0 & B-Meas.([.a,b.[) = 0
& B-Meas.(].a,b.]) = 0 & B-Meas.(].a,b.[) = 0
& L-Meas.([.a,b.]) = 0 & L-Meas.([.a,b.[) = 0
& L-Meas.(].a,b.]) = 0 & L-Meas.(].a,b.[) = 0
proof
let a,b be Real;
assume
A1: a > b;
reconsider a1=a, b1=b as R_eal by XXREAL_0:def 1;
B-Meas.([.a,b.]) = diameter [.a1,b1.]
& B-Meas.([.a,b.[) = diameter [.a1,b1.[
& B-Meas.(].a,b.]) = diameter ].a1,b1.]
& B-Meas.(].a,b.[) = diameter ].a1,b1.[
& L-Meas.([.a,b.]) = diameter [.a1,b1.]
& L-Meas.([.a,b.[) = diameter [.a1,b1.[
& L-Meas.(].a,b.]) = diameter ].a1,b1.]
& L-Meas.(].a,b.[) = diameter ].a1,b1.[ by MEASUR12:71,76;
hence thesis by A1,MEASURE5:5,6,7,8;
end;
theorem
for A1 be Element of Borel_Sets, A2 be Element of L-Field,
f be PartFunc of REAL,ExtREAL
st A1 = A2 & f is A1-measurable holds f is A2-measurable
proof
let A1 be Element of Borel_Sets, A2 be Element of L-Field,
f be PartFunc of REAL,ExtREAL;
assume that
A1: A1 = A2 and
A2: f is A1-measurable;
for r be Real holds A2 /\ less_dom(f,r) in L-Field
by A1,A2,MESFUNC1:def 16,MEASUR12:75;
hence f is A2-measurable by MESFUNC1:def 16;
end;
theorem Th8:
for a,b be Real, A be non empty closed_interval Subset of REAL
st a < b & A = [.a,b.] holds
for n be Nat st n > 0 ex D be Division of A st D divide_into_equal n
proof
let a,b be Real, A be non empty closed_interval Subset of REAL;
assume that
A1: a < b and
A2: A = [.a,b.];
A3: b-a > 0 by A1,XREAL_1:50;
hereby let n be Nat;
assume A4: n > 0;
defpred P[Nat,Real] means $2 = a + (b-a) * $1 / n;
A5: for k be Nat st k in Seg n ex r be Element of REAL st P[k,r]
proof
let k be Nat;
assume k in Seg n;
a + (b-a) * k / n is Element of REAL by XREAL_0:def 1;
hence thesis;
end;
consider D be FinSequence of REAL such that
A6: dom D = Seg n & for k be Nat st k in Seg n holds P[k,D.k]
from FINSEQ_1:sch 5(A5);
reconsider D as non empty FinSequence of REAL by A6,A4;
for k be Nat st 1 <= k & k < len D holds D.k < D.(k+1)
proof
let k be Nat;
assume A7: 1 <= k & k < len D; then
1 <= k+1 & k+1 <= len D by NAT_1:13; then
A8: D.k = a + (b-a)*k / n
& D.(k+1) = a + (b-a)*(k+1) / n by A6,A7,FINSEQ_3:25;
k < k+1 by NAT_1:13; then
(b-a)*k < (b-a)*(k+1) by A3,XREAL_1:68; then
(b-a)*k/ n < (b-a)*(k+1)/ n by A4,XREAL_1:74;
hence D.k < D.(k+1) by A8,XREAL_1:8;
end; then
reconsider D as non empty increasing FinSequence of REAL
by EUCLID_7:def 1;
now let x be object;
assume x in rng D; then
consider k be Element of NAT such that
A9: k in dom D & x = D.k by PARTFUN1:3;
A10: D.k = a + (b-a)*k / n by A6,A9;
1 <= k & k <= n by A6,A9,FINSEQ_1:1; then
0 < k / n <= 1 by XREAL_1:139,183; then
0 < (b-a) * (k / n) <= b-a by A3,XREAL_1:129,153; then
A11: 0 < (b-a) * k / n <= b-a by XCMPLX_1:74;
a + (b-a) = b; then
a < a + (b-a)*k / n <= b by A11,XREAL_1:29,6;
hence x in A by A2,A9,A10,XXREAL_1:1;
end; then
A12: rng D c= A;
dom D = Seg len D by FINSEQ_1:def 3; then
A13: len D = n by A6,FINSEQ_1:6; then
D.(len D) = a + (b-a) * n / n by A6,FINSEQ_1:3; then
A14: D.(len D) = a + (b-a) by A4,XCMPLX_1:89;
A = [.lower_bound A,upper_bound A.] by INTEGRA1:4; then
upper_bound A = b by A2,INTEGRA1:5; then
reconsider D as Division of A by A12,A14,INTEGRA1:def 2;
for k be Nat st k in dom D holds D.k = lower_bound A + vol(A)/(len D)*k
proof
let k be Nat;
assume k in dom D; then
A15: D.k = a + (b-a) * k / n by A6;
A = [.lower_bound A,upper_bound A.] by INTEGRA1:4; then
A16: lower_bound A = a & upper_bound A = b by A2,INTEGRA1:5; then
vol A = b-a by INTEGRA1:def 5;
hence D.k = lower_bound A + vol(A)/(len D)*k by A13,A15,A16,XCMPLX_1:74;
end;
hence ex D be Division of A st D divide_into_equal n
by A13,INTEGRA4:def 1;
end;
end;
Lm2:
for r be Real, F be FinSequence of REAL st
(for n be Nat st n in dom F holds F.n = r) holds Sum F = r*(len F)
proof
let r be Real, F be FinSequence of REAL;
assume for n be Nat st n in dom F holds F.n = r; then
for z be object st z in dom F holds F.z = r; then
F = dom F --> r by FUNCOP_1:11; then
F = Seg len F --> r by FINSEQ_1:def 3; then
F = (len F) |-> r by FINSEQ_2:def 2;
hence Sum F = r*(len F) by RVSUM_1:80;
end;
definition
let F be FinSequence of Borel_Sets;
let n be Nat;
redefine func F.n -> ext-real-membered set; :: redefines . (FUNCT_1, definition)
correctness
proof
thus F.n is ext-real-membered set;
end;
end;
theorem Th9:
for a,b be Real, A be non empty closed_interval Subset of REAL,
D be Division of A st A = [.a,b.] holds
ex F be Finite_Sep_Sequence of Borel_Sets
st dom D = dom F
& union rng F = A
& for k be Nat st k in dom F holds
(len D = 1 implies F.k = [. a,b .])
& (len D <> 1 implies
(k = 1 implies F.k = [. a,D.k .[)
& (1 < k < len D implies F.k = [. D.(k-'1), D.k .[)
& (k = len D implies F.k = [. D.(k-'1), D.k.]))
proof
let a,b be Real, A be non empty closed_interval Subset of REAL,
D be Division of A;
assume
A1: A = [.a,b.];
defpred P[Nat,set] means
(len D = 1 implies $2 = [. a,b .])
& (len D <> 1 implies
( ($1 = 1 implies $2 = [. a,D.$1 .[)
& (1 < $1 < len D implies $2 = [. D.($1-'1), D.$1 .[)
& ($1 = len D implies $2 = [. D.($1-'1), D.$1.])));
A2: for k be Nat st k in Seg len D ex x be Element of Borel_Sets st P[k,x]
proof
let k be Nat;
assume k in Seg len D; then
1 <= k <= len D by FINSEQ_1:1; then
A3: (k = 1 & k <> len D) or (1 < k < len D) or k = len D by XXREAL_0:1;
A4: [. a,b .] is Element of Borel_Sets
& [. a, D.k .[ is Element of Borel_Sets
& [. D.(k-'1), D.k .[ is Element of Borel_Sets
& [.D.(k-'1),D.k .] is Element of Borel_Sets by MEASUR10:5;
len D = 1 or len D <> 1;
hence ex x be Element of Borel_Sets st P[k,x] by A3,A4;
end;
consider F be FinSequence of Borel_Sets such that
A5: dom F = Seg len D &
for k be Nat st k in Seg len D holds P[k,F.k] from FINSEQ_1:sch 5(A2);
A6:dom F = dom D by A5,FINSEQ_1:def 3;
for x,y be object st x <> y holds F.x misses F.y
proof
let x,y be object;
assume A7: x <> y;
per cases;
suppose not x in dom F or not y in dom F; then
F.x = {} or F.y = {} by FUNCT_1:def 2;
hence F.x misses F.y by XBOOLE_1:65;
end;
suppose A8: x in dom F & y in dom F; then
reconsider x1=x, y1=y as Nat;
A9: x in dom D & y in dom D by A8,A5,FINSEQ_1:def 3;
A10: 1 <= x1 <= len D & 1 <= y1 <= len D by A8,A5,FINSEQ_1:1;
A11: now assume len D = 1; then
x1 = 1 & y1 = 1 by A10,XXREAL_0:1;
hence contradiction by A7;
end;
per cases by A10,XXREAL_0:1;
suppose A12: 1 = x1; then
A13: 1 < y1 <= len D by A7,A10,XXREAL_0:1; then
A14: x1 <= y1-'1 <= len D by A12,NAT_D:44,49; then
A15: y1-'1 in dom D by A12,FINSEQ_3:25;
A16: F.x = [.a,D.x1 .[ by A8,A5,A12,A11;
y1 < len D or y1 = len D by A10,XXREAL_0:1; then
F.y = [. D.(y1-'1),D.y1 .[ or F.y = [. D.(y1-'1), D.y1 .]
by A8,A5,A13;
hence F.x misses F.y by A16,A14,A9,A15,VALUED_0:def 15,XXREAL_1:95,96;
end;
suppose A17: 1 < x1 < len D; then
x1 in Seg len D by FINSEQ_1:1; then
A18: F.x = [. D.(x1-'1),D.x1 .[ by A5,A17;
per cases by A7,XXREAL_0:1;
suppose A19: x1 < y1; then
A20: x1 <= y1-'1 by NAT_D:49; then
1 <= y1-'1 & y1-'1 <= len D by A10,NAT_D:44,XXREAL_0:2; then
A21: y1-'1 in dom D by FINSEQ_3:25;
y1 = len D or 1 < y1 < len D by A19,A10,XXREAL_0:1; then
F.y = [. D.(y1-'1),D.y1 .] or F.y = [. D.(y1-'1),D.y1 .[ by A8,A11,A5;
hence F.x misses F.y by A21,A18,A9,A20,VALUED_0:def 15,XXREAL_1:95,96;
end;
suppose A22: x1 > y1; then
A23: y1 <= x1-'1 by NAT_D:49; then
1 <= x1-'1 & x1-'1 <= len D by A10,XXREAL_0:2,NAT_D:44; then
A24: x1-'1 in dom D by FINSEQ_3:25;
y1 = 1 or 1 < y1 < len D by A10,A22,XXREAL_0:1; then
F.y = [. a,D.y1 .[ or F.y = [. D.(y1-'1), D.y1 .[ by A5,A8,A11;
hence F.x misses F.y by A18,A24,A9,A23,VALUED_0:def 15,XXREAL_1:96;
end;
end;
suppose A25: x1 = len D; then
A26: F.x = [. D.(x1-'1),D.x1 .] by A5,A8,A11;
A27: y1 < len D by A7,A10,A25,XXREAL_0:1; then
A28: y1 <= x1-'1 by A25,NAT_D:49; then
1 <= x1-'1 <= len D by A10,XXREAL_0:2,NAT_D:44; then
A29: x1-'1 in dom D by FINSEQ_3:25;
y1 = 1 or 1 < y1 by A10,XXREAL_0:1; then
F.y = [. a,D.y1 .[ or F.y = [. D.(y1-'1),D.y1 .[ by A5,A8,A27;
hence F.x misses F.y by A26,A29,A9,A28,VALUED_0:def 15,XXREAL_1:95;
end;
end;
end; then
reconsider F as Finite_Sep_Sequence of Borel_Sets by PROB_2:def 2;
take F;
A30: for k be Nat st k in dom F & k <> len D holds union rng(F|k) = [.a,D.k .[
proof
let k be Nat;
assume that
A31: k in dom F and
A32: k <> len D;
A33: k <= len F by A31,FINSEQ_3:25;
len D = len F by A5,FINSEQ_1:def 3; then
A34: k < len D by A32,A33,XXREAL_0:1;
defpred P[Nat] means 1 <= $1 <= k implies union rng(F|$1) = [.a,D.$1 .[;
A35: P[0];
A36: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume A37: P[i];
assume A38: 1 <= i+1 <= k; then
A39: i+1 < len D by A34,XXREAL_0:2;
i+1 <= len F by A38,A33,XXREAL_0:2; then
A40: i+1 in dom F by A38,FINSEQ_3:25;
per cases;
suppose A41: i=0; then
len(F|(i+1)) = 1 by A38,A33,XXREAL_0:2,FINSEQ_1:59; then
F|(i+1) = <* (F|(i+1)).1 *> by FINSEQ_1:40; then
F|(i+1) = <* F.1 *> by A41,FINSEQ_3:112; then
rng(F|(i+1)) = {F.1} by FINSEQ_1:38;
hence union rng(F|(i+1)) = [.a,D.(i+1) .[ by A5,A40,A41,A38,A34;
end;
suppose A42: i<>0; then
A43: i >= 1 by NAT_1:14;
A44: i < i+1 by NAT_1:13; then
F|(i+1)|i = F|i by FINSEQ_1:82; then
A45: F|i = (F|(i+1))|(Seg i) by FINSEQ_1:def 16;
len(F|(i+1)) = i+1 by A38,A33,XXREAL_0:2,FINSEQ_1:59; then
F|(i+1) = F|i ^ <* (F|(i+1)).(i+1) *> by A45,FINSEQ_3:55; then
F|(i+1) = F|i ^ <* F.(i+1) *> by FINSEQ_3:112; then
rng(F|(i+1)) = rng(F|i) \/ rng <* F.(i+1) *> by FINSEQ_1:31; then
rng(F|(i+1)) = rng(F|i) \/ {F.(i+1)} by FINSEQ_1:38; then
A46: union rng(F|(i+1)) = union rng(F|i) \/ union {F.(i+1)}
by ZFMISC_1:78;
i <= k by A38,NAT_1:13; then
i < len D by A34,XXREAL_0:2; then
A47: i in dom D by A43,FINSEQ_3:25; then
D.i in [.a,b.] by A1,INTEGRA1:6; then
A48: a <= D.i by XXREAL_1:1;
A49: D.i < D.(i+1) by A44,A47,A40,A6,VALUED_0:def 13;
1 < i+1 by A42,NAT_1:13,14; then
F.(i+1) = [. D.(i+1-'1), D.(i+1) .[ by A5,A39,A40; then
F.(i+1) = [. D.i, D.(i+1) .[ by NAT_D:34;
hence union rng(F|(i+1)) = [.a,D.(i+1) .[
by A46,A48,A49,A37,A42,A38,NAT_1:13,14,XXREAL_1:168;
end;
end;
A50: for i be Nat holds P[i] from NAT_1:sch 2(A35,A36);
1 <= k by A31,FINSEQ_3:25;
hence union rng(F|k) = [.a,D.k .[ by A50;
end;
union rng F = A
proof
per cases;
suppose A51: len D = 1; then
A52: 1 in dom F by A6,FINSEQ_3:25;
len F = 1 by A51,A5,FINSEQ_1:def 3; then
F = <* F.1 *> by FINSEQ_1:40; then
rng F = {F.1} by FINSEQ_1:38;
hence union rng F = A by A1,A5,A51,A52;
end;
suppose A53: len D <> 1;
consider k be Nat such that
A54: len D = k + 1 by NAT_1:6;
A55: 1 <= len D by FINSEQ_1:20; then
1 < len D by A53,XXREAL_0:1; then
A56: 1 <= k < len D by A54,NAT_1:13; then
A57: k in dom F by A6,FINSEQ_3:25;
A58: union rng(F|k) = [. a,D.k .[ by A56,A30,A6,FINSEQ_3:25;
reconsider a1=lower_bound A, a2=upper_bound A as Real;
A = [.a1,a2.] by INTEGRA1:4; then
A59: b = upper_bound A by A1,INTEGRA1:5;
k+1 in dom F by A54,A55,A6,FINSEQ_3:25; then
F.(k+1) = [. D.(k+1-'1), D.(k+1) .] by A54,A53,A5; then
F.(k+1) = [. D.k,D.(k+1) .] by NAT_D:34; then
A60: F.(k+1) = [. D.k,b .] by A54,A59,INTEGRA1:def 2;
D.k in A by A57,A6,INTEGRA1:6; then
A61: a <= D.k <= b by A1,XXREAL_1:1;
A62: len F = k+1 by A54,A5,FINSEQ_1:def 3;
F|k = F|Seg k by FINSEQ_1:def 16; then
F = F|k ^ <* F.(k+1) *> by A62,FINSEQ_3:55; then
rng F = rng(F|k) \/ rng <* F.(k+1) *> by FINSEQ_1:31; then
union rng F = union rng(F|k) \/ union rng <* F.(k+1) *>
by ZFMISC_1:78; then
union rng F = [. a,D.k .[ \/ union {F.(k+1)} by A58,FINSEQ_1:38;
hence union rng F = A by A1,A60,A61,XXREAL_1:166;
end;
end;
hence thesis by A5,FINSEQ_1:def 3;
end;
theorem Th10:
for a,b be Real, A be non empty closed_interval Subset of REAL,
D be Division of A, f be PartFunc of A,REAL st A = [.a,b.] holds
ex F be Finite_Sep_Sequence of Borel_Sets, g be PartFunc of REAL,ExtREAL
st dom F = dom D
& union rng F = A
& (for k be Nat st k in dom F holds
(len D = 1 implies F.k = [. a,b .])
& (len D <> 1 implies
(k = 1 implies F.k = [. a,D.k .[)
& (1 < k < len D implies F.k = [. D.(k-'1), D.k .[)
& (k = len D implies F.k = [. D.(k-'1), D.k.])))
& g is_simple_func_in Borel_Sets
& dom g = A
& for x be Real st x in dom g holds
ex k be Nat st 1 <= k <= len F & x in F.k
& g.x = lower_bound rng(f|divset(D,k))
proof
let a,b be Real, A be non empty closed_interval Subset of REAL,
D be Division of A, f be PartFunc of A,REAL;
assume A = [.a,b.]; then
consider F be Finite_Sep_Sequence of Borel_Sets such that
A1: dom F = dom D and
A2: union rng F = A and
A3: for k be Nat st k in dom F holds
(len D = 1 implies F.k = [. a,b .])
& (len D <> 1 implies
(k = 1 implies F.k = [. a,D.k .[)
& (1 < k < len D implies F.k = [. D.(k-'1), D.k .[)
& (k = len D implies F.k = [. D.(k-'1), D.k.])) by Th9;
defpred P[object,object] means
ex k be Nat st 1 <= k <= len F & $1 in F.k &
$2 = lower_bound rng(f|divset(D,k));
A4: for x,y be object st x in REAL & P[x,y] holds y in ExtREAL
by XXREAL_0:def 1;
A5: for x,y1,y2 be object st x in REAL & P[x,y1] & P[x,y2] holds y1 = y2
by PROB_2:def 2,XBOOLE_0:3;
consider g be PartFunc of REAL,ExtREAL such that
A6: for x be object holds x in dom g iff
x in REAL & ex y be object st P[x,y] and
A7: for x be object st x in dom g holds P[x,g.x] from PARTFUN1:sch 2(A4,A5);
now let y be object;
assume y in rng g; then
consider x be Element of REAL such that
A8: x in dom g & y = g.x by PARTFUN1:3;
ex k be Nat st
1 <= k <= len F & x in F.k & g.x = lower_bound rng(f|divset(D,k))
by A7,A8;
hence y in REAL by A8,XREAL_0:def 1;
end; then
rng g c= REAL; then
A9: g is real-valued by VALUED_0:def 3;
now let x be object;
assume x in dom g; then
consider y be object such that
A10: ex k be Nat st 1 <= k <= len F & x in F.k
& y = lower_bound rng(f|divset(D,k)) by A6;
consider k be Nat such that
A11: 1 <= k <= len F and
A12: x in F.k and
y = lower_bound rng(f|divset(D,k)) by A10;
k in dom F by A11,FINSEQ_3:25; then
F.k in rng F by FUNCT_1:3;
hence x in union rng F by A12,TARSKI:def 4;
end; then
A13: dom g c= union rng F;
now let x be object;
assume A14: x in union rng F; then
consider P be set such that
A15: x in P & P in rng F by TARSKI:def 4;
consider k be Element of NAT such that
A16: k in dom F & P = F.k by A15,PARTFUN1:3;
A17: 1 <= k <= len F by A16,FINSEQ_3:25;
lower_bound rng(f|divset(D,k)) in REAL by XREAL_0:def 1;
hence x in dom g by A6,A15,A16,A14,A2,A17;
end; then
union rng F c= dom g; then
A18:dom g = union rng F by A13,XBOOLE_0:def 10;
A19:for k be Nat, x,y be Element of REAL st
k in dom F & x in F.k & y in F.k holds g.x = g.y
proof
let k be Nat, x,y be Element of REAL;
assume that
A20: k in dom F and
A21: x in F.k and
A22: y in F.k;
F.k in rng F by A20,FUNCT_1:3; then
A23: x in dom g & y in dom g by A18,A21,A22,TARSKI:def 4; then
consider k1 be Nat such that
1 <= k1 <= len F and
A24: x in F.k1 and
A25: g.x = lower_bound rng(f|divset(D,k1)) by A7;
consider k2 be Nat such that
1 <= k2 <= len F and
A26: y in F.k2 and
A27: g.y = lower_bound rng(f|divset(D,k2)) by A23,A7;
k = k1 & k = k2 by A21,A22,A24,A26,XBOOLE_0:3,PROB_2:def 2;
hence g.x = g.y by A25,A27;
end;
for x be Real st x in dom g holds
ex k be Nat st 1 <= k <= len F & x in F.k
& g.x = lower_bound rng(f|divset(D,k)) by A7;
hence thesis by A1,A3,A2,A18,A19,A9,MESFUNC2:def 4;
end;
theorem Th11:
for a,b be Real, A be non empty closed_interval Subset of REAL,
D be Division of A, f be PartFunc of A,REAL st A = [.a,b.] holds
ex F be Finite_Sep_Sequence of Borel_Sets, g be PartFunc of REAL,ExtREAL
st dom F = dom D
& union rng F = A
& (for k be Nat st k in dom F holds
(len D = 1 implies F.k = [. a,b .])
& (len D <> 1 implies
(k = 1 implies F.k = [. a,D.k .[)
& (1 < k < len D implies F.k = [. D.(k-'1), D.k .[)
& (k = len D implies F.k = [. D.(k-'1), D.k.])))
& g is_simple_func_in Borel_Sets
& dom g = A
& for x be Real st x in dom g holds
ex k be Nat st 1 <= k <= len F & x in F.k
& g.x = upper_bound rng(f|divset(D,k))
proof
let a,b be Real, A be non empty closed_interval Subset of REAL,
D be Division of A, f be PartFunc of A,REAL;
assume A = [.a,b.]; then
consider F be Finite_Sep_Sequence of Borel_Sets such that
A1: dom F = dom D and
A2: union rng F = A and
A3: for k be Nat st k in dom F holds
(len D = 1 implies F.k = [. a,b .])
& (len D <> 1 implies
(k = 1 implies F.k = [. a,D.k .[)
& (1 < k < len D implies F.k = [. D.(k-'1), D.k .[)
& (k = len D implies F.k = [. D.(k-'1), D.k.])) by Th9;
defpred P[object,object] means
ex k be Nat st 1 <= k <= len F & $1 in F.k &
$2 = upper_bound rng(f|divset(D,k));
A4: for x,y be object st x in REAL & P[x,y] holds y in ExtREAL
by XXREAL_0:def 1;
A5: for x,y1,y2 be object st x in REAL & P[x,y1] & P[x,y2] holds y1 = y2
by PROB_2:def 2,XBOOLE_0:3;
consider g be PartFunc of REAL,ExtREAL such that
A6: for x be object holds x in dom g iff
x in REAL & ex y be object st P[x,y] and
A7: for x be object st x in dom g holds P[x,g.x] from PARTFUN1:sch 2(A4,A5);
now let y be object;
assume y in rng g; then
consider x be Element of REAL such that
A8: x in dom g & y = g.x by PARTFUN1:3;
ex k be Nat st
1 <= k <= len F & x in F.k & g.x = upper_bound rng(f|divset(D,k))
by A7,A8;
hence y in REAL by A8,XREAL_0:def 1;
end; then
rng g c= REAL; then
A9: g is real-valued by VALUED_0:def 3;
now let x be object;
assume x in dom g; then
consider y be object such that
A10: ex k be Nat st 1 <= k <= len F & x in F.k
& y = upper_bound rng(f|divset(D,k)) by A6;
consider k be Nat such that
A11: 1 <= k <= len F and
A12: x in F.k and
y = upper_bound rng(f|divset(D,k)) by A10;
k in dom F by A11,FINSEQ_3:25; then
F.k in rng F by FUNCT_1:3;
hence x in union rng F by A12,TARSKI:def 4;
end; then
A13: dom g c= union rng F;
now let x be object;
assume A14: x in union rng F; then
consider P be set such that
A15: x in P & P in rng F by TARSKI:def 4;
consider k be Element of NAT such that
A16: k in dom F & P = F.k by A15,PARTFUN1:3;
A17: 1 <= k <= len F by A16,FINSEQ_3:25;
upper_bound rng(f|divset(D,k)) in REAL by XREAL_0:def 1;
hence x in dom g by A6,A14,A2,A15,A16,A17;
end; then
union rng F c= dom g; then
A18:dom g = union rng F by A13,XBOOLE_0:def 10;
A19:for k be Nat, x,y be Element of REAL st
k in dom F & x in F.k & y in F.k holds g.x = g.y
proof
let k be Nat, x,y be Element of REAL;
assume that
A20: k in dom F and
A21: x in F.k and
A22: y in F.k;
F.k in rng F by A20,FUNCT_1:3; then
A23: x in dom g & y in dom g by A18,A21,A22,TARSKI:def 4; then
consider k1 be Nat such that
1 <= k1 <= len F and
A24: x in F.k1 and
A25: g.x = upper_bound rng(f|divset(D,k1)) by A7;
consider k2 be Nat such that
1 <= k2 <= len F and
A26: y in F.k2 and
A27: g.y = upper_bound rng(f|divset(D,k2)) by A23,A7;
k = k1 & k = k2 by A21,A22,A24,A26,XBOOLE_0:3,PROB_2:def 2;
hence g.x = g.y by A25,A27;
end;
for x be Real st x in dom g holds
ex k be Nat st 1 <= k <= len F & x in F.k
& g.x = upper_bound rng(f|divset(D,k)) by A7;
hence thesis by A1,A3,A2,A18,A19,A9,MESFUNC2:def 4;
end;
theorem Th12:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, F be Finite_Sep_Sequence of S,
a be FinSequence of ExtREAL, n be Nat
st f is_simple_func_in S & F,a are_Re-presentation_of f & n in dom F
holds F.n = {} or a.n is Real
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, F be Finite_Sep_Sequence of S,
a be FinSequence of ExtREAL, n be Nat;
assume that
A1: f is_simple_func_in S and
A2: F,a are_Re-presentation_of f and
A3: n in dom F;
A4: f is real-valued by A1,MESFUNC2:def 4;
now assume F.n <> {}; then
consider x be object such that
A5: x in F.n by XBOOLE_0:def 1;
a.n = f.x by A2,A3,A5,MESFUNC3:def 1;
hence a.n is Real by A4;
end;
hence F.n = {} or a.n is Real;
end;
Lm3:
for A be non empty closed_interval Subset of REAL, n be Nat
st n > 0 & vol A > 0
ex D be Division of A st D divide_into_equal n
proof
let A be non empty closed_interval Subset of REAL;
let n be Nat;
assume A1: n > 0;
assume A2: vol A > 0;
consider a,b be Real such that
a <= b and
A3: A = [.a,b.] by MEASURE5:14;
A = [.lower_bound A,upper_bound A.] by INTEGRA1:4; then
lower_bound A = a & upper_bound A = b by A3,INTEGRA1:5; then
A4: b-a > 0 by A2,INTEGRA1:def 5;
defpred P[Nat,Real] means
$2 = a + (b-a) * $1 / n;
A5: for k be Nat st k in Seg n ex r be Element of REAL st P[k,r]
proof
let k be Nat;
assume k in Seg n;
a + (b-a) * k / n is Element of REAL by XREAL_0:def 1;
hence thesis;
end;
consider D be FinSequence of REAL such that
A6: dom D = Seg n & for k be Nat st k in Seg n holds P[k,D.k]
from FINSEQ_1:sch 5(A5);
reconsider D as non empty FinSequence of REAL by A6,A1;
for k be Nat st 1 <= k & k < len D holds D.k < D.(k+1)
proof
let k be Nat;
assume A7: 1 <= k & k < len D; then
1 <= k+1 & k+1 <= len D by NAT_1:13; then
A8: D.k = a + (b-a)*k / n
& D.(k+1) = a + (b-a)*(k+1) / n by A6, A7,FINSEQ_3:25;
k < k+1 by NAT_1:13; then
(b-a)*k < (b-a)*(k+1) by A4,XREAL_1:68; then
(b-a)*k/ n < (b-a)*(k+1)/ n by A1,XREAL_1:74;
hence D.k < D.(k+1) by A8,XREAL_1:8;
end; then
reconsider D as non empty increasing FinSequence of REAL
by EUCLID_7:def 1;
now let x be object;
assume x in rng D; then
consider k be Element of NAT such that
A9: k in dom D & x = D.k by PARTFUN1:3;
A10: D.k = a + (b-a)*k / n by A6,A9;
1 <= k & k <= n by A6,A9,FINSEQ_1:1; then
0 < k / n <= 1 by XREAL_1:139,183; then
0 < (b-a) * (k / n) <= b-a by A4,XREAL_1:129,153; then
A11: 0 < (b-a) * k / n <= b-a by XCMPLX_1:74;
a + (b-a) = b; then
a < a + (b-a)*k / n <= b by A11,XREAL_1:29,6;
hence x in A by A3,A9,A10,XXREAL_1:1;
end; then
A12: rng D c= A;
dom D = Seg len D by FINSEQ_1:def 3; then
A13: len D = n by A6,FINSEQ_1:6; then
D.(len D) = a + (b-a) * n / n by A6,FINSEQ_1:3; then
A14: D.(len D) = a + (b-a) by A1,XCMPLX_1:89;
A = [.lower_bound A,upper_bound A.] by INTEGRA1:4; then
upper_bound A = b by A3,INTEGRA1:5; then
reconsider D as Division of A by A12,A14,INTEGRA1:def 2;
for k be Nat st k in dom D holds D.k = lower_bound A + vol(A)/(len D)*k
proof
let k be Nat;
assume k in dom D; then
A15: D.k = a + (b-a) * k / n by A6;
A = [.lower_bound A,upper_bound A.] by INTEGRA1:4; then
A16: lower_bound A = a & upper_bound A = b by A3,INTEGRA1:5; then
vol A = b-a by INTEGRA1:def 5;
hence D.k = lower_bound A + vol(A)/(len D)*k by A13,A15,A16,XCMPLX_1:74;
end;
hence ex D be Division of A st D divide_into_equal n
by A13,INTEGRA4:def 1;
end;
definition
let A be non empty closed_interval Subset of REAL;
let n be Nat;
assume A1: n > 0 & vol A > 0;
func EqDiv(A,n) -> Division of A means :Def1:
it divide_into_equal n;
existence by A1,Lm3;
uniqueness
proof
let F1,F2 be Division of A;
assume that
A2: F1 divide_into_equal n and
A3: F2 divide_into_equal n;
A4: len F1 = n & len F2 = n by A2,A3,INTEGRA4:def 1; then
A5: dom F1 = dom F2 by FINSEQ_3:29;
for n be Element of NAT st n in dom F1 holds F1.n = F2.n
proof
let n be Element of NAT;
assume A6: n in dom F1; then
F1.n = lower_bound A + vol A / (len F1)*n by A2,INTEGRA4:def 1;
hence F1.n = F2.n by A3,A6,A5,A4,INTEGRA4:def 1;
end;
hence F1=F2 by A5,PARTFUN1:5;
end;
end;
theorem
for A be non empty closed_interval Subset of REAL, n be Nat st
vol A > 0 & len EqDiv(A,2|^n) = 1 holds n = 0
proof
let A be non empty closed_interval Subset of REAL, n be Nat;
assume that
A1: vol A > 0 and
A2: len EqDiv(A,2|^n) = 1;
2|^n > 0 by NEWTON:83; then
EqDiv(A,2|^n) divide_into_equal 2|^n by A1,Def1; then
len EqDiv(A,2|^n) = 2|^n by INTEGRA4:def 1;
hence n = 0 by A2,NAT_1:14,NEWTON:86;
end;
theorem
for a,b be Real, A be non empty closed_interval Subset of REAL
st a < b & A = [.a,b.] holds
ex D be DivSequence of A st
for n be Nat holds D.n divide_into_equal 2|^n
proof
let a,b be Real, A be non empty closed_interval Subset of REAL;
assume that
A1: a < b and
A2: A = [.a,b.];
defpred P[Nat,object] means ex D be Division of A st
D = $2 & D divide_into_equal 2|^$1;
A3: for n be Element of NAT ex D be Element of divs A st P[n,D]
proof
let n be Element of NAT;
2|^n > 0 by NEWTON:83; then
consider D1 be Division of A such that
A4: D1 divide_into_equal 2|^n by A1,A2,Th8;
D1 is Element of divs A by INTEGRA1:def 3;
hence thesis by A4;
end;
consider D be Function of NAT,divs A such that
A5: for n be Element of NAT holds P[n,D.n] from FUNCT_2:sch 3(A3);
reconsider D as DivSequence of A;
take D;
thus for n be Nat holds D.n divide_into_equal 2|^n
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 12; then
ex d be Division of A st d = D.n & d divide_into_equal 2|^n by A5;
hence thesis;
end;
end;
theorem Th15:
for A be non empty closed_interval Subset of REAL, D be Division of A,
n,k be Nat st D divide_into_equal n & k in dom D
holds vol divset(D,k) = (vol A)/n
proof
let A be non empty closed_interval Subset of REAL, D be Division of A,
n,k be Nat;
assume that
A1: D divide_into_equal n and
A2: k in dom D;
A3:len D = n by A1,INTEGRA4:def 1; then
A4:D.k = lower_bound A + (vol A)/n*k by A1,A2,INTEGRA4:def 1;
per cases;
suppose A5: k = 1; then
lower_bound divset(D,k) = lower_bound A
& upper_bound divset(D,k) = D.k by A2,INTEGRA1:def 4; then
vol divset(D,k) = D.k - lower_bound A by INTEGRA1:def 5;
hence vol divset(D,k) = (vol A)/n by A4,A5;
end;
suppose A6: k <> 1; then
A7: lower_bound divset(D,k) = D.(k-1)
& upper_bound divset(D,k) = D.k by A2,INTEGRA1:def 4;
A8: 1 <= k <= len D by A2,FINSEQ_3:25; then
A9: 1 < k by A6,XXREAL_0:1; then
reconsider j = k-1 as Nat by NAT_1:20;
k = j+1; then
1 <= j <= k by A9,NAT_1:19; then
1 <= j <= len D by A8,XXREAL_0:2; then
j in dom D by FINSEQ_3:25; then
A10: D.j = lower_bound A + (vol A)/n*j by A1,A3,INTEGRA4:def 1;
vol divset(D,k) = D.k - D.j by A7,INTEGRA1:def 5
.= (vol A)/n*1 by A4,A10;
hence vol divset(D,k) = (vol A)/n;
end;
end;
theorem Th16:
for x be Complex, r be natural Number st x <> 0 holds (x|^r)" = x"|^r
proof
let x be Complex, r be natural Number;
assume A1: x <> 0;
reconsider y = x* x" as Complex;
A2: y = x / x by XCMPLX_0:def 9 .= 1 by A1,XCMPLX_1:60;
x|^r * (x")|^r = y |^r by NEWTON:7
.= 1 by A2,NEWTON:10;
hence thesis by XCMPLX_1:210;
end;
theorem Th17:
for A be non empty closed_interval Subset of REAL, T be sequence of divs A st
vol A > 0 & (for n be Nat holds T.n = EqDiv(A,2|^n)) holds
delta T is 0-convergent non-zero
proof
let A be non empty closed_interval Subset of REAL;
let T be sequence of divs A;
assume that
A1: vol A > 0 and
A2: for n be Nat holds T.n = EqDiv(A,2|^n);
A3: for n be Nat holds (delta T).n = 2*(vol A)*(2"|^(n+1))
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 12; then
(delta T).n = delta(T.n) by INTEGRA3:def 2; then
(delta T).n = delta(EqDiv(A,2|^n)) by A2; then
A4: (delta T).n = max rng (upper_volume(chi(A,A),EqDiv(A,2|^n)))
by INTEGRA3:def 1;
A5: for k be Nat st k in dom EqDiv(A,2|^n)
holds (upper_volume(chi(A,A),EqDiv(A,2|^n))).k = 2*(vol A)*(2"|^(n+1))
proof
let k be Nat;
assume A6: k in dom EqDiv(A,2|^n);
2|^n > 0 by NEWTON:83; then
EqDiv(A,2|^n) divide_into_equal 2|^n by A1,Def1; then
vol divset(EqDiv(A,2|^n),k) = (vol A)/(2|^n) by A6,Th15; then
upper_volume(chi(A,A),EqDiv(A,2|^n)).k
= (vol A)/(2|^n) by A6,INTEGRA1:20
.= (vol A)/(2|^n * 2)*2 by XCMPLX_1:92
.= (vol A)/(2|^(n+1))*2 by NEWTON:6
.= (vol A)*(2|^(n+1))"*2 by XCMPLX_0:def 9
.= 2*(vol A)*(2|^(n+1))";
hence thesis by Th16;
end;
now let q be object;
assume q in rng (upper_volume(chi(A,A),EqDiv(A,2|^n))); then
consider p be Element of NAT such that
A7: p in dom (upper_volume(chi(A,A),EqDiv(A,2|^n))) &
q = (upper_volume(chi(A,A),EqDiv(A,2|^n))).p by PARTFUN1:3;
len (upper_volume(chi(A,A),EqDiv(A,2|^n))) = len EqDiv(A,2|^n)
by INTEGRA1:def 6; then
dom (upper_volume(chi(A,A),EqDiv(A,2|^n))) = dom EqDiv(A,2|^n)
by FINSEQ_3:29; then
q = 2*(vol A)*(2"|^(n+1)) by A5,A7;
hence q in {2*(vol A)*(2"|^(n+1))} by TARSKI:def 1;
end; then
rng (upper_volume(chi(A,A),EqDiv(A,2|^n)))
c= {2*(vol A)*(2"|^(n+1))}; then
rng (upper_volume(chi(A,A),EqDiv(A,2|^n)))
= {2*(vol A)*(2"|^(n+1))} by ZFMISC_1:33;
hence (delta T).n = 2*(vol A)*(2"|^(n+1)) by A4,XXREAL_2:11;
end;
deffunc SEQ(Nat) = (2") to_power ($1+1);
consider seq be Real_Sequence such that
A8: for n be Nat holds seq.n = SEQ(n) from SEQ_1:sch 1;
A9: seq is convergent & lim seq = 0 by A8,SERIES_1:1;
for n be Nat holds (delta T).n = (2*(vol A))*(seq.n)
proof
let n be Nat;
seq.n = 2" to_power (n+1) by A8
.= 2"|^(n+1) by POWER:41;
hence (delta T).n = 2*(vol A)*seq.n by A3;
end; then
A10:delta T = (2*(vol A))(#)seq by SEQ_1:9; then
A11:delta T is convergent by A8,SERIES_1:1,SEQ_2:7;
A12:lim (delta T) = (2*(vol A))*0 by A9,A10,SEQ_2:8
.= 0;
now assume 0 in rng(delta T); then
consider m be Element of NAT such that
A13: m in dom(delta T) & 0 = (delta T).m by PARTFUN1:3;
A14: 2*(vol A)*(2"|^(m+1)) = 0 by A3,A13;
2*(vol A) <> 0 & 2"|^(m+1) <> 0 by A1,NEWTON:83;
hence contradiction by A14,XCMPLX_1:6;
end;
hence thesis by A11,A12,FDIFF_1:def 1,ORDINAL1:def 15;
end;
Lm4:
for A be non empty closed_interval Subset of REAL, n be Nat st
vol A > 0 & len EqDiv(A,2|^n) = 1 holds divset(EqDiv(A,2|^n),1) = A
proof
let A be non empty closed_interval Subset of REAL, n be Nat;
assume that
A1: vol A > 0 and
A2: len EqDiv(A,2|^n) = 1;
2|^n > 0 by NEWTON:83; then
A3: EqDiv(A,2|^n) divide_into_equal 2|^n by A1,Def1;
A4: 1 in dom EqDiv(A,2|^n) by A2,FINSEQ_3:25; then
lower_bound divset(EqDiv(A,2|^n),1) = lower_bound A &
upper_bound divset(EqDiv(A,2|^n),1) = EqDiv(A,2|^n).1
by INTEGRA1:def 4; then
A5: divset(EqDiv(A,2|^n),1) = [.lower_bound A,EqDiv(A,2|^n).1 .]
by INTEGRA1:4;
EqDiv(A,2|^n).1 = (lower_bound A) + (vol A)/1*1
by A2,A3,A4,INTEGRA4:def 1; then
EqDiv(A,2|^n).1 = lower_bound A + (upper_bound A - lower_bound A)
by INTEGRA1:def 5;
hence divset(EqDiv(A,2|^n),1) = A by A5,INTEGRA1:4;
end;
Lm5:
for l be Real, m,n be Nat st l > 1 & n <= m holds
l|^n * l|^(m-'n) = l|^m & l|^n * (l|^(m-'n)-'1) < l|^m
proof
let l be Real, m,n be Nat;
assume that
A1: l > 1 and
A2: n <= m;
consider k be Nat such that
A3: m = n + k by A2,NAT_1:10;
k = m - n by A3; then
k = m -'n by XREAL_0:def 2;
hence A4: l|^n * l|^(m-'n) = l|^m by A3,NEWTON:8;
per cases;
suppose m-'n = 0; then
l|^(m-'n) = 1 by NEWTON:4; then
l|^(m-'n) - 1 = 0; then
A5: l|^(m-'n) -'1 = 0 by XREAL_0:def 2;
l|^0 <= l|^m by A1,PREPOWER:93;
hence l|^n * (l|^(m-'n)-'1) < l|^m by A5,NEWTON:4;
end;
suppose m-'n <> 0; then
l|^(m-'n) - 1 > 0 by A1,PEPIN:65,XREAL_1:50; then
A6: l|^(m-'n)-'1 = l|^(m-'n)-1 by XREAL_0:def 2;
l|^n > 0 by A1,NEWTON:83;
hence l|^n * (l|^(m-'n)-'1) < l|^m by A4,A6,XREAL_1:44,68;
end;
end;
theorem Th18:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S,
f be PartFunc of X,ExtREAL, F be Finite_Sep_Sequence of S,
a,x be FinSequence of ExtREAL
st f is_simple_func_in S & E = dom f & M.E < +infty &
F,a are_Re-presentation_of f &
dom x = dom F & (for i be Nat st i in dom x holds x.i=a.i*(M*F).i)
holds Integral(M,f)=Sum(x)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S,
f be PartFunc of X,ExtREAL, F be Finite_Sep_Sequence of S,
a,x be FinSequence of ExtREAL;
assume that
A1: f is_simple_func_in S and
A2: E = dom f and
A3: M.E < +infty and
A4: F,a are_Re-presentation_of f and
A5: dom x = dom F and
A6: for i be Nat st i in dom x holds x.i=a.i*(M*F).i;
A7: max+f is_simple_func_in S & max-f is_simple_func_in S by A1,Th4;
A8:max+f is nonnegative & max-f is nonnegative by MESFUN11:5;
defpred P1[Nat,ExtReal] means
for x be object st x in F.$1 holds $2 = max(f.x,0);
A9: dom a = dom F by A4,MESFUNC3:def 1;
dom max+f = dom f & dom max-f = dom f by MESFUNC2:def 2,def 3; then
A10: dom max+f = union rng F & dom max-f = union rng F by A4,MESFUNC3:def 1;
A11: for k be Nat st k in Seg len a ex y be Element of ExtREAL st P1[k,y]
proof
let k be Nat;
assume k in Seg len a; then
A12: k in dom a by FINSEQ_1:def 3;
per cases;
suppose A13: F.k = {};
A14: 0 is Element of ExtREAL by XXREAL_0:def 1;
for x be object st x in F.k holds 0 = max(f.x,0) by A13;
hence ex y be Element of ExtREAL st P1[k,y] by A14;
end;
suppose F.k <> {}; then
consider p be object such that
A15: p in F.k by XBOOLE_0:def 1;
A16: max(f.p,0) is Element of ExtREAL by XXREAL_0:def 1;
for x be object st x in F.k holds max(f.p,0) = max(f.x,0)
proof
let x be object;
assume x in F.k; then
f.x = a.k & f.p = a.k by A4,A15,A9,A12,MESFUNC3:def 1;
hence max(f.p,0) = max(f.x,0);
end;
hence ex y be Element of ExtREAL st P1[k,y] by A16;
end;
end;
consider a1 be FinSequence of ExtREAL such that
A17: dom a1 = Seg len a and
A18: for k be Nat st k in Seg len a holds P1[k,a1.k] from FINSEQ_1:sch 5(A11);
A19:dom a1 = dom a by A17,FINSEQ_1:def 3;
A20:for k be Nat st k in dom F
for x be object st x in F.k holds (max+f).x = a1.k
proof
let k be Nat;
assume
A21: k in dom F;
let x be object;
assume
A22: x in F.k;
F.k in rng F by A21,FUNCT_1:3; then
x in union rng F by A22,TARSKI:def 4; then
x in dom f by A4,MESFUNC3:def 1; then
A23: x in dom(max+f) by MESFUNC2:def 2;
a1.k = max(f.x,0) by A22,A21,A9,A19,A17,A18;
hence (max+f).x = a1.k by A23,MESFUNC2:def 2;
end; then
A24:F,a1 are_Re-presentation_of (max+f) by A10,A9,A19,MESFUNC3:def 1;
defpred Q1[Nat,ExtReal] means $2 = a1.$1*(M*F).$1;
A25:for k be Nat st k in Seg len F ex y be Element of ExtREAL st Q1[k,y];
consider x1 be FinSequence of ExtREAL such that
A26: dom x1 = Seg len F &
for k be Nat st k in Seg len F holds Q1[k,x1.k]
from FINSEQ_1:sch 5(A25);
A27:dom x1 = dom F by A26,FINSEQ_1:def 3;
A28:dom F = Seg len F by FINSEQ_1:def 3;
now let q be object;
assume q in rng x1; then
consider p be Element of NAT such that
A29: p in dom x1 & q = x1.p by PARTFUN1:3;
A30: q = a1.p * (M*F).p by A26,A29;
per cases by A1,A24,A29,A27,Th4,Th12;
suppose A31: a1.p is Real;
F.p c= union rng F by A29,A27,FUNCT_1:3,ZFMISC_1:74; then
F.p c= E by A2,A4,MESFUNC3:def 1; then
0 <= M.(F.p) <= M.E by SUPINF_2:51,MEASURE1:31; then
0 <= (M*F).p <= M.E by A29,A27,FUNCT_1:13; then
(M*F).p in REAL by A3,XXREAL_0:14;
hence q in REAL by A30,A31,XREAL_0:def 1;
end;
suppose F.p = {}; then
M.(F.p) = 0 by VALUED_0:def 19; then
(M*F).p = 0 by A29,A27,FUNCT_1:13;
hence q in REAL by A30,XREAL_0:def 1;
end;
end; then
rng x1 c= REAL; then
reconsider rx1 = x1 as FinSequence of REAL by FINSEQ_1:def 4;
A32: Sum rx1 = Sum x1 by MESFUNC3:2;
integral'(M,max+f) = Sum x1
proof
per cases;
suppose A33: dom(max+f) = {};
for k be Nat st k in dom x1 holds x1.k = 0
proof
let k be Nat;
assume A34: k in dom x1; then
F.k c= {} by A10,A27,A33,FUNCT_1:3,ZFMISC_1:74; then
F.k = {}; then
M.(F.k) = 0 by VALUED_0:def 19; then
(M*F).k = 0 by A27,A34,FUNCT_1:13; then
a1.k * (M*F).k = 0;
hence x1.k = 0 by A26,A34;
end; then
Sum rx1 = 0*(len rx1) by Lm2;
hence integral'(M,max+f) = Sum x1 by A33,A32,MESFUNC5:def 14;
end;
suppose A35: dom(max+f) <> {}; then
integral(M,max+f) = Sum x1
by A7,A10,A9,A19,A20,A26,A28,A8,MESFUNC3:def 1,MESFUNC4:3;
hence integral'(M,max+f) = Sum x1 by A35,MESFUNC5:def 14;
end;
end; then
A36:Integral(M,max+f) = Sum rx1 by A7,A8,A32,MESFUNC5:89;
defpred P2[Nat,ExtReal] means
for x be object st x in F.$1 holds $2 = max(-(f.x),0);
A37: for k be Nat st k in Seg len a ex y be Element of ExtREAL st P2[k,y]
proof
let k be Nat;
assume k in Seg len a; then
A38: k in dom a by FINSEQ_1:def 3;
per cases;
suppose A39: F.k = {};
A40: 0 is Element of ExtREAL by XXREAL_0:def 1;
for x be object st x in F.k holds 0 = max(-(f.x),0) by A39;
hence ex y be Element of ExtREAL st P2[k,y] by A40;
end;
suppose F.k <> {}; then
consider p be object such that
A41: p in F.k by XBOOLE_0:def 1;
A42: max(-(f.p),0) is Element of ExtREAL by XXREAL_0:def 1;
for x be object st x in F.k holds max(-(f.p),0) = max(-(f.x),0)
proof
let x be object;
assume x in F.k; then
f.x = a.k & f.p = a.k by A9,A38,A41,A4,MESFUNC3:def 1;
hence max(-(f.p),0) = max(-(f.x),0);
end;
hence ex y be Element of ExtREAL st P2[k,y] by A42;
end;
end;
consider a2 be FinSequence of ExtREAL such that
A43: dom a2 = Seg len a and
A44: for k be Nat st k in Seg len a holds P2[k,a2.k] from FINSEQ_1:sch 5(A37);
A45:dom a2 = dom a by A43,FINSEQ_1:def 3;
A46:for k be Nat st k in dom F
for x be object st x in F.k holds (max-f).x = a2.k
proof
let k be Nat;
assume
A47: k in dom F;
let x be object;
assume
A48: x in F.k;
F.k in rng F by A47,FUNCT_1:3; then
x in union rng F by A48,TARSKI:def 4; then
x in dom f by A4,MESFUNC3:def 1; then
A49: x in dom(max-f) by MESFUNC2:def 3;
a2.k = max(-(f.x),0) by A48,A47,A9,A45,A43,A44;
hence (max-f).x = a2.k by A49,MESFUNC2:def 3;
end;
A50:F,a2 are_Re-presentation_of (max-f) by A10,A9,A45,A46,MESFUNC3:def 1;
defpred Q2[Nat,ExtReal] means $2 = a2.$1*(M*F).$1;
A51:for k be Nat st k in Seg len F ex y be Element of ExtREAL st Q2[k,y];
consider x2 be FinSequence of ExtREAL such that
A52: dom x2 = Seg len F &
for k be Nat st k in Seg len F holds Q2[k,x2.k]
from FINSEQ_1:sch 5(A51);
A53:dom x2 = dom F by A52,FINSEQ_1:def 3;
A54:dom F = Seg len F by FINSEQ_1:def 3;
now let q be object;
assume q in rng x2; then
consider p be Element of NAT such that
A55: p in dom x2 & q = x2.p by PARTFUN1:3;
reconsider p as Nat;
A56: q = a2.p * (M*F).p by A55,A52;
per cases by A1,A50,A55,A53,Th4,Th12;
suppose A57: a2.p is Real;
F.p c= union rng F by A55,A53,FUNCT_1:3,ZFMISC_1:74; then
F.p c= E by A2,A4,MESFUNC3:def 1; then
0 <= M.(F.p) <= M.E by SUPINF_2:51,MEASURE1:31; then
0 <= (M*F).p <= M.E by A55,A53,FUNCT_1:13; then
(M*F).p in REAL by A3,XXREAL_0:14;
hence q in REAL by A56,A57,XREAL_0:def 1;
end;
suppose F.p = {}; then
M.(F.p) = 0 by VALUED_0:def 19; then
(M*F).p = 0 by A55,A53,FUNCT_1:13;
hence q in REAL by A56,XREAL_0:def 1;
end;
end; then
rng x2 c= REAL; then
reconsider rx2 = x2 as FinSequence of REAL by FINSEQ_1:def 4;
A58: Sum rx2 = Sum x2 by MESFUNC3:2;
integral'(M,max-f) = Sum x2
proof
per cases;
suppose A59: dom(max-f) = {};
for k be Nat st k in dom x2 holds x2.k = 0
proof
let k be Nat;
assume A60: k in dom x2; then
F.k c= {} by A10,A59,A53,FUNCT_1:3,ZFMISC_1:74; then
F.k = {}; then
M.(F.k) = 0 by VALUED_0:def 19; then
(M*F).k = 0 by A53,A60,FUNCT_1:13; then
a2.k * (M*F).k = 0;
hence x2.k = 0 by A60,A52;
end; then
Sum rx2 = 0*(len rx2) by Lm2;
hence integral'(M,max-f) = Sum x2 by A59,A58,MESFUNC5:def 14;
end;
suppose A61: dom(max-f) <> {}; then
integral(M,max-f) = Sum x2
by A7,A52,A54,A8,A10,A9,A45,A46,MESFUNC3:def 1,MESFUNC4:3;
hence integral'(M,max-f) = Sum x2 by A61,MESFUNC5:def 14;
end;
end; then
A62:Integral(M,max-f) = Sum rx2 by A7,A8,A58,MESFUNC5:89;
A63: len rx1 = len F & len rx2 = len F by A26,A52,FINSEQ_1:def 3;
Integral(M,f) = Integral(M,max+f) - Integral(M,max-f)
by A1,A2,MESFUNC2:34,MESFUN11:54; then
Integral(M,f) = Sum rx1 - Sum rx2 by A36,A62,Lm1; then
A64: Integral(M,f) = Sum(rx1-rx2) by A63,INTEGRA5:2;
len(rx1-rx2) = len rx1 by A63,INTEGRA5:2; then
A65: dom(rx1-rx2) = dom x by A5,A27,FINSEQ_3:29;
for k be object st k in dom x holds x.k = (rx1-rx2).k
proof
let k be object;
assume A66: k in dom x; then
reconsider k1=k as Nat;
A67: x.k = a.k1*(M*F).k1 by A6,A66;
A68: (rx1-rx2).k = rx1.k1 - rx2.k1 by A65,A66,VALUED_1:13;
A69: rx1.k1 = a1.k1 * (M*F).k1 & rx2.k1 = a2.k1 * (M*F).k1
by A5,A26,A28,A52,A66;
per cases;
suppose F.k1 = {}; then
M.(F.k1) = 0 by VALUED_0:def 19; then
(M*F).k1 = 0 by A5,A66,FUNCT_1:13; then
x.k = 0 & rx1.k1 = 0 & rx2.k1 = 0 by A67,A69;
hence x.k = (rx1-rx2).k by A68;
end;
suppose A70: F.k1 <> {}; then
consider p be object such that
A71: p in F.k1 by XBOOLE_0:def 1;
F.k1 in rng F by A5,A66,FUNCT_1:3; then
p in union rng F by A71,TARSKI:def 4; then
A72: p in dom f by A4,MESFUNC3:def 1; then
A73: (max-f).p = 0 implies (max+f).p = f.p by MESFUNC2:22;
reconsider p as Element of X by A71;
a.k1 is Real by A1,A4,A5,A66,A70,Th12; then
reconsider r = f.p as Real by A4,A5,A66,A71,MESFUNC3:def 1;
A74: a1.k1 = (max+f).p & a2.k1 = (max-f).p by A5,A66,A71,A20,A46;
A75: (max-f).p = -(f.p) implies (max+f).p = 0 by MESFUNC2:21;
per cases by MESFUNC2:18;
suppose A76: (max+f).p = f.p or (max-f).p = 0; then
(max-f).p = 0 by MESFUNC2:19; then
rx2.k1 = 0 by A69,A74;
hence x.k = (rx1-rx2).k
by A4,A5,A67,A68,A69,A74,A76,A66,A71,A73,MESFUNC3:def 1;
end;
suppose A77: (max+f).p = 0 or (max-f).p = -(f.p); then
rx1.k1 = 0 by A69,A74,A75; then
A78: (rx1-rx2).k = - ((rx2.k1) qua ExtReal) by A68;
a2.k1 = -(f.p) by A74,A72,A77,MESFUNC2:20; then
rx2.k1 = -(f.p * (M*F).k1) by A69,XXREAL_3:92;
hence x.k = (rx1-rx2).k by A4,A5,A78,A67,A66,A71,MESFUNC3:def 1;
end;
end;
end;
hence Integral(M,f)=Sum x by A64,A65,FUNCT_1:2,MESFUNC3:2;
end;
theorem Th19:
for A be non empty closed_interval Subset of REAL, f be PartFunc of A,REAL,
D be Division of A st f is bounded & A c= dom f holds
ex F be Finite_Sep_Sequence of Borel_Sets,
g be PartFunc of REAL,ExtREAL st
dom F = dom D
& union rng F = A
& (for k be Nat st k in dom F holds
(len D = 1 implies F.k = [.inf A,sup A.])
& (len D <> 1 implies
(k = 1 implies F.k = [. inf A,D.k .[)
& (1 < k < len D implies F.k = [. D.(k-'1), D.k .[)
& (k = len D implies F.k = [. D.(k-'1), D.k.])))
& g is_simple_func_in Borel_Sets
& (for x be Real st x in dom g holds
ex k be Nat st 1 <= k <= len F & x in F.k
& g.x = lower_bound rng(f|divset(D,k)) )
& dom g = A
& Integral(B-Meas,g) = lower_sum(f,D)
& for x be Real st x in A holds lower_bound rng f <= g.x <= f.x
proof
let A be non empty closed_interval Subset of REAL, f be PartFunc of A,REAL,
D be Division of A;
assume that
A1: f is bounded and
A2: A c= dom f;
consider a,b be Real such that
A3: a <= b & A = [.a,b.] by MEASURE5:14;
reconsider a1=a, b1=b as R_eal by XXREAL_0:def 1;
consider F be Finite_Sep_Sequence of Borel_Sets,
g be PartFunc of REAL,ExtREAL such that
A4: dom F = dom D and
A5: union rng F = A and
A6: for k be Nat st k in dom F holds
(len D = 1 implies F.k = [. a,b .])
& (len D <> 1 implies
(k = 1 implies F.k = [. a,D.k .[)
& (1 < k < len D implies F.k = [. D.(k-'1), D.k .[)
& (k = len D implies F.k = [. D.(k-'1), D.k.])) and
A7: g is_simple_func_in Borel_Sets and
A8: dom g = A and
A9: for x be Real st x in dom g holds
ex k be Nat st 1 <= k <= len F & x in F.k
& g.x = lower_bound rng(f|divset(D,k)) by A3,Th10;
A = [.lower_bound A,upper_bound A.] by INTEGRA1:4; then
A10: inf A = a & sup A = b by A3,INTEGRA1:5;
take F,g;
thus dom F = dom D by A4;
thus union rng F = A by A5;
thus for k be Nat st k in dom F holds
(len D = 1 implies F.k = [.inf A,sup A.])
& (len D <> 1 implies
(k = 1 implies F.k = [. inf A,D.k .[)
& (1 < k < len D implies F.k = [. D.(k-'1), D.k .[)
& (k = len D implies F.k = [. D.(k-'1), D.k.])) by A6,A10;
thus g is_simple_func_in Borel_Sets by A7;
thus for x be Real st x in dom g holds
ex k be Nat st 1 <= k <= len F & x in F.k
& g.x = lower_bound rng(f|divset(D,k)) by A9;
thus dom g = A by A8;
reconsider A1=A as Element of Borel_Sets by MEASUR12:72;
B-Meas.A = diameter A by MEASUR12:71; then
A11:B-Meas.A = b1-a1 by A3,MEASURE5:6; then
A12:B-Meas.A1 < +infty by XXREAL_0:4;
defpred H[Nat,ExtReal] means
$2 = lower_bound rng(f|divset(D,$1)) & $2 is Real;
A13: for k be Nat st k in Seg len F
ex r be Element of ExtREAL st H[k,r]
proof
let k be Nat;
assume k in Seg len F;
reconsider r = lower_bound rng(f|divset(D,k)) as
Element of ExtREAL by XXREAL_0:def 1;
take r;
thus H[k,r];
end;
consider h be FinSequence of ExtREAL such that
A14: dom h = Seg len F &
for k be Nat st k in Seg len F holds H[k,h.k] from FINSEQ_1:sch 5(A13);
A15:dom h = dom F by A14,FINSEQ_1:def 3;
A16:for k be Nat st k in dom F
for x be object st x in F.k holds g.x = h.k
proof
let k be Nat;
assume A17: k in dom F; then
A18: F.k in rng F by FUNCT_1:3;
let x be object;
assume A19: x in F.k; then
x in dom g by A5,A8,A18,TARSKI:def 4; then
consider i be Nat such that
A20: 1 <= i <= len F & x in F.i &
g.x = lower_bound rng(f|divset(D,i)) by A9;
k=i by A19,A20,PROB_2:def 2,XBOOLE_0:3;
hence g.x = h.k by A14,A17,A15,A20;
end;
defpred Z[Nat,ExtReal] means
$2 = h.$1*(B-Meas*F).$1 & $2 is Real;
A21: for k be Nat st k in Seg len F
ex r be Element of ExtREAL st Z[k,r]
proof
let k be Nat;
assume A22: k in Seg len F; then
A23: h.k = lower_bound rng(f|divset(D,k)) & h.k is Real by A14;
A24: F.k c= A by A5,A22,A14,A15,FUNCT_1:3,ZFMISC_1:74;
F.k in Borel_Sets by A22,A14,A15,PARTFUN1:4; then
0 <= B-Meas.(F.k) <= B-Meas.A1 by A24,SUPINF_2:51,MEASURE1:31; then
0 <= B-Meas.(F.k) < +infty by A11,XXREAL_0:2,4; then
0 <= (B-Meas*F).k < +infty by A22,A14,A15,FUNCT_1:13; then
A25: (B-Meas*F).k in REAL by XXREAL_0:14;
reconsider r = h.k * (B-Meas*F).k as Element of ExtREAL;
thus ex r be Element of ExtREAL st Z[k,r] by A25,A23;
end;
consider z be FinSequence of ExtREAL such that
A26: dom z = Seg len F &
for k be Nat st k in Seg len F holds Z[k,z.k] from FINSEQ_1:sch 5(A21);
A27: dom z = dom F by A26,FINSEQ_1:def 3;
A28: for k be Nat st k in dom z holds z.k = h.k*(B-Meas*F).k by A26;
A29:Integral(B-Meas,g) = Sum z
by A7,A8,A12,A16,A27,A28,Th18,A5,A15,MESFUNC3:def 1;
len lower_volume(f,D) = len D by INTEGRA1:def 7; then
A30:dom z = dom lower_volume(f,D) by A27,A4,FINSEQ_3:29;
A31:A = [.lower_bound A,upper_bound A.] by INTEGRA1:4; then
A32: lower_bound A = a & upper_bound A = b by A3,INTEGRA1:5;
for p be object st p in dom z holds z.p = lower_volume(f,D).p
proof
let p be object;
assume A33: p in dom z; then
reconsider p1=p as Nat;
A34: (B-Meas*F).p1 = vol divset(D,p1)
proof
per cases;
suppose A35: len D = 1; then
F.p1 = [.a,b.] by A33,A27,A6; then
B-Meas.(F.p1) = b-a by A3,Th5; then
A36: (B-Meas*F).p1 = b-a by A33,A27,FUNCT_1:13;
1 <= p1 <= 1 by A33,A27,A4,A35,FINSEQ_3:25; then
p1=1 by XXREAL_0:1; then
lower_bound divset(D,p1) = lower_bound A
& upper_bound divset(D,p1) = D.(len D)
by A33,A27,A4,A35,INTEGRA1:def 4; then
lower_bound divset(D,p1) = a & upper_bound divset(D,p1) = b
by A32,INTEGRA1:def 2;
hence (B-Meas*F).p1 = vol divset(D,p1) by A36,INTEGRA1:def 5;
end;
suppose A37: len D <> 1;
D.p1 in rng D & rng D c= A by A33,A27,A4,FUNCT_1:3,INTEGRA1:def 2; then
A38: a <= D.p1 <= b by A3,XXREAL_1:1;
per cases;
suppose A39: p1 = 1; then
F.p1 = [. a,D.1 .[ by A6,A33,A27,A37; then
B-Meas.(F.p1) = D.1 - a by A38,A39,Th5; then
A40: (B-Meas*F).p1 = D.1 - a by A33,A27,FUNCT_1:13;
lower_bound divset(D,p1) = lower_bound A
& upper_bound divset(D,p1) = D.1
by A33,A27,A4,A39,INTEGRA1:def 4;
hence (B-Meas*F).p1 = vol divset(D,p1) by A40,A32,INTEGRA1:def 5;
end;
suppose A41: p1 = len D;
len D >= 1 by FINSEQ_1:20; then
len D > 1 by A37,XXREAL_0:1; then
A42: p1-'1 >= 1 by A41,NAT_D:49; then
A43: p1-'1 = p1-1 by NAT_D:39; then
A44: F.p1 = [. D.(p1-1), D.p1 .] by A6,A33,A27,A37,A41;
p1-'1 in dom D by A42,A41,A43,FINSEQ_3:25,XREAL_1:43; then
D.(p1-1) <= D.p1 by A43,A33,A27,A4,VALUED_0:def 15,XREAL_1:43; then
B-Meas.(F.p1) = D.p1 - D.(p1-1) by A44,Th5; then
A45: (B-Meas*F).p1 = D.p1 - D.(p1-1) by A33,A27,FUNCT_1:13;
lower_bound divset(D,p1) = D.(p1-1) & upper_bound divset(D,p1) = D.p1
by A33,A27,A4,A41,A37,INTEGRA1:def 4;
hence (B-Meas*F).p1 = vol divset(D,p1) by A45,INTEGRA1:def 5;
end;
suppose A46: p1 <> 1 & p1 <> len D;
1 <= p1 <= len D by A33,A27,A4,FINSEQ_3:25; then
A47: 1 < p1 < len D by A46,XXREAL_0:1; then
A48: F.p1 = [. D.(p1-'1),D.p1 .[ by A6,A33,A27;
A49: 1 <= p1-'1 by A47,NAT_D:49; then
A50: p1-'1 = p1-1 by NAT_D:39;
p1-1 <= p1 by XREAL_1:43; then
p1-'1 < len D by A47,A50,XXREAL_0:2; then
p1-'1 in dom D by A49,FINSEQ_3:25; then
D.(p1-'1) <= D.p1 by A50,A33,A27,A4,VALUED_0:def 15,XREAL_1:43; then
B-Meas.(F.p1) = D.p1 - D.(p1-1) by A48,A50,Th5; then
A51: (B-Meas*F).p1 = D.p1 - D.(p1-1) by A33,A27,FUNCT_1:13;
lower_bound divset(D,p1) = D.(p1-1) & upper_bound divset(D,p1) = D.p1
by A33,A27,A4,A46,INTEGRA1:def 4;
hence (B-Meas*F).p1 = vol divset(D,p1) by A51,INTEGRA1:def 5;
end;
end;
end;
A52: h.p1 = lower_bound rng(f|divset(D,p1)) by A33,A14,A26;
z.p = h.p1 * (B-Meas*F).p1 by A26,A33; then
z.p = lower_bound rng(f|divset(D,p1)) * (vol divset(D,p1))
by A34,A52,XXREAL_3:def 5;
hence z.p = lower_volume(f,D).p by A33,A27,A4,INTEGRA1:def 7;
end; then
Sum z = Sum(lower_volume(f,D)) by A30,FUNCT_1:2,MESFUNC3:2;
hence Integral(B-Meas,g) = lower_sum(f,D) by A29,INTEGRA1:def 9;
thus for x be Real st x in A holds lower_bound rng f <= g.x <= f.x
proof
let x be Real;
assume A53: x in A; then
consider k be Nat such that
A54: 1 <= k <= len F & x in F.k
& g.x = lower_bound rng(f|divset(D,k)) by A8,A9;
A55: k in dom F by A54,FINSEQ_3:25;
A56: F.k c= divset(D,k)
proof
per cases;
suppose A57: len D = 1; then
A58: F.k = [. a,b .] by A6,A55;
len D = len F by A4,FINSEQ_3:29; then
k = 1 by A54,A57,XXREAL_0:1; then
lower_bound divset(D,k) = lower_bound A
& upper_bound divset(D,k) = D.1 by A55,A4,INTEGRA1:def 4; then
lower_bound divset(D,k) = lower_bound A
& upper_bound divset(D,k) = upper_bound A by A57,INTEGRA1:def 2;
hence F.k c= divset(D,k) by A31,A58,A3,INTEGRA1:4;
end;
suppose A59: len D <> 1;
per cases;
suppose A60: k = 1; then
lower_bound divset(D,k) = lower_bound A
& upper_bound divset(D,k) = D.k by A55,A4,INTEGRA1:def 4; then
A61: divset(D,k) = [. a,D.k .] by A32,INTEGRA1:4;
F.k = [. a, D.k .[ by A55,A59,A60,A6;
hence F.k c= divset(D,k) by A61,XXREAL_1:24;
end;
suppose A62: k = len D; then
lower_bound divset(D,k) = D.(k-1)
& upper_bound divset(D,k) = D.k by A55,A4,A59,INTEGRA1:def 4; then
A63: divset(D,k) = [. D.(k-1),D.k .] by INTEGRA1:4;
1 < k by A54,A62,A59,XXREAL_0:1; then
1 <= k-'1 by NAT_D:49; then
k-'1 = k-1 by NAT_D:39;
hence F.k c= divset(D,k) by A55,A59,A62,A6,A63;
end;
suppose A64: k <> 1 & k <> len D; then
lower_bound divset(D,k) = D.(k-1)
& upper_bound divset(D,k) = D.k by A55,A4,INTEGRA1:def 4; then
A65: divset(D,k) = [. D.(k-1),D.k .] by INTEGRA1:4;
len D = len F by A4,FINSEQ_3:29; then
A66: 1 < k & k < len D by A54,A64,XXREAL_0:1; then
1 <= k-'1 by NAT_D:49; then
k-'1 = k-1 by NAT_D:39; then
F.k = [. D.(k-1),D.k .[ by A55,A66,A6;
hence F.k c= divset(D,k) by A65,XXREAL_1:24;
end;
end;
end; then
A67: x in dom(f|divset(D,k)) by A54,A2,A53,RELAT_1:57;
divset(D,k) c= A by A55,A4,INTEGRA1:8; then
A68: divset(D,k) c= dom f by A2;
A69: rng f is bounded_below by A1,SEQ_2:def 8,INTEGRA1:11;
f = f|dom f; then
f|divset(D,k) is bounded by A1,A68,RFUNCT_1:74; then
A70: rng(f|divset(D,k)) is real-bounded by INTEGRA1:15;
(f|divset(D,k)).x = f.x by A54,A56,FUNCT_1:49; then
f.x in rng(f|divset(D,k)) by A67,FUNCT_1:3;
hence lower_bound rng f <= g.x <= f.x
by A69,A54,A70,RELAT_1:70,SEQ_4:def 2,47;
end;
end;
theorem Th20:
for A be non empty closed_interval Subset of REAL, f be PartFunc of A,REAL,
D be Division of A st f is bounded & A c= dom f holds
ex F be Finite_Sep_Sequence of Borel_Sets,
g be PartFunc of REAL,ExtREAL st
dom F = dom D
& union rng F = A
& (for k be Nat st k in dom F holds
(len D = 1 implies F.k = [.inf A,sup A.])
& (len D <> 1 implies
(k = 1 implies F.k = [. inf A,D.k .[)
& (1 < k < len D implies F.k = [. D.(k-'1), D.k .[)
& (k = len D implies F.k = [. D.(k-'1), D.k.])))
& g is_simple_func_in Borel_Sets
& (for x be Real st x in dom g holds
ex k be Nat st 1 <= k <= len F & x in F.k
& g.x = upper_bound rng(f|divset(D,k)) )
& dom g = A
& Integral(B-Meas,g) = upper_sum(f,D)
& for x be Real st x in A holds upper_bound rng f >= g.x >= f.x
proof
let A be non empty closed_interval Subset of REAL, f be PartFunc of A,REAL,
D be Division of A;
assume that
A1: f is bounded and
A2: A c= dom f;
consider a,b be Real such that
A3: a <= b & A = [.a,b.] by MEASURE5:14;
reconsider a1=a, b1=b as R_eal by XXREAL_0:def 1;
consider F be Finite_Sep_Sequence of Borel_Sets,
g be PartFunc of REAL,ExtREAL such that
A4: dom F = dom D and
A5: union rng F = A and
A6: for k be Nat st k in dom F holds
(len D = 1 implies F.k = [. a,b .])
& (len D <> 1 implies
(k = 1 implies F.k = [. a,D.k .[)
& (1 < k < len D implies F.k = [. D.(k-'1), D.k .[)
& (k = len D implies F.k = [. D.(k-'1), D.k.])) and
A7: g is_simple_func_in Borel_Sets and
A8: dom g = A and
A9: for x be Real st x in dom g holds
ex k be Nat st 1 <= k <= len F & x in F.k
& g.x = upper_bound rng(f|divset(D,k)) by A3,Th11;
A = [.lower_bound A,upper_bound A.] by INTEGRA1:4; then
A10: inf A = a & sup A = b by A3,INTEGRA1:5;
take F,g;
thus dom F = dom D by A4;
thus union rng F = A by A5;
thus for k be Nat st k in dom F holds
(len D = 1 implies F.k = [.inf A,sup A.])
& (len D <> 1 implies
(k = 1 implies F.k = [. inf A,D.k .[)
& (1 < k < len D implies F.k = [. D.(k-'1), D.k .[)
& (k = len D implies F.k = [. D.(k-'1), D.k.])) by A6,A10;
thus
g is_simple_func_in Borel_Sets by A7;
thus
for x be Real st x in dom g holds
ex k be Nat st 1 <= k <= len F & x in F.k
& g.x = upper_bound rng(f|divset(D,k)) by A9;
thus dom g = A by A8;
reconsider A1=A as Element of Borel_Sets by MEASUR12:72;
B-Meas.A = diameter A by MEASUR12:71; then
B-Meas.A = b1-a1 by A3,MEASURE5:6; then
A11:B-Meas.A1 < +infty by XXREAL_0:4;
defpred H[Nat,ExtReal] means
$2 = upper_bound rng(f|divset(D,$1)) & $2 is Real;
A12: for k be Nat st k in Seg len F
ex r be Element of ExtREAL st H[k,r]
proof
let k be Nat;
assume k in Seg len F;
upper_bound rng(f|divset(D,k)) is Element of ExtREAL by XXREAL_0:def 1;
hence thesis;
end;
consider h be FinSequence of ExtREAL such that
A13: dom h = Seg len F &
for k be Nat st k in Seg len F holds H[k,h.k] from FINSEQ_1:sch 5(A12);
A14:dom h = dom F by A13,FINSEQ_1:def 3;
A15:for k be Nat st k in dom F
for x be object st x in F.k holds g.x = h.k
proof
let k be Nat;
assume A16: k in dom F; then
A17: F.k in rng F by FUNCT_1:3;
let x be object;
assume A18: x in F.k; then
x in dom g by A5,A8,A17,TARSKI:def 4; then
consider i be Nat such that
A19: 1 <= i <= len F & x in F.i &
g.x = upper_bound rng(f|divset(D,i)) by A9;
k=i by A18,A19,XBOOLE_0:3,PROB_2:def 2;
hence g.x = h.k by A19,A13,A16,A14;
end;
defpred Z[Nat,ExtReal] means
$2 = h.$1*(B-Meas*F).$1 & $2 is Real;
A20: for k be Nat st k in Seg len F
ex r be Element of ExtREAL st Z[k,r]
proof
let k be Nat;
assume A21: k in Seg len F; then
A22: h.k = upper_bound rng(f|divset(D,k)) & h.k is Real by A13;
A23: F.k c= A by A5,A21,A14,A13,FUNCT_1:3,ZFMISC_1:74;
F.k in Borel_Sets by A21,A14,A13,PARTFUN1:4; then
0 <= B-Meas.(F.k) <= B-Meas.A1 by A23,SUPINF_2:51,MEASURE1:31; then
0 <= B-Meas.(F.k) < +infty by A11,XXREAL_0:4; then
0 <= (B-Meas*F).k < +infty by A21,A13,A14,FUNCT_1:13; then
(B-Meas*F).k in REAL by XXREAL_0:14;
hence ex r be Element of ExtREAL st Z[k,r] by A22;
end;
consider z be FinSequence of ExtREAL such that
A24: dom z = Seg len F &
for k be Nat st k in Seg len F holds Z[k,z.k] from FINSEQ_1:sch 5(A20);
A25:dom z = dom F by A24,FINSEQ_1:def 3;
for k be Nat st k in dom z holds z.k = h.k*(B-Meas*F).k by A24; then
A26:Integral(B-Meas,g) = Sum z
by A5,A8,A14,A7,A11,A15,A25,Th18,MESFUNC3:def 1;
len upper_volume(f,D) = len D by INTEGRA1:def 6; then
A27:dom z = dom upper_volume(f,D) by A25,A4,FINSEQ_3:29;
A28:A = [.lower_bound A,upper_bound A.] by INTEGRA1:4; then
A29: lower_bound A = a & upper_bound A = b by A3,INTEGRA1:5;
for p be object st p in dom z holds z.p = upper_volume(f,D).p
proof
let p be object;
assume A30: p in dom z; then
reconsider p1=p as Nat;
A31: (B-Meas*F).p1 = vol divset(D,p1)
proof
per cases;
suppose A32: len D = 1; then
F.p1 = [.a,b.] by A30,A25,A6; then
B-Meas.(F.p1) = b-a by A3,Th5; then
A33: (B-Meas*F).p1 = b-a by A30,A25,FUNCT_1:13;
1 <= p1 <= 1 by A30,A25,A4,A32,FINSEQ_3:25; then
p1=1 by XXREAL_0:1; then
lower_bound divset(D,p1) = lower_bound A
& upper_bound divset(D,p1) = D.(len D)
by A30,A25,A4,A32,INTEGRA1:def 4; then
lower_bound divset(D,p1) = a & upper_bound divset(D,p1) = b
by A29,INTEGRA1:def 2;
hence (B-Meas*F).p1 = vol divset(D,p1) by A33,INTEGRA1:def 5;
end;
suppose A34: len D <> 1;
D.p1 in rng D & rng D c= A by A30,A25,A4,FUNCT_1:3,INTEGRA1:def 2; then
A35: a <= D.p1 <= b by A3,XXREAL_1:1;
per cases;
suppose A36: p1 = 1; then
F.p1 = [. a,D.1 .[ by A6,A30,A25,A34; then
B-Meas.(F.p1) = D.1 - a by A35,A36,Th5; then
A37: (B-Meas*F).p1 = D.1 - a by A30,A25,FUNCT_1:13;
lower_bound divset(D,p1) = a & upper_bound divset(D,p1) = D.1
by A29,A30,A25,A4,A36,INTEGRA1:def 4;
hence (B-Meas*F).p1 = vol divset(D,p1) by A37,INTEGRA1:def 5;
end;
suppose A38: p1 = len D;
len D >= 1 by FINSEQ_1:20; then
len D > 1 by A34,XXREAL_0:1; then
A39: p1-'1 >= 1 by A38,NAT_D:49; then
A40: p1-'1 = p1-1 by NAT_D:39; then
A41: F.p1 = [. D.(p1-1), D.p1 .] by A6,A30,A25,A34,A38;
p1-'1 in dom D by A39,A38,A40,FINSEQ_3:25,XREAL_1:43; then
D.(p1-1) <= D.p1 by A40,A30,A25,A4,VALUED_0:def 15,XREAL_1:43; then
B-Meas.(F.p1) = D.p1 - D.(p1-1) by A41,Th5; then
A42: (B-Meas*F).p1 = D.p1 - D.(p1-1) by A30,A25,FUNCT_1:13;
lower_bound divset(D,p1) = D.(p1-1) & upper_bound divset(D,p1) = D.p1
by A30,A25,A4,A38,A34,INTEGRA1:def 4;
hence (B-Meas*F).p1 = vol divset(D,p1) by A42,INTEGRA1:def 5;
end;
suppose A43: p1 <> 1 & p1 <> len D;
1 <= p1 <= len D by A30,A25,A4,FINSEQ_3:25; then
A44: 1 < p1 < len D by A43,XXREAL_0:1; then
A45: F.p1 = [. D.(p1-'1),D.p1 .[ by A6,A30,A25;
A46: 1 <= p1-'1 by A44,NAT_D:49; then
A47: p1-'1 = p1-1 by NAT_D:39;
p1-1 <= p1 by XREAL_1:43; then
p1-'1 < len D by A44,A47,XXREAL_0:2; then
p1-'1 in dom D by A46,FINSEQ_3:25; then
D.(p1-'1) <= D.p1 by A47,A30,A25,A4,VALUED_0:def 15,XREAL_1:43; then
B-Meas.(F.p1) = D.p1 - D.(p1-1) by A45,A47,Th5; then
A48: (B-Meas*F).p1 = D.p1 - D.(p1-1) by A30,A25,FUNCT_1:13;
lower_bound divset(D,p1) = D.(p1-1) & upper_bound divset(D,p1) = D.p1
by A30,A25,A4,A43,INTEGRA1:def 4;
hence (B-Meas*F).p1 = vol divset(D,p1) by A48,INTEGRA1:def 5;
end;
end;
end;
A49: h.p1 = upper_bound rng(f|divset(D,p1)) by A30,A13,A24;
z.p = h.p1 * (B-Meas*F).p1 by A24,A30; then
z.p = upper_bound rng(f|divset(D,p1)) * (vol divset(D,p1))
by A31,A49,XXREAL_3:def 5;
hence z.p = upper_volume(f,D).p by A30,A25,A4,INTEGRA1:def 6;
end; then
Sum z = Sum(upper_volume(f,D)) by A27,FUNCT_1:2,MESFUNC3:2;
hence Integral(B-Meas,g) = upper_sum(f,D) by A26,INTEGRA1:def 8;
thus for x be Real st x in A holds upper_bound rng f >= g.x >= f.x
proof
let x be Real;
assume A50: x in A; then
consider k be Nat such that
A51: 1 <= k <= len F & x in F.k
& g.x = upper_bound rng(f|divset(D,k)) by A8,A9;
A52: k in dom F by A51,FINSEQ_3:25;
A53: F.k c= divset(D,k)
proof
per cases;
suppose A54: len D = 1; then
A55: F.k = [. a,b .] by A6,A52;
len D = len F by A4,FINSEQ_3:29; then
k = 1 by A51,A54,XXREAL_0:1; then
lower_bound divset(D,k) = lower_bound A
& upper_bound divset(D,k) = D.1 by A52,A4,INTEGRA1:def 4; then
lower_bound divset(D,k) = lower_bound A
& upper_bound divset(D,k) = upper_bound A by A54,INTEGRA1:def 2;
hence F.k c= divset(D,k) by A55,A28,A3,INTEGRA1:4;
end;
suppose A56: len D <> 1;
per cases;
suppose A57: k = 1; then
lower_bound divset(D,k) = lower_bound A
& upper_bound divset(D,k) = D.k by A52,A4,INTEGRA1:def 4; then
A58: divset(D,k) = [. a,D.k .] by A29,INTEGRA1:4;
F.k = [. a, D.k .[ by A52,A56,A57,A6;
hence F.k c= divset(D,k) by A58,XXREAL_1:24;
end;
suppose A59: k = len D; then
lower_bound divset(D,k) = D.(k-1)
& upper_bound divset(D,k) = D.k by A52,A4,A56,INTEGRA1:def 4; then
A60: divset(D,k) = [. D.(k-1),D.k .] by INTEGRA1:4;
1 < k by A51,A59,A56,XXREAL_0:1; then
1 <= k-'1 by NAT_D:49; then
k-'1 = k-1 by NAT_D:39;
hence F.k c= divset(D,k) by A52,A56,A59,A6,A60;
end;
suppose A61: k <> 1 & k <> len D; then
lower_bound divset(D,k) = D.(k-1)
& upper_bound divset(D,k) = D.k by A52,A4,INTEGRA1:def 4; then
A62: divset(D,k) = [. D.(k-1),D.k .] by INTEGRA1:4;
len D = len F by A4,FINSEQ_3:29; then
A63: 1 < k & k < len D by A51,A61,XXREAL_0:1; then
1 <= k-'1 by NAT_D:49; then
k-'1 = k-1 by NAT_D:39; then
F.k = [. D.(k-1),D.k .[ by A52,A63,A6;
hence F.k c= divset(D,k) by A62,XXREAL_1:24;
end;
end;
end; then
A64: x in dom(f|divset(D,k)) by A51,A2,A50,RELAT_1:57;
divset(D,k) c= A by A52,A4,INTEGRA1:8; then
A65: divset(D,k) c= dom f by A2;
A66: rng f is bounded_above by A1,SEQ_2:def 8,INTEGRA1:13;
f = f|dom f; then
f|divset(D,k) is bounded by A1,A65,RFUNCT_1:74; then
A67: rng(f|divset(D,k)) is real-bounded by INTEGRA1:15;
(f|divset(D,k)).x = f.x by A51,A53,FUNCT_1:49; then
f.x in rng(f|divset(D,k)) by A64,FUNCT_1:3;
hence upper_bound rng f >= g.x >= f.x by
A66,A51,A67,SEQ_4:def 1,48,RELAT_1:70;
end;
end;
theorem Th21:
for A be non empty closed_interval Subset of REAL, f be PartFunc of A,REAL
st f is bounded & A c= dom f & vol A > 0 holds
ex F be with_the_same_dom Functional_Sequence of REAL,ExtREAL,
I be ExtREAL_sequence st
A = dom(F.0)
& (for n be Nat holds
F.n is_simple_func_in Borel_Sets
& Integral(B-Meas,F.n) = lower_sum(f,EqDiv(A,2|^n))
& (for x be Real st x in A holds lower_bound rng f <= (F.n).x <= f.x) )
& (for n,m be Nat st n <= m holds for x be Element of REAL st x in A holds
(F.n).x <= (F.m).x)
& (for x be Element of REAL st x in A holds
F#x is convergent & lim(F#x) = sup(F#x) & sup(F#x) <= f.x)
& lim F is_integrable_on B-Meas
& (for n be Nat holds I.n = Integral(B-Meas,F.n))
& I is convergent & lim I = Integral(B-Meas,lim F)
proof
let A be non empty closed_interval Subset of REAL, f be PartFunc of A,REAL;
assume that
A1: f is bounded and
A2: A c= dom f and
A3: vol A > 0;
reconsider A1 =A as Element of Borel_Sets
by MEASUR12:72;
defpred P[Nat,PartFunc of REAL,ExtREAL] means
A = dom $2
& $2 is_simple_func_in Borel_Sets
& Integral(B-Meas,$2) = lower_sum(f,EqDiv(A,2|^$1))
& (for x be Real st x in A holds lower_bound rng f <= $2.x <= f.x)
& ex K be Finite_Sep_Sequence of Borel_Sets st
dom K = dom EqDiv(A,2|^$1)
& union rng K = A
& (for k be Nat st k in dom K holds
(len EqDiv(A,2|^$1) = 1 implies K.k = [.inf A,sup A.])
& (len EqDiv(A,2|^$1) <> 1 implies
(k = 1 implies K.k = [. inf A,EqDiv(A,2|^$1).k .[)
& (1 < k < len EqDiv(A,2|^$1) implies
K.k = [. EqDiv(A,2|^$1).(k-'1), EqDiv(A,2|^$1).k .[)
& (k = len EqDiv(A,2|^$1) implies
K.k = [. EqDiv(A,2|^$1).(k-'1), EqDiv(A,2|^$1).k.])))
& (for x be Real st x in dom $2 holds
ex k be Nat st 1 <= k <= len K & x in K.k
& $2.x = lower_bound rng(f|divset(EqDiv(A,2|^$1),k)) );
A4: for n be Element of NAT ex g be Element of PFuncs(REAL,ExtREAL) st P[n,g]
proof
let n be Element of NAT;
consider K be Finite_Sep_Sequence of Borel_Sets,
g be PartFunc of REAL,ExtREAL such that
A5: dom K = dom EqDiv(A,2|^n)
& union rng K = A
& (for k be Nat st k in dom K holds
(len EqDiv(A,2|^n) = 1 implies K.k = [.inf A,sup A.])
& (len EqDiv(A,2|^n) <> 1 implies
(k = 1 implies K.k = [. inf A,EqDiv(A,2|^n).k .[)
& (1 < k < len EqDiv(A,2|^n) implies
K.k = [. EqDiv(A,2|^n).(k-'1), EqDiv(A,2|^n).k .[)
& (k = len EqDiv(A,2|^n) implies
K.k = [. EqDiv(A,2|^n).(k-'1), EqDiv(A,2|^n).k.])))
& g is_simple_func_in Borel_Sets
& (for x be Real st x in dom g holds
ex k be Nat st 1 <= k <= len K & x in K.k
& g.x = lower_bound rng(f|divset(EqDiv(A,2|^n),k)) )
& dom g = A
& Integral(B-Meas,g) = lower_sum(f,EqDiv(A,2|^n))
& for x be Real st x in A holds lower_bound rng f <= g.x <= f.x
by A1,A2,Th19;
g is Element of PFuncs(REAL,ExtREAL) by PARTFUN1:45;
hence thesis by A5;
end;
consider F be Function of NAT,PFuncs(REAL,ExtREAL) such that
A6: for n be Element of NAT holds P[n,F.n] from FUNCT_2:sch 3(A4);
reconsider F as Functional_Sequence of REAL,ExtREAL;
for n,m be Nat holds dom(F.n) = dom(F.m)
proof
let n,m be Nat;
n is Element of NAT & m is Element of NAT by ORDINAL1:def 12; then
P[n,F.n] & P[m,F.m] by A6;
hence thesis;
end; then
reconsider F as with_the_same_dom Functional_Sequence of REAL,ExtREAL
by MESFUNC8:def 2;
take F;
A7:A = dom(F.0) by A6;
A8:for n be Nat holds
F.n is_simple_func_in Borel_Sets
& Integral(B-Meas,F.n) = lower_sum(f,EqDiv(A,2|^n))
& (for x be Real st x in A holds lower_bound rng f <= (F.n).x <= f.x)
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 12;
hence thesis by A6;
end;
A9: for n,m be Nat st n <= m holds
for x be Element of REAL st x in A holds (F.n).x <= (F.m).x
proof
let n,m be Nat;
assume A10: n <= m;
A11: n is Element of NAT & m is Element of NAT by ORDINAL1:def 12;
let x be Element of REAL;
assume A12: x in A;
consider Kn be Finite_Sep_Sequence of Borel_Sets such that
A13: dom Kn = dom EqDiv(A,2|^n)
& union rng Kn = A
& (for k be Nat st k in dom Kn holds
(len EqDiv(A,2|^n) = 1 implies Kn.k = [.inf A,sup A.])
& (len EqDiv(A,2|^n) <> 1 implies
(k = 1 implies Kn.k = [. inf A,EqDiv(A,2|^n).k .[)
& (1 < k < len EqDiv(A,2|^n) implies
Kn.k = [. EqDiv(A,2|^n).(k-'1), EqDiv(A,2|^n).k .[)
& (k = len EqDiv(A,2|^n) implies
Kn.k = [. EqDiv(A,2|^n).(k-'1), EqDiv(A,2|^n).k.])))
& (for x be Real st x in dom (F.n) holds
ex k be Nat st 1 <= k <= len Kn & x in Kn.k
& (F.n).x = lower_bound rng(f|divset(EqDiv(A,2|^n),k)) ) by A6,A11;
consider Km be Finite_Sep_Sequence of Borel_Sets such that
A14: dom Km = dom EqDiv(A,2|^m)
& union rng Km = A
& (for k be Nat st k in dom Km holds
(len EqDiv(A,2|^m) = 1 implies Km.k = [.inf A,sup A.])
& (len EqDiv(A,2|^m) <> 1 implies
(k = 1 implies Km.k = [. inf A,EqDiv(A,2|^m).k .[)
& (1 < k < len EqDiv(A,2|^m) implies
Km.k = [. EqDiv(A,2|^m).(k-'1), EqDiv(A,2|^m).k .[)
& (k = len EqDiv(A,2|^m) implies
Km.k = [. EqDiv(A,2|^m).(k-'1), EqDiv(A,2|^m).k.])))
& (for x be Real st x in dom (F.m) holds
ex k be Nat st 1 <= k <= len Km & x in Km.k
& (F.m).x = lower_bound rng(f|divset(EqDiv(A,2|^m),k)) ) by A6,A11;
A15: len EqDiv(A,2|^n) = len Kn & len EqDiv(A,2|^m) = len Km
by A13,A14,FINSEQ_3:29;
x in dom(F.n) by A6,A11,A12; then
consider k1 be Nat such that
A16: 1 <= k1 <= len Kn & x in Kn.k1
& (F.n).x = lower_bound rng(f|divset(EqDiv(A,2|^n),k1)) by A13;
x in dom(F.m) by A6,A11,A12; then
consider k2 be Nat such that
A17: 1 <= k2 <= len Km & x in Km.k2
& (F.m).x = lower_bound rng(f|divset(EqDiv(A,2|^m),k2)) by A14;
A18:k1-1 = k1-'1 & k2-1 = k2-'1 by A16,A17,XREAL_1:48,XREAL_0:def 2;
A19: k1 in dom Kn & k2 in dom Km by A16,A17,FINSEQ_3:25; then
divset(EqDiv(A,2|^n),k1) c= A by A13,INTEGRA1:8; then
A20: divset(EqDiv(A,2|^n),k1) c= dom f by A2;
f = f|dom f; then
f|divset(EqDiv(A,2|^n),k1) is bounded by A1,A20,RFUNCT_1:74; then
A21:rng(f|divset(EqDiv(A,2|^n),k1)) is real-bounded by INTEGRA1:15;
divset(EqDiv(A,2|^m),k2) c= A by A14,A19,INTEGRA1:8; then
divset(EqDiv(A,2|^m),k2) c= dom f by A2; then
dom(f|divset(EqDiv(A,2|^m),k2)) = divset(EqDiv(A,2|^m),k2)
by RELAT_1:62; then
A22: rng(f|divset(EqDiv(A,2|^m),k2)) <> {} by RELAT_1:42;
A23: 2|^n > 0 & 2|^m > 0 by NEWTON:83; then
A24: EqDiv(A,2|^n) divide_into_equal 2|^n
& EqDiv(A,2|^m) divide_into_equal 2|^m by A3,Def1; then
A25: len EqDiv(A,2|^n) = 2|^n & len EqDiv(A,2|^m) = 2|^m
by INTEGRA4:def 1; then
A26: EqDiv(A,2|^n).k1 = lower_bound A + (vol A)/(2|^n)*k1
& EqDiv(A,2|^m).k2 = lower_bound A + (vol A)/(2|^m)*k2
by A24,A13,A14,A16,A17,FINSEQ_3:25,INTEGRA4:def 1;
A27: m-n >= 0 by A10,XREAL_1:48;
A28: m-'n = m-n by A10,XREAL_1:48,XREAL_0:def 2;
2|^n >= 1 & 2|^m >= 1 by A23,NAT_1:14; then
A29: 2|^n-'1 = 2|^n-1 & 2|^m-'1 = 2|^m-1 by XREAL_0:def 2,XREAL_1:48;
A30: 2|^(m-'n)*(2|^n-1) = 2|^(m-'n)*2|^n - 2|^(m-'n)
.= 2|^(m-'n+n) - 2|^(m-'n) by NEWTON:8
.= 2|^m - 2|^(m-'n) by A27,NAT_D:72;
A31: 2|^(m-'n) <= 2|^m by PREPOWER:93,NAT_D:35;
A32: now assume 1 <> k1; then
1 < k1 by A16,XXREAL_0:1; then
A33: k1 -' 1 >= 1 by NAT_1:14,NAT_D:36;
k1 -' 1 <= k1 by NAT_D:35; then
k1 -' 1 <= len Kn by A16,XXREAL_0:2;
hence EqDiv(A,2|^n).(k1-'1) = lower_bound A + (vol A)/(2|^n)*(k1-'1)
by A24,A25,A33,A13,FINSEQ_3:25,INTEGRA4:def 1;
end;
A34: now assume 1 <> k2; then
1 < k2 by A17,XXREAL_0:1; then
A35: k2 -' 1 >= 1 by NAT_1:14,NAT_D:36;
k2 -' 1 <= k2 by NAT_D:35; then
k2 -' 1 <= len Km by A17,XXREAL_0:2;
hence EqDiv(A,2|^m).(k2-'1) = lower_bound A + (vol A)/(2|^m)*(k2-'1)
by A24,A25,A35,A14,FINSEQ_3:25,INTEGRA4:def 1;
end;
A36: 2|^(m-'n) > 0 by NEWTON:83;
2|^n * 2|^(m-'n) = 2|^m & 2|^n * (2|^(m-'n)-'1) < 2|^m
by A10,Lm5; then
A37: 2|^n = 2|^m / 2|^(m-'n) by A36,XCMPLX_1:89;
A38: (vol A)/2|^n = (vol A)/2|^m * 2|^(m-'n)
by A37,XCMPLX_1:81; then
A39: (vol A)/(2|^n)*k1 = (vol A)/(2|^m)*(k1*(2|^(m-'n))) &
(vol A)/(2|^n)*(k1-'1) = (vol A)/(2|^m) * ((k1-'1)*(2|^(m-'n)));
divset(EqDiv(A,2|^m),k2) c= divset(EqDiv(A,2|^n),k1)
proof
per cases;
suppose A40: len EqDiv(A,2|^m) = 1; then
A41: 2|^n <= 1 by A10,A25,PREPOWER:93;
len EqDiv(A,2|^n) = 1 by A25,A10,A40,PREPOWER:93,NAT_1:25; then
len Kn = 1 by A13,FINSEQ_3:29; then
k1 = 1 by A16,XXREAL_0:1; then
divset(EqDiv(A,2|^n),k1) = A by A3,A41,A25,Lm4,NAT_1:25;
hence divset(EqDiv(A,2|^m),k2) c= divset(EqDiv(A,2|^n),k1)
by A19,A14,INTEGRA1:8;
end;
suppose A42: len EqDiv(A,2|^m) <> 1;
per cases;
suppose A43: len EqDiv(A,2|^n) = 1; then
len Kn = 1 by A13,FINSEQ_3:29; then
k1 = 1 by A16,XXREAL_0:1; then
divset(EqDiv(A,2|^n),k1) = A by A3,A43,Lm4;
hence divset(EqDiv(A,2|^m),k2) c= divset(EqDiv(A,2|^n),k1)
by A19,A14,INTEGRA1:8;
end;
suppose A44: len EqDiv(A,2|^n) <> 1 & k2 = 1; then
Km.k2 = [. inf A,EqDiv(A,2|^m).k2 .[ by A14,A19,A42; then
A45: inf A <= x < EqDiv(A,2|^m).k2 by A17,XXREAL_1:3;
2|^n divides 2|^m by A10,NEWTON:89; then
2|^n <= 2|^m by A23,NAT_D:7; then
A46: (vol A)/(2|^m)*1 <= (vol A)/(2|^n)*1 by A3,A23,XREAL_1:118;
(vol A)/(2|^n)*1 <= (vol A)/(2|^n)*k1
by A16,A3,XREAL_1:64; then
(vol A)/(2|^m)*1 <= (vol A)/(2|^n)*k1 by A46,XXREAL_0:2; then
A47: EqDiv(A,2|^m).k2 <= EqDiv(A,2|^n).k1 by A44,A26,XREAL_1:7;
now assume A48: k1 <> 1; then
1 < k1 by A16,XXREAL_0:1; then
k1 -' 1 >= 1 by NAT_1:14,NAT_D:36; then
(vol A)/(2|^n)*1 <= (vol A)/(2|^n)*(k1-'1)
by A3,XREAL_1:64; then
(vol A)/(2|^m)*1 <= (vol A)/(2|^n)*(k1-'1) by A46,XXREAL_0:2; then
A49: EqDiv(A,2|^m).k2 <= EqDiv(A,2|^n).(k1-'1) by A44,A26,A48,A32
,XREAL_1:7;
per cases by A48,A16,A15,XXREAL_0:1;
suppose 1 < k1 < len EqDiv(A,2|^n); then
Kn.k1 = [. EqDiv(A,2|^n).(k1-'1),EqDiv(A,2|^n).k1 .[
by A13,A19; then
EqDiv(A,2|^n).(k1-'1) <= x < EqDiv(A,2|^n).k1 by A16,XXREAL_1:3;
hence contradiction by A45,A49,XXREAL_0:2;
end;
suppose k1 = len EqDiv(A,2|^n); then
Kn.k1 = [. EqDiv(A,2|^n).(k1-'1),EqDiv(A,2|^n).k1 .]
by A13,A19,A44; then
EqDiv(A,2|^n).(k1-'1) <= x <= EqDiv(A,2|^n).k1 by A16,XXREAL_1:1;
hence contradiction by A45,A49,XXREAL_0:2;
end;
end; then
lower_bound divset(EqDiv(A,2|^n),k1) = lower_bound A
& upper_bound divset(EqDiv(A,2|^n),k1) = EqDiv(A,2|^n).k1
by A13,A19,INTEGRA1:def 4; then
A50: divset(EqDiv(A,2|^n),k1)
= [.lower_bound A, EqDiv(A,2|^n).k1 .] by INTEGRA1:4;
lower_bound divset(EqDiv(A,2|^m),k2) = lower_bound A
& upper_bound divset(EqDiv(A,2|^m),k2) = EqDiv(A,2|^m).k2
by A44,A14,A19,INTEGRA1:def 4; then
divset(EqDiv(A,2|^m),k2)
= [.lower_bound A, EqDiv(A,2|^m).k2 .] by INTEGRA1:4;
hence divset(EqDiv(A,2|^m),k2) c= divset(EqDiv(A,2|^n),k1)
by A47,A50,XXREAL_1:34;
end;
suppose A51: len EqDiv(A,2|^n) <> 1 & k2 = len EqDiv(A,2|^m); then
Km.k2 = [. EqDiv(A,2|^m).(k2-'1), EqDiv(A,2|^m).k2 .]
by A14,A19,A42; then
A52: lower_bound A + (vol A)/(2|^m)*(k2-'1) <= x
& x <= lower_bound A + (vol A)/(2|^m)*k2
by A26,A42,A51,A34,A17,XXREAL_1:1;
A53: now assume A54: k1 <> len EqDiv(A,2|^n);
per cases by A15,A16,A54,XXREAL_0:1;
suppose A55: k1 = 1; then
Kn.k1 = [. inf A, EqDiv(A,2|^n).1 .[ by A51,A13,A19; then
inf A <= x < EqDiv(A,2|^n).1 by A16,XXREAL_1:3; then
A56: x < lower_bound A + (vol A)/(2|^m)*2|^(m-'n)
by A55,A26,A37,XCMPLX_1:82;
now assume 2|^(m-'n) = 2|^m; then
m-'n = m by PEPIN:30; then
2|^n = 1 by A28,NEWTON:4;
hence contradiction by A51,A24,INTEGRA4:def 1;
end; then
2|^(m-'n) < 2|^m by A31,XXREAL_0:1; then
2|^(m-'n)+1 <= 2|^m by NAT_1:13; then
2|^(m-'n) <= k2-'1 by A29,A51,A25,XREAL_1:19; then
(vol A)/(2|^m)*2|^(m-'n) <= (vol A)/(2|^m)*(k2-'1)
by A3,XREAL_1:64; then
lower_bound A + (vol A)/(2|^m)*2|^(m-'n)
<= lower_bound A + (vol A)/(2|^m)*(k2-'1) by XREAL_1:6;
hence contradiction by A52,A56,XXREAL_0:2;
end;
suppose A57: 1 < k1 < len EqDiv(A,2|^n); then
Kn.k1 = [. EqDiv(A,2|^n).(k1-'1), EqDiv(A,2|^n).k1 .[
by A13,A19; then
A58: lower_bound A + (vol A)/(2|^n)*(k1-'1) <= x
& x < lower_bound A + (vol A)/(2|^n)*k1 by A26,A57,A32,A16,XXREAL_1:3;
k1 < len EqDiv(A,2|^n) by A54,A15,A16,XXREAL_0:1; then
k1+1 <= 2|^n by A25,NAT_1:13; then
k1 <= 2|^n-1 by XREAL_1:19; then
A59: (vol A)/(2|^n)*k1 <= (vol A)/(2|^n)*(2|^n-1)
by A3,XREAL_1:64;
2|^m - 2|^(m-'n) <= k2-'1 by A29,A51,A25,A36
,NAT_1:14,XREAL_1:10; then
(vol A)/(2|^m)*(2|^(m-'n)*(2|^n-1))
<= (vol A)/(2|^m)*(k2-'1) by A30,A3,XREAL_1:64; then
(vol A)/(2|^n)*k1 <= (vol A)/(2|^m)*(k2-'1)
by A38,A59,XXREAL_0:2; then
lower_bound A + (vol A)/(2|^n)*k1
<= lower_bound A + (vol A)/(2|^m)*(k2-'1) by XREAL_1:6;
hence contradiction by A52,A58,XXREAL_0:2;
end;
end; then
A60: lower_bound divset(EqDiv(A,2|^n),k1)
= lower_bound A + (vol A)/(2|^n)*(k1-'1)
& upper_bound divset(EqDiv(A,2|^n),k1)
= lower_bound A + (vol A)/(2|^n)*k1
by A26,A32,A51,A18,A19,A13,INTEGRA1:def 4;
A61: lower_bound divset(EqDiv(A,2|^m),k2)
= lower_bound A + (vol A)/(2|^m)*(k2-'1)
& upper_bound divset(EqDiv(A,2|^m),k2)
= lower_bound A + (vol A)/(2|^m)*k2
by A26,A34,A18,A51,A42,A19,A14,INTEGRA1:def 4;
2|^m - 2|^(m-'n) <= 2|^m - 1 by A36,NAT_1:14,XREAL_1:10; then
(vol A)/(2|^m)*((k1-'1)*2|^(m-'n))
<= (vol A)/(2|^m)*(k2-'1)
by A30,A53,A51,A25,A18,A3,XREAL_1:64; then
A62: lower_bound divset(EqDiv(A,2|^n),k1)
<= lower_bound divset(EqDiv(A,2|^m),k2)
by A38,A60,A61,XREAL_1:6;
(vol A)/(2|^n)*k1 = (vol A) / (2|^n / 2|^n)
& (vol A)/(2|^m)*k2 = (vol A) / (2|^m / 2|^m)
by A53,A51,A25,XCMPLX_1:82; then
A63: (vol A)/(2|^n)*k1 = vol A & (vol A)/(2|^m)*k2 = vol A
by A23,XCMPLX_1:51;
divset(EqDiv(A,2|^n),k1)
= [. lower_bound divset(EqDiv(A,2|^n),k1),
upper_bound divset(EqDiv(A,2|^n),k1) .]
& divset(EqDiv(A,2|^m),k2)
= [. lower_bound divset(EqDiv(A,2|^m),k2),
upper_bound divset(EqDiv(A,2|^m),k2) .] by INTEGRA1:4;
hence divset(EqDiv(A,2|^m),k2) c= divset(EqDiv(A,2|^n),k1)
by A60,A61,A62,A63,XXREAL_1:34;
end;
suppose A64: len EqDiv(A,2|^n) <> 1 & k2 <> 1 & k2 <> len EqDiv(A,2|^m);
then
A65: 1 < k2 < len EqDiv(A,2|^m) by A17,A15,XXREAL_0:1; then
Km.k2 = [. EqDiv(A,2|^m).(k2-'1), EqDiv(A,2|^m).k2 .[
by A14,A19; then
A66: EqDiv(A,2|^m).(k2-'1) <= x < EqDiv(A,2|^m).k2 by A17,XXREAL_1:3;
per cases by A16,A15,XXREAL_0:1;
suppose A67: k1 = 1; then
Kn.k1 = [. inf A, EqDiv(A,2|^n).k1 .[ by A64,A13,A19; then
A68: x < lower_bound A + (vol A)/(2|^n)*k1 by A26,A16,XXREAL_1:3;
now assume k1*(2|^(m-'n)) < k2; then
k1*2|^(m-'n) + 1 <= k2 by NAT_1:13; then
k1*2|^(m-'n) + 1 -'1 <= k2-'1 by NAT_D:42; then
A69: k1*2|^(m-'n) <= k2-'1 by NAT_D:34;
(vol A)/(2|^n)*k1 <= (vol A)/(2|^m)*(k2-'1)
by A39,A69,A3,XREAL_1:64; then
lower_bound A + (vol A)/(2|^n)*k1
<= lower_bound A + (vol A)/(2|^m)*(k2-'1) by XREAL_1:6;
hence contradiction by A66,A68,A34,A64,XXREAL_0:2;
end; then
(vol A)/(2|^m)*k2 <= (vol A)/(2|^n)*k1
by A39,A3,XREAL_1:64; then
A70: EqDiv(A,2|^m).k2 <= EqDiv(A,2|^n).k1 by A26,XREAL_1:6;
A71: inf A + 0 <= lower_bound A + (vol A)/(2|^m)*(k2-'1)
by A3,XREAL_1:6;
A72: lower_bound divset(EqDiv(A,2|^n),k1) = lower_bound A
& upper_bound divset(EqDiv(A,2|^n),k1) = EqDiv(A,2|^n).k1
by A19,A13,A67,INTEGRA1:def 4;
A73: lower_bound divset(EqDiv(A,2|^m),k2) = EqDiv(A,2|^m).(k2-'1)
& upper_bound divset(EqDiv(A,2|^m),k2) = EqDiv(A,2|^m).k2
by A19,A14,A18,A64,INTEGRA1:def 4;
divset(EqDiv(A,2|^n),k1)
= [. lower_bound divset(EqDiv(A,2|^n),k1),
upper_bound divset(EqDiv(A,2|^n),k1) .]
& divset(EqDiv(A,2|^m),k2)
= [. lower_bound divset(EqDiv(A,2|^m),k2),
upper_bound divset(EqDiv(A,2|^m),k2) .]
by INTEGRA1:4;
hence divset(EqDiv(A,2|^m),k2) c= divset(EqDiv(A,2|^n),k1)
by A34,A64,A70,A71,A72,A73,XXREAL_1:34;
end;
suppose A74: 1 < k1 < len EqDiv(A,2|^n); then
Kn.k1 = [. EqDiv(A,2|^n).(k1-'1), EqDiv(A,2|^n).k1 .[
by A13,A19; then
A75: lower_bound A + (vol A)/(2|^n)*(k1-'1) <= x
& x < lower_bound A + (vol A)/(2|^n)*k1
by A74,A26,A32,A16,XXREAL_1:3;
now assume k1*(2|^(m-'n)) < k2; then
k1*2|^(m-'n) + 1 <= k2 by NAT_1:13; then
k1*2|^(m-'n) + 1 -'1 <= k2-'1 by NAT_D:42; then
k1*2|^(m-'n) <= k2-'1 by NAT_D:34; then
(vol A)/(2|^m)*(k1*(2|^(m-'n))) <= (vol A)/(2|^m)*(k2-'1)
by A3,XREAL_1:64; then
lower_bound A + (vol A)/(2|^n)*k1
<= lower_bound A + (vol A)/(2|^m)*(k2-'1) by A38,XREAL_1:6;
hence contradiction by A66,A75,A34,A64,XXREAL_0:2;
end; then
(vol A)/(2|^m)*k2 <= (vol A)/(2|^n)*k1
by A39,A3,XREAL_1:64; then
A76: EqDiv(A,2|^m).k2 <= EqDiv(A,2|^n).k1 by A26,XREAL_1:6;
A77: k2 -' 1 >= 1 by A65,NAT_D:36,NAT_1:14;
now assume k2-'1 < (k1-'1)*(2|^(m-'n)); then
k2-'1+1 <= (k1-'1)*(2|^(m-'n)) by NAT_1:13; then
k2 <= (k1-'1)*(2|^(m-'n)) by A77,NAT_D:43; then
(vol A)/(2|^m)*k2 <= (vol A)/(2|^m)*((k1-'1)*(2|^(m-'n)))
by A3,XREAL_1:64; then
lower_bound A + (vol A)/(2|^m)*k2
<= lower_bound A + (vol A)/(2|^n)*(k1-'1) by A38,XREAL_1:6;
hence contradiction by A75,A66,A26,XXREAL_0:2;
end; then
(vol A)/(2|^n)*(k1-'1) <= (vol A)/(2|^m)*(k2-'1)
by A39,A3,XREAL_1:64; then
A78: EqDiv(A,2|^n).(k1-'1) <= EqDiv(A,2|^m).(k2-'1)
by A32,A34,A74,A64,XREAL_1:6;
A79: lower_bound divset(EqDiv(A,2|^n),k1) = EqDiv(A,2|^n).(k1-'1)
& upper_bound divset(EqDiv(A,2|^n),k1) = EqDiv(A,2|^n).k1
by A19,A13,A18,A74,INTEGRA1:def 4;
A80: lower_bound divset(EqDiv(A,2|^m),k2) = EqDiv(A,2|^m).(k2-'1)
& upper_bound divset(EqDiv(A,2|^m),k2) = EqDiv(A,2|^m).k2
by A19,A14,A18,A64,INTEGRA1:def 4;
divset(EqDiv(A,2|^n),k1)
= [. lower_bound divset(EqDiv(A,2|^n),k1),
upper_bound divset(EqDiv(A,2|^n),k1) .]
& divset(EqDiv(A,2|^m),k2)
= [. lower_bound divset(EqDiv(A,2|^m),k2),
upper_bound divset(EqDiv(A,2|^m),k2) .]
by INTEGRA1:4;
hence divset(EqDiv(A,2|^m),k2) c= divset(EqDiv(A,2|^n),k1)
by A76,A78,A79,A80,XXREAL_1:34;
end;
suppose A81: k1 = len EqDiv(A,2|^n); then
Kn.k1 = [. EqDiv(A,2|^n).(k1-'1), EqDiv(A,2|^n).k1 .]
by A64,A13,A19; then
A82: EqDiv(A,2|^n).(k1-'1) <= x <= EqDiv(A,2|^n).k1 by A16,XXREAL_1:1;
A83: k2 -' 1 >= 1 by A65,NAT_D:36,NAT_1:14;
now assume k2-'1 < (k1-'1)*(2|^(m-'n)); then
k2-'1+1 <= (k1-'1)*(2|^(m-'n)) by NAT_1:13; then
k2 <= (k1-'1)*(2|^(m-'n)) by A83,NAT_D:43; then
(vol A)/(2|^m)*k2 <= (vol A)/(2|^m)*((k1-'1)*(2|^(m-'n)))
by A3,XREAL_1:64; then
lower_bound A + (vol A)/(2|^m)*k2
<= lower_bound A + (vol A)/(2|^n)*(k1-'1) by A38,XREAL_1:6;
hence contradiction by A82,A66,A26,A64,A81,A32,XXREAL_0:2;
end; then
(vol A)/(2|^n)*(k1-'1) <= (vol A)/(2|^m)*(k2-'1)
by A39,A3,XREAL_1:64; then
A84: EqDiv(A,2|^n).(k1-'1) <= EqDiv(A,2|^m).(k2-'1)
by A32,A34,A81,A64,XREAL_1:6;
A85: lower_bound divset(EqDiv(A,2|^n),k1) = EqDiv(A,2|^n).(k1-'1)
& upper_bound divset(EqDiv(A,2|^n),k1) = EqDiv(A,2|^n).k1
by A19,A13,A18,A81,A64,INTEGRA1:def 4;
A86: lower_bound divset(EqDiv(A,2|^m),k2) = EqDiv(A,2|^m).(k2-'1)
& upper_bound divset(EqDiv(A,2|^m),k2) = EqDiv(A,2|^m).k2
by A19,A14,A18,A64,INTEGRA1:def 4;
A87: divset(EqDiv(A,2|^n),k1)
= [. lower_bound divset(EqDiv(A,2|^n),k1),
upper_bound divset(EqDiv(A,2|^n),k1) .]
& divset(EqDiv(A,2|^m),k2)
= [. lower_bound divset(EqDiv(A,2|^m),k2),
upper_bound divset(EqDiv(A,2|^m),k2) .]
by INTEGRA1:4;
A88: EqDiv(A,2|^m).(k2-'1) <= EqDiv(A,2|^m).k2 by A66,XXREAL_0:2;
divset(EqDiv(A,2|^m),k2) c= A by A14,A19,INTEGRA1:8; then
divset(EqDiv(A,2|^m),k2) c= [. lower_bound A, upper_bound A .]
by INTEGRA1:4; then
upper_bound divset(EqDiv(A,2|^m),k2) <= upper_bound A
by A87,A88,A86,XXREAL_1:50; then
EqDiv(A,2|^m).k2 <= EqDiv(A,2|^n).k1 by A86,A81,INTEGRA1:def 2;
hence divset(EqDiv(A,2|^m),k2) c= divset(EqDiv(A,2|^n),k1)
by A84,A85,A86,A87,XXREAL_1:34;
end;
end;
end;
end; then
f|divset(EqDiv(A,2|^m),k2) c= f|divset(EqDiv(A,2|^n),k1)
by RELAT_1:75;
hence (F.n).x <= (F.m).x by A16,A17,A21,A22,SEQ_4:47,RELAT_1:11;
end;
A89:for x be Element of REAL st x in A holds
F#x is convergent & lim(F#x) = sup(F#x) & sup(F#x) <= f.x
proof
let x be Element of REAL;
assume A90: x in A;
for m,n be Nat st n <= m holds (F#x).n <= (F#x).m
proof
let m,n be Nat;
assume n <= m; then
(F.n).x <= (F.m).x by A90,A9; then
(F#x).n <= (F.m).x by MESFUNC5:def 13;
hence (F#x).n <= (F#x).m by MESFUNC5:def 13;
end; then
F#x is non-decreasing by RINFSUP2:7;
hence F#x is convergent & lim(F#x) = sup(F#x) by RINFSUP2:37;
for y be ExtReal holds y in rng(F#x) implies y <= f.x
proof
let y be ExtReal;
assume y in rng(F#x); then
consider n be Element of NAT such that
A91: n in dom(F#x) & y = (F#x).n by PARTFUN1:3;
y = (F.n).x by A91,MESFUNC5:def 13;
hence y <= f.x by A6,A90;
end; then
f.x is UpperBound of rng(F#x) by XXREAL_2:def 1; then
sup rng(F#x) <= f.x by XXREAL_2:def 3;
hence sup(F#x) <= f.x by RINFSUP2:def 1;
end;
consider a,b be Real such that
A92: a <= b and
A93: A = [.a,b.] by MEASURE5:14;
reconsider a1=a, b1=b as R_eal by XXREAL_0:def 1;
A94:diameter A = b1-a1 by A92,A93,MEASURE5:6;
B-Meas.A1 = diameter A by MEASUR12:71; then
A95:B-Meas.A1 < +infty by A94,XXREAL_0:4;
A96:for x be Element of REAL st x in A1 holds F#x is convergent by A89;
A97:for n be Nat holds F.n is A1-measurable by A8,MESFUNC2:34;
reconsider K = max(|.lower_bound rng f.|,|.upper_bound rng f.|) as Real;
A98: -|.lower_bound rng f.| <= lower_bound rng f by ABSVALUE:4;
-K <= - |.lower_bound rng f.| by XXREAL_0:25,XREAL_1:24; then
A99: -K <= lower_bound rng f by A98,XXREAL_0:2;
A100: upper_bound rng f <= |.upper_bound rng f.| by ABSVALUE:4;
|.upper_bound rng f.| <= K by XXREAL_0:25; then
A101: upper_bound rng f <= K by A100,XXREAL_0:2;
for n be Nat, x be set st x in dom(F.0) holds
|. (F.n).x .| <= K
proof
let n be Nat, x be set;
assume A102: x in dom(F.0); then
reconsider x0=x as Real;
n is Element of NAT by ORDINAL1:def 12; then
A103: lower_bound rng f <= (F.n).x0 <= f.x0 by A102,A6,A7;
A104: rng f is bounded_above by A1,SEQ_2:def 8,INTEGRA1:13;
reconsider K1 = K as ExtReal;
f.x0 in rng f by A102,A2,A7,FUNCT_1:3; then
f.x0 <= upper_bound rng f by A104,SEQ_4:def 1; then
(F.n).x0 <= upper_bound rng f by A103,XXREAL_0:2; then
-K <= (F.n).x0 & (F.n).x0 <= K by A99,A101,A103,XXREAL_0:2; then
-K1 <= (F.n).x0 & (F.n).x0 <= K1 by XXREAL_3:def 3;
hence |. (F.n).x .| <= K by EXTREAL1:23;
end; then
A105: F is uniformly_bounded by MESFUN10:def 1; then
ex I be ExtREAL_sequence st
(for n be Nat holds I.n = Integral(B-Meas,F.n))
& I is convergent & lim I = Integral(B-Meas,lim F)
by A96,A97,A95,A7,MESFUN10:19;
hence thesis by A7,A8,A9,A89,A105,A96,A97,A95,MESFUN10:19;
end;
theorem Th22:
for A be non empty closed_interval Subset of REAL, f be PartFunc of A,REAL
st f is bounded & A c= dom f & vol A > 0 holds
ex F be with_the_same_dom Functional_Sequence of REAL,ExtREAL,
I be ExtREAL_sequence st
A = dom(F.0)
& (for n be Nat holds
F.n is_simple_func_in Borel_Sets
& Integral(B-Meas,F.n) = upper_sum(f,EqDiv(A,2|^n))
& (for x be Real st x in A holds upper_bound rng f >= (F.n).x >= f.x) )
& (for n,m be Nat st n <= m holds for x be Element of REAL st x in A holds
(F.n).x >= (F.m).x)
& (for x be Element of REAL st x in A holds
F#x is convergent & lim(F#x) = inf(F#x) & inf(F#x) >= f.x)
& lim F is_integrable_on B-Meas
& (for n be Nat holds I.n = Integral(B-Meas,F.n))
& I is convergent & lim I = Integral(B-Meas,lim F)
proof
let A be non empty closed_interval Subset of REAL, f be PartFunc of A,REAL;
assume that
A1: f is bounded and
A2: A c= dom f and
A3: vol A > 0;
reconsider A1 = A as Element of Borel_Sets by MEASUR12:72;
defpred P[Nat,PartFunc of REAL,ExtREAL] means
A = dom $2
& $2 is_simple_func_in Borel_Sets
& Integral(B-Meas,$2) = upper_sum(f,EqDiv(A,2|^$1))
& (for x be Real st x in A holds upper_bound rng f >= $2.x >= f.x)
& ex K be Finite_Sep_Sequence of Borel_Sets st
dom K = dom EqDiv(A,2|^$1)
& union rng K = A
& (for k be Nat st k in dom K holds
(len EqDiv(A,2|^$1) = 1 implies K.k = [.inf A,sup A.])
& (len EqDiv(A,2|^$1) <> 1 implies
(k = 1 implies K.k = [. inf A,EqDiv(A,2|^$1).k .[)
& (1 < k < len EqDiv(A,2|^$1) implies
K.k = [. EqDiv(A,2|^$1).(k-'1), EqDiv(A,2|^$1).k .[)
& (k = len EqDiv(A,2|^$1) implies
K.k = [. EqDiv(A,2|^$1).(k-'1), EqDiv(A,2|^$1).k.])))
& (for x be Real st x in dom $2 holds
ex k be Nat st 1 <= k <= len K & x in K.k
& $2.x = upper_bound rng(f|divset(EqDiv(A,2|^$1),k)) );
A4: for n be Element of NAT ex g be Element of PFuncs(REAL,ExtREAL) st P[n,g]
proof
let n be Element of NAT;
consider K be Finite_Sep_Sequence of Borel_Sets,
g be PartFunc of REAL,ExtREAL such that
A5: dom K = dom EqDiv(A,2|^n)
& union rng K = A
& (for k be Nat st k in dom K holds
(len EqDiv(A,2|^n) = 1 implies K.k = [.inf A,sup A.])
& (len EqDiv(A,2|^n) <> 1 implies
(k = 1 implies K.k = [. inf A,EqDiv(A,2|^n).k .[)
& (1 < k < len EqDiv(A,2|^n) implies
K.k = [. EqDiv(A,2|^n).(k-'1), EqDiv(A,2|^n).k .[)
& (k = len EqDiv(A,2|^n) implies
K.k = [. EqDiv(A,2|^n).(k-'1), EqDiv(A,2|^n).k.])))
& g is_simple_func_in Borel_Sets
& (for x be Real st x in dom g holds
ex k be Nat st 1 <= k <= len K & x in K.k
& g.x = upper_bound rng(f|divset(EqDiv(A,2|^n),k)) )
& dom g = A
& Integral(B-Meas,g) = upper_sum(f,EqDiv(A,2|^n))
& for x be Real st x in A holds upper_bound rng f >= g.x >= f.x
by A1,A2,Th20;
g is Element of PFuncs(REAL,ExtREAL) by PARTFUN1:45;
hence thesis by A5;
end;
consider F be Function of NAT,PFuncs(REAL,ExtREAL) such that
A6: for n be Element of NAT holds P[n,F.n] from FUNCT_2:sch 3(A4);
reconsider F as Functional_Sequence of REAL,ExtREAL;
for n,m be Nat holds dom(F.n) = dom(F.m)
proof
let n,m be Nat;
n is Element of NAT & m is Element of NAT by ORDINAL1:def 12; then
P[n,F.n] & P[m,F.m] by A6;
hence thesis;
end; then
reconsider F as with_the_same_dom Functional_Sequence of REAL,ExtREAL
by MESFUNC8:def 2;
take F;
A7:A = dom(F.0) by A6;
A8:for n be Nat holds
F.n is_simple_func_in Borel_Sets
& Integral(B-Meas,F.n) = upper_sum(f,EqDiv(A,2|^n))
& (for x be Real st x in A holds upper_bound rng f >= (F.n).x >= f.x)
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 12;
hence thesis by A6;
end;
A9: for n,m be Nat st n <= m holds
for x be Element of REAL st x in A holds (F.n).x >= (F.m).x
proof
let n,m be Nat;
assume A10: n <= m;
A11: n is Element of NAT & m is Element of NAT by ORDINAL1:def 12;
let x be Element of REAL;
assume A12: x in A;
consider Kn be Finite_Sep_Sequence of Borel_Sets such that
A13: dom Kn = dom EqDiv(A,2|^n)
& union rng Kn = A
& (for k be Nat st k in dom Kn holds
(len EqDiv(A,2|^n) = 1 implies Kn.k = [.inf A,sup A.])
& (len EqDiv(A,2|^n) <> 1 implies
(k = 1 implies Kn.k = [. inf A,EqDiv(A,2|^n).k .[)
& (1 < k < len EqDiv(A,2|^n) implies
Kn.k = [. EqDiv(A,2|^n).(k-'1), EqDiv(A,2|^n).k .[)
& (k = len EqDiv(A,2|^n) implies
Kn.k = [. EqDiv(A,2|^n).(k-'1), EqDiv(A,2|^n).k.])))
& (for x be Real st x in dom (F.n) holds
ex k be Nat st 1 <= k <= len Kn & x in Kn.k
& (F.n).x = upper_bound rng(f|divset(EqDiv(A,2|^n),k)) ) by A6,A11;
consider Km be Finite_Sep_Sequence of Borel_Sets such that
A14: dom Km = dom EqDiv(A,2|^m)
& union rng Km = A
& (for k be Nat st k in dom Km holds
(len EqDiv(A,2|^m) = 1 implies Km.k = [.inf A,sup A.])
& (len EqDiv(A,2|^m) <> 1 implies
(k = 1 implies Km.k = [. inf A,EqDiv(A,2|^m).k .[)
& (1 < k < len EqDiv(A,2|^m) implies
Km.k = [. EqDiv(A,2|^m).(k-'1), EqDiv(A,2|^m).k .[)
& (k = len EqDiv(A,2|^m) implies
Km.k = [. EqDiv(A,2|^m).(k-'1), EqDiv(A,2|^m).k.])))
& (for x be Real st x in dom (F.m) holds
ex k be Nat st 1 <= k <= len Km & x in Km.k
& (F.m).x = upper_bound rng(f|divset(EqDiv(A,2|^m),k)) ) by A6,A11;
A15: len EqDiv(A,2|^n) = len Kn & len EqDiv(A,2|^m) = len Km
by A13,A14,FINSEQ_3:29;
x in dom(F.n) by A6,A11,A12; then
consider k1 be Nat such that
A16: 1 <= k1 <= len Kn & x in Kn.k1
& (F.n).x = upper_bound rng(f|divset(EqDiv(A,2|^n),k1)) by A13;
x in dom(F.m) by A6,A11,A12; then
consider k2 be Nat such that
A17: 1 <= k2 <= len Km & x in Km.k2
& (F.m).x = upper_bound rng(f|divset(EqDiv(A,2|^m),k2)) by A14;
A18:k1-1 = k1-'1 & k2-1 = k2-'1 by A16,A17,XREAL_1:48,XREAL_0:def 2;
A19: k1 in dom Kn & k2 in dom Km by A16,A17,FINSEQ_3:25; then
divset(EqDiv(A,2|^n),k1) c= A by A13,INTEGRA1:8; then
A20: divset(EqDiv(A,2|^n),k1) c= dom f by A2; then
A21:dom(f|divset(EqDiv(A,2|^n),k1)) = divset(EqDiv(A,2|^n),k1)
by RELAT_1:62;
f = f|dom f; then
f|divset(EqDiv(A,2|^n),k1) is bounded by A1,A20,RFUNCT_1:74; then
rng(f|divset(EqDiv(A,2|^n),k1)) is real-bounded by INTEGRA1:15; then
A22: rng(f|divset(EqDiv(A,2|^n),k1)) is non empty bounded_above
by A21,RELAT_1:42;
divset(EqDiv(A,2|^m),k2) c= A by A14,A19,INTEGRA1:8; then
divset(EqDiv(A,2|^m),k2) c= dom f by A2; then
dom(f|divset(EqDiv(A,2|^m),k2)) = divset(EqDiv(A,2|^m),k2)
by RELAT_1:62; then
A23: rng(f|divset(EqDiv(A,2|^m),k2)) <> {} by RELAT_1:42;
A24: 2|^n > 0 & 2|^m > 0 by NEWTON:83; then
A25: EqDiv(A,2|^n) divide_into_equal 2|^n
& EqDiv(A,2|^m) divide_into_equal 2|^m by A3,Def1; then
A26: len EqDiv(A,2|^n) = 2|^n & len EqDiv(A,2|^m) = 2|^m
by INTEGRA4:def 1; then
A27: EqDiv(A,2|^n).k1 = lower_bound A + (vol A)/(2|^n)*k1
& EqDiv(A,2|^m).k2 = lower_bound A + (vol A)/(2|^m)*k2
by A25,A13,A14,A16,A17,FINSEQ_3:25,INTEGRA4:def 1;
A28: m-n >= 0 by A10,XREAL_1:48;
A29: m-'n = m-n by A10,XREAL_1:48,XREAL_0:def 2;
2|^n >= 1 & 2|^m >= 1 by A24,NAT_1:14; then
A30: 2|^n-'1 = 2|^n-1 & 2|^m-'1 = 2|^m-1 by XREAL_1:48,XREAL_0:def 2;
A31: 2|^(m-'n)*(2|^n-1) = 2|^(m-'n)*2|^n - 2|^(m-'n)
.= 2|^(m-'n+n) - 2|^(m-'n) by NEWTON:8
.= 2|^m - 2|^(m-'n) by A28,NAT_D:72;
A32: 2|^(m-'n) <= 2|^m by NAT_D:35,PREPOWER:93;
A33: now assume 1 <> k1; then
1 < k1 by A16,XXREAL_0:1; then
A34: k1 -' 1 >= 1 by NAT_1:14,NAT_D:36;
k1 -' 1 <= k1 by NAT_D:35; then
k1 -' 1 <= len Kn by A16,XXREAL_0:2;
hence EqDiv(A,2|^n).(k1-'1) = lower_bound A + (vol A)/(2|^n)*(k1-'1)
by A25,A26,A34,A13,FINSEQ_3:25,INTEGRA4:def 1;
end;
A35: now assume 1 <> k2; then
1 < k2 by A17,XXREAL_0:1; then
A36: k2 -' 1 >= 1 by NAT_1:14,NAT_D:36;
k2 -' 1 <= k2 by NAT_D:35; then
k2 -' 1 <= len Km by A17,XXREAL_0:2;
hence EqDiv(A,2|^m).(k2-'1) = lower_bound A + (vol A)/(2|^m)*(k2-'1)
by A25,A26,A36,A14,FINSEQ_3:25,INTEGRA4:def 1;
end;
A37: 2|^(m-'n) > 0 by NEWTON:83;
2|^n * 2|^(m-'n) = 2|^m & 2|^n * (2|^(m-'n)-'1) < 2|^m
by A10,Lm5; then
A38: 2|^n = 2|^m / 2|^(m-'n) by A37,XCMPLX_1:89; then
A39: (vol A)/2|^n = (vol A)/2|^m * 2|^(m-'n) by XCMPLX_1:81; then
A40: (vol A)/(2|^n)*k1 = (vol A)/(2|^m)*(k1*(2|^(m-'n)))
& (vol A)/(2|^n)*(k1-'1) = (vol A)/(2|^m) * ((k1-'1)*(2|^(m-'n)));
divset(EqDiv(A,2|^m),k2) c= divset(EqDiv(A,2|^n),k1)
proof
per cases;
suppose len EqDiv(A,2|^m) = 1; then
A41: len EqDiv(A,2|^n) = 1 by A26,A10,PREPOWER:93,NAT_1:25; then
len Kn = 1 by A13,FINSEQ_3:29; then
k1 = 1 by A16,XXREAL_0:1; then
divset(EqDiv(A,2|^n),k1) = A by A3,A41,Lm4;
hence divset(EqDiv(A,2|^m),k2) c= divset(EqDiv(A,2|^n),k1)
by A19,A14,INTEGRA1:8;
end;
suppose A42: len EqDiv(A,2|^m) <> 1;
per cases;
suppose A43: len EqDiv(A,2|^n) = 1; then
len Kn = 1 by A13,FINSEQ_3:29; then
k1 = 1 by A16,XXREAL_0:1; then
divset(EqDiv(A,2|^n),k1) = A by A3,A43,Lm4;
hence divset(EqDiv(A,2|^m),k2) c= divset(EqDiv(A,2|^n),k1)
by A19,A14,INTEGRA1:8;
end;
suppose A44: len EqDiv(A,2|^n) <> 1 & k2 = 1; then
Km.k2 = [. inf A,EqDiv(A,2|^m).k2 .[ by A14,A19,A42; then
A45: inf A <= x < EqDiv(A,2|^m).k2 by A17,XXREAL_1:3;
2|^n divides 2|^m by A10,NEWTON:89; then
2|^n <= 2|^m by A24,NAT_D:7; then
A46: (vol A)/(2|^m)*1 <= (vol A)/(2|^n)*1 by A3,A24,XREAL_1:118;
(vol A)/(2|^n)*1 <= (vol A)/(2|^n)*k1 by A16,A3,XREAL_1:64; then
(vol A)/(2|^m)*1 <= (vol A)/(2|^n)*k1 by A46,XXREAL_0:2; then
A47: EqDiv(A,2|^m).k2 <= EqDiv(A,2|^n).k1 by A44,A27,XREAL_1:7;
now assume A48: k1 <> 1; then
1 < k1 by A16,XXREAL_0:1; then
k1 -' 1 >= 1 by NAT_1:14,NAT_D:36; then
(vol A)/(2|^n)*1 <= (vol A)/(2|^n)*(k1-'1) by A3,XREAL_1:64; then
(vol A)/(2|^m)*1 <= (vol A)/(2|^n)*(k1-'1) by A46,XXREAL_0:2; then
A49: EqDiv(A,2|^m).k2 <= EqDiv(A,2|^n).(k1-'1) by A44,A27,A48,A33
,XREAL_1:7;
per cases by A48,A16,A15,XXREAL_0:1;
suppose 1 < k1 < len EqDiv(A,2|^n); then
Kn.k1 = [. EqDiv(A,2|^n).(k1-'1),EqDiv(A,2|^n).k1 .[
by A13,A19; then
EqDiv(A,2|^n).(k1-'1) <= x < EqDiv(A,2|^n).k1 by A16,XXREAL_1:3;
hence contradiction by A45,A49,XXREAL_0:2;
end;
suppose k1 = len EqDiv(A,2|^n); then
Kn.k1 = [. EqDiv(A,2|^n).(k1-'1),EqDiv(A,2|^n).k1 .]
by A13,A19,A44; then
EqDiv(A,2|^n).(k1-'1) <= x <= EqDiv(A,2|^n).k1 by A16,XXREAL_1:1;
hence contradiction by A45,A49,XXREAL_0:2;
end;
end; then
lower_bound divset(EqDiv(A,2|^n),k1) = lower_bound A
& upper_bound divset(EqDiv(A,2|^n),k1) = EqDiv(A,2|^n).k1
by A13,A19,INTEGRA1:def 4; then
A50: divset(EqDiv(A,2|^n),k1)
= [.lower_bound A, EqDiv(A,2|^n).k1 .] by INTEGRA1:4;
lower_bound divset(EqDiv(A,2|^m),k2) = lower_bound A
& upper_bound divset(EqDiv(A,2|^m),k2) = EqDiv(A,2|^m).k2
by A44,A14,A19,INTEGRA1:def 4; then
divset(EqDiv(A,2|^m),k2)
= [.lower_bound A, EqDiv(A,2|^m).k2 .] by INTEGRA1:4;
hence divset(EqDiv(A,2|^m),k2) c= divset(EqDiv(A,2|^n),k1)
by A47,A50,XXREAL_1:34;
end;
suppose A51: len EqDiv(A,2|^n) <> 1 & k2 = len EqDiv(A,2|^m); then
Km.k2 = [. EqDiv(A,2|^m).(k2-'1), EqDiv(A,2|^m).k2 .]
by A14,A19,A42; then
A52: lower_bound A + (vol A)/(2|^m)*(k2-'1) <= x
& x <= lower_bound A + (vol A)/(2|^m)*k2
by A27,A42,A51,A35,A17,XXREAL_1:1;
A53: (vol A)/(2|^n)*(2|^n-1)
= (vol A)/(2|^m)* 2|^(m-'n)*(2|^n-1) by A38,XCMPLX_1:81;
A54: now assume A55: k1 <> len EqDiv(A,2|^n);
per cases by A15,A16,A55,XXREAL_0:1;
suppose A56: k1 = 1; then
Kn.k1 = [. inf A, EqDiv(A,2|^n).1 .[ by A51,A13,A19; then
inf A <= x < EqDiv(A,2|^n).1 by A16,XXREAL_1:3; then
A57: x < lower_bound A + (vol A)/(2|^m)*2|^(m-'n)
by A56,A27,A38,XCMPLX_1:82;
now assume 2|^(m-'n) = 2|^m; then
m-n = m by A29,PEPIN:30; then
2|^n = 1 by NEWTON:4;
hence contradiction by A51,A25,INTEGRA4:def 1;
end; then
2|^(m-'n) < 2|^m by A32,XXREAL_0:1; then
2|^(m-'n)+1 <= 2|^m by NAT_1:13; then
2|^(m-'n) <= k2-'1 by A30,A51,A26,XREAL_1:19; then
(vol A)/(2|^m)*2|^(m-'n) <= (vol A)/(2|^m)*(k2-'1)
by A3,XREAL_1:64; then
lower_bound A + (vol A)/(2|^m)*2|^(m-'n)
<= lower_bound A + (vol A)/(2|^m)*(k2-'1) by XREAL_1:6;
hence contradiction by A52,A57,XXREAL_0:2;
end;
suppose A58: 1 < k1 < len EqDiv(A,2|^n); then
Kn.k1 = [. EqDiv(A,2|^n).(k1-'1), EqDiv(A,2|^n).k1 .[
by A13,A19; then
A59: lower_bound A + (vol A)/(2|^n)*(k1-'1) <= x
& x < lower_bound A + (vol A)/(2|^n)*k1 by A27,A58,A33,A16,XXREAL_1:3;
k1 < len EqDiv(A,2|^n) by A55,A15,A16,XXREAL_0:1; then
k1+1 <= 2|^n by A26,NAT_1:13; then
k1 <= 2|^n-1 by XREAL_1:19; then
A60: (vol A)/(2|^n)*k1 <= (vol A)/(2|^n)*(2|^n-1)
by A3,XREAL_1:64;
2|^m - 2|^(m-'n) <= k2-'1 by A30,A51,A26,A37
,NAT_1:14,XREAL_1:10; then
(vol A)/(2|^m)*(2|^(m-'n)*(2|^n-1))
<= (vol A)/(2|^m)*(k2-'1) by A31,A3,XREAL_1:64; then
(vol A)/(2|^n)*k1 <= (vol A)/(2|^m)*(k2-'1) by A53,A60
,XXREAL_0:2; then
lower_bound A + (vol A)/(2|^n)*k1
<= lower_bound A + (vol A)/(2|^m)*(k2-'1) by XREAL_1:6;
hence contradiction by A52,A59,XXREAL_0:2;
end;
end; then
A61: lower_bound divset(EqDiv(A,2|^n),k1)
= lower_bound A + (vol A)/(2|^n)*(k1-'1)
& upper_bound divset(EqDiv(A,2|^n),k1)
= lower_bound A + (vol A)/(2|^n)*k1
by A27,A33,A51,A18,A19,A13,INTEGRA1:def 4;
A62: lower_bound divset(EqDiv(A,2|^m),k2)
= lower_bound A + (vol A)/(2|^m)*(k2-'1)
& upper_bound divset(EqDiv(A,2|^m),k2)
= lower_bound A + (vol A)/(2|^m)*k2
by A27,A35,A18,A51,A42,A19,A14,INTEGRA1:def 4;
2|^(m-'n)*(2|^n-1) <= 2|^m - 1 by A31,A37,NAT_1:14,XREAL_1:10; then
(vol A)/(2|^m)*((k1-'1)*2|^(m-'n)) <= (vol A)/(2|^m)*(k2-'1)
by A54,A51,A26,A18,A3,XREAL_1:64; then
A63: lower_bound divset(EqDiv(A,2|^n),k1)
<= lower_bound divset(EqDiv(A,2|^m),k2)
by A53,A54,A18,A26,A61,A62,XREAL_1:6;
(vol A)/(2|^n)*k1 = (vol A) / (2|^n / 2|^n)
& (vol A)/(2|^m)*k2 = (vol A) / (2|^m / 2|^m)
by A54,A51,A26,XCMPLX_1:82; then
A64: (vol A)/(2|^n)*k1 = vol A & (vol A)/(2|^m)*k2 = vol A
by A24,XCMPLX_1:51;
divset(EqDiv(A,2|^n),k1)
= [. lower_bound divset(EqDiv(A,2|^n),k1),
upper_bound divset(EqDiv(A,2|^n),k1) .]
& divset(EqDiv(A,2|^m),k2)
= [. lower_bound divset(EqDiv(A,2|^m),k2),
upper_bound divset(EqDiv(A,2|^m),k2) .]
by INTEGRA1:4;
hence divset(EqDiv(A,2|^m),k2) c= divset(EqDiv(A,2|^n),k1)
by A61,A62,A63,A64,XXREAL_1:34;
end;
suppose A65: len EqDiv(A,2|^n) <> 1 & k2 <> 1 & k2 <> len EqDiv(A,2|^m);
then
A66: 1 < k2 < len EqDiv(A,2|^m) by A17,A15,XXREAL_0:1; then
Km.k2 = [. EqDiv(A,2|^m).(k2-'1), EqDiv(A,2|^m).k2 .[
by A14,A19; then
A67: EqDiv(A,2|^m).(k2-'1) <= x < EqDiv(A,2|^m).k2 by A17,XXREAL_1:3;
per cases by A16,A15,XXREAL_0:1;
suppose A68: k1 = 1; then
Kn.k1 = [. inf A, EqDiv(A,2|^n).k1 .[ by A65,A13,A19; then
A69: x < lower_bound A + (vol A)/(2|^n)*k1 by A27,A16,XXREAL_1:3;
now assume k1*(2|^(m-'n)) < k2; then
k1*2|^(m-'n) + 1 <= k2 by NAT_1:13; then
k1*2|^(m-'n) + 1 -'1 <= k2-'1 by NAT_D:42; then
A70: k1*2|^(m-'n) <= k2-'1 by NAT_D:34;
(vol A)/(2|^m)*(k1*(2|^(m-'n))) <= (vol A)/(2|^m)*(k2-'1)
by A70,A3,XREAL_1:64; then
lower_bound A + (vol A)/(2|^n)*k1
<= lower_bound A + (vol A)/(2|^m)*(k2-'1) by A39,XREAL_1:6;
hence contradiction by A67,A35,A65,A69,XXREAL_0:2;
end; then
(vol A)/(2|^m)*k2 <= (vol A)/(2|^n)*k1 by A40,A3,XREAL_1:64; then
A71: EqDiv(A,2|^m).k2 <= EqDiv(A,2|^n).k1 by A27,XREAL_1:6;
A72: inf A + 0 <= lower_bound A + (vol A)/(2|^m)*(k2-'1)
by A3,XREAL_1:6;
A73: lower_bound divset(EqDiv(A,2|^n),k1) = lower_bound A
& upper_bound divset(EqDiv(A,2|^n),k1) = EqDiv(A,2|^n).k1
by A19,A13,A68,INTEGRA1:def 4;
A74: lower_bound divset(EqDiv(A,2|^m),k2) = EqDiv(A,2|^m).(k2-'1)
& upper_bound divset(EqDiv(A,2|^m),k2) = EqDiv(A,2|^m).k2
by A19,A14,A18,A65,INTEGRA1:def 4;
divset(EqDiv(A,2|^n),k1)
= [. lower_bound divset(EqDiv(A,2|^n),k1),
upper_bound divset(EqDiv(A,2|^n),k1) .]
& divset(EqDiv(A,2|^m),k2)
= [. lower_bound divset(EqDiv(A,2|^m),k2),
upper_bound divset(EqDiv(A,2|^m),k2) .]
by INTEGRA1:4;
hence divset(EqDiv(A,2|^m),k2) c= divset(EqDiv(A,2|^n),k1)
by A71,A72,A35,A65,A73,A74,XXREAL_1:34;
end;
suppose A75: 1 < k1 < len EqDiv(A,2|^n); then
Kn.k1 = [. EqDiv(A,2|^n).(k1-'1), EqDiv(A,2|^n).k1 .[
by A13,A19; then
A76: lower_bound A + (vol A)/(2|^n)*(k1-'1) <= x
& x < lower_bound A + (vol A)/(2|^n)*k1
by A75,A27,A33,A16,XXREAL_1:3;
now assume k1*(2|^(m-'n)) < k2; then
k1*2|^(m-'n) + 1 <= k2 by NAT_1:13; then
k1*2|^(m-'n) + 1 -'1 <= k2-'1 by NAT_D:42; then
k1*2|^(m-'n) <= k2-'1 by NAT_D:34; then
(vol A)/(2|^m)*(k1*(2|^(m-'n))) <= (vol A)/(2|^m)*(k2-'1)
by A3,XREAL_1:64; then
lower_bound A + (vol A)/(2|^n)*k1
<= lower_bound A + (vol A)/(2|^m)*(k2-'1) by A39,XREAL_1:6;
hence contradiction by A67,A35,A65,A76,XXREAL_0:2;
end; then
(vol A)/(2|^m)*k2 <= (vol A)/(2|^n)*k1 by A40,A3,XREAL_1:64; then
A77: EqDiv(A,2|^m).k2 <= EqDiv(A,2|^n).k1 by A27,XREAL_1:6;
A78: k2 -' 1 >= 1 by A66,NAT_D:36,NAT_1:14;
now assume k2-'1 < (k1-'1)*(2|^(m-'n)); then
k2-'1+1 <= (k1-'1)*(2|^(m-'n)) by NAT_1:13; then
k2 <= (k1-'1)*(2|^(m-'n)) by A78,NAT_D:43; then
(vol A)/(2|^m)*k2 <= (vol A)/(2|^m)*((k1-'1)*(2|^(m-'n)))
by A3,XREAL_1:64; then
lower_bound A + (vol A)/(2|^m)*k2
<= lower_bound A + (vol A)/(2|^n)*(k1-'1) by A39,XREAL_1:6;
hence contradiction by A76,A67,A27,XXREAL_0:2;
end; then
(vol A)/(2|^n)*(k1-'1) <= (vol A)/(2|^m)*(k2-'1)
by A40,A3,XREAL_1:64; then
A79: EqDiv(A,2|^n).(k1-'1) <= EqDiv(A,2|^m).(k2-'1)
by A33,A35,A75,A65,XREAL_1:6;
A80: lower_bound divset(EqDiv(A,2|^n),k1) = EqDiv(A,2|^n).(k1-'1)
& upper_bound divset(EqDiv(A,2|^n),k1) = EqDiv(A,2|^n).k1
by A19,A13,A18,A75,INTEGRA1:def 4;
A81: lower_bound divset(EqDiv(A,2|^m),k2) = EqDiv(A,2|^m).(k2-'1)
& upper_bound divset(EqDiv(A,2|^m),k2) = EqDiv(A,2|^m).k2
by A19,A14,A18,A65,INTEGRA1:def 4;
divset(EqDiv(A,2|^n),k1)
= [. lower_bound divset(EqDiv(A,2|^n),k1),
upper_bound divset(EqDiv(A,2|^n),k1) .]
& divset(EqDiv(A,2|^m),k2)
= [. lower_bound divset(EqDiv(A,2|^m),k2),
upper_bound divset(EqDiv(A,2|^m),k2) .]
by INTEGRA1:4;
hence divset(EqDiv(A,2|^m),k2) c= divset(EqDiv(A,2|^n),k1)
by A77,A79,A80,A81,XXREAL_1:34;
end;
suppose A82: k1 = len EqDiv(A,2|^n); then
Kn.k1 = [. EqDiv(A,2|^n).(k1-'1), EqDiv(A,2|^n).k1 .]
by A65,A13,A19; then
A83: EqDiv(A,2|^n).(k1-'1) <= x <= EqDiv(A,2|^n).k1
by A16,XXREAL_1:1;
A84: k2 -' 1 >= 1 by A66,NAT_D:36,NAT_1:14;
now assume k2-'1 < (k1-'1)*(2|^(m-'n)); then
k2-'1+1 <= (k1-'1)*(2|^(m-'n)) by NAT_1:13; then
k2 <= (k1-'1)*(2|^(m-'n)) by A84,NAT_D:43; then
(vol A)/(2|^m)*k2 <= (vol A)/(2|^m)*((k1-'1)*(2|^(m-'n)))
by A3,XREAL_1:64; then
lower_bound A + (vol A)/(2|^m)*k2
<= lower_bound A + (vol A)/(2|^n)*(k1-'1) by A39,XREAL_1:6;
hence contradiction by A83,A67,A27,A65,A82,A33,XXREAL_0:2;
end; then
(vol A)/(2|^n)*(k1-'1) <= (vol A)/(2|^m)*(k2-'1)
by A40,A3,XREAL_1:64; then
A85: EqDiv(A,2|^n).(k1-'1) <= EqDiv(A,2|^m).(k2-'1)
by A33,A35,A82,A65,XREAL_1:6;
A86: lower_bound divset(EqDiv(A,2|^n),k1) = EqDiv(A,2|^n).(k1-'1)
& upper_bound divset(EqDiv(A,2|^n),k1) = EqDiv(A,2|^n).k1
by A19,A13,A18,A82,A65,INTEGRA1:def 4;
A87: lower_bound divset(EqDiv(A,2|^m),k2) = EqDiv(A,2|^m).(k2-'1)
& upper_bound divset(EqDiv(A,2|^m),k2) = EqDiv(A,2|^m).k2
by A19,A14,A18,A65,INTEGRA1:def 4;
A88: divset(EqDiv(A,2|^n),k1)
= [. lower_bound divset(EqDiv(A,2|^n),k1),
upper_bound divset(EqDiv(A,2|^n),k1) .]
& divset(EqDiv(A,2|^m),k2)
= [. lower_bound divset(EqDiv(A,2|^m),k2),
upper_bound divset(EqDiv(A,2|^m),k2) .]
by INTEGRA1:4;
A89: EqDiv(A,2|^m).(k2-'1) <= EqDiv(A,2|^m).k2 by A67,XXREAL_0:2;
divset(EqDiv(A,2|^m),k2) c= A by A14,A19,INTEGRA1:8; then
divset(EqDiv(A,2|^m),k2) c= [. lower_bound A, upper_bound A .]
by INTEGRA1:4; then
upper_bound divset(EqDiv(A,2|^m),k2) <= upper_bound A
by A88,A89,A87,XXREAL_1:50; then
EqDiv(A,2|^m).k2 <= EqDiv(A,2|^n).k1 by A87,A82,INTEGRA1:def 2;
hence divset(EqDiv(A,2|^m),k2) c= divset(EqDiv(A,2|^n),k1)
by A85,A86,A87,A88,XXREAL_1:34;
end;
end;
end;
end; then
f|divset(EqDiv(A,2|^m),k2) c= f|divset(EqDiv(A,2|^n),k1)
by RELAT_1:75;
hence (F.n).x >= (F.m).x by A16,A17,A22,A23,SEQ_4:48,RELAT_1:11;
end;
A90:for x be Element of REAL st x in A holds
F#x is convergent & lim(F#x) = inf(F#x) & inf(F#x) >= f.x
proof
let x be Element of REAL;
assume A91: x in A;
for m,n be Nat st n <= m holds (F#x).n >= (F#x).m
proof
let m,n be Nat;
assume n <= m; then
(F.n).x >= (F.m).x by A91,A9; then
(F#x).n >= (F.m).x by MESFUNC5:def 13;
hence (F#x).n >= (F#x).m by MESFUNC5:def 13;
end; then
F#x is non-increasing by RINFSUP2:7;
hence F#x is convergent & lim(F#x) = inf(F#x) by RINFSUP2:36;
for y be ExtReal holds y in rng(F#x) implies y >= f.x
proof
let y be ExtReal;
assume y in rng(F#x); then
consider n be Element of NAT such that
A92: n in dom(F#x) & y = (F#x).n by PARTFUN1:3;
y = (F.n).x by A92,MESFUNC5:def 13;
hence y >= f.x by A6,A91;
end; then
f.x is LowerBound of rng(F#x) by XXREAL_2:def 2; then
inf rng(F#x) >= f.x by XXREAL_2:def 4;
hence inf(F#x) >= f.x by RINFSUP2:def 2;
end;
consider a,b be Real such that
A93: a <= b and
A94: A = [.a,b.] by MEASURE5:14;
reconsider a1=a, b1=b as R_eal by XXREAL_0:def 1;
A95:diameter A = b1-a1 by A93,A94,MEASURE5:6;
B-Meas.A1 = diameter A by MEASUR12:71; then
A96:B-Meas.A1 < +infty by A95,XXREAL_0:4;
A97:for x be Element of REAL st x in A1 holds F#x is convergent by A90;
A98:for n be Nat holds F.n is A1-measurable by A8,MESFUNC2:34;
set K = max(|.lower_bound rng f.|,|.upper_bound rng f.|);
A99: -|.lower_bound rng f.| <= lower_bound rng f by ABSVALUE:4;
-K <= - |.lower_bound rng f.| by XXREAL_0:25,XREAL_1:24; then
A100: -K <= lower_bound rng f by A99,XXREAL_0:2;
A101: upper_bound rng f <= |.upper_bound rng f.| by ABSVALUE:4;
|.upper_bound rng f.| <= K by XXREAL_0:25; then
A102: upper_bound rng f <= K by A101,XXREAL_0:2;
for n be Nat, x be set st x in dom(F.0) holds
|. (F.n).x .| <= K
proof
let n be Nat, x be set;
assume A103: x in dom(F.0); then
reconsider x0=x as Real;
n is Element of NAT by ORDINAL1:def 12; then
A104: upper_bound rng f >= (F.n).x0 >= f.x0 by A103,A7,A6;
A105: rng f is bounded_below by A1,SEQ_2:def 8,INTEGRA1:11;
reconsider K1 = K as ExtReal;
f.x0 in rng f by A103,A7,A2,FUNCT_1:3; then
f.x0 >= lower_bound rng f by A105,SEQ_4:def 2; then
(F.n).x0 >= lower_bound rng f by A104,XXREAL_0:2; then
-K <= (F.n).x0 & (F.n).x0 <= K by A100,A102,A104,XXREAL_0:2; then
-K1 <= (F.n).x0 & (F.n).x0 <= K1 by XXREAL_3:def 3;
hence |. (F.n).x .| <= K by EXTREAL1:23;
end; then
A106:F is uniformly_bounded by MESFUN10:def 1;
ex I be ExtREAL_sequence st
(for n be Nat holds I.n = Integral(B-Meas,F.n))
& I is convergent & lim I = Integral(B-Meas,lim F)
by A97,A98,A96,A7,A106,MESFUN10:19;
hence thesis by A7,A8,A9,A90,A106,A97,A98,A96,MESFUN10:19;
end;
begin :: Properties of Complete Measure Space
theorem Th23:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, E be Element of S, n be Nat
st E = dom f & f is nonnegative & f is E-measurable & Integral(M,f) = 0
holds M.(E /\ great_eq_dom(f,1/(n+1))) = 0
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, E be Element of S, n be Nat;
assume that
A1: E = dom f and
A2: f is nonnegative and
A3: f is E-measurable and
A4: Integral(M,f) = 0;
assume A5: M.(E /\ great_eq_dom(f,1/(n+1))) <> 0;
E /\ great_eq_dom(f,1/(n+1)) in S by A1,A3,MESFUNC1:27; then
A6: M.(E /\ great_eq_dom(f,1/(n+1))) > 0 by A5,MEASURE1:def 2;
great_eq_dom(f,1/(n+1)) c= E by A1,MESFUNC1:def 14; then
A7: M.(great_eq_dom(f,1/(n+1))) > 0 by A6,XBOOLE_1:28;
1/(n+1) > 0 by XREAL_1:139; then
1/(n+1)*M.(great_eq_dom(f,1/(n+1))) > 0 by A7;
hence contradiction by A3,A1,A2,A4,MESFUN13:16;
end;
theorem Th24:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, E be Element of S
st E = dom f & f is nonnegative & f is E-measurable & Integral(M,f) = 0
holds M.(E /\ great_dom(f,0)) = 0
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, E be Element of S;
assume that
A1: E = dom f and
A2: f is nonnegative and
A3: f is E-measurable and
A4: Integral(M,f) = 0;
defpred P[Nat,object] means
$2 = E /\ great_eq_dom(f,1/($1+1));
A5: for n be Element of NAT ex y be Element of S st P[n,y]
proof
let n be Element of NAT;
E /\ great_eq_dom(f,1/(n+1)) is Element of S by A1,A3,MESFUNC1:27;
hence thesis;
end;
consider F be Function of NAT,S such that
A6: for n be Element of NAT holds P[n,F.n] from FUNCT_2:sch 3(A5);
A7: for n be Element of NAT holds (M*F).n = 0
proof
let n be Element of NAT;
dom F = NAT by FUNCT_2:def 1; then
(M*F).n = M.(F.n) by FUNCT_1:13
.= M.(E /\ great_eq_dom(f,1/(n+1))) by A6;
hence (M*F).n = 0 by A1,A2,A3,A4,Th23;
end;
rng F is N_Sub_set_fam of X & rng F c= S
by MEASURE1:23,RELAT_1:def 19; then
reconsider T = rng F as N_Measure_fam of S by MEASURE2:def 1;
for n be Element of NAT holds F.n = E /\ great_eq_dom(f,(0+1/(n+1)))
by A6; then
E /\ great_dom(f,0) = union T by MESFUNC1:22; then
M.(E /\ great_dom(f,0)) <= SUM(M*F) by MEASURE2:11; then
M.(E /\ great_dom(f,0)) <= 0 by A7,MEASURE7:1;
hence thesis by SUPINF_2:51;
end;
theorem Th25:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,REAL, E be Element of S
st E = dom f & f is nonnegative & f is E-measurable & Integral(M,f) = 0
holds f a.e.= (X-->0)|E,M
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,REAL, E be Element of S;
assume that
A1: E = dom f and
A2: f is nonnegative and
A3: f is E-measurable and
A4: Integral(M,f) = 0;
A5: E = dom (R_EAL f) & R_EAL f is nonnegative & R_EAL f is E-measurable
& Integral(M,R_EAL f) = 0
by A1,A2,A3,A4,MESFUNC5:def 7,MESFUNC6:def 1,def 3; then
A6: M.(E /\ great_dom(R_EAL f,0)) = 0 by Th24;
reconsider A = E /\ great_dom(R_EAL f,0) as Element of S
by A5,MESFUNC1:29;
A7: (X --> 0)|E = X /\ E --> 0 by FUNCOP_1:12 .= E --> 0 by XBOOLE_1:28; then
A8: dom(f|A`) = dom f /\ A`
& dom(((X-->0)|E)|A`) = dom(E-->0) /\ A` by RELAT_1:61;
now let x be Element of X;
assume A9: x in dom(f|A`); then
A10: x in dom f & x in A` by RELAT_1:57; then
x in X \ A by SUBSET_1:def 4; then
not x in A by XBOOLE_0:def 5; then
not x in E or not x in great_dom(R_EAL f,0) by XBOOLE_0:def 4; then
A11: not x in dom(R_EAL f) or (R_EAL f).x <= 0
by A9,A1,RELAT_1:57,MESFUNC1:def 13;
(R_EAL f).x >= 0 by A5,SUPINF_2:51; then
f.x = 0 by A10,A11,MESFUNC5:def 7; then
A12: (f|A`).x = 0 by A9,FUNCT_1:47;
A13: x in E /\ A` by A10,A1,XBOOLE_0:def 4;
(((X-->0)|E)|A`).x
= (E /\ A` --> 0).x by A7,FUNCOP_1:12;
hence (f|A`).x = (((X-->0)|E)|A`).x by A12,A13,FUNCOP_1:7;
end;
hence f a.e.= (X-->0)|E,M by A1,A6,A8,PARTFUN1:5,LPSPACE1:def 10;
end;
theorem Th26:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f,g be PartFunc of X,REAL, E1 be Element of S
st M is complete & f is E1-measurable & f a.e.= g,M & E1 = dom f
holds g is E1-measurable
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f,g be PartFunc of X,REAL, E1 be Element of S;
assume that
A1: M is complete and
A2: f is E1-measurable and
A3: f a.e.= g,M and
A4: E1 = dom f;
consider E be Element of S such that
A5: M.E = 0 & f|E` = g|E` by A3,LPSPACE1:def 10;
set E2 = dom g;
E` = X \ E & X in S by SUBSET_1:def 4,MEASURE1:7; then
A6: E` in S by MEASURE1:6; then
reconsider A = E1 /\ E` as Element of S by FINSUB_1:def 2;
A c= dom f by A4,XBOOLE_1:17; then
A7: A c= dom (R_EAL f) by MESFUNC5:def 7;
dom(f|E`) = A by A4,RELAT_1:61; then
A8: A c= dom(R_EAL(g|E`)) by A5,MESFUNC5:def 7;
A9: (R_EAL f)|A = f|A by MESFUNC5:def 7
.= (f|E`)|A by XBOOLE_1:17,RELAT_1:74
.= g|A by A5,XBOOLE_1:17,RELAT_1:74
.= R_EAL(g|A) by MESFUNC5:def 7;
(g|A) = (g|E`)|A by XBOOLE_1:17,RELAT_1:74; then
R_EAL(g|A) = (g|E`)|A by MESFUNC5:def 7; then
A10: R_EAL(g|A) = (R_EAL(g|E`))|A by MESFUNC5:def 7;
A11: R_EAL(g|E`) = g|E` by MESFUNC5:def 7
.= (R_EAL g)|E` by MESFUNC5:def 7;
A c= E1 by XBOOLE_1:17; then
R_EAL f is A-measurable by A2,MESFUNC6:def 1,MESFUNC1:30; then
R_EAL(g|E`) is A-measurable by A7,A8,A9,A10,MESFUN12:36; then
A12: R_EAL g is A-measurable by A11,A6,XBOOLE_1:17,MESFUN13:19;
for r be Real holds E1 /\ less_dom(R_EAL g,r) in S
proof
let r be Real;
A13: E1 \ A = E1 \ E` by XBOOLE_1:47 .= E1 \ (X \ E) by SUBSET_1:def 4
.= (E1 \ X) \/ E1 /\ E by XBOOLE_1:52
.= {} \/ E1 /\ E by XBOOLE_1:37
.= E1 /\ E;
M.(E1 /\ E) <= 0 by A5,MEASURE1:8,XBOOLE_1:17; then
M.(E1 /\ E) = 0 by SUPINF_2:51; then
A14: (E1 \ A) /\ less_dom(R_EAL g,r) in S by A13,A1,XBOOLE_1:17,
MEASURE3:def 1;
A15: A /\ less_dom(R_EAL g,r) in S by A12,MESFUNC1:def 16;
((E1 \ A) /\ less_dom(R_EAL g,r)) \/ (A /\ less_dom(R_EAL g,r))
= ((E1 \ A) \/ A) /\ less_dom(R_EAL g,r) by XBOOLE_1:23
.= (E1 \/ A) /\ less_dom(R_EAL g,r) by XBOOLE_1:39
.= E1 /\ less_dom(R_EAL g,r) by XBOOLE_1:12,17;
hence E1 /\ less_dom(R_EAL g,r) in S by A14,A15,FINSUB_1:def 1;
end;
hence g is E1-measurable by MESFUNC1:def 16,MESFUNC6:def 1;
end;
theorem Th27:
for X be set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S holds E is Element of COM(S,M)
proof
let X be set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S;
reconsider E0 = {} as Element of S by MEASURE1:7;
M.E0 = 0 by VALUED_0:def 19; then
A1: E0 is thin of M by MEASURE3:def 2;
E = E \/ E0;
hence E is Element of COM(S,M) by A1,MEASURE3:def 3;
end;
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f,g be PartFunc of X,REAL st f a.e.= g,M holds f a.e.= g,COM M
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f,g be PartFunc of X,REAL;
assume f a.e.= g,M; then
consider E be Element of S such that
A1: M.E = 0 & f|E` = g|E` by LPSPACE1:def 10;
reconsider E0 = {} as Element of S by MEASURE1:7;
M.E0 = 0 by VALUED_0:def 19; then
A2: E0 is thin of M by MEASURE3:def 2;
A3: E = E \/ E0;
reconsider E1 = E as Element of COM(S,M) by Th27;
(COM M).E1 = 0 by A1,A2,A3,MEASURE3:def 5;
hence f a.e.= g,COM M by A1,LPSPACE1:def 10;
end;
theorem Th29:
for f,g be PartFunc of REAL,REAL st f a.e.= g,B-Meas holds f a.e.= g,L-Meas
proof
let f,g be PartFunc of REAL,REAL;
assume f a.e.= g,B-Meas; then
consider E be Element of Borel_Sets such that
A1: B-Meas.E = 0 & f|E` = g|E` by LPSPACE1:def 10;
{} is empty & {} c= REAL; then
reconsider E0 = {} as Element of Borel_Sets by MEASUR12:72;
A2: E = E \/ E0; then
reconsider E1 = E as Element of L-Field
by MEASURE3:def 3,MEASUR12:73,def 11;
(COM B-Meas).E1 = 0 by A1,A2,MEASURE3:def 5,MEASUR12:73;
hence f a.e.= g,L-Meas by A1,LPSPACE1:def 10,MEASUR12:def 12;
end;
theorem Th30:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E1 be Element of S, E2 be Element of COM(S,M), f be PartFunc of X,ExtREAL
st E1 = E2 & f is E1-measurable holds f is E2-measurable
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E1 be Element of S, E2 be Element of COM(S,M), f be PartFunc of X,ExtREAL;
assume that
A1: E1 = E2 and
A2: f is E1-measurable;
for r be Real holds E2 /\ less_dom(f,r) in COM(S,M)
proof
let r be Real;
E1 /\ less_dom(f,r) in S by A2,MESFUNC1:def 16; then
E2 /\ less_dom(f,r) is Element of COM(S,M) by A1,Th27;
hence E2 /\ less_dom(f,r) in COM(S,M);
end;
hence f is E2-measurable by MESFUNC1:def 16;
end;
theorem
for E1 be Element of Borel_Sets,
E2 be Element of L-Field, f be PartFunc of REAL,ExtREAL
st E1 = E2 & f is E1-measurable holds f is E2-measurable
by Th30,MEASUR12:def 11;
theorem Th32:
for X be set, S be SigmaField of X, M be sigma_Measure of S,
F be Finite_Sep_Sequence of S
holds F is Finite_Sep_Sequence of COM(S,M)
proof
let X be set, S be SigmaField of X, M be sigma_Measure of S,
F be Finite_Sep_Sequence of S;
now let y be object;
assume y in rng F; then
y is Element of COM(S,M) by Th27;
hence y in COM(S,M);
end; then
rng F c= COM(S,M);
hence F is Finite_Sep_Sequence of COM(S,M) by FINSEQ_1:def 4;
end;
theorem Th33:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL st f is_simple_func_in S holds
f is_simple_func_in COM(S,M)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL;
assume A1: f is_simple_func_in S; then
A2: f is real-valued by MESFUNC2:def 4;
consider F be Finite_Sep_Sequence of S such that
A3: dom f = union rng F and
A4: for n be Nat, x,y be Element of X st
n in dom F & x in F.n & y in F.n holds f.x = f.y by A1,MESFUNC2:def 4;
reconsider F1=F as Finite_Sep_Sequence of COM(S,M) by Th32;
dom f = union rng F1 by A3;
hence f is_simple_func_in COM(S,M) by A2,A4,MESFUNC2:def 4;
end;
theorem Th34:
for X be set, S be SigmaField of X, M be sigma_Measure of S
holds {} is thin of M
proof
let X be set, S be SigmaField of X, M be sigma_Measure of S;
set E0 = {};
A1: E0 in S by MEASURE1:7;
M.E0 = 0 by VALUED_0:def 19;
hence {} is thin of M by A1,MEASURE3:def 2;
end;
theorem Th35:
for X be set, S be SigmaField of X, M be sigma_Measure of S, E be Element of S
holds M.E = (COM M).E
proof
let X be set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S;
reconsider E0 = {} as thin of M by Th34;
(COM M).(E \/ E0) = M.E by MEASURE3:def 5;
hence thesis;
end;
theorem Th36:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative
holds integral(M,f) = integral(COM M,f)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL;
assume that
A1: f is_simple_func_in S and
A2: f is nonnegative;
consider F be Finite_Sep_Sequence of S, a,x be FinSequence of ExtREAL
such that
A3: F,a are_Re-presentation_of f and
A4: a.1 = 0. and
A5: for n be Nat st 2 <= n & n in dom a holds
0. < a.n & a.n < +infty and
A6: dom x = dom F and
A7: for n be Nat st n in dom x holds x.n = a.n*(M*F).n and
A8: integral(M,f) = Sum x by A1,A2,MESFUNC3:def 2;
A9:f is_simple_func_in COM(S,M) by A1,Th33;
reconsider F1=F as Finite_Sep_Sequence of COM(S,M) by Th32;
A10: dom f = union rng F1 by A3,MESFUNC3:def 1;
A11: dom F1 = dom a by A3,MESFUNC3:def 1;
for n be Nat st n in dom F1
for x be object st x in F1.n holds f.x=a.n by A3,MESFUNC3:def 1; then
A12: F1,a are_Re-presentation_of f by A10,A11,MESFUNC3:def 1;
for n be Nat st n in dom x holds x.n = a.n*((COM M)*F1).n
proof
let n be Nat;
assume A13: n in dom x; then
(M*F).n = M.(F.n) by A6,FUNCT_1:13; then
(M*F).n = (COM M).(F1.n) by Th35; then
(M*F).n = ((COM M)*F1).n by A13,A6,FUNCT_1:13;
hence x.n = a.n*((COM M)*F1).n by A7,A13;
end;
hence integral(M,f) = integral(COM M,f)
by A8,A9,A2,A12,A4,A5,A6,MESFUNC3:def 2;
end;
theorem Th37:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, E be Element of S
st E = dom f & f is E-measurable & f is nonnegative
holds integral+(M,f) = integral+(COM M,f)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, E be Element of S;
assume that
A1: E = dom f and
A2: f is E-measurable and
A3: f is nonnegative;
consider F be Functional_Sequence of X,ExtREAL such that
A4: for n be Nat holds F.n is_simple_func_in S & dom(F.n) = dom f and
A5: for n be Nat holds F.n is nonnegative and
A6: for n,m be Nat st n<=m holds for x be Element of X st x in dom f holds
(F.n).x <= (F.m).x and
A7: for x be Element of X st x in dom f
holds (F#x) is convergent & lim(F#x)=f.x by A1,A2,A3,MESFUNC5:64;
reconsider g = F.0 as PartFunc of X,ExtREAL;
A8: g is nonnegative by A5;
A9:dom f = dom g by A4;
A10:for x be Element of X st x in dom g
holds (F#x) is convergent & g.x <= lim(F#x)
proof
let x be Element of X;
assume
A11: x in dom g;
hence (F#x) is convergent by A7,A9;
A12: now let n,m be Nat;
assume A13: n <= m;
A14: (F#x).m = (F.m).x by MESFUNC5:def 13;
(F#x).n = (F.n).x by MESFUNC5:def 13;
hence (F#x).n <= (F#x).m by A6,A13,A11,A9,A14;
end;
A15: g.x = (F#x).0 by MESFUNC5:def 13;
lim(F#x) = sup rng(F#x) by A12,MESFUNC5:54;
hence g.x <= lim(F#x) by A15,MESFUNC5:56;
end;
consider K be ExtREAL_sequence such that
A16: for n be Nat holds K.n = integral'(M,F.n) and
A17: K is convergent and
sup rng K = lim K and
integral'(M,g) <= lim K by A8,A4,A9,A5,A6,A10,MESFUNC5:75;
A18:integral+(M,f) = lim K by A1,A2,A3,A4,A5,A6,A7,A16,A17,MESFUNC5:def 15;
reconsider E1=E as Element of COM(S,M) by Th27;
A19: f is E1-measurable by A2,Th30;
A20:for n be Nat holds F.n is_simple_func_in COM(S,M) & dom(F.n) = dom f
by A4,Th33;
for n be Nat holds K.n = integral'(COM M,F.n)
proof
let n be Nat;
A21: K.n = integral'(M,F.n) by A16;
per cases;
suppose A22: dom(F.n) <> {};
F.n is_simple_func_in S & F.n is nonnegative by A4,A5; then
integral(M,F.n) = integral(COM M,F.n) by Th36; then
K.n = integral(COM M,F.n) by A22,A21,MESFUNC5:def 14;
hence K.n = integral'(COM M,F.n) by A22,MESFUNC5:def 14;
end;
suppose A23: dom(F.n) = {}; then
K.n = 0 by A21,MESFUNC5:def 14;
hence K.n = integral'(COM M,F.n) by A23,MESFUNC5:def 14;
end;
end;
hence integral+(M,f) = integral+(COM M,f)
by A18,A1,A19,A3,A20,A5,A6,A7,A17,MESFUNC5:def 15;
end;
theorem Th38:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL st f is_integrable_on M
holds f is_integrable_on (COM M) & Integral(M,f) = Integral(COM M,f)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL;
assume A1: f is_integrable_on M; then
consider E be Element of S such that
A2: E = dom f & f is E-measurable by MESFUNC5:def 17;
A3:integral+(M,max+f) < +infty & integral+(M,max-f) < +infty
by A1,MESFUNC5:def 17;
A4:E = dom(max+f) & E = dom(max-f) by A2,MESFUNC2:def 2,def 3;
reconsider E1=E as Element of COM(S,M) by Th27;
max+f is E-measurable & max-f is E-measurable by A2,MESFUN11:10; then
A5:integral+(M,max+f) = integral+(COM M,max+f)
& integral+(M,max-f) = integral+(COM M,max-f) by A4,Th37,MESFUN11:5;
f is E1-measurable by A2,Th30;
hence f is_integrable_on (COM M) by A2,A5,A3,MESFUNC5:def 17;
Integral(M,f) = integral+(M,max+f) - integral+(M,max-f)
by MESFUNC5:def 16;
hence thesis by A5,MESFUNC5:def 16;
end;
begin :: Relation Between Riemann and Lebesgue Integrals
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f,g be PartFunc of X,REAL
st (E = dom f or E = dom g) & f a.e.= g,M
holds (f-g) a.e.= (X-->0)|E,M
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f,g be PartFunc of X,REAL;
assume that
A1: E = dom f or E = dom g and
A2: f a.e.= g,M;
consider A be Element of S such that
A3: M.A = 0 & f|A` = g|A` by A2,LPSPACE1:def 10;
A4: dom f /\ A` = dom(g|A`) by A3,RELAT_1:61
.= dom g /\ A` by RELAT_1:61;
A5: dom((f-g)|A`) = dom(f-g) /\ A` by RELAT_1:61; then
A6: dom((f-g)|A`)
= (dom f /\ dom g) /\ A` by VALUED_1:12
.= (dom f /\ A`) /\ (dom f /\ A`) by A4,XBOOLE_1:116;
A7: dom((f-g)|A`)
= (dom f /\ dom g) /\ A` by A5,VALUED_1:12
.= (dom g /\ A`) /\ (dom g /\ A`) by A4,XBOOLE_1:116;
A8: dom(((X-->0)|E)|A`) = dom((X-->0)|E) /\ A` by RELAT_1:61
.= dom(X-->0) /\ E /\ A` by RELAT_1:61
.= E /\ A` by XBOOLE_1:28;
for x be Element of X st x in dom((f-g)|A`) holds
((f-g)|A`).x = (((X-->0)|E)|A`).x
proof
let x be Element of X;
assume A9: x in dom((f-g)|A`); then
A10: x in E by A7,A1,A6,XBOOLE_0:def 4;
A11: x in dom(f-g) & x in A` by A5,A9,XBOOLE_0:def 4; then
A12: ((f-g)|A`).x = (f-g).x by FUNCT_1:49
.= f.x - g.x by A11,VALUED_1:13
.= (f|A`).x - g.x by A11,FUNCT_1:49
.= (f|A`).x - (g|A`).x by A11,FUNCT_1:49
.= 0 by A3;
(((X-->0)|E)|A`).x = ((X-->0)|E).x by A11,FUNCT_1:49
.= (X-->0).x by A10,FUNCT_1:49;
hence ((f-g)|A`).x = (((X-->0)|E)|A`).x by A12;
end;
hence (f-g) a.e.= (X-->0)|E,M by A3,A7,A1,A6,A8,PARTFUN1:5,LPSPACE1:def 10;
end;
theorem Th40:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f,g be PartFunc of X,REAL st E = dom(f-g)
& (f-g) a.e.= (X-->0)|E,M holds f|E a.e.= g|E,M
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f,g be PartFunc of X,REAL;
assume that
A1: E = dom(f-g) and
A2: (f-g) a.e.= (X-->0)|E,M;
consider A be Element of S such that
A3: M.A = 0 & (f-g)|A` = ((X-->0)|E)|A` by A2,LPSPACE1:def 10;
dom f /\ dom g = E by A1,VALUED_1:12; then
A4: dom(f|E) = E & dom(g|E) = E by XBOOLE_1:17,RELAT_1:62; then
A5: dom((f|E)|A`) = dom(g|E) /\ A` by RELAT_1:61
.= dom((g|E)|A`) by RELAT_1:61;
for x be Element of X st x in dom((f|E)|A`) holds
((f|E)|A`).x = ((g|E)|A`).x
proof
let x be Element of X;
assume x in dom((f|E)|A`); then
A6: x in dom(f|E) & x in A` by RELAT_1:57;
A7: ((f-g)|A`).x = (f-g).x by A6,FUNCT_1:49
.= f.x - g.x by A1,A6,A4,VALUED_1:13;
A8: (((X-->0)|E)|A`).x = ((X-->0)|E).x by A6,FUNCT_1:49
.= (X-->0).x by A6,A4,FUNCT_1:49
.= 0;
((f|E)|A`).x = (f|E).x by A6,FUNCT_1:49
.= g.x by A6,A8,A3,A7,A4,FUNCT_1:49
.= (g|E).x by A6,A4,FUNCT_1:49;
hence ((f|E)|A`).x = ((g|E)|A`).x by A6,FUNCT_1:49;
end;
hence f|E a.e.= g|E,M by A3,A5,PARTFUN1:5,LPSPACE1:def 10;
end;
theorem Th41:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f be PartFunc of X,REAL st E = dom f &
M.E < +infty & f is bounded & f is E-measurable
holds f is_integrable_on M
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f be PartFunc of X,REAL;
assume that
A1: E = dom f and
A2: M.E < +infty and
A3: f is bounded and
A4: f is E-measurable;
A5: E = dom(R_EAL f) by A1,MESFUNC5:def 7;
A6: R_EAL f is E-measurable by A4,MESFUNC6:def 1;
A7: rng f is real-bounded by A3,INTEGRA1:15;
per cases;
suppose E <> {}; then
A8: rng f <> {} by A1,RELAT_1:42; then
reconsider LB = inf rng f as Real by A7;
reconsider UB = sup rng f as Real by A7,A8;
set r = max(|.LB.|, |.UB.|);
reconsider g = chi(E,X) as PartFunc of X,ExtREAL by RELSET_1:7,NUMBERS:31;
dom g = X by FUNCT_3:def 3; then
A9: dom(r(#)g) = X by MESFUNC1:def 6;
g is_integrable_on M by A2,MESFUNC7:24; then
r(#)g is_integrable_on M by MESFUNC5:110; then
A10: (r(#)g)|E is_integrable_on M by MESFUNC5:112;
A11: dom((r(#)g)|E) = dom(r(#)g) /\ E by RELAT_1:61
.= dom g /\ E by MESFUNC1:def 6
.= X /\ E by FUNCT_3:def 3
.= E by XBOOLE_1:28;
for x be Element of X st x in dom(R_EAL f)
holds |.(R_EAL f).x .| <= ((r(#)g)|E).x
proof
let x be Element of X;
assume A12: x in dom(R_EAL f); then
x in dom f by MESFUNC5:def 7; then
A13: LB <= f.x & f.x <= UB by XXREAL_2:3,4,FUNCT_1:3;
A14: r >= |.UB.| & r >= |.LB.| & -r <= -|.LB.| by XXREAL_0:25,XREAL_1:24;
A15: R_EAL f = f by MESFUNC5:def 7;
-|.LB.| <= LB & UB <= |.UB.| by ABSVALUE:4; then
-|.LB.| <= f.x & f.x <= |.UB.| by A13,XXREAL_0:2; then
-r <= f.x & f.x <= r by A14,XXREAL_0:2; then
A16: |. f.x .| <= r by ABSVALUE:5;
A17: g.x = 1 by A12,A5,FUNCT_3:def 3;
((r(#)g)|E).x = (r(#)g).x by A12,A11,A5,FUNCT_1:47
.= r*(g.x) by A9,MESFUNC1:def 6
.= r*1 by A17,XXREAL_3:def 5;
hence |.(R_EAL f).x .| <= ((r(#)g)|E).x by A16,A15,EXTREAL1:12;
end; then
R_EAL f is_integrable_on M by A6,A5,A10,A11,MESFUNC5:102;
hence f is_integrable_on M by MESFUNC6:def 4;
end;
suppose A18: E = {};
A19: dom(max+(R_EAL f)) = E & dom(max-(R_EAL f)) = E
by A5,MESFUNC2:def 2,def 3;
for x be Element of X st x in dom(max+(R_EAL f)) holds
(max+(R_EAL f)).x = 0 by A18,A5,MESFUNC2:def 2; then
A20: integral+(M,max+(R_EAL f)) = 0 by A19,A6,MESFUNC2:25,MESFUNC5:87;
for x be Element of X st x in dom(max-(R_EAL f)) holds
(max-(R_EAL f)).x = 0 by A18,A5,MESFUNC2:def 3; then
integral+(M,max-(R_EAL f)) = 0 by A19,A6,A5,MESFUNC2:26,MESFUNC5:87;
hence f is_integrable_on M by A6,A5,A20,MESFUNC5:def 17,MESFUNC6:def 4;
end;
end;
theorem Th42:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f,g be PartFunc of X,REAL holds f a.e.= g,M iff
max+f a.e.= max+g,M & max-f a.e.= max-g,M
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f,g be PartFunc of X,REAL;
hereby assume f a.e.= g,M; then
consider E be Element of S such that
A1: M.E = 0 & f|E` = g|E` by LPSPACE1:def 10;
(max+f)|E` = max+(f|E`) by RFUNCT_3:44; then
(max+f)|E` = (max+g)|E` by A1,RFUNCT_3:44;
hence max+f a.e.= max+g,M by A1,LPSPACE1:def 10;
(max-f)|E` = max-(f|E`) by RFUNCT_3:45; then
(max-f)|E` = (max-g)|E` by A1,RFUNCT_3:45;
hence max-f a.e.= max-g,M by A1,LPSPACE1:def 10;
end;
assume that
A2: max+f a.e.= max+g,M and
A3: max-f a.e.= max-g,M;
consider E1 be Element of S such that
A4: M.E1 = 0 & (max+f)|E1` = (max+g)|E1` by A2,LPSPACE1:def 10;
consider E2 be Element of S such that
A5: M.E2 = 0 & (max-f)|E2` = (max-g)|E2` by A3,LPSPACE1:def 10;
set E = E1 \/ E2;
M.E <= M.E1 + M.E2 by MEASURE1:10; then
M.E <= 0 + 0 by A4,A5; then
A6: M.E = 0 by SUPINF_2:51;
(max+f)|E` = ((max+g)|E1`)|E` by A4,SUBSET_1:21,RELAT_1:74; then
A7: (max+f)|E` = (max+g)|E` by SUBSET_1:21,RELAT_1:74;
(max-f)|E` = ((max-g)|E2`)|E` by A5,SUBSET_1:21,RELAT_1:74; then
A8: (max-f)|E` = (max-g)|E` by SUBSET_1:21,RELAT_1:74;
A9:dom(max+f - max-f) = dom f & dom(max+g - max-g) = dom g by RFUNCT_3:34;
dom(f|E`) = dom(max+(f|E`)) by RFUNCT_3:def 10; then
dom(f|E`) = dom((max+f)|E`) by RFUNCT_3:44; then
dom(f|E`) = dom(max+(g|E`)) by A7,RFUNCT_3:44; then
A10: dom(f|E`) = dom(g|E`) by RFUNCT_3:def 10;
for x be Element of X st x in dom(f|E`) holds
(f|E`).x = (g|E`).x
proof
let x be Element of X;
assume A11: x in dom(f|E`); then
A12: x in dom f & x in E` by RELAT_1:57;
A13: x in dom g & x in E` by A10,A11,RELAT_1:57;
(f|E`).x = f.x by A11,FUNCT_1:47; then
(f|E`).x = (max+f - max-f).x by RFUNCT_3:34; then
(f|E`).x = (max+f).x - (max-f).x by A12,A9,VALUED_1:13; then
(f|E`).x = ((max+f)|E`).x - (max-f).x by A12,FUNCT_1:49; then
(f|E`).x = ((max+f)|E`).x - ((max-f)|E`).x by A12,FUNCT_1:49; then
(f|E`).x = (max+g).x - ((max-g)|E`).x by A12,A7,A8,FUNCT_1:49; then
(f|E`).x = (max+g).x - (max-g).x by A12,FUNCT_1:49; then
(f|E`).x = (max+g - max-g).x by A13,A9,VALUED_1:13; then
(f|E`).x = g.x by RFUNCT_3:34;
hence (f|E`).x = (g|E`).x by A13,FUNCT_1:49;
end;
hence f a.e.= g,M by A6,A10,PARTFUN1:5,LPSPACE1:def 10;
end;
theorem Th43:
for X be non empty set, f be PartFunc of X,REAL holds
max+(R_EAL f) = R_EAL(max+f) & max-(R_EAL f) = R_EAL(max-f)
proof
let X be non empty set, f be PartFunc of X,REAL;
dom(max+(R_EAL f)) = dom(R_EAL f) by MESFUNC2:def 2; then
dom(max+(R_EAL f)) = dom f by MESFUNC5:def 7; then
A1: dom(max+(R_EAL f)) = dom(max+f) by RFUNCT_3:def 10; then
A2: dom(max+(R_EAL f)) = dom(R_EAL(max+f)) by MESFUNC5:def 7;
dom(max-(R_EAL f)) = dom(R_EAL f) by MESFUNC2:def 3; then
dom(max-(R_EAL f)) = dom f by MESFUNC5:def 7; then
A3: dom(max-(R_EAL f)) = dom(max-f) by RFUNCT_3:def 11; then
A4: dom(max-(R_EAL f)) = dom(R_EAL(max-f)) by MESFUNC5:def 7;
for x be Element of X st x in dom(max+(R_EAL f)) holds
(max+(R_EAL f)).x = (R_EAL(max+f)).x
proof
let x be Element of X;
assume A5: x in dom(max+(R_EAL f));
per cases;
suppose A6: f.x >= 0; then
A7: (R_EAL f).x >= 0 by MESFUNC5:def 7;
(max+(R_EAL f)).x = max((R_EAL f).x,0) by A5,MESFUNC2:def 2; then
(max+(R_EAL f)).x = (R_EAL f).x by A7,XXREAL_0:def 10; then
(max+(R_EAL f)).x = f.x by MESFUNC5:def 7; then
(max+(R_EAL f)).x = max(f.x,0) by A6,XXREAL_0:def 10; then
(max+(R_EAL f)).x = max+(f.x) by RFUNCT_3:def 1; then
(max+(R_EAL f)).x = (max+f).x by A1,A5,RFUNCT_3:def 10;
hence (max+(R_EAL f)).x = (R_EAL(max+f)).x by MESFUNC5:def 7;
end;
suppose A8: f.x < 0; then
A9: (R_EAL f).x < 0 by MESFUNC5:def 7;
(max+(R_EAL f)).x = max((R_EAL f).x,0) by A5,MESFUNC2:def 2; then
(max+(R_EAL f)).x = 0 by A9,XXREAL_0:def 10; then
(max+(R_EAL f)).x = max(f.x,0) by A8,XXREAL_0:def 10; then
(max+(R_EAL f)).x = max+(f.x) by RFUNCT_3:def 1; then
(max+(R_EAL f)).x = (max+f).x by A1,A5,RFUNCT_3:def 10;
hence (max+(R_EAL f)).x = (R_EAL(max+f)).x by MESFUNC5:def 7;
end;
end;
hence max+(R_EAL f) = R_EAL(max+f) by A2,PARTFUN1:5;
for x be Element of X st x in dom(max-(R_EAL f)) holds
(max-(R_EAL f)).x = (R_EAL(max-f)).x
proof
let x be Element of X;
assume A10: x in dom(max-(R_EAL f));
per cases;
suppose A11: f.x <= 0; then
A12: (R_EAL f).x <= 0 by MESFUNC5:def 7;
(max-(R_EAL f)).x = max(-((R_EAL f).x),0) by A10,MESFUNC2:def 3; then
(max-(R_EAL f)).x = -((R_EAL f).x) by A12,XXREAL_0:def 10; then
(max-(R_EAL f)).x = -((f.x) qua ExtReal) by MESFUNC5:def 7; then
(max-(R_EAL f)).x = max(-(f.x),0) by A11,XXREAL_0:def 10; then
(max-(R_EAL f)).x = max-(f.x) by RFUNCT_3:def 2; then
(max-(R_EAL f)).x = (max-f).x by A3,A10,RFUNCT_3:def 11;
hence (max-(R_EAL f)).x = (R_EAL(max-f)).x by MESFUNC5:def 7;
end;
suppose A13: f.x > 0; then
A14: (R_EAL f).x > 0 by MESFUNC5:def 7;
(max-(R_EAL f)).x = max(-((R_EAL f).x),0) by A10,MESFUNC2:def 3; then
(max-(R_EAL f)).x = 0 by A14,XXREAL_0:def 10; then
(max-(R_EAL f)).x = max(-(f.x),0) by A13,XXREAL_0:def 10; then
(max-(R_EAL f)).x = max-(f.x) by RFUNCT_3:def 2; then
(max-(R_EAL f)).x = (max-f).x by A3,A10,RFUNCT_3:def 11;
hence (max-(R_EAL f)).x = (R_EAL(max-f)).x by MESFUNC5:def 7;
end;
end;
hence max-(R_EAL f) = R_EAL(max-f) by A4,PARTFUN1:5;
end;
theorem Th44:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f,g be PartFunc of X,REAL, E be Element of S
st M is complete & f is_integrable_on M & f a.e.= g,M & E = dom f & E = dom g
holds g is_integrable_on M & Integral(M,f) = Integral(M,g)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f,g be PartFunc of X,REAL, E be Element of S;
assume that
A1: M is complete and
A2: f is_integrable_on M and
A3: f a.e.= g,M and
A4: E = dom f and
A5: E = dom g;
A6: R_EAL f is_integrable_on M by A2,MESFUNC6:def 4; then
consider E1 be Element of S such that
A7: E1 = dom(R_EAL f) & (R_EAL f) is E1-measurable by MESFUNC5:def 17;
A8: integral+(M,max+(R_EAL f)) < +infty by A6,MESFUNC5:def 17;
A9:integral+(M,max-(R_EAL f)) < +infty by A6,MESFUNC5:def 17;
A10: (R_EAL f) = f & (R_EAL g) = g by MESFUNC5:def 7; then
A11: f is E-measurable by A4,A7,MESFUNC6:def 1; then
A12: (R_EAL g) is E-measurable by A1,A3,A4,Th26,MESFUNC6:def 1;
A13: E = dom(max+f) & E = dom(max+g) by A4,A5,RFUNCT_3:def 10;
max+(R_EAL f) is E-measurable
& max+(R_EAL g) is E-measurable by A4,A7,A12,A10,A5,MESFUN11:10; then
A14:R_EAL(max+f) is E-measurable
& R_EAL(max+g) is E-measurable by Th43; then
A15: max+f is E-measurable & max+g is E-measurable by MESFUNC6:def 1; then
Integral(M,max+f) = integral+(M,R_EAL(max+f)) by A13,MESFUNC6:61,82; then
A16: Integral(M,max+f) < +infty by A8,Th43;
consider E0 be Element of S such that
A17: M.E0 = 0 & f|E0` = g|E0` by A3,LPSPACE1:def 10;
consider E2 be Element of S such that
A18: M.E2 = 0 & (max+f)|E2` = (max+g)|E2` by A3,Th42,LPSPACE1:def 10;
(max+f)|(X\E2) = (max+f)|E2` by SUBSET_1:def 4; then
(max+f)|(X\E2) = (max+g)|(X\E2) by A18,SUBSET_1:def 4; then
(max+f)|(E\E2) = ((max+g)|(X\E2))|(E\E2) by XBOOLE_1:33,RELAT_1:74; then
A19: (max+f)|(E\E2) = (max+g)|(E\E2) by XBOOLE_1:33,RELAT_1:74;
Integral(M,max+f) = Integral(M,(max+f)|(E\E2))
by A13,A14,A18,MESFUNC6:def 1,89; then
Integral(M,max+f) = Integral(M,max+g)
by A13,A14,A18,A19,MESFUNC6:def 1,89; then
integral+(M,R_EAL(max+g)) < +infty by A13,A15,A16,MESFUNC6:61,82; then
A20: integral+(M,max+(R_EAL g)) < +infty by Th43;
A21: E = dom(max-f) & E = dom(max-g) by A4,A5,RFUNCT_3:def 11;
max-(R_EAL f) is E-measurable
& max-(R_EAL g) is E-measurable by A4,A7,A12,A10,A5,MESFUN11:10; then
A22: R_EAL(max-f) is E-measurable
& R_EAL(max-g) is E-measurable by Th43; then
A23:max-f is E-measurable & max-g is E-measurable by MESFUNC6:def 1; then
Integral(M,max-f) = integral+(M,R_EAL(max-f)) by A21,MESFUNC6:61,82; then
A24: Integral(M,max-f) < +infty by A9,Th43;
consider E3 be Element of S such that
A25: M.E3 = 0 & (max-f)|E3` = (max-g)|E3` by A3,Th42,LPSPACE1:def 10;
(max-f)|(X\E3) = (max-f)|E3` by SUBSET_1:def 4; then
(max-f)|(X\E3) = (max-g)|(X\E3) by A25,SUBSET_1:def 4; then
(max-f)|(E\E3) = ((max-g)|(X\E3))|(E\E3) by XBOOLE_1:33,RELAT_1:74; then
A26:(max-f)|(E\E3) = (max-g)|(E\E3) by XBOOLE_1:33,RELAT_1:74;
Integral(M,max-f) = Integral(M,(max-f)|(E\E3))
by A21,A22,A25,MESFUNC6:def 1,89; then
Integral(M,max-f) = Integral(M,max-g)
by A26,A21,A22,A25,MESFUNC6:def 1,89; then
integral+(M,R_EAL(max-g)) < +infty by A21,A23,A24,MESFUNC6:61,82; then
integral+(M,max-(R_EAL g)) < +infty by Th43;
hence g is_integrable_on M by A12,A10,A5,A20
,MESFUNC5:def 17,MESFUNC6:def 4;
f|(E\E0) = (f|(X\E0))|(E\E0) by XBOOLE_1:33,RELAT_1:74; then
f|(E\E0) = (f|E0`)|(E\E0) by SUBSET_1:def 4; then
f|(E\E0) = (g|(X\E0))|(E\E0) by A17,SUBSET_1:def 4; then
A27: f|(E\E0) = g|(E\E0) by XBOOLE_1:33,RELAT_1:74;
Integral(M,f) = Integral(M,f|(E\E0)) by A4,A10,A17,A7,MESFUNC6:def 1,89;
hence Integral(M,f) = Integral(M,g)
by A5,A17,A27,A11,A1,A3,A4,Th26,MESFUNC6:89;
end;
Lm6:
for a be Real holds {a} is Element of Borel_Sets
proof
let a be Real;
{a} = [.a,a.] by XXREAL_1:17;
hence thesis by MEASUR10:5;
end;
theorem Th45:
for f be PartFunc of REAL,ExtREAL, a be Real st a in dom f
ex A be Element of Borel_Sets
st A = {a} & f is A-measurable & f|A is_integrable_on B-Meas &
Integral(B-Meas,f|A) = 0
proof
let f be PartFunc of REAL,ExtREAL, a be Real;
assume
A1: a in dom f;
reconsider A = {a} as Element of Borel_Sets by Lm6;
take A;
thus A = {a};
A2: now let r be Real;
per cases;
suppose a in less_dom(f,r); then
A /\ less_dom(f,r) = A by ZFMISC_1:46;
hence A /\ less_dom(f,r) in Borel_Sets;
end;
suppose not a in less_dom(f,r); then
A /\ less_dom(f,r) = {} by XBOOLE_0:def 7,ZFMISC_1:50;
hence A /\ less_dom(f,r) in Borel_Sets by MEASURE1:7;
end;
end;
hence
A3: f is A-measurable by MESFUNC1:def 16;
A4: A = dom f /\ A by A1,ZFMISC_1:31,XBOOLE_1:28; then
A5: f|A is A-measurable by A2,MESFUNC1:def 16,MESFUNC5:42;
reconsider a1=a as R_eal by XXREAL_0:def 1;
A6: A = [.a,a.] & A = [.a1,a1.] by XXREAL_1:17; then
A7: B-Meas.A = diameter A by MEASUR12:71 .= 0 by A6,MEASURE5:11;
A8: dom(f|A) = A by A4,RELAT_1:61; then
A9: dom(max+(f|A)) = A & dom(max-(f|A)) = A by MESFUNC2:def 2,def 3;
A10: max+(f|A) is A-measurable & max-(f|A) is A-measurable
by A5,A8,MESFUN11:10; then
Integral(B-Meas,max+(f|A)|A) = 0 by A7,A9,MESFUNC5:94; then
A11: integral+(B-Meas,max+(f|A)) < +infty by A9,A10,MESFUNC5:88,MESFUN11:5;
Integral(B-Meas,max-(f|A)|A) = 0 by A7,A9,A10,MESFUNC5:94; then
integral+(B-Meas,max-(f|A)) = 0 by A9,A10,MESFUNC5:88,MESFUN11:5;
hence f|A is_integrable_on B-Meas by A8,A4,A11,A3,MESFUNC5:42,def 17;
Integral(B-Meas,f|A|A) = 0 by A4,A8,A7,A3,MESFUNC5:42,94;
hence Integral(B-Meas,f|A) = 0;
end;
theorem Th46:
for f be PartFunc of REAL,REAL, a be Real st a in dom f
ex A be Element of Borel_Sets
st A = {a} & f is A-measurable & f|A is_integrable_on B-Meas &
Integral(B-Meas,f|A) = 0
proof
let f be PartFunc of REAL,REAL, a be Real;
assume a in dom f; then
a in dom(R_EAL f) by MESFUNC5:def 7; then
consider A be Element of Borel_Sets such that
A1: A = {a} and
A2: (R_EAL f) is A-measurable and
A3: (R_EAL f)|A is_integrable_on B-Meas and
A4: Integral(B-Meas,(R_EAL f)|A) = 0 by Th45;
take A;
thus A = {a} by A1;
thus f is A-measurable by A2,MESFUNC6:def 1;
(R_EAL f)|A = f|A by MESFUNC5:def 7; then
(R_EAL f)|A = (R_EAL(f|A)) by MESFUNC5:def 7;
hence thesis by A3,A4,MESFUNC6:def 3,def 4;
end;
theorem
for f be PartFunc of REAL,ExtREAL st f is_integrable_on B-Meas
holds f is_integrable_on L-Meas & Integral(B-Meas,f) = Integral(L-Meas,f)
by Th38,MEASUR12:def 11,def 12;
theorem Th48:
for f be PartFunc of REAL,REAL st f is_integrable_on B-Meas
holds f is_integrable_on L-Meas & Integral(B-Meas,f) = Integral(L-Meas,f)
proof
let f be PartFunc of REAL,REAL;
assume f is_integrable_on B-Meas; then
A1: R_EAL f is_integrable_on B-Meas by MESFUNC6:def 4;
hence f is_integrable_on L-Meas
by Th38,MEASUR12:def 11,def 12,MESFUNC6:def 4;
Integral(B-Meas,f) = Integral(B-Meas,R_EAL f)
& Integral(L-Meas,f) = Integral(L-Meas,R_EAL f) by MESFUNC6:def 3;
hence Integral(B-Meas,f) = Integral(L-Meas,f)
by A1,Th38,MEASUR12:def 11,def 12;
end;
theorem Th49:
for A be non empty closed_interval Subset of REAL, A1 be Element of L-Field,
f be PartFunc of REAL,REAL
st A = A1 & A c= dom f & f||A is bounded & f is_integrable_on A
holds f is A1-measurable & f|A1 is_integrable_on L-Meas &
integral(f||A) = Integral(L-Meas,f|A)
proof
let A be non empty closed_interval Subset of REAL,
A1 be Element of L-Field, f be PartFunc of REAL,REAL;
assume that
A1: A = A1 and
A2: A c= dom f and
A3: f||A is bounded and
A4: f is_integrable_on A;
f||A is total by A2,INTEGRA5:6; then
reconsider g = f||A as Function of A,REAL;
consider a,b be Real such that
A5: a <= b and
A6: A = [.a,b.] by MEASURE5:14;
f||A is integrable by A4,INTEGRA5:def 1; then
A7: f||A is upper_integrable & f||A is lower_integrable
& upper_integral f||A = lower_integral f||A by INTEGRA1:def 16;
per cases;
suppose A8: a = b; then
A9: A = {a} by A6,XXREAL_1:17; then
consider AA be Element of Borel_Sets
such that
A10: AA = {a} and
A11: f is AA-measurable and
A12: f|AA is_integrable_on B-Meas and
A13: Integral(B-Meas,f|AA) = 0 by A2,Th46,ZFMISC_1:31;
(R_EAL f) is AA-measurable by A11,MESFUNC6:def 1;
hence f is A1-measurable
by A1,A9,A10,Th30,MEASUR12:def 11,MESFUNC6:def 1;
thus f|A1 is_integrable_on L-Meas by A1,A9,A10,A12,Th48;
A = [. lower_bound A, upper_bound A .] by INTEGRA1:4; then
a = lower_bound A & b = upper_bound A by A6,INTEGRA1:5; then
vol A = b-a by INTEGRA1:def 5; then
integral(f||A) = 0 by A8,INTEGRA4:6;
hence integral(f||A) = Integral(L-Meas,f|A) by A9,A10,A12,A13,Th48;
end;
suppose a <> b; then
A14: a < b by A5,XXREAL_0:1;
A = [. lower_bound A, upper_bound A .] by INTEGRA1:4; then
a = lower_bound A & b = upper_bound A by A6,INTEGRA1:5; then
A15: vol A = b-a by INTEGRA1:def 5; then
A16: vol A > 0 by A14,XREAL_1:50;
f||A is total by A2,INTEGRA5:6; then
A17: dom(f||A) = A by PARTFUN1:def 2;
consider F1 be with_the_same_dom Functional_Sequence of REAL,ExtREAL,
I1 be ExtREAL_sequence such that
A18: A = dom(F1.0)
& (for n be Nat holds
F1.n is_simple_func_in Borel_Sets
& Integral(B-Meas,F1.n) = lower_sum(f||A,EqDiv(A,2|^n))
& (for x be Real st x in A holds
lower_bound rng(f||A) <= (F1.n).x <= (f||A).x) )
& (for n,m be Nat st n <= m holds for x be Element of REAL st x in A holds
(F1.n).x <= (F1.m).x)
& (for x be Element of REAL st x in A holds
F1#x is convergent & lim(F1#x) = sup(F1#x) & sup(F1#x) <= (f||A).x)
& lim F1 is_integrable_on B-Meas
& (for n be Nat holds I1.n = Integral(B-Meas,F1.n))
& I1 is convergent & lim I1 = Integral(B-Meas,lim F1)
by A3,A17,A15,Th21,A14,XREAL_1:50;
consider F2 be with_the_same_dom Functional_Sequence of REAL,ExtREAL,
I2 be ExtREAL_sequence such that
A19: A = dom(F2.0)
& (for n be Nat holds
F2.n is_simple_func_in Borel_Sets
& Integral(B-Meas,F2.n) = upper_sum(f||A,EqDiv(A,2|^n))
& (for x be Real st x in A holds
upper_bound rng(f||A) >= (F2.n).x >= (f||A).x) )
& (for n,m be Nat st n <= m holds for x be Element of REAL st x in A holds
(F2.n).x >= (F2.m).x)
& (for x be Element of REAL st x in A holds
F2#x is convergent & lim(F2#x) = inf(F2#x) & inf(F2#x) >= (f||A).x)
& lim F2 is_integrable_on B-Meas
& (for n be Nat holds I2.n = Integral(B-Meas,F2.n))
& I2 is convergent & lim I2 = Integral(B-Meas,lim F2)
by A3,A17,A15,Th22,A14,XREAL_1:50;
A20: for n be Nat holds
(upper_sum_set(f||A)).EqDiv(A,2|^n) = I2.n
& (lower_sum_set(f||A)).EqDiv(A,2|^n) = I1.n
proof
let n be Nat;
(upper_sum_set(f||A)).EqDiv(A,2|^n)
= upper_sum(f||A,EqDiv(A,2|^n)) by INTEGRA1:def 10
.= Integral(B-Meas,F2.n) by A19;
hence (upper_sum_set(f||A)).EqDiv(A,2|^n) = I2.n by A19;
(lower_sum_set(f||A)).EqDiv(A,2|^n)
= lower_sum(f||A,EqDiv(A,2|^n)) by INTEGRA1:def 11
.= Integral(B-Meas,F1.n) by A18;
hence (lower_sum_set(f||A)).EqDiv(A,2|^n) = I1.n by A18;
end;
defpred T[Element of NAT,object] means
$2 = EqDiv(A,2|^$1);
A21: for n be Element of NAT ex D be Element of divs A st T[n,D]
proof
let n be Element of NAT;
reconsider D = EqDiv(A,2|^n) as Element of divs A by INTEGRA1:def 3;
take D;
thus thesis;
end;
consider T be Function of NAT,divs A such that
A22: for n be Element of NAT holds T[n,T.n] from FUNCT_2:sch 3(A21);
A23: for n be Nat holds T.n = EqDiv(A,2|^n)
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 12;
hence thesis by A22;
end;
A24: (f||A)|A is bounded by A3;
A25: delta(T) is 0-convergent non-zero by A16,A23,Th17; then
A26: upper_sum(g,T) is convergent
& lim upper_sum(g,T) = upper_integral(g) by A16,A24,INTEGRA3:26;
A27: lower_sum(g,T) is convergent
& lim lower_sum(g,T) = lower_integral(g) by A16,A24,A25,INTEGRA3:25;
for n be Element of NAT holds I1.n = lower_sum(f||A,T).n
proof
let n be Element of NAT;
I1.n = (lower_sum_set(f||A)).EqDiv(A,2|^n) by A20
.= (lower_sum_set(f||A)).(T.n) by A23
.= lower_sum(f||A,(T.n)) by INTEGRA1:def 11;
hence I1.n = lower_sum(f||A,T).n by INTEGRA2:def 3;
end; then
I1 = lower_sum(f||A,T) by FUNCT_2:def 7; then
A28: lim I1 = lower_integral(f||A) by A27,RINFSUP2:14;
for n be Element of NAT holds I2.n = upper_sum(f||A,T).n
proof
let n be Element of NAT;
I2.n = (upper_sum_set(f||A)).EqDiv(A,2|^n) by A20
.= (upper_sum_set(f||A)).(T.n) by A23
.= upper_sum(f||A,(T.n)) by INTEGRA1:def 10;
hence I2.n = upper_sum(f||A,T).n by INTEGRA2:def 2;
end; then
I2 = upper_sum(f||A,T) by FUNCT_2:def 7; then
A29: lim I2 = upper_integral(f||A) by A26,RINFSUP2:14;
A30: for x be Element of REAL st x in A holds (lim F1).x <= (f||A).x
proof
let x be Element of REAL;
assume A31: x in A; then
A32: x in dom (lim F1) by A18,MESFUNC8:def 9;
lim(F1#x) = sup(F1#x) by A31,A18; then
lim(F1#x) <= (f||A).x by A31,A18;
hence (lim F1).x <= (f||A).x by A32,MESFUNC8:def 9;
end;
A33: for x be set st x in dom(lim F1) holds -infty < (lim F1).x
proof
let x be set;
assume A34: x in dom(lim F1); then
reconsider x1=x as Element of REAL;
A35: x in A by A34,A18,MESFUNC8:def 9; then
lim(F1#x1) = sup(F1#x1) by A18; then
(lim F1).x = sup(F1#x1) by A34,MESFUNC8:def 9; then
(F1#x1).0 <= (lim F1).x by RINFSUP2:23; then
A36: (F1.0).x1 <= (lim F1).x by MESFUNC5:def 13;
lower_bound rng(f||A) <= (F1.0).x1 by A35,A18; then
lower_bound rng(f||A) <= (lim F1).x by A36,XXREAL_0:2;
hence -infty < (lim F1).x by XXREAL_0:2,6;
end;
A37: for x be set st x in dom(lim F1) holds +infty > (lim F1).x
proof
let x be set;
assume A38: x in dom(lim F1); then
reconsider x1=x as Element of REAL;
A39: x in A by A38,A18,MESFUNC8:def 9; then
lim(F1#x1) = sup(F1#x1) by A18; then
(lim F1).x = sup(F1#x1) by A38,MESFUNC8:def 9; then
(lim F1).x <= (f||A).x1 by A39,A18; then
A40: (lim F1).x <= f.x1 by A39,FUNCT_1:49;
f.x1 in REAL by A2,A39,PARTFUN1:4;
hence +infty > (lim F1).x by A40,XXREAL_0:2,9;
end;
A41: lim F1 is without-infty without+infty by A33,A37,MESFUNC5:10,11; then
reconsider Lf1 = lim F1 as PartFunc of REAL,REAL by Th3;
A42: for x be set st x in dom(lim F2) holds +infty > (lim F2).x
proof
let x be set;
assume A43: x in dom(lim F2); then
reconsider x1=x as Element of REAL;
A44: x in A by A43,A19,MESFUNC8:def 9; then
lim(F2#x1) = inf(F2#x1) by A19; then
(lim F2).x = inf(F2#x1) by A43,MESFUNC8:def 9; then
(F2#x1).0 >= (lim F2).x by RINFSUP2:23; then
A45: (F2.0).x1 >= (lim F2).x by MESFUNC5:def 13;
upper_bound rng(f||A) >= (F2.0).x1 by A44,A19; then
upper_bound rng(f||A) >= (lim F2).x by A45,XXREAL_0:2;
hence +infty > (lim F2).x by XXREAL_0:2,4;
end;
A46: for x be set st x in dom(lim F2) holds -infty < (lim F2).x
proof
let x be set;
assume A47: x in dom(lim F2); then
reconsider x1=x as Element of REAL;
A48: x in A by A47,A19,MESFUNC8:def 9; then
lim(F2#x1) = inf(F2#x1) by A19; then
(lim F2).x = inf(F2#x1) by A47,MESFUNC8:def 9; then
(lim F2).x >= (f||A).x1 by A48,A19; then
A49: (lim F2).x >= f.x1 by A48,FUNCT_1:49;
f.x1 in REAL by A2,A48,PARTFUN1:4;
hence -infty < (lim F2).x by A49,XXREAL_0:2,12;
end;
lim F2 is without-infty without+infty by A42,A46,MESFUNC5:10,11; then
reconsider Lf2 = lim F2 as PartFunc of REAL,REAL by Th3;
A50: R_EAL Lf2 = lim F2 by MESFUNC5:def 7;
lim F2 - lim F1 is without-infty without+infty
by A41,A42,A46,MESFUNC5:10,11,MESFUNC9:5,6; then
reconsider Lf3 = lim F2 - lim F1 as PartFunc of REAL,REAL by Th3;
A51: R_EAL Lf3 = lim F2 - lim F1 by MESFUNC5:def 7;
A52: dom(Lf2 - Lf1) = dom(lim F2) /\ dom(lim F1) by VALUED_1:12
.= dom Lf3 by A41,A46,MESFUNC5:10,17;
for x be Element of REAL st x in dom(Lf2-Lf1) holds
(Lf2-Lf1).x = Lf3.x
proof
let x be Element of REAL;
assume A53: x in dom(Lf2-Lf1); then
x in dom(lim F2) /\ dom(lim F1) by VALUED_1:12; then
A54: x in dom(lim F2 - lim F1) by A41,A46,MESFUNC5:10,17;
(Lf2-Lf1).x = Lf2.x - Lf1.x by A53,VALUED_1:13
.= (Lf2.x) qua ExtReal - Lf1.x;
hence (Lf2-Lf1).x = Lf3.x by A54,MESFUNC1:def 4;
end; then
A55: Lf2-Lf1 = Lf3 by A52,PARTFUN1:5;
A56: for x be Element of REAL st x in A holds (lim F2).x >= (f||A).x
proof
let x be Element of REAL;
assume A57: x in A; then
A58: x in dom(lim F2) by A19,MESFUNC8:def 9;
lim(F2#x) = inf(F2#x) by A57,A19; then
lim(F2#x) >= (f||A).x by A57,A19;
hence (lim F2).x >= (f||A).x by A58,MESFUNC8:def 9;
end;
A59: dom |. lim F2 - lim F1 .| = dom(lim F2 - lim F1) by MESFUNC1:def 10;
A60: dom(lim F1) = A & dom(lim F2) = A by A18,A19,MESFUNC8:def 9;
A61: for x be Element of REAL st x in dom |.lim F2 - lim F1.|
holds |.lim F2 - lim F1.| .x = (lim F2 - lim F1).x
proof
let x be Element of REAL;
assume A62: x in dom |.lim F2 - lim F1.|; then
A63: x in dom(lim F2 - lim F1) by MESFUNC1:def 10; then
x in (dom(lim F2) /\ dom(lim F1)) \
(((lim F2)"{+infty} /\ (lim F1)"{+infty}) \/ ((lim F2)"{-infty} /\
(lim F1)"{-infty})) by MESFUNC1:def 4; then
x in (dom(lim F2) /\ dom(lim F1)) by XBOOLE_0:def 5; then
(lim F2).x >= (f||A).x & (f||A).x >= (lim F1).x by A56,A30,A60; then
A64: (lim F2).x >= (lim F1).x by XXREAL_0:2;
|.lim F2 - lim F1.| .x
= |. (lim F2 - lim F1).x .| by A62,MESFUNC1:def 10
.= |. (lim F2).x - (lim F1).x .| by A63,MESFUNC1:def 4
.= (lim F2).x - (lim F1).x by A64,EXTREAL1:def 1,XXREAL_3:40;
hence |.lim F2 - lim F1.| .x = (lim F2 - lim F1).x by A63,MESFUNC1:def 4;
end; then
A65: |.lim F2 - lim F1.| = R_EAL Lf3 by A51,A59,PARTFUN1:5;
reconsider A2 = A as Subset of REAL;
reconsider A3 = A1 as Element of Borel_Sets by A1,MEASUR12:72;
Integral(B-Meas,|. lim F2 - lim F1 .|)
= Integral(B-Meas, lim F2 - lim F1) by A61,A59,PARTFUN1:5
.= Integral(B-Meas, (lim F2)|(dom(lim F2) /\ dom(lim F1)))
- Integral(B-Meas, (lim F1)|(dom(lim F2) /\ dom(lim F1)))
by A18,A19,MESFUN13:17
.= lim I2 + -lim I2 by A29,A7,A18,A19,A28,A60,XXREAL_3:def 4
.= 0 by XXREAL_3:7; then
A66: Integral(B-Meas,Lf3) = 0 by A65,MESFUNC6:def 3;
A67: Lf2 is_integrable_on B-Meas by A19,A50,MESFUNC6:def 4;
consider ELf2 be Element of Borel_Sets such that
A68: ELf2 = dom(R_EAL Lf2) & (R_EAL Lf2) is ELf2-measurable
by A19,A50,MESFUNC5:def 17;
R_EAL f = f by MESFUNC5:def 7; then
A69: (R_EAL f)|A1 = R_EAL(f|A1) by MESFUNC5:def 7;
A70: Lf2|A1 is A1-measurable
by A1,A60,A50,A68,Th30,MEASUR12:def 11,MESFUNC6:def 1;
reconsider z = 0 as Element of REAL by XREAL_0:def 1;
A71: dom Lf3 = dom(lim F2) /\ dom(lim F1) by A41,A46,MESFUNC5:10,17;
A72: for x be Element of REAL st x in A holds Lf2.x >= f.x
proof
let x be Element of REAL;
assume A73: x in A; then
lim(F2#x) = inf(F2#x) & inf(F2#x) >= (f||A).x by A19; then
Lf2.x >= (f||A).x by A73,A60,MESFUNC8:def 9;
hence Lf2.x >= f.x by A73,FUNCT_1:49;
end;
A74: for x be Element of REAL st x in A holds f.x >= Lf1.x
proof
let x be Element of REAL;
assume A75: x in A; then
lim(F1#x) = sup(F1#x) & sup(F1#x) <= (f||A).x by A18; then
Lf1.x <= (f||A).x by A75,A60,MESFUNC8:def 9;
hence Lf1.x <= f.x by A75,FUNCT_1:49;
end;
for x be object st x in dom Lf3 holds Lf3.x >= 0
proof
let x be object;
assume A76: x in dom Lf3; then
reconsider x1 = x as Element of REAL;
A77: Lf3.x = Lf2.x - Lf1.x by A55,A76,VALUED_1:13;
Lf2.x >= f.x1 & f.x1 >= Lf1.x by A72,A74,A76,A71,A60; then
Lf2.x >= Lf1.x by XXREAL_0:2;
hence Lf3.x >= 0 by A77,XREAL_1:48;
end; then
A78: Lf3 is nonnegative by SUPINF_2:52;
A79: R_EAL Lf3 = Lf3 by MESFUNC5:def 7;
R_EAL Lf3 is_integrable_on B-Meas by A51,A18,A19,MESFUN10:12; then
ex ELf3 be Element of Borel_Sets
st ELf3 = dom(R_EAL Lf3) & (R_EAL Lf3) is ELf3-measurable
by MESFUNC5:def 17; then
Lf3 is A3-measurable by A79,A71,A60,A1,MESFUNC6:def 1; then
A80: Lf3 a.e.= (REAL-->0)|A1,L-Meas by A1,A66,A71,A60,A78,Th25,Th29;
consider E0 be Element of L-Field such that
A82: L-Meas.E0 = 0 & Lf3|E0` = ((REAL-->0)|A1)|E0` by A80,LPSPACE1:def 10;
dom(Lf2 - f) = dom Lf2 /\ dom f by VALUED_1:12; then
A81: dom(Lf2 - f) = A1 by A1,A60,A2,XBOOLE_1:28; then
A83: dom((Lf2-f)|E0`) = A1 /\ E0` by RELAT_1:61;
dom((REAL-->0)|A1) = dom(REAL-->0) /\ A1 by RELAT_1:61; then
dom((REAL-->0)|A1) = A1 by XBOOLE_1:28; then
A84: dom(((REAL-->0)|A1)|E0`) = A1 /\ E0` by RELAT_1:61;
for x be Element of REAL st x in dom((Lf2-f)|E0`)
holds ((Lf2 - f)|E0`).x = (((REAL-->0)|A1)|E0`).x
proof
let x be Element of REAL;
assume A85: x in dom((Lf2-f)|E0`); then
A86: x in A1 & x in E0` by A83,XBOOLE_0:def 4; then
A87: Lf2.x - f.x >= 0 by A72,A1,XREAL_1:48;
((Lf2 - f)|E0`).x = (Lf2 - f).x by A85,FUNCT_1:47; then
A88: ((Lf2 - f)|E0`).x = Lf2.x - f.x by A81,A86,VALUED_1:13;
(Lf3|E0`).x = Lf3.x by A85,FUNCT_1:49; then
A89: (Lf3|E0`).x = Lf2.x - Lf1.x by A86,A1,A71,A60,A55,VALUED_1:13;
(((REAL-->0)|A1)|E0`).x = ((REAL-->0)|A1).x by A85,FUNCT_1:49; then
(((REAL-->0)|A1)|E0`).x = (REAL-->0).x by A86,FUNCT_1:49;
hence ((Lf2 - f)|E0`).x = (((REAL-->0)|A1)|E0`).x
by A74,A86,A1,A88,A87,A89,A82,XREAL_1:10;
end; then
(Lf2 - f)|E0` = ((REAL-->0)|A1)|E0` by A84,A81,RELAT_1:61,PARTFUN1:5; then
A90: Lf2|A1 a.e.= f|A1,L-Meas by A81,A82,Th40,LPSPACE1:def 10; then
(R_EAL f)|A1 is A1-measurable by A69,A1,A60,A70,Th26,MESFUNC6:def 1;
hence f is A1-measurable by MESFUN13:19,MESFUNC6:def 1;
dom(f|A1) = dom f /\ A1 by RELAT_1:61; then
A91: dom(f|A1) = A1 by A1,A2,XBOOLE_1:28;
reconsider a1=a, b1=b as R_eal by XXREAL_0:def 1;
L-Meas.A1 = diameter A by A1,MEASUR12:76; then
L-Meas.A1 = b1-a1 by A5,A6,MEASURE5:6; then
L-Meas.A1 < +infty by XXREAL_0:9,XREAL_0:def 1;
hence f|A1 is_integrable_on L-Meas
by A1,A3,A90,A60,A70,A91,Th26,Th41;
integral(f||A) = lim I2 by A29,INTEGRA1:def 17; then
integral(f||A) = Integral(L-Meas,lim F2)
by A19,Th38,MEASUR12:def 11,def 12; then
A92: integral(f||A) = Integral(L-Meas,Lf2) by A50,MESFUNC6:def 3;
Lf2 is_integrable_on L-Meas by A67,Th48;
hence integral(f||A) = Integral(L-Meas,f|A) by A1,A60,A90,A91,A92,Th44;
end;
end;
theorem
for a,b be Real, f be PartFunc of REAL,REAL st a <= b & [.a,b.] c= dom f &
f||['a,b'] is bounded & f is_integrable_on ['a,b']
holds integral(f,a,b) = Integral(L-Meas,f|[.a,b.])
proof
let a,b be Real, f be PartFunc of REAL,REAL;
assume that
A1: a <= b and
A2: [.a,b.] c= dom f and
A3: f||['a,b'] is bounded and
A4: f is_integrable_on ['a,b'];
reconsider A1 = [.a,b.] as Element of L-Field by MEASUR10:5,MEASUR12:75;
A1 = ['a,b'] by A1,INTEGRA5:def 3; then
Integral(L-Meas,f|[.a,b.]) = integral(f||['a,b']) by A2,A3,A4,Th49; then
Integral(L-Meas,f|[.a,b.]) = integral(f,['a,b']) by INTEGRA5:def 2;
hence integral(f,a,b) = Integral(L-Meas,f|[.a,b.]) by A1,INTEGRA5:def 4;
end;