:: Scaling Properties of Jordan, Borel and Lebesgue Measures under Affine
:: Maps
:: by Noboru Endou and Yasunari Shidama
::
:: Received November 5, 2026
:: Copyright (c) 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 4.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/4.0/.
environ
vocabularies RELAT_1, FUNCT_1, VALUED_0, ARYTM_1, COMPLEX1, ARYTM_3, FINSEQ_1,
ORDINAL2, SUBSET_1, JGRAPH_2, CARD_3, SETFAM_1, FUNCT_2, TARSKI, CARD_1,
NAT_1, ZFMISC_1, XBOOLE_0, NUMBERS, XXREAL_0, XXREAL_1, REAL_1, SUPINF_1,
SUPINF_2, XXREAL_2, PROB_1, MEASUR10, ORDINAL4, FINSUB_1, PROB_2,
MSSUBFAM, MEASURE5, MEASUR12, MEASURE8, SRINGS_3, MEASURE4, MEASURE7,
MEASURE3;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, SUPINF_2, FUNCT_2, FUNCT_3, ORDINAL1, CARD_3, NUMBERS, XREAL_0,
XXREAL_0, XXREAL_1, XXREAL_3, NAT_1, XXREAL_2, MEASURE8, FINSEQ_1,
FINSEQOP, FCONT_1, PROB_1, PROB_2, SUPINF_1, FINSUB_1, SRINGS_3,
VALUED_0, MEASURE1, MEASURE3, MEASURE4, MEASURE5, EXTREAL1, MEASUR10,
MEASUR12;
constructors TOPREALB, MESFUNC2, COMPLEX1, FCONT_1, MEASURE3, PROB_2,
EXTREAL1, FINSEQOP, MEASURE8, MEASUR12, SEQ_4;
registrations XBOOLE_0, FUNCT_1, XREAL_0, NAT_1, CARD_1, ORDINAL1, SUBSET_1,
RELSET_1, FUNCT_2, VALUED_0, MEASURE1, MEASURE4, MEASURE9, EXTREAL1,
MEMBERED, FINSEQ_1, RELAT_1, ROUGHS_1, NUMBERS, XXREAL_1, XXREAL_2,
XXREAL_3, ABSVALUE, MEASUR12;
requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
equalities CARD_3, SRINGS_3, MEASUR10, FINSEQ_1, RCOMP_1, MEASUR12, SUPINF_2,
XXREAL_3;
expansions TARSKI, XBOOLE_0, VALUED_0, MEASURE1, FUNCT_2, MESFUN12, MEASURE5,
PROB_2, FINSUB_1, MEMBERED;
theorems TARSKI, FUNCT_1, PARTFUN1, FUNCT_2, XBOOLE_1, XXREAL_0, XREAL_1,
XREAL_0, FINSEQ_1, COMPLEX1, XXREAL_1, RELAT_1, XCMPLX_1, ORDINAL1,
ZFMISC_1, FINSEQ_3, XXREAL_2, MEASURE1, VALUED_0, SUPINF_2, MESFUNC3,
MEASUR10, MEASUR11, NAT_1, FUNCT_3, PROB_1, ABSVALUE, FCONT_1, MEASUR12,
MEASUR14, MEASURE4, MEASURE8, MEASURE9, SRINGS_3, MEASURE3, MEASURE5,
EXTREAL1, XXREAL_3, NUMBERS, MESFUN14, XCMPLX_0, ROUGHS_1, MEASURE7;
schemes NAT_1;
begin :: Affine Maps on Intervals and Jordan Measure
Lm1:
for b be Real, X be Subset of REAL holds AffineMap(0,b).:X c= {b}
proof
let b be Real, X be Subset of REAL;
now let y be Real;
assume y in (AffineMap(0,b).:X); then
consider x be Element of REAL such that
A1: x in X & y = AffineMap(0,b).x by FUNCT_2:65;
y = 0 * x + b by A1,FCONT_1:def 4;
hence y in {b} by TARSKI:def 1;
end;
hence (AffineMap(0,b).:X) c= {b};
end;
theorem Th1:
for a,b be Real, I be Interval holds AffineMap(a,b).:I is Interval
proof
let a,b be Real, I be Interval;
set f = AffineMap(a,b);
per cases;
suppose a= 0; then
f.:I = {} or f.:I = {b} by Lm1,ZFMISC_1:33; then
f.:I = {} or f.:I = [.b,b.] by XXREAL_1:17;
hence (f.:I) is Interval;
end;
suppose A1: 0 < a or a < 0;
for r,s being ExtReal st r in (f.:I) & s in (f.:I) holds [.r,s.] c= (f.:I)
proof
let r,s be ExtReal;
assume A2: r in (f.:I) & s in (f.:I); then
consider x be Element of REAL such that
A3: x in I & r = f.x by FUNCT_2:65;
consider y be Element of REAL such that
A4: y in I & s = f.y by A2,FUNCT_2:65;
A5: [.x,y.] c= I & [.y,x.] c= I by A3,A4,XXREAL_2:def 12;
for z be object st z in [.r,s.] holds z in (f.:I)
proof
let z be object;
assume
A6: z in [.r,s.]; then
reconsider u = z as ExtReal;
r = a*x + b & s = a*y + b by A3,A4,FCONT_1:def 4; then
a*x + b<=u & u <= a*y + b by A6,XXREAL_1:1; then
a*x + b-b <= u-b & u-b <= a*y + b-b by XXREAL_3:37; then
( (a*x)/a <= (u-b)/a & (u-b)/a <= (a*y)/a )
or ( (a*y)/a <= (u-b)/a & (u-b)/a <= (a*x)/a )
by A1,XXREAL_3:103,79; then
( x <= (u-b)/a & (u-b)/a <= y )
or ( y <= (u-b)/a & (u-b)/a <= x ) by A1,XXREAL_3:88; then
A7: (u-b)/a in I by A5,XXREAL_1:1;
dom f = REAL by FUNCT_2:def 1; then
A8: f. ((u-b)/a) in f.:I by A7,FUNCT_1:def 6;
reconsider uba = (u-b)/a as Real by A7;
a*uba+b in f.:I by A8,FCONT_1:def 4; then
a*(a")*(u-b) + b in f.:I by XXREAL_3:66; then
1*(u-b) + b in f.:I by A1,XCMPLX_0:def 7; then
u-b + b in f.:I by XXREAL_3:81;
hence thesis by XXREAL_3:22;
end;
hence [.r,s.] c= (f.:I);
end;
hence thesis by XXREAL_2:def 12;
end;
end;
Lm2:
for a,b,s,t be Real st 0 < a holds AffineMap(a,b).:[.s,t.] = [.a*s+b,a*t+b.]
proof
let a,b,s,t be Real;
assume
A1: 0 < a;
A2: now let z be Real;
assume z in AffineMap(a,b).:[.s,t.]; then
consider x be Element of REAL such that
A3: x in [.s,t.] & z = AffineMap(a,b).x by FUNCT_2:65;
s <= x <= t by A3,XXREAL_1:1; then
a*s <= a*x <= a*t by A1,XREAL_1:64; then
a*s+b <= a*x+b <= a*t+b by XREAL_1:6; then
a*s+b <= z <= a*t+b by A3,FCONT_1:def 4;
hence z in [.a*s+b,a*t+b.];
end;
now let x be Real;
assume x in [.a*s+b,a*t+b.]; then
a*s+b <= x <= a*t+b by XXREAL_1:1; then
a*s <= x-b <= a*t by XREAL_1:19,20; then
s <= (x-b)/a & (x-b)/a <= t by A1,XREAL_1:77,79; then
A4: (x-b)/a in [.s,t.];
dom AffineMap(a,b) = REAL by FUNCT_2:def 1; then
A5: (x-b)/a in dom AffineMap(a,b) by XREAL_0:def 1;
AffineMap(a,b).((x-b)/a) = a*((x-b)/a) + b by FCONT_1:def 4; then
AffineMap(a,b).((x-b)/a) = (x-b) + b by A1,XCMPLX_1:87;
hence x in AffineMap(a,b).:[.s,t.] by A4,A5,FUNCT_1:def 6;
end;
hence thesis by A2;
end;
Lm3:
for a,b,s,t be Real st a < 0 holds AffineMap(a,b).:[.s,t.] = [.a*t+b,a*s+b.]
proof
let a,b,s,t be Real;
assume
A1: a < 0;
A2: now let z be Real;
assume z in AffineMap(a,b).:[.s,t.]; then
consider x be Element of REAL such that
A3: x in [.s,t.] & z = AffineMap(a,b).x by FUNCT_2:65;
s <= x <= t by A3,XXREAL_1:1; then
a*t <= a*x <= a*s by A1,XREAL_1:65; then
a*t+b <= a*x+b <= a*s+b by XREAL_1:6; then
a*t+b <= z <= a*s+b by A3,FCONT_1:def 4;
hence z in [.a*t+b,a*s+b.];
end;
now let x be Real;
assume x in [.a*t+b,a*s+b.]; then
a*t+b <= x & x <= a*s+b by XXREAL_1:1; then
a*t <= x-b & x-b <= a*s by XREAL_1:19,20; then
s <= (x-b)/a & (x-b)/a <= t by A1,XREAL_1:78,80; then
A4: (x-b)/a in [.s,t.];
dom AffineMap(a,b) = REAL by FUNCT_2:def 1; then
A5: (x-b)/a in dom AffineMap(a,b) by XREAL_0:def 1;
AffineMap(a,b).((x-b)/a) = a*((x-b)/a) + b by FCONT_1:def 4; then
AffineMap(a,b).((x-b)/a) = (x-b) + b by A1,XCMPLX_1:87;
hence x in AffineMap(a,b).:[.s,t.] by A4,A5,FUNCT_1:def 6;
end;
hence thesis by A2;
end;
Lm4:
for a,b,s,t be Real st a = 0 & s <= t holds AffineMap(a,b).:[.s,t.] = [.b,b.]
proof
let a,b,s,t be Real;
assume that
A1: a = 0 and
A2:s <= t;
A3: now let z be Real;
assume z in AffineMap(a,b).:[.s,t.]; then
consider x be Element of REAL such that
A4: x in [.s,t.] & z = AffineMap(a,b).x by FUNCT_2:65;
z = a*x + b by A4,FCONT_1:def 4;
hence z in [.b,b.] by A1;
end;
now let x be Real;
assume x in [.b,b.]; then
x in {b} by XXREAL_1:17; then
x = a*s + b by A1,TARSKI:def 1; then
A5: x = AffineMap(a,b).s by FCONT_1:def 4;
A6: s in [.s,t.] by A2;
dom AffineMap(a,b) = REAL by FUNCT_2:def 1; then
s in dom AffineMap(a,b) by XREAL_0:def 1;
hence x in AffineMap(a,b).:[.s,t.] by A5,A6,FUNCT_1:def 6;
end;
hence thesis by A3;
end;
Lm5:
for I be Interval, a,b be Real st 0 < a & I is closed_interval
holds B-Meas.(AffineMap(a,b).:I) = a*B-Meas.I
proof
let I be Interval, a,b be Real;
assume that
A1: 0 < a and
A2: I is closed_interval;
per cases;
suppose
A3: I = {}; then
AffineMap(a,b).:I = {}; then
B-Meas.I =0 & B-Meas.(AffineMap(a,b).:I) = 0 by A3,VALUED_0:def 19;
hence B-Meas.(AffineMap(a,b).:I) = a*B-Meas.I;
end;
suppose I <> {}; then
consider s,t being Real such that
A4: s <= t & I = [.s,t.] by A2,MEASURE5:14;
a*s <= a*t by A1,A4,XREAL_1:64; then
A5: a*s + b <= a*t + b by XREAL_1:6;
AffineMap(a,b).:[.s,t.] = [.a*s+b,a*t+b.] by A1,Lm2; then
B-Meas.(AffineMap(a,b).:I) = (a*t+b) - (a*s+b) by A4,A5,MESFUN14:5; then
B-Meas.(AffineMap(a,b).:I) = a * (t-s);
hence B-Meas.(AffineMap(a,b).:I) = a * (B-Meas.I) by A4,MESFUN14:5;
end;
end;
Lm6:
for I be Interval, a,b be Real st a < 0 & I is closed_interval
holds B-Meas.(AffineMap(a,b).:I) = (-a)*B-Meas.I
proof
let I be Interval, a,b be Real;
assume that
A1: a < 0 and
A2: I is closed_interval;
per cases;
suppose
A3: I = {}; then
AffineMap(a,b).:I = {}; then
B-Meas.I =0 & B-Meas.(AffineMap(a,b).:I) = 0 by A3,VALUED_0:def 19;
hence B-Meas.(AffineMap(a,b).:I) = (-a) *B-Meas.I;
end;
suppose I <> {}; then
consider s,t being Real such that
A4: s <= t & I = [.s,t.] by A2,MEASURE5:14;
a*t <= a*s by A1,A4,XREAL_1:65; then
A5: a*t+b <= a*s+b by XREAL_1:6;
AffineMap(a,b).:[.s,t.] =[.a*t+b,a*s+b.] by A1,Lm3; then
B-Meas.(AffineMap(a,b).:I) =(a*s+b)-(a*t+b ) by A4,A5,MESFUN14:5; then
B-Meas.(AffineMap(a,b).:I) = (-a)*(t-s);
hence B-Meas.(AffineMap(a,b).:I) = (-a) * (B-Meas. I) by A4,MESFUN14:5;
end;
end;
Lm7:
for I be Interval, a,b be Real st I is closed_interval
holds B-Meas.(AffineMap(a,b).:I) = |.a.| * B-Meas.I
proof
let I be Interval, a,b be Real;
assume
A1: I is closed_interval;
per cases;
suppose
A2: I = {}; then
AffineMap(a,b).:I = {}; then
B-Meas.I =0 & B-Meas.(AffineMap(a,b).:I) = 0 by A2,VALUED_0:def 19;
hence B-Meas.(AffineMap(a,b).:I) = |.a.| *B-Meas.I;
end;
suppose I <> {}; then
consider s,t being Real such that
A3: s <= t & I = [.s,t.] by A1,MEASURE5:14;
per cases;
suppose A4: a > 0; then
B-Meas.(AffineMap(a,b).:I) = a *B-Meas. I by Lm5,A1;
hence B-Meas.(AffineMap(a,b).:I) =|.a.| *B-Meas.I by A4,ABSVALUE:def 1;
end;
suppose A5: a = 0; then
AffineMap(a,b).:[.s,t.] = [.b,b.] by A3,Lm4; then
B-Meas.(AffineMap(a,b).:I) = b-b by A3,MESFUN14:5;
hence B-Meas.(AffineMap(a,b).:I) = |.a.| *B-Meas.I by A5;
end;
suppose A6: a < 0; then
B-Meas.(AffineMap(a,b).:I) = (-a) *B-Meas.I by Lm6,A1;
hence B-Meas.(AffineMap(a,b).:I) =|.a.| *B-Meas. I by A6,ABSVALUE:def 1;
end;
end;
end;
Lm8:
for a,b be Real, s,t be R_eal st 0 < a
holds AffineMap(a,b).:].s,t.[ = ].a*s+b,a*t+b.[
proof
let a,b be Real, s,t be R_eal;
assume
A1: 0 < a;
A2: a in REAL & b in REAL by XREAL_0:def 1;
A3: now let z be Real;
assume z in AffineMap(a,b).:].s,t.[; then
consider x be Element of REAL such that
A4: x in ].s,t.[ & z = AffineMap(a,b).x by FUNCT_2:65;
s < x & x < t by A4,XXREAL_1:4; then
a*s < a*x & a*x < a*t by A1,XXREAL_3:72; then
a*s+b < a*x+b & a*x+b < a*t+b by A2,XXREAL_3:43; then
a*s+b < z & z < a*t+b by A4,FCONT_1:def 4;
hence z in ].a*s+b,a*t+b.[;
end;
now let x be Real;
assume x in ].a*s+b,a*t+b.[; then
a*s+b < x < a*t+b by XXREAL_1:4; then
a*s+b-b < x-b < a*t+b-b by A2,XXREAL_3:43; then
a*s < x-b < a*t by XXREAL_3:24; then
(a*s)/a < (x-b)/a < (a*t)/a by A1,XXREAL_3:80; then
s < (x-b)/a < t by A1,XXREAL_3:88; then
A5: (x-b)/a in ].s,t.[;
A6: dom AffineMap(a,b) = REAL by FUNCT_2:def 1;
AffineMap(a,b).((x-b)/a) = a*((x-b)/a) + b by FCONT_1:def 4; then
AffineMap(a,b).((x-b)/a) = (x-b) + b by A1,XCMPLX_1:87;
hence x in AffineMap(a,b).:].s,t.[
by A5,A6,FUNCT_1:def 6;
end;
hence thesis by A3;
end;
Lm9:
for I be Interval, a,b be Real st 0 < a & I is open_interval
holds B-Meas.(AffineMap(a,b).:I) = a*B-Meas.I
proof
let I be Interval, a,b be Real;
assume that
A1: 0 < a and
A2: I is open_interval;
A3: a in REAL & b in REAL by XREAL_0:def 1;
per cases;
suppose
A4: I = {}; then
AffineMap(a,b).:I = {}; then
B-Meas.I =0 & B-Meas.(AffineMap(a,b).:I) = 0 by A4,VALUED_0:def 19;
hence B-Meas.(AffineMap(a,b).:I) = a * B-Meas.I;
end;
suppose A5: I <> {};
consider s,t being R_eal such that
A6: I = ].s,t.[ by A2;
s < t by XXREAL_1:28,A6,A5; then
A7: a*s < a*t by A1,XXREAL_3:72;
B-Meas.I = diameter I by MEASUR12:71; then
B-Meas.I = t-s by A5,A6,XXREAL_1:28,MEASURE5:5; then
A8: a*(B-Meas.I) = a*t-a*s by XXREAL_3:100;
A9: a*s+b is R_eal & a*t+b is R_eal by XXREAL_0:def 1;
AffineMap(a,b).:].s,t.[ = ].a*s+b,a*t+b.[ by A1,Lm8; then
B-Meas.(AffineMap(a,b).:I) = diameter ].a*s+b,a*t+b.[
by A6,MEASUR12:71; then
B-Meas.(AffineMap(a,b).:I) = (a*t+b) - (a*s+b)
by A3,A7,A9,XXREAL_3:43,MEASURE5:5;
hence B-Meas.(AffineMap(a,b).:I) = a*(B-Meas.I) by A8,XXREAL_3:33;
end;
end;
Lm10:
for a,b be Real, s,t be R_eal st a < 0
holds AffineMap(a,b).:].s,t.[ = ].a*t+b,a*s+b.[
proof
let a,b be Real, s,t be R_eal;
assume
A1: a < 0;
A2: a in REAL & b in REAL by XREAL_0:def 1;
A3: now let z be Real;
assume z in AffineMap(a,b).:].s,t.[; then
consider x be Element of REAL such that
A4: x in ].s,t.[ & z = AffineMap(a,b).x by FUNCT_2:65;
s < x & x < t by A4,XXREAL_1:4; then
a*t < a*x & a*x < a*s by A1,XXREAL_3:102; then
a*t+b < a*x+b & a*x+b < a*s+b by A2,XXREAL_3:43; then
a*t+b < z & z < a*s+b by A4,FCONT_1:def 4;
hence z in ].a*t+b,a*s+b.[;
end;
now let x be Real;
assume x in ].a*t+b,a*s+b.[; then
a*t+b < x & x < a*s+b by XXREAL_1:4; then
a*t+b-b < x-b & x-b < a*s+b-b by A2,XXREAL_3:43; then
a*t < x-b & x-b < a*s by XXREAL_3:24; then
(a*s)/a < (x-b)/a & (x-b)/a < (a*t)/a by A1,XXREAL_3:104; then
s < (x-b)/a & (x-b)/a < t by A1,XXREAL_3:88; then
A5: (x-b)/a in ].s,t.[;
A6: dom AffineMap(a,b) = REAL by FUNCT_2:def 1;
AffineMap(a,b).((x-b)/a) = a*((x-b)/a) + b by FCONT_1:def 4; then
AffineMap(a,b).((x-b)/a) = (x-b) + b by A1,XCMPLX_1:87;
hence x in AffineMap(a,b).:].s,t.[ by A5,A6,FUNCT_1:def 6;
end;
hence thesis by A3;
end;
Lm11:
for I be Interval, a,b be Real st a < 0 & I is open_interval
holds B-Meas.(AffineMap(a,b).:I) = (-a)*B-Meas.I
proof
let I be Interval, a,b be Real;
assume that
A1: a < 0 and
A2: I is open_interval;
A3: a in REAL & b in REAL by XREAL_0:def 1;
per cases;
suppose
A4: I = {}; then
AffineMap(a,b).:I = {}; then
B-Meas.I =0 & B-Meas.(AffineMap(a,b).:I) = 0 by A4,VALUED_0:def 19;
hence B-Meas.(AffineMap(a,b).:I) = (-a) * B-Meas.I;
end;
suppose A5: I <> {};
consider s,t being R_eal such that
A6: I = ].s,t.[ by A2;
s < t by XXREAL_1:28,A6,A5; then
A7: a*t < a*s by A1,XXREAL_3:102;
B-Meas.I = diameter I by MEASUR12:71; then
A8: (-a)*(B-Meas.I) = a*(-1)*(t-s) by A5,A6,XXREAL_1:28,MEASURE5:5
.= a*((-1)*(t-s)) by XXREAL_3:66
.= a*(-(t-s)) by XXREAL_3:91
.= a*(s-t) by XXREAL_3:26;
A9: a*s+b is R_eal & a*t+b is R_eal by XXREAL_0:def 1;
AffineMap(a,b).:].s,t.[ = ].a*t+b,a*s+b.[ by A1,Lm10; then
B-Meas.(AffineMap(a,b).:I) = diameter ].a*t+b,a*s+b.[
by A6,MEASUR12:71; then
B-Meas.(AffineMap(a,b).:I) = (a*s+b) - (a*t+b)
by A3,A7,A9,XXREAL_3:43,MEASURE5:5; then
B-Meas.(AffineMap(a,b).:I) = a*s - a*t by XXREAL_3:33;
hence B-Meas.(AffineMap(a,b).:I) = (-a)*(B-Meas.I) by A8,XXREAL_3:100;
end;
end;
Lm12:
for I be Interval, a,b be Real st I is open_interval
holds B-Meas.(AffineMap(a,b).:I) = |.a.|*B-Meas.I
proof
let I be Interval, a,b be Real;
assume
A1: I is open_interval;
per cases;
suppose A2: a > 0; then
B-Meas.(AffineMap(a,b).:I) = a *B-Meas. I by A1,Lm9;
hence B-Meas.(AffineMap(a,b).:I) = |.a.|*B-Meas.I by A2,ABSVALUE:def 1;
end;
suppose A3: a = 0; then
AffineMap(a,b).:I c= {b} by Lm1; then
A4: AffineMap(a,b).:I c= [.b,b.] by XXREAL_1:17;
[.b,b.] = {b} by XXREAL_1:17; then
A5: [.b,b.] is Interval by XREAL_0:def 1,ZFMISC_1:31;
AffineMap(a,b).:I is Interval by Th1; then
A6: AffineMap(a,b).:I is Element of Borel_Sets
& [.b,b.] is Element of Borel_Sets by A5,MEASUR12:72; then
A7: B-Meas.(AffineMap(a,b).:I) <= B-Meas.([.b,b.]) by A4,MEASURE1:8;
B-Meas. [.b,b.] = b-b by MESFUN14:5; then
B-Meas.(AffineMap(a,b).:I) = 0 by A7,A6,MEASURE1:def 2;
hence B-Meas.(AffineMap(a,b).:I) = |.a.|*B-Meas.I by A3;
end;
suppose A8:a < 0; then
B-Meas.(AffineMap(a,b).:I) = (-a)*B-Meas.I by Lm11,A1;
hence B-Meas.(AffineMap(a,b).:I) =|.a.| *B-Meas. I by A8,ABSVALUE:def 1;
end;
end;
Lm13:
for a,b be Real, s be R_eal, t be Real st 0 < a
holds AffineMap(a,b).:].s,t.] = ].a*s+b,a*t+b.]
proof
let a,b be Real, s be R_eal, t be Real;
assume
A1: 0 < a;
A2: a in REAL & b in REAL by XREAL_0:def 1;
A3: now let z be Real;
assume z in AffineMap(a,b).:].s,t.]; then
consider x be Element of REAL such that
A4: x in ].s,t.] & z = AffineMap(a,b).x by FUNCT_2:65;
s < x <= t by A4,XXREAL_1:2; then
a*s < a*x <= a*t by A1,XXREAL_3:72,XREAL_1:64; then
a*s+b < a*x+b <= a*t+b by A2,XXREAL_3:43,XREAL_1:6; then
a*s+b < z <= a*t+b by A4,FCONT_1:def 4;
hence z in ].a*s+b,a*t+b.];
end;
now let x be Real;
assume x in ].a*s+b,a*t+b.]; then
a*s+b < x <= a*t+b by XXREAL_1:2; then
a*s+b-b < x-b <= a*t+b-b by A2,XXREAL_3:43,XREAL_1:9; then
a*s < x-b <= a*t by XXREAL_3:24; then
(a*s)/a < (x-b)/a <= (a*t)/a by A1,XXREAL_3:80,XREAL_1:72; then
s < (x-b)/a <= t by A1,XXREAL_3:88; then
A5: (x-b)/a in ].s,t.];
dom AffineMap(a,b) = REAL by FUNCT_2:def 1; then
A6: (x-b)/a in dom AffineMap(a,b) by XREAL_0:def 1;
AffineMap(a,b).((x-b)/a) = a*((x-b)/a) + b by FCONT_1:def 4; then
AffineMap(a,b).((x-b)/a) = (x-b) + b by A1,XCMPLX_1:87;
hence x in AffineMap(a,b).: ].s,t.] by A5,A6,FUNCT_1:def 6;
end;
hence thesis by A3;
end;
Lm14:
for I be Interval, a,b be Real
st 0 < a & I is left_open_interval
holds B-Meas.(AffineMap(a,b).:I) = a * B-Meas.I
proof
let I be Interval, a,b be Real;
assume that
A1: 0 < a and
A2: I is left_open_interval;
A3: a in REAL & b in REAL by XREAL_0:def 1;
per cases;
suppose
A4: I = {}; then
AffineMap(a,b).:I = {}; then
B-Meas.I =0 & B-Meas.(AffineMap(a,b).:I) = 0 by A4,VALUED_0:def 19;
hence B-Meas.(AffineMap(a,b).:I) = a *B-Meas.I;
end;
suppose A5: I <> {};
consider s being R_eal,t be Real such that
A6: I = ].s,t.] by A2;
A7: t is R_eal & a*s+b is R_eal & a*t+b is R_eal by XXREAL_0:def 1;
s < t by XXREAL_1:26,A6,A5; then
A8: a*s < a*t by A1,XXREAL_3:72;
B-Meas.I = diameter I by MEASUR12:71; then
A9: B-Meas.I =t-s by A5,A6,XXREAL_1:26,MEASURE5:8,A7;
AffineMap(a,b).:].s,t.] = ].a*s+b,a*t+b.] by A1,Lm13; then
B-Meas.(AffineMap(a,b).:I) = diameter ].a*s+b,a*t+b.]
by A6,MEASUR12:71; then
B-Meas.(AffineMap(a,b).:I) =(a*t+b) - (a*s+b)
by A7,A8,A3,XXREAL_3:43,MEASURE5:8; then
B-Meas.(AffineMap(a,b).:I) = a*t -a*s by XXREAL_3:33;
hence B-Meas.(AffineMap(a,b).:I) = a * (B-Meas. I) by A9,XXREAL_3:100;
end;
end;
Lm15:
for a,b be Real, s being R_eal,t be Real st a < 0
holds AffineMap(a,b).:].s,t.] = [.a*t+b,a*s+b.[
proof
let a,b be Real, s be R_eal, t be Real;
assume
A1: a < 0;
A2: a in REAL & b in REAL by XREAL_0:def 1;
A3: now let z be Real;
assume z in AffineMap(a,b).:].s,t.]; then
consider x be Element of REAL such that
A4: x in ].s,t.] & z = AffineMap(a,b).x by FUNCT_2:65;
s < x <= t by A4,XXREAL_1:2; then
a*t <= a*x < a*s by A1,XXREAL_3:102,XREAL_1:65; then
a*t+b <= a*x+b < a*s+b by A2,XXREAL_3:43,XREAL_1:6; then
a*t+b <= z < a*s+b by A4,FCONT_1:def 4;
hence z in [.a*t+b,a*s+b.[;
end;
now let x be Real;
assume x in [.a*t+b,a*s+b.[; then
a*t+b <= x < a*s+b by XXREAL_1:3; then
a*t+b-b <= x-b < a*s+b-b by A2,XXREAL_3:43,XREAL_1:9; then
a*t <= x-b < a*s by XXREAL_3:24; then
(a*s)/a < (x-b)/a <= (a*t)/a by A1,XXREAL_3:104,XREAL_1:73; then
s < (x-b)/a <= t by A1,XXREAL_3:88; then
A5: (x-b)/a in ].s,t.];
dom AffineMap(a,b) = REAL by FUNCT_2:def 1; then
A6: (x-b)/a in dom AffineMap(a,b) by XREAL_0:def 1;
AffineMap(a,b).((x-b)/a) = a*((x-b)/a) + b by FCONT_1:def 4; then
AffineMap(a,b).((x-b)/a) = (x-b) + b by A1,XCMPLX_1:87;
hence x in AffineMap(a,b).: ].s,t.] by A5,A6,FUNCT_1:def 6;
end;
hence thesis by A3;
end;
Lm16:
for I be Interval, a,b be Real st a < 0 & I is left_open_interval
holds B-Meas.(AffineMap(a,b).:I) = (-a)*B-Meas.I
proof
let I be Interval, a,b be Real;
assume that
A1: a < 0 and
A2: I is left_open_interval;
A3: a in REAL & b in REAL by XREAL_0:def 1;
per cases;
suppose
A4: I = {}; then
AffineMap(a,b).:I = {}; then
B-Meas.I =0 & B-Meas.(AffineMap(a,b).:I) = 0 by A4,VALUED_0:def 19;
hence B-Meas.(AffineMap(a,b).:I) = (-a) *B-Meas.I;
end;
suppose A5: I <> {};
consider s being R_eal,t be Real such that
A6: I = ].s,t.] by A2;
A7: t is R_eal & a*s+b is R_eal & a*t+b is R_eal by XXREAL_0:def 1;
A8: B-Meas.I = diameter I by MEASUR12:71;
s < t by A5,A6,XXREAL_1:26; then
A9: a*t < a*s by A1,XXREAL_3:102;
AffineMap(a,b).:].s,t.] = [.a*t+b,a*s+b.[ by A1,Lm15; then
B-Meas.(AffineMap(a,b).:I) = diameter [.a*t+b,a*s+b.[
by A6,MEASUR12:71; then
B-Meas.(AffineMap(a,b).:I) =(a*s+b) - (a*t+b)
by A7,A9,A3,XXREAL_3:43,MEASURE5:7
.= a*s -a*t by XXREAL_3:33
.= a * (s-t) by XXREAL_3:100
.= a *( -(t-s)) by XXREAL_3:26
.= a*((-1)*(t-s)) by XXREAL_3:91
.= (-1)*a*(t-s) by XXREAL_3:66;
hence B-Meas.(AffineMap(a,b).:I) = (-a)*(B-Meas. I)
by A8,A6,A7,A5,XXREAL_1:26,MEASURE5:8;
end;
end;
Lm17:
for I be Interval, a,b be Real st I is left_open_interval
holds B-Meas.(AffineMap(a,b).:I) = |.a.|*B-Meas.I
proof
let I be Interval, a,b be Real;
assume
A1: I is left_open_interval;
per cases;
suppose A2: a > 0; then
B-Meas.(AffineMap(a,b).:I) = a *B-Meas. I by Lm14,A1;
hence B-Meas.(AffineMap(a,b).:I) =|.a.| *B-Meas.I by A2,ABSVALUE:def 1;
end;
suppose A3: a = 0; then
AffineMap(a,b).:I c= {b} by Lm1; then
A4: AffineMap(a,b).:I c= [.b,b.] by XXREAL_1:17;
[.b,b.] = {b} by XXREAL_1:17; then
A5: [.b,b.] is Interval by XREAL_0:def 1,ZFMISC_1:31;
AffineMap(a,b).:I is Interval by Th1; then
A6: AffineMap(a,b).:I is Element of Borel_Sets
& [.b,b.] is Element of Borel_Sets by A5,MEASUR12:72; then
A7: B-Meas.(AffineMap(a,b).:I) <= B-Meas.([.b,b.]) by A4,MEASURE1:8;
B-Meas. [.b,b.] = b-b by MESFUN14:5; then
B-Meas.(AffineMap(a,b).:I) = 0 by A7,A6,MEASURE1:def 2;
hence B-Meas.(AffineMap(a,b).:I) = |.a.|*B-Meas.I by A3;
end;
suppose A8:a < 0; then
B-Meas.(AffineMap(a,b).:I) = (-a)*B-Meas.I by Lm16,A1;
hence B-Meas.(AffineMap(a,b).:I) =|.a.| *B-Meas.I by A8,ABSVALUE:def 1;
end;
end;
Lm18:
for a,b,s be Real, t being R_eal st 0 < a
holds AffineMap(a,b).:[.s,t.[ = [.a*s+b,a*t+b.[
proof
let a,b,s be Real, t be R_eal;
assume
A1: 0 < a;
A2: a in REAL & b in REAL by XREAL_0:def 1;
A3: now let z be Real;
assume z in AffineMap(a,b).:[.s,t.[; then
consider x be Element of REAL such that
A4: x in [.s,t.[ & z = AffineMap(a,b).x by FUNCT_2:65;
s <= x < t by A4,XXREAL_1:3; then
a*s <= a*x < a*t by A1,XXREAL_3:72,XREAL_1:64; then
a*s+b <= a*x+b < a*t+b by A2,XXREAL_3:43,XREAL_1:6; then
a*s+b <= z < a*t+b by A4,FCONT_1:def 4;
hence z in [.a*s+b,a*t+b.[;
end;
now let x be Real;
assume x in [.a*s+b,a*t+b.[; then
a*s+b <= x < a*t+b by XXREAL_1:3; then
a*s+b-b <= x-b < a*t+b-b by A2,XXREAL_3:43,XREAL_1:9; then
a*s <= x-b < a*t by XXREAL_3:24; then
(a*s)/a <= (x-b)/a < (a*t)/a by A1,XXREAL_3:80,XREAL_1:72; then
s <= (x-b)/a < t by A1,XXREAL_3:88; then
A5: (x-b)/a in [.s,t.[;
dom AffineMap(a,b) = REAL by FUNCT_2:def 1; then
A6: (x-b)/a in dom AffineMap(a,b) by XREAL_0:def 1;
AffineMap(a,b).((x-b)/a) = a*((x-b)/a) + b by FCONT_1:def 4; then
AffineMap(a,b).((x-b)/a) = (x-b) + b by A1,XCMPLX_1:87;
hence x in AffineMap(a,b).: [.s,t.[ by A5,A6,FUNCT_1:def 6;
end;
hence thesis by A3;
end;
Lm19:
for I be Interval, a,b be Real st 0 < a & I is right_open_interval
holds B-Meas.(AffineMap(a,b).:I) = a*B-Meas.I
proof
let I be Interval, a,b be Real;
assume that
A1: 0 < a and
A2: I is right_open_interval;
A3: a in REAL & b in REAL by XREAL_0:def 1;
per cases;
suppose
A4: I = {}; then
AffineMap(a,b).:I = {}; then
B-Meas.I =0 & B-Meas.(AffineMap(a,b).:I) = 0 by A4,VALUED_0:def 19;
hence B-Meas.(AffineMap(a,b).:I) = a *B-Meas.I;
end;
suppose A5: I <> {};
consider t being R_eal,s be Real such that
A6: I = [.s,t.[ by A2;
A7: t is R_eal & s is R_eal & a*s+b is R_eal & a*t+b is R_eal
by XXREAL_0:def 1;
s < t by XXREAL_1:27,A6,A5; then
A8: a*s < a*t by A1,XXREAL_3:72;
B-Meas.I = diameter I by MEASUR12:71; then
A9: B-Meas.I = t-s by A5,A6,XXREAL_1:27,MEASURE5:7,A7;
AffineMap(a,b).:[.s,t.[ = [.a*s+b,a*t+b.[ by A1,Lm18; then
B-Meas.(AffineMap(a,b).:I) = diameter [.a*s+b,a*t+b.[
by A6,MEASUR12:71; then
B-Meas.(AffineMap(a,b).:I) =(a*t+b) - (a*s+b )
by A3,A7,A8,XXREAL_3:43,MEASURE5:7; then
B-Meas.(AffineMap(a,b).:I) = a*t -a*s by XXREAL_3:33;
hence B-Meas.(AffineMap(a,b).:I) = a*(B-Meas. I) by A9,XXREAL_3:100;
end;
end;
Lm20:
for a,b,s be Real, t being R_eal st a < 0
holds AffineMap(a,b).:[.s,t.[ = ].a*t+b,a*s+b.]
proof
let a,b,s be Real, t be R_eal;
assume
A1: a < 0;
A2: a in REAL & b in REAL by XREAL_0:def 1;
A3: now let z be Real;
assume z in AffineMap(a,b).:[.s,t.[; then
consider x be Element of REAL such that
A4: x in [.s,t.[ & z = AffineMap(a,b).x by FUNCT_2:65;
s <= x & x < t by A4,XXREAL_1:3; then
a*t < a*x <= a*s by A1,XXREAL_3:102,XREAL_1:65; then
a*t+b < a*x+b <= a*s+b by A2,XXREAL_3:43,XREAL_1:6; then
a*t+b < z <= a*s+b by A4,FCONT_1:def 4;
hence z in ].a*t+b,a*s+b.];
end;
now let x be Real;
assume x in ].a*t+b,a*s+b.]; then
a*t+b < x <= a*s+b by XXREAL_1:2; then
a*t+b-b < x-b <= a*s+b-b by A2,XXREAL_3:43,XREAL_1:9; then
a*t < x-b <= a*s by XXREAL_3:24; then
(a*s)/a <= (x-b)/a < (a*t)/a by A1,XXREAL_3:102,XREAL_1:65; then
s <= (x-b)/a < t by A1,XXREAL_3:88; then
A5: (x-b)/a in [.s,t.[;
dom AffineMap(a,b) = REAL by FUNCT_2:def 1; then
A6: (x-b)/a in dom AffineMap(a,b) by XREAL_0:def 1;
AffineMap(a,b).((x-b)/a) = a*((x-b)/a) + b by FCONT_1:def 4; then
AffineMap(a,b).((x-b)/a) = (x-b) + b by A1,XCMPLX_1:87;
hence x in AffineMap(a,b).: [.s,t.[ by A5,A6,FUNCT_1:def 6;
end;
hence thesis by A3;
end;
Lm21:
for I be Interval, a,b be Real st a < 0 & I is right_open_interval
holds B-Meas.(AffineMap(a,b).:I) = (-a)*B-Meas.I
proof
let I be Interval, a,b be Real;
assume that
A1: a < 0 and
A2: I is right_open_interval;
A3: a in REAL & b in REAL by XREAL_0:def 1;
per cases;
suppose
A4: I = {}; then
AffineMap(a,b).:I = {}; then
B-Meas.I =0 & B-Meas.(AffineMap(a,b).:I) = 0 by A4,VALUED_0:def 19;
hence B-Meas.(AffineMap(a,b).:I) = (-a)*B-Meas.I;
end;
suppose A5: I <> {};
consider t being R_eal,s be Real such that
A6: I = [.s,t.[ by A2;
A7: t is R_eal & s is R_eal &
a*s+b is R_eal & a*t+b is R_eal by XXREAL_0:def 1;
A8: B-Meas.I = diameter I by MEASUR12:71;
s < t by XXREAL_1:27,A6,A5; then
A9: a*t < a*s by A1,XXREAL_3:102;
AffineMap(a,b).:[.s,t.[ = ].a*t+b,a*s+b.] by A1,Lm20; then
B-Meas.(AffineMap(a,b).:I) = diameter ].a*t+b,a*s+b.]
by A6,MEASUR12:71; then
B-Meas.(AffineMap(a,b).:I) = (a*s+b) - (a*t+b)
by A3,A7,A9,XXREAL_3:43,MEASURE5:8; then
B-Meas.(AffineMap(a,b).:I) = a*s -a*t by XXREAL_3:33
.= a * (s-t) by XXREAL_3:100
.= a *( -(t-s)) by XXREAL_3:26
.= a*((-1)*(t-s)) by XXREAL_3:91
.= (-1)*a*(t-s) by XXREAL_3:66;
hence B-Meas.(AffineMap(a,b).:I) = (-a)*(B-Meas.I)
by A8,A5,A6,A7,XXREAL_1:27,MEASURE5:7;
end;
end;
Lm22:
for I be Interval, a,b be Real st I is right_open_interval
holds B-Meas.(AffineMap(a,b).:I) = |.a.|*B-Meas.I
proof
let I be Interval, a,b be Real;
assume
A1: I is right_open_interval;
per cases;
suppose A2: a > 0; then
B-Meas.(AffineMap(a,b).:I) = a *B-Meas. I by Lm19,A1;
hence B-Meas.(AffineMap(a,b).:I) =|.a.| *B-Meas.I by A2,ABSVALUE:def 1;
end;
suppose A3: a = 0; then
AffineMap(a,b).:I c= {b} by Lm1; then
A4: AffineMap(a,b).:I c= [.b,b.] by XXREAL_1:17;
[.b,b.] = {b} by XXREAL_1:17; then
A5: [.b,b.] is Interval by XREAL_0:def 1,ZFMISC_1:31;
AffineMap(a,b).:I is Interval by Th1; then
A6: AffineMap(a,b).:I is Element of Borel_Sets
& [.b,b.] is Element of Borel_Sets by A5,MEASUR12:72; then
A7: B-Meas.(AffineMap(a,b).:I) <= B-Meas.([.b,b.]) by A4,MEASURE1:8;
B-Meas. [.b,b.] = b-b by MESFUN14:5; then
B-Meas.(AffineMap(a,b).:I) = 0 by A7,A6,MEASURE1:def 2;
hence B-Meas.(AffineMap(a,b).:I) = |.a.|*B-Meas.I by A3;
end;
suppose A8:a < 0; then
B-Meas.(AffineMap(a,b).:I) = (-a)*B-Meas.I by Lm21,A1;
hence B-Meas.(AffineMap(a,b).:I) =|.a.|*B-Meas. I by A8,ABSVALUE:def 1;
end;
end;
Lm23:
for a,b be Real, I be interval Subset of REAL
holds B-Meas.(AffineMap(a,b).:I) = |.a.|*B-Meas.I
proof
let a,b be Real, I be interval Subset of REAL;
I is open_interval or I is closed_interval
or I is right_open_interval or I is left_open_interval by MEASURE5:1;
hence thesis by Lm7,Lm12,Lm17,Lm22;
end;
theorem Th2:
for a,b be Real, I be interval Subset of REAL
holds J-Meas.(AffineMap(a,b).:I) = |.a.|*J-Meas.I
proof
let a,b be Real, I be interval Subset of REAL;
A1: B-Meas.(AffineMap(a,b).:I) = |.a.|*B-Meas.I by Lm23;
A2: AffineMap(a,b).:I is interval Subset of REAL by Th1; then
B-Meas.(AffineMap(a,b).:I) = diameter (AffineMap(a,b).:I)
by MEASUR12:71; then
A3: B-Meas.(AffineMap(a,b).:I) = J-Meas.(AffineMap(a,b).:I) by A2,MEASUR12:70;
B-Meas.I = diameter I by MEASUR12:71;
hence thesis by A1,A3,MEASUR12:70;
end;
theorem Th5:
for X,Y be non empty set, f be Function of X,Y, F be Function
st rng F c= bool X
holds dom ((.:f)*F) = dom F
& for i be object st i in dom ((.:f)*F) holds ((.:f)*F).i =f.:(F.i)
proof
let X,Y be non empty set, f be Function of X,Y, F be Function;
set G = (.:f)*F;
assume
A1: rng F c= bool X; then
rng F c= dom (.:f) by FUNCT_2:def 1;
hence
A2: dom G = dom F by RELAT_1:27;
let i be object;
assume
A3: i in dom G; then
F.i in rng F by A2,FUNCT_1:def 3; then
F.i c= X by A1; then
A4: F.i c= dom f by FUNCT_2:def 1;
G.i = (.:f).(F.i) by A2,A3,FUNCT_1:13;
hence G.i = f.:(F.i) by FUNCT_3:def 1,A4;
end;
theorem Th4:
for a,b be Real, F be FinSequence of Family_of_Intervals
holds (.:AffineMap(a,b))*F is FinSequence of Family_of_Intervals
& for i be Nat st i in dom ((.:AffineMap(a,b))*F) holds
((.:AffineMap(a,b))*F).i =AffineMap(a,b).:(F.i)
proof
let a,b be Real, F be FinSequence of Family_of_Intervals;
set G = (.:AffineMap(a,b))*F;
A0: rng F c= bool REAL by XBOOLE_1:1; then
reconsider F1=F as FinSequence of bool REAL by FINSEQ_1:def 4;
A1: for i be Nat st i in dom((.:AffineMap(a,b))*F1) holds
((.:AffineMap(a,b))*F1).i = AffineMap(a,b).:(F1.i)
by A0,Th5;
for z be object st z in rng G holds z in Family_of_Intervals
proof
let z be object;
assume z in rng G; then
consider i be Element of NAT such that
A2: i in dom G & z = G.i by PARTFUN1:3;
A3: G.i = AffineMap(a,b).:(F.i) by A0,Th5,A2;
AffineMap(a,b).:(F.i) is interval Subset of REAL by Th1;
hence z in Family_of_Intervals by A3,A2;
end; then
rng G c= Family_of_Intervals;
hence thesis by A1,FINSEQ_1:def 4;
end;
theorem Th6:
for X,Y be non empty set, f be Function of X,Y, F be FinSequence
st rng F c= bool X & f is one-to-one & F is disjoint_valued
holds (.:f)*F is disjoint_valued
proof
let X,Y be non empty set, f be Function of X,Y, F be FinSequence;
assume that
A1: rng F c= bool X and
A2: f is one-to-one and
A3: F is disjoint_valued;
set G = (.:f)*F;
for x, y being object st x <> y holds G.x misses G.y
proof
let i,j be object;
assume i <> j; then
A4: F.i misses F.j by A3;
per cases;
suppose (not i in dom G) or (not j in dom G); then
G.i ={} or G.j ={} by FUNCT_1:def 2;
hence G.i misses G.j;
end;
suppose i in dom G & j in dom G; then
G.i = f.:(F.i) & G.j = f.:(F.j) by A1,Th5; then
(G.i) /\ (G.j) = f.:({}) by A4,A2,FUNCT_1:62;
hence G.i misses G.j;
end;
end;
hence thesis;
end;
theorem Th7:
for X,Y be non empty set, f be Function of X,Y, F be Function
st rng F c= bool X holds Union ((.:f)*F) = f.:(Union F)
proof
let X,Y be non empty set, f be Function of X,Y, F be Function;
assume rng F c= bool X; then
rng F c= bool dom f by FUNCT_2:def 1; then
f.:(union rng F) = union ((.:f).: rng F) by FUNCT_3:14;
hence thesis by RELAT_1:127;
end;
theorem Th8:
for X be set, S be non empty Subset-Family of X,
M be Function of S,ExtREAL, F be FinSequence of S
ex x be FinSequence of ExtREAL
st dom x = dom F & for i be Nat st i in dom x holds x.i = M.(F.i)
proof
let X be set, S be non empty Subset-Family of X,
M be Function of S,ExtREAL, F be FinSequence of S;
reconsider G = M*F as FinSequence of ExtREAL;
take G;
thus dom G = dom F by FUNCT_2:123;
thus thesis by FUNCT_1:12;
end;
theorem Th9:
for X be set, S be non empty Subset-Family of X, M be Function of S,ExtREAL,
F be disjoint_valued FinSequence of S, x be FinSequence of ExtREAL
st {} in S & S is cup-closed & M is zeroed additive & dom x = dom F
& for i be Nat st i in dom x holds x.i = M.(F.i) holds Sum x = M.(Union F)
proof
let X be set, S be non empty Subset-Family of X,
M be Function of S,ExtREAL,
F be disjoint_valued FinSequence of S, x be FinSequence of ExtREAL;
assume that
A1: {} in S and
A2: S is cup-closed and
A3: M is zeroed additive and
A4: dom x = dom F and
A5: for i be Nat st i in dom x holds x.i = M.(F.i);
defpred P[Nat] means
for F be disjoint_valued FinSequence of S, x be FinSequence of ExtREAL
st len F = $1 & dom x = dom F
& for i be Nat st i in dom x holds x.i = M.(F.i)
holds Sum x = M.(Union F);
A6: P[0]
proof
let F be disjoint_valued FinSequence of S, x be FinSequence of ExtREAL;
assume that
A7: len F = 0 and
A8: dom x = dom F and
for i be Nat st i in dom x holds x.i = M.(F.i);
A9: F = {} by A7; then
x = {} by A8;
hence thesis by A3,A9,ZFMISC_1:2,EXTREAL1:7;
end;
A10: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A11: P[n];
let F be disjoint_valued FinSequence of S, x be FinSequence of ExtREAL;
assume that
A12: len F = n+1 and
A13: dom x = dom F and
A14: for i be Nat st i in dom x holds x.i = M.(F.i);
reconsider Fn = F|n as disjoint_valued FinSequence of S
by ROUGHS_1:6,RELAT_1:59;
reconsider xn = x|n as FinSequence of ExtREAL;
A15: len Fn = n by A12,NAT_1:11,FINSEQ_1:59;
A16: dom x = Seg len F by A13,FINSEQ_1:def 3; then
A17: len x = n+1 by A12,FINSEQ_1:def 3; then
A18: len xn = n by FINSEQ_1:59,NAT_1:11;
A19: Seg n c= Seg (n+1) by FINSEQ_1:5,NAT_1:11;
A20: Fn is disjoint_valued;
A21: dom xn = Seg len xn by FINSEQ_1:def 3;
for i be Nat st i in dom xn holds xn.i = M.(Fn.i)
proof
let i be Nat;
assume i in dom xn; then
A22: i in Seg n by FINSEQ_1:def 3, A18; then
xn.i = x.i by FUNCT_1:49; then
xn.i = M.(F.i) by A14,A16,A12,A22,A19;
hence xn.i = M.(Fn.i) by A22,FUNCT_1:49;
end; then
A23: Sum xn = M.(Union Fn) by A11,A15,A20,A21,A18,FINSEQ_1:def 3;
reconsider xn1 = x.(n+1) as Element of ExtREAL;
x = xn^<*xn1*> by FINSEQ_3:55,A17; then
A24: Sum x = (Sum xn) + xn1 by MEASURE9:21;
A25: x.(n+1) = M.(F.(n+1)) by A14,A12,A16,FINSEQ_1:4;
F| (n+1) = F by A12,FINSEQ_1:58; then
A26: Union F = (Union Fn) \/ F.(n+1) by MEASUR11:3;
n < n+1 by NAT_1:13; then
A27: (Union Fn) misses F.(n+1) by MEASUR11:1;
now let i be Nat;
assume i in dom Fn; then
Fn.i in rng Fn by FUNCT_1:3;
hence Fn.i in S;
end; then
A28: Union Fn is Element of S by A1,A2,MEASUR11:5;
F.(n+1) in rng F by A13,A12,A16,FINSEQ_1:4,FUNCT_1:3;
hence Sum x = M.(Union F) by A2,A3,A24,A23,A25,A27,A28,A26;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A6,A10); then
P[len F];
hence Sum x = M.(Union F) by A4,A5;
end;
theorem Th10:
for r be Real,x,y be FinSequence of ExtREAL
st dom x = dom y & for i be Nat st i in dom x holds y.i = r*(x.i)
holds Sum y = r * Sum x
proof
let r be Real,x,y be FinSequence of ExtREAL;
assume
A1: dom x = dom y & for i be Nat st i in dom x holds y.i = r*(x.i);
r is R_eal by XXREAL_0:def 1;
hence Sum y = r * Sum x by A1,MESFUNC3:10;
end;
theorem
<* {} *> is disjoint_valued FinSequence of Family_of_Intervals
proof
{} c= REAL; then
A1: {} in Family_of_Intervals;
rng <* {} *> = { {} } by FINSEQ_1:39;
hence thesis by A1,ZFMISC_1:31,FINSEQ_1:def 4;
end;
theorem Th12:
for a,b be Real, I be Element of Field_generated_by Family_of_Intervals
holds AffineMap(a,b).:I in Field_generated_by Family_of_Intervals
proof
let a,b be Real, I be Element of Field_generated_by Family_of_Intervals;
set f = AffineMap(a,b);
A1: Field_generated_by Family_of_Intervals
= DisUnion Family_of_Intervals by SRINGS_3:22;
I in DisUnion Family_of_Intervals by A1; then
ex A be Subset of REAL st
A=I & ex F being disjoint_valued FinSequence of Family_of_Intervals
st A=Union F; then
consider F being disjoint_valued FinSequence of Family_of_Intervals
such that
A2: I=Union F;
reconsider K = (.:f)*F as FinSequence of Family_of_Intervals by Th4;
Family_of_Intervals c= Field_generated_by Family_of_Intervals
by SRINGS_3:21; then
rng K c= Field_generated_by Family_of_Intervals; then
for n be Nat st n in dom K
holds K.n in Field_generated_by Family_of_Intervals
by FUNCT_1:3; then
A9: Union K in Field_generated_by Family_of_Intervals
by PROB_1:4,MEASUR11:5;
rng F c= bool REAL by XBOOLE_1:1;
hence thesis by A2,A9,Th7;
end;
theorem
for I be Element of Field_generated_by Family_of_Intervals
holds J-Meas.I = B-Meas.I & J-Meas.I = L-Meas.I
proof
let I be Element of Field_generated_by Family_of_Intervals;
A1: Field_generated_by Family_of_Intervals c= Borel_Sets
by PROB_1:def 9,MEASUR10:6;
A2: Field_generated_by Family_of_Intervals
c= sigma_Field(C_Meas J-Meas) by MEASURE8:20;
A5: B-Meas.I = (sigma_Meas(C_Meas J-Meas)).I
by A1,FUNCT_1:49
.= (C_Meas J-Meas).I by A2,MEASURE4:def 3
.= J-Meas.I by MEASURE8:18;
hence J-Meas.I = B-Meas.I;
I \/ {} = I;
hence J-Meas.I = L-Meas.I by A5,A1,MEASUR12:73,MEASURE3:def 5;
end;
theorem Th14:
for a,b be Real, I be Element of Field_generated_by Family_of_Intervals
holds J-Meas.(AffineMap(a,b).:I) = |.a.| * J-Meas.I
proof
let a,b be Real, I be Element of Field_generated_by Family_of_Intervals;
set f = AffineMap(a,b);
A1: Family_of_Intervals c= Field_generated_by Family_of_Intervals
by SRINGS_3:21;
A2: b is R_eal by NUMBERS:31,XREAL_0:def 1;
per cases;
suppose
A3: a = 0; then
A4: f.:I = {} or f.:I = {b} by Lm1,ZFMISC_1:33;
now assume f.:I = {b}; then
f.:I = [.b,b.] by XXREAL_1:17; then
J-Meas.(f.:I) = diameter [.b,b.] by MEASUR12:70; then
J-Meas.(f.:I) = b-b by MEASURE5:6,A2;
hence J-Meas.(f.:I) = 0;
end; then
J-Meas.(f.:I) = 0 by A4,VALUED_0:def 19;
hence J-Meas.(f.:I) = |.a.| *J-Meas. I by A3;
end;
suppose
A5: a <> 0;
Field_generated_by Family_of_Intervals
= DisUnion Family_of_Intervals by SRINGS_3:22; then
I in DisUnion Family_of_Intervals; then
ex A be Subset of REAL st
A = I & ex F being disjoint_valued FinSequence of Family_of_Intervals
st A = Union F; then
consider F being disjoint_valued FinSequence of Family_of_Intervals
such that
A6: I = Union F;
A7: Family_of_Intervals c= Field_generated_by Family_of_Intervals
by SRINGS_3:21;
A8: rng F c= bool REAL by XBOOLE_1:1;
reconsider K = (.:f)*F as FinSequence of Family_of_Intervals by Th4;
A9: dom F = dom K by A8,Th5;
A10: K is disjoint_valued & Union K = f.: (Union F)
by A5,A8,Th6,Th7,FCONT_1:50;
rng F c= Field_generated_by Family_of_Intervals by A7; then
A11: F is FinSequence of Field_generated_by Family_of_Intervals
by FINSEQ_1:def 4; then
consider x be FinSequence of ExtREAL such that
A12:dom x = dom F
& for i be Nat st i in dom x holds x.i = J-Meas.(F.i) by Th8;
rng K c= Field_generated_by Family_of_Intervals by A7; then
A13: K is FinSequence of Field_generated_by Family_of_Intervals
by FINSEQ_1:def 4; then
consider y be FinSequence of ExtREAL such that
A14:dom y = dom K
& for i be Nat st i in dom y holds y.i = J-Meas.(K.i) by Th8;
{} c= REAL; then
A15: {} in Family_of_Intervals; then
A16:Sum x = J-Meas.I by A6,A11,A12,A1,Th9;
A17:Sum y = J-Meas.(f.: I ) by A6,A13,A14,A10,A1,A15,Th9;
reconsider r = |.a.| as Real;
for i being Nat st i in dom x holds y.i = r*(x.i)
proof
let i be Nat;
assume
A18: i in dom x; then
y.i = J-Meas.(K.i) by A9,A12,A14; then
y.i = J-Meas.(f.:(F.i)) by A9,A12,A18,Th4; then
y.i =r * J-Meas.(F.i) by Th2;
hence y.i = r * (x.i) by A12,A18;
end;
hence J-Meas.(f.:I) = |.a.| * J-Meas.I by A16,A17,A9,Th10,A12,A14;
end;
end;
begin :: Affine Invariance of Borel Structures
theorem Th15:
for X being set holds .:(id X) = id bool X
proof
let X be set;
A1: dom id X = X; then
A2: dom (.:(id X)) = bool X by FUNCT_3:def 1;
for A being object st A in bool X holds (.:(id X)).A = A
proof
let A be object;
assume A in bool X;
then reconsider A as Subset of X;
(.:(id X)).A = (id X).:A by A1,FUNCT_3:def 1
.= A by FUNCT_1:92;
hence thesis;
end;
hence thesis by A2,FUNCT_1:17;
end;
theorem Th16:
for X,Y be non empty set, F be Function of X,Y, S be non empty set
st S c= bool X & F is bijective
holds S is SigmaField of X iff (.:F).:S is SigmaField of Y
proof
let X,Y be non empty set, F be Function of X,Y, S be non empty set;
assume that
A1: S c= bool X and
A2: F is bijective;
thus S is SigmaField of X implies (.:F).:S is SigmaField of Y
by A2,MEASUR14:3;
F is one-to-one & rng F = Y by A2,FUNCT_2:def 3; then
reconsider G = F" as Function of Y,X by FUNCT_2:25;
rng G = dom F by A2,FUNCT_1:33; then
A3: G is onto by FUNCT_2:def 1;
assume
A4: (.:F).:S is SigmaField of Y;
A5: dom F = X by FUNCT_2:def 1;
(.:G).:((.:F).:S) = ((.:G)*(.:F)).:S by RELAT_1:126
.= (.:(G*F)).:S by FUNCT_3:18
.= (.:(id X)).:S by A5,A2,FUNCT_1:39
.= id (bool X) .: S by Th15
.= S by FUNCT_1:92,A1;
hence S is SigmaField of X by A2,A3,A4,MEASUR14:3;
end;
theorem Th17:
for X,Y be non empty set, F be Function of X,Y, S be Subset-Family of X
st F is bijective holds (.:F).:(sigma S) = sigma((.:F).:S)
proof
let X,Y be non empty set, F be Function of X,Y, S be Subset-Family of X;
assume
A1: F is bijective; then
reconsider G = (.:F).:(sigma S) as SigmaField of Y by Th16;
set K = (.:F).:S;
A2: S c= sigma S by PROB_1:def 9;
for Z being set st K c= Z & Z is SigmaField of Y holds G c= Z
proof
let Z be set;
assume that
A3: K c= Z and
A4: Z is SigmaField of Y;
A5: Z c= bool Y by A4;
A6: F is one-to-one & rng F = Y by A1,FUNCT_2:def 3; then
reconsider H = F" as Function of Y,X by FUNCT_2:25;
rng H = dom F by A1,FUNCT_1:33; then
A7: H is onto by FUNCT_2:def 1;
A8: dom F = X by FUNCT_2:def 1;
A9: (.:F).:((.:H).:Z) = ((.:F)*(.:H)).:Z by RELAT_1:126
.= (.:(F*H)).:Z by FUNCT_3:18
.= (.:(id Y)).:Z by A6,FUNCT_1:39
.= id (bool Y) .: Z by Th15
.= Z by A4,FUNCT_1:92;
Z <> {} & Z c= dom (.:H) by A4,A5,FUNCT_2:def 1; then
reconsider L = (.:H).:Z as non empty set;
A10: (.:H).:((.:F).:S) c= (.:H).:Z by A3,RELAT_1:123;
(.:H).:((.:F).:S) = ((.:H)*(.:F)).:S by RELAT_1:126
.= (.:(H*F)).:S by FUNCT_3:18
.= (.:(id X)).:S by A8,A1,FUNCT_1:39
.= id (bool X).:S by Th15; then
A11: S c= L by A10,FUNCT_1:92;
L is SigmaField of X by A1,A4,A7,Th16; then
sigma S c= L by A11,PROB_1:def 9;
hence G c= Z by A9,RELAT_1:123;
end;
hence thesis by A2,RELAT_1:123,PROB_1:def 9;
end;
Lm24:
for A be Subset of REAL holds
Svc(J-Meas,A) = {r where r is R_eal: ex CA being Covering of A,
Field_generated_by Family_of_Intervals st r = SUM(vol(J-Meas,CA))}
proof
let A be Subset of REAL;
set S = {r where r is R_eal: ex CA being Covering of A,
Field_generated_by Family_of_Intervals st r = SUM(vol(J-Meas,CA))};
for x be object holds x in Svc(J-Meas,A) iff x in S
proof
let x be object;
hereby assume
A1: x in Svc(J-Meas,A); then
reconsider z=x as R_eal;
ex CA being Covering of A,Field_generated_by Family_of_Intervals
st z = SUM(vol(J-Meas,CA)) by MEASURE8:def 7,A1;
hence x in S;
end;
assume x in S; then
ex r be R_eal st x=r
& ex CA being Covering of A,Field_generated_by Family_of_Intervals
st r = SUM(vol(J-Meas,CA));
hence x in Svc(J-Meas,A) by MEASURE8:def 7;
end;
hence thesis by TARSKI:2;
end;
Field_generated_by Family_of_Intervals
c= sigma_Field (C_Meas J-Meas) by MEASURE8:20; then
Lm25: Borel_Sets c= sigma_Field (C_Meas J-Meas)
by PROB_1:def 9,MEASUR10:6;
theorem Th18:
for A,B be Subset of ExtREAL, a be Real
st 0 < a & B = { a * r where r is R_eal : r in A } holds
sup B = a * sup A & inf B = a * inf A
proof
let A,B be Subset of ExtREAL, a be Real;
assume that
A1: 0 < a and
A2: B = { a * r where r is R_eal : r in A };
now let x be ExtReal;
assume x in B; then
consider r be R_eal such that
A3: x = a*r & r in A by A2;
sup A is UpperBound of A by XXREAL_2:def 3; then
r<= sup A by A3,XXREAL_2:def 1;
hence x <= a*sup A by A3,A1,XXREAL_3:71;
end; then
A4: a*sup A is UpperBound of B by XXREAL_2:def 1;
for x being UpperBound of B holds a*sup A <= x
proof
let x be UpperBound of B;
assume not a*sup A <= x; then
x/a < (a*sup A)/a by A1,XXREAL_3:80; then
A5: x/a < sup A by A1,XXREAL_3:88;
for r being ExtReal st r in A holds r <= x/a
proof
let r be ExtReal;
assume r in A; then
a*r in B by A2; then
(a*r)/a <= x/a by A1,XXREAL_2:def 1,XXREAL_3:79;
hence r <= x/a by A1,XXREAL_3:88;
end; then
x/a is UpperBound of A by XXREAL_2:def 1;
hence contradiction by A5,XXREAL_2:def 3;
end;
hence sup B = a*sup A by A4,XXREAL_2:def 3;
now let x be ExtReal;
assume x in B; then
consider r be R_eal such that
A6: x= a*r & r in A by A2;
inf A is LowerBound of A by XXREAL_2:def 4; then
inf A <= r by A6,XXREAL_2:def 2;
hence a*inf A <= x by A6,A1,XXREAL_3:71;
end; then
A7: a*inf A is LowerBound of B by XXREAL_2:def 2;
for x being LowerBound of B holds x <= a*inf A
proof
let x be LowerBound of B;
assume x > a*inf A; then
(a*inf A)/a < x/a by A1,XXREAL_3:80; then
A8: inf A < x/a by A1,XXREAL_3:88;
for r being ExtReal st r in A holds x/a <= r
proof
let r be ExtReal;
assume r in A; then
a*r in B by A2; then
x/a <= (a*r)/a by A1,XXREAL_2:def 2,XXREAL_3:79;
hence x/a <= r by A1,XXREAL_3:88;
end; then
x/a is LowerBound of A by XXREAL_2:def 2;
hence contradiction by A8,XXREAL_2:def 4;
end;
hence inf B = a * inf A by A7,XXREAL_2:def 4;
end;
theorem
for A,B be Subset of ExtREAL, a be Real
st a < 0 & B = { a * r where r is R_eal : r in A } holds
inf B = a * sup A & sup B = a * inf A
proof
let A,B be Subset of ExtREAL, a be Real;
assume that
A1: a < 0 and
A2: B = { a * r where r is R_eal : r in A };
now let x be ExtReal;
assume x in B; then
consider r be R_eal such that
A3: x = a*r & r in A by A2;
sup A is UpperBound of A by XXREAL_2:def 3; then
r <= sup A by A3,XXREAL_2:def 1;
hence x >= a*sup A by A3,A1,XXREAL_3:101;
end; then
A4: a*sup A is LowerBound of B by XXREAL_2:def 2;
for x being LowerBound of B holds x <= a*sup A
proof
let x be LowerBound of B;
assume x > a*sup A; then
x/a < (a*sup A)/a by A1,XXREAL_3:104; then
A5: x/a < sup A by A1,XXREAL_3:88;
for r being ExtReal st r in A holds r <= x/a
proof
let r be ExtReal;
assume r in A; then
a*r in B by A2; then
(a*r)/a <= x/a by A1,XXREAL_2:def 2,XXREAL_3:103;
hence r <= x/a by A1,XXREAL_3:88;
end; then
x/a is UpperBound of A by XXREAL_2:def 1;
hence contradiction by A5,XXREAL_2:def 3;
end;
hence inf B = a*sup A by A4,XXREAL_2:def 4;
now let x be ExtReal;
assume x in B; then
consider r be R_eal such that
A6: x= a*r & r in A by A2;
inf A is LowerBound of A by XXREAL_2:def 4; then
inf A <= r by A6,XXREAL_2:def 2;
hence a*inf A >= x by A6,A1,XXREAL_3:101;
end; then
A7: a*inf A is UpperBound of B by XXREAL_2:def 1;
for x being UpperBound of B holds x >= a*inf A
proof
let x be UpperBound of B;
assume x < a*inf A; then
(a*inf A)/a < x/a by A1,XXREAL_3:104; then
A8: inf A < x/a by A1,XXREAL_3:88;
for r being ExtReal st r in A holds x/a <= r
proof
let r be ExtReal;
assume r in A; then
a*r in B by A2; then
x/a <= (a*r)/a by A1,XXREAL_2:def 1,XXREAL_3:103;
hence x/a <= r by A1,XXREAL_3:88;
end; then
x/a is LowerBound of A by XXREAL_2:def 2;
hence contradiction by A8,XXREAL_2:def 4;
end;
hence sup B = a * inf A by A7,XXREAL_2:def 3;
end;
theorem Th20:
for p,q be sequence of ExtREAL, a be Real
st 0 <= a & for n be Element of NAT holds q.n = a * p.n
holds SUM q = a * (SUM p)
proof
let p,q be sequence of ExtREAL, a be Real;
assume that
A1: 0 <= a and
A2: for n be Element of NAT holds q.n = a * p.n;
defpred P[Nat] means (Ser q).$1 = a * (Ser p).$1;
(Ser q).0 = q.0 by SUPINF_2:def 11; then
(Ser q).0 = a * p.0 by A2; then
A3: P[0] by SUPINF_2:def 11;
A4: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A5: P[n];
(Ser q).(n+1) = (Ser q).n + q.(n+1) by SUPINF_2:def 11; then
(Ser q).(n+1) = a * (Ser p).n + a * p.(n+1) by A2,A5; then
(Ser q).(n+1) = a * ( (Ser p).n + p.(n+1)) by XXREAL_3:95;
hence (Ser q).(n+1) = a * (Ser p).(n+1) by SUPINF_2:def 11;
end;
A6: for n be Nat holds P[n] from NAT_1:sch 2(A3,A4);
for z be object holds z in rng (Ser q)
iff z in { a * r where r is R_eal : r in rng (Ser p) }
proof
let z be object;
hereby assume z in rng (Ser q); then
consider i be object such that
A7: i in dom (Ser q) & z=(Ser q).i by FUNCT_1:def 3;
reconsider i as Nat by A7;
A8: z = a * (Ser p).i by A6,A7;
(Ser p).i in rng (Ser p) by A7,FUNCT_2:4;
hence z in { a * r where r is R_eal : r in rng (Ser p) } by A8;
end;
assume z in { a * r where r is R_eal : r in rng (Ser p) }; then
consider r be R_eal such that
A9: z= a * r & r in rng (Ser p);
consider i be Element of NAT such that
A10: r = (Ser p).i by FUNCT_2:113,A9;
reconsider i as Nat;
z = (Ser q).i by A6,A9,A10;
hence z in rng (Ser q) by FUNCT_2:4;
end; then
T1: rng (Ser q) = { a * r where r is R_eal : r in rng (Ser p) }
by TARSKI:2;
per cases by A1;
suppose a > 0;
hence thesis by T1,Th18;
end;
suppose B1: a = 0;
for n be Element of NAT holds q.n = 0.
proof
let n be Element of NAT;
q.n = 0 * p.n by B1,A2 .= 0.;
hence thesis;
end; then
SUM q = 0 by MEASURE7:1;
hence thesis by B1;
end;
end;
theorem Th21:
for a,b be Real holds
(.:AffineMap(a,b)).:(Family_of_Intervals) c= Family_of_Intervals
proof
let a,b be Real;
set f = AffineMap(a,b);
for x be object st x in (.:AffineMap(a,b)).:(Family_of_Intervals)
holds x in Family_of_Intervals
proof
let x be object;
assume x in (.:f).:(Family_of_Intervals); then
consider I be object such that
A1: I in dom (.:f) & I in Family_of_Intervals & x = (.:f).I by FUNCT_1:def 6;
ex J be Interval st I=J by A1; then
reconsider I as interval Subset of REAL;
(.:f).I = f.:I by FUNCT_3:7,A1; then
x is interval Subset of REAL by A1,Th1;
hence x in Family_of_Intervals;
end;
hence thesis;
end;
theorem Th22:
for a,b be Real st a <> 0 holds
(.:AffineMap(a,b)).:(Family_of_Intervals) = Family_of_Intervals
proof
let a,b be Real;
set f = AffineMap(a,b);
set g = AffineMap(1/a,-b/a);
assume
A1: a <> 0; then
a1: g = f" by FCONT_1:56;
rng f = REAL & f is one-to-one by A1,FCONT_1:50,55; then
A2: f*g = id REAL by a1,FUNCT_1:39;
for z be object st z in Family_of_Intervals holds
z in (.:f).:(Family_of_Intervals)
proof
let z be object;
assume z in Family_of_Intervals; then
ex I be Interval st z=I; then
reconsider I = z as interval Subset of REAL;
g.:I is interval Subset of REAL by Th1; then
A3: g.:I in Family_of_Intervals;
g.:I in bool REAL; then
A4: g.:I in dom (.:f) by FUNCT_2:def 1; then
(.:f).(g.:I) = f.:(g.:I) by FUNCT_3:7
.= (f*g).:I by RELAT_1:126
.= I by A2,FUNCT_1:92;
hence z in (.:f).:(Family_of_Intervals) by A4,A3,FUNCT_1:def 6;
end; then
Family_of_Intervals c= (.:f).:(Family_of_Intervals);
hence thesis by Th21;
end;
theorem Th23:
for a,b be Real st a <> 0 holds (.:AffineMap(a,b)).:Borel_Sets = Borel_Sets
proof
let a,b be Real;
assume A1: a <> 0;
set f = AffineMap(a,b);
set S = Family_of_Intervals;
f is one-to-one & f is onto by A1,FCONT_1:50,55; then
(.:f).: sigma S = sigma ((.:f).:S) by Th17;
hence (.:f).: Borel_Sets = Borel_Sets by A1,Th22,MEASUR10:6;
end;
theorem Th24:
for a,b be Real, I be Element of Borel_Sets
holds AffineMap(a,b).:I in Borel_Sets
proof
let a,b be Real, I be Element of Borel_Sets;
set f = AffineMap(a,b);
A1: Family_of_Intervals c= sigma Family_of_Intervals by PROB_1:def 9;
per cases;
suppose a = 0; then
f.:I = {} or f.:I = {b} by Lm1,ZFMISC_1:33; then
f.:I = {} or f.:I = [.b,b.] by XXREAL_1:17; then
f.:I in Family_of_Intervals;
hence f.:I in Borel_Sets by A1,MEASUR10:6;
end;
suppose a <> 0; then
A2: (.:f).:Borel_Sets = Borel_Sets by Th23;
dom (.:f) = bool REAL by FUNCT_2:def 1; then
I in dom (.:f) & I in Borel_Sets & f.:I = (.:f).I by FUNCT_3:7;
hence f.:I in Borel_Sets by A2,FUNCT_1:def 6;
end;
end;
begin :: Scaling Properties of Borel and Lebesgue Measures
theorem Th25:
for a,b be Real, I be Element of Borel_Sets
holds B-Meas.(AffineMap(a,b).:I) = |.a.| * B-Meas.I
proof
let a,b be Real, I be Element of Borel_Sets;
set f = AffineMap(a,b);
set F = Field_generated_by Family_of_Intervals;
per cases;
suppose
A1: a = 0; then
A2: f.:I = {} or f.:I = {b} by Lm1,ZFMISC_1:33;
A3: f.:I in Borel_Sets by Th24;
f.:I is thin of B-Meas by A2,MEASUR12:73,74; then
ex J be set st
J in Borel_Sets & f.:I c= J & B-Meas.J = 0. by MEASURE3:def 2; then
B-Meas.(f.:I) <= 0 by A3,MEASURE1:8; then
B-Meas.(f.:I) = 0 by A3,MEASURE1:def 2;
hence B-Meas.(f.:I) = |.a.| * B-Meas.I by A1;
end;
suppose
A4: a <> 0; then
A5: |.a.| > 0 by COMPLEX1:47;
A6: f.:I in sigma_Field (C_Meas J-Meas) by Lm25,Th24;
(B-Meas).(f.:I) = (sigma_Meas C_Meas J-Meas).(f.:I)
by Th24,FUNCT_1:49; then
(B-Meas).(f.:I) = (C_Meas J-Meas).(f.:I) by A6,MEASURE4:def 3; then
A7: (B-Meas).(f.:I) = inf (Svc (J-Meas,(f.:I))) by MEASURE8:def 8;
A8: Svc (J-Meas,(f.:I)) = {r where r is R_eal: ex CA being Covering of
(f.:I),F st r = SUM (vol (J-Meas,CA)) } by Lm24;
set g = (AffineMap(a,b) qua Function)";
A9: g = AffineMap(a",-b/a) by A4,FCONT_1:56;
A10: rng f = REAL & f is one-to-one by A4,FCONT_1:55,50; then
A11: f*g = id REAL & g*f = id REAL by FUNCT_2:29;
reconsider g as Function of REAL,REAL by A10,FUNCT_2:25;
A12: for CA being Covering of f.:I,F holds
ex CB be Covering of I,F st
for i be Element of NAT holds CA.i = f.:(CB.i)
proof
let CA be Covering of f.:I,F;
set CB = (.:g)*CA;
A13: for i be Element of NAT holds CB.i = g.:(CA.i)
proof
let i be Element of NAT;
(CA.i) in bool REAL; then
(CA.i) in dom (.:g) by FUNCT_2:def 1; then
(.:g).(CA.i) = g.:(CA.i) by FUNCT_3:7;
hence CB.i = g.:(CA.i) by FUNCT_2:15;
end;
for i being Nat holds CB.i in F
proof
let i be Nat;
i is Element of NAT by ORDINAL1:def 12; then
CB.i = g.:(CA.i) by A13;
hence CB.i in F by A9,Th12;
end; then
reconsider CB as Set_Sequence of F by MEASURE8:def 2;
A14: (g.:(f.:I)) c= g.:(Union CA) by RELAT_1:125,MEASURE8:def 3;
rng CA c= bool REAL; then
A15: (g.:(f.:I)) c= Union ((.:g)*CA) by A14,Th7;
(g.:(f.:I)) = (g*f).:I by RELAT_1:126; then
(g.:(f.:I)) = I by A11,FUNCT_1:92; then
reconsider CB as Covering of I,F by A15,MEASURE8:def 3;
take CB;
hereby let i be Element of NAT;
CB.i = g.:(CA.i) by A13; then
f.:(CB.i) = (f*g).:(CA.i) by RELAT_1:126;
hence CA.i = f.:(CB.i) by A11,FUNCT_1:92;
end;
end;
A16: for CB being Covering of I,F holds
ex CA be Covering of f.:I,F
st for i be Element of NAT holds CA.i = f.:(CB.i)
proof
let CB be Covering of I,F;
set CA = (.:f)*CB;
A17: for i be Nat holds CA.i = f.:(CB.i)
proof
let i be Nat;
(CB.i) in bool REAL; then
A18: (CB.i) in dom (.:f) by FUNCT_2:def 1;
CA.i = (.:f).(CB.i) by ORDINAL1:def 12,FUNCT_2:15;
hence CA.i = f.:(CB.i) by FUNCT_3:7,A18;
end;
for i being Nat holds CA.i in F
proof
let i be Nat;
CA.i = f.:(CB.i) by A17;
hence CA.i in F by Th12;
end; then
reconsider CA as Set_Sequence of F by MEASURE8:def 2;
A19: (f.:I) c= f.:(Union CB) by RELAT_1:125,MEASURE8:def 3;
rng CB c= bool REAL; then
(f.:I) c=Union ((.:f)*CB) by A19,Th7; then
reconsider CA as Covering of f.:I,F by MEASURE8:def 3;
take CA;
thus thesis by A17;
end;
A20: for CB be Covering of I,F, CA be Covering of f.:I,F
st for i be Element of NAT holds CA.i = f.:(CB.i) holds
SUM (vol (J-Meas,CA)) = |.a.| * SUM (vol (J-Meas,CB))
proof
let CB be Covering of I,F, CA be Covering of f.:I,F;
assume
A21: for i be Element of NAT holds CA.i = f.:(CB.i);
now let i be Element of NAT;
(vol (J-Meas,CA)).i =J-Meas.(CA.i) by MEASURE8:def 5; then
(vol (J-Meas,CA)).i =J-Meas.(f.:(CB.i)) by A21; then
(vol (J-Meas,CA)).i = |.a.| *J-Meas.(CB.i) by Th14;
hence (vol(J-Meas,CA)).i = |.a.|*(vol (J-Meas,CB)).i by MEASURE8:def 5;
end;
hence SUM (vol (J-Meas,CA)) = |.a.| *SUM (vol (J-Meas,CB))
by COMPLEX1:46,Th20;
end;
for z be object holds z in Svc (J-Meas,(f.:I))
iff z in {|.a.|*r where r is R_eal: r in Svc (J-Meas,I) }
proof
let z be object;
hereby assume z in Svc (J-Meas,(f.:I)); then
consider r be R_eal such that
A22: z=r & ex CA being Covering of (f.:I),F st r =SUM (vol (J-Meas,CA))
by A8;
consider CA being Covering of (f.:I),F such that
A23: r =SUM (vol (J-Meas,CA)) by A22;
consider CB be Covering of I,F such that
A24: for i be Element of NAT holds CA.i = f.:(CB.i) by A12;
A25: r =|.a.| *SUM (vol (J-Meas,CB)) by A20,A24,A23;
Svc (J-Meas,I) = {r where r is R_eal: ex CA being Covering of I,F
st r = SUM (vol (J-Meas,CA) ) } by Lm24; then
SUM (vol (J-Meas,CB)) in Svc (J-Meas,I);
hence z in {|.a.|*r where r is R_eal: r in Svc (J-Meas,I) } by A25,A22;
end;
assume z in {|.a.|*r where r is R_eal: r in Svc (J-Meas,I) }; then
consider r be R_eal such that
A26: z=|.a.|*r & r in Svc (J-Meas,I);
Svc (J-Meas,I) = {r where r is R_eal: ex CB being Covering of I,F
st r = SUM (vol (J-Meas,CB) ) } by Lm24; then
consider t be R_eal such that
A27: r=t & ex CB being Covering of I,F st t = SUM (vol (J-Meas,CB) ) by A26;
consider CB being Covering of I,F such that
A28: t = SUM (vol (J-Meas,CB) ) by A27;
consider CA be Covering of f.:I,F such that
A29: for i be Element of NAT holds CA.i = f.:(CB.i) by A16;
A30: SUM (vol (J-Meas,CA)) = z by A26,A27,A20,A29,A28;
Svc (J-Meas,f.:I)
= {r where r is R_eal: ex CA being Covering of f.:I,F
st r = SUM (vol (J-Meas,CA) ) } by Lm24;
hence z in Svc (J-Meas,(f.:I)) by A30;
end; then
Svc (J-Meas,(f.:I)) = {|.a.|*r where r is R_eal: r in Svc (J-Meas,I) }
by TARSKI:2; then
A31: inf Svc (J-Meas,(f.:I)) = |.a.| * inf Svc (J-Meas,I) by A5,Th18;
(B-Meas). I = (sigma_Meas (C_Meas J-Meas)).I by FUNCT_1:49; then
(B-Meas). I = (C_Meas J-Meas).I by Lm25,MEASURE4:def 3;
hence (B-Meas). (f.:I) =|.a.| * (B-Meas). I by A7,A31,MEASURE8:def 8;
end;
end;
theorem
for a,b be Real, I be Element of L-Field
holds AffineMap(a,b).:I in L-Field
proof
let a,b be Real, I be Element of L-Field;
set f = AffineMap(a,b);
consider J being set such that
A1: J in Borel_Sets &
ex C being thin of B-Meas st I = J \/ C by MEASURE3:def 3;
consider C being thin of B-Meas such that
A2: I = J \/ C by A1;
A3: f.:I = (f.:J) \/ (f.:C) by A2,RELAT_1:120;
A4: f.:J in Borel_Sets by Th24,A1;
consider D be set such that
A5: D in Borel_Sets & C c= D & B-Meas.D = 0 by MEASURE3:def 2;
A6: f.:C c= f.:D by A5,RELAT_1:123;
B-Meas.(f.:D) = |.a.| * 0 by A5,Th25; then
f.:C is thin of B-Meas by A6,A5,Th24,MEASURE3:def 2;
hence f.:I in L-Field by MEASURE3:def 3,A3,A4;
end;
theorem
for a,b be Real, I be Element of L-Field holds
L-Meas.(AffineMap(a,b).:I) = |.a.| * L-Meas.I
proof
let a,b be Real, I be Element of L-Field;
set f = AffineMap(a,b);
consider J being set such that
A1: J in Borel_Sets &
ex C being thin of B-Meas st I = J \/ C by MEASURE3:def 3;
consider C being thin of B-Meas such that
A2: I = J \/ C by A1;
A3: L-Meas.I = B-Meas.J by A1,MEASURE3:def 5;
A4: f.:I = (f.:J) \/ (f.:C) by A2,RELAT_1:120;
consider D be set such that
A5: D in Borel_Sets & C c= D & B-Meas.D = 0 by MEASURE3:def 2;
A6: f.:C c= f.:D by A5,RELAT_1:123;
B-Meas.(f.:D) = |.a.| * 0 by A5,Th25; then
f.:C is thin of B-Meas by A6,A5,Th24,MEASURE3:def 2; then
L-Meas.(f.:I) = B-Meas.(f.:J) by A4,A1,Th24,MEASURE3:def 5;
hence L-Meas.(f.:I) = |.a.| * L-Meas.I by A3,A1,Th25;
end;