:: Integrability of Multivariable Continuous Functions
:: by Noboru Endou and Yasunari Shidama
::
:: Received December 12, 2025
:: Copyright (c) 2025-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 MEASUR14, INTEGRA1, MEASUR13, FINSEQ_1, FINSEQ_2, NUMBERS,
XXREAL_0, SUBSET_1, CARD_1, ARYTM_3, ARYTM_1, RELAT_1, REAL_1, FUNCT_1,
XBOOLE_0, TARSKI, ZFMISC_1, PROB_1, SUPINF_2, PARTFUN1, MEASURE1,
MESFUNC5, MESFUNC1, MEASUR10, MEASUR11, COMPLEX1, MESFUN12, ORDINAL2,
INTEGRA5, NAT_1, FUNCT_2, FUNCOP_1, CARD_3, XCMPLX_0, MEASURE5, XXREAL_1,
MEASUR12, DUALSP02, NFCONT_2, CFCONT_1, RCOMP_1, PRE_TOPC, XXREAL_2,
GROUP_2, STRUCT_0, SQUARE_1, NORMSP_1, MEASURE6, REALSET1, FCONT_1,
MEASUR15, FCONT_2, SUPINF_1, VALUED_1, REAL_NS1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_3, DOMAIN_1, SUPINF_1,
FUNCOP_1, CARD_1, CARD_3, NUMBERS, XXREAL_3, XCMPLX_0, XXREAL_0, XREAL_0,
VALUED_1, SQUARE_1, EXTREAL1, COMPLEX1, MESFUNC1, FCONT_1, FCONT_2,
FINSEQ_1, FINSEQ_2, EUCLID, RVSUM_1, SUPINF_2, PROB_1, RCOMP_1, MEASURE1,
MEASURE5, MEASUR12, MESFUNC5, MESFUNC6, INTEGRA5, MEASUR10, MEASUR11,
MESFUN12, MEASUR13, MESFUN16, MEASUR14, SEQ_2, STRUCT_0, PRE_TOPC,
RLVECT_1, NORMSP_0, NORMSP_1, NFCONT_1, PRVECT_1, PRVECT_2, PRVECT_4,
NFCONT_2, REAL_NS1, DUALSP02, PRVECT_3, MEASUR15;
constructors EXTREAL1, SUPINF_1, MESFUNC2, MEASUR11, MESFUN12, MESFUNC6,
LPSPACE1, SQUARE_1, DOMAIN_1, FCONT_1, FCONT_2, MEASUR12, INTEGRA1,
WSIERP_1, COMSEQ_2, MEASUR14, NEWTON, INTEGRA5, BINOP_2, NFCONT_1,
NFCONT_2, DUALSP02, PRVECT_4, REAL_NS1, MESFUN16, MEASUR15;
registrations ORDINAL1, XBOOLE_0, RELAT_1, SUBSET_1, XXREAL_0, XREAL_0, NAT_1,
NUMBERS, VALUED_0, RELSET_1, MEASURE1, XXREAL_3, FINSEQ_2, FUNCT_1,
FUNCT_2, FUNCOP_1, CARD_1, CARD_3, PRVECT_3, MEMBERED, XXREAL_2,
SRINGS_4, MEASUR13, EUCLID, SQUARE_1, STRUCT_0, NORMSP_0, NORMSP_1,
FOMODEL0, PRVECT_2, PRVECT_1, FINSEQ_9, MEASURE5, FCONT_1, MESFUN13,
COMPLEX1, MEASUR15, REAL_NS1;
requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
equalities FINSEQ_1, MEASUR10, BINOP_1, PRVECT_3, MEASUR13, RCOMP_1, ALGSTR_0,
NORMSP_0, SQUARE_1, DUALSP02, MESFUNC6, INTEGRA5, MEASUR15;
expansions TARSKI, XBOOLE_0, FUNCT_1, NFCONT_1, NFCONT_2, INTEGRA5, MESFUNC1,
MEASURE1, FCONT_1, MESFUNC6;
theorems XBOOLE_0, FUNCT_1, XXREAL_0, XBOOLE_1, XXREAL_3, MEASURE1, VALUED_0,
FUNCT_2, RELAT_1, MESFUNC5, EXTREAL1, PARTFUN1, MESFUNC1, MEASUR10,
MEASUR11, MESFUN12, RELSET_1, MESFUNC6, LPSPACE1, FINSEQ_1, FINSEQ_2,
TARSKI, ZFMISC_1, NAT_1, FUNCOP_1, XREAL_1, PROB_1, CARD_1, CARD_3,
PRVECT_3, FINSEQ_3, XREAL_0, MESFUN13, FINSUB_1, MEASUR13, SRINGS_5,
MEASUR12, MESFUN16, VALUED_1, COMPLEX1, XXREAL_1, MEASURE5, NFCONT_2,
EUCLID, SQUARE_1, MEASUR14, RLVECT_1, DUALSP03, NORMSP_1, XCMPLX_1,
LOPBAN11, NFCONT_1, NDIFF_8, INTEGRA5, FCONT_1, INTEGRA6, REAL_NS1,
PRVECT_4, MESFUN14, FCONT_2, NDIFF_9, NORMSP_0, MESFUN6C, ABSVALUE,
MESFUNC7, LOPBAN15, MEASUR15;
schemes NAT_1;
begin :: Preliminaries
theorem Th1:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,REAL st dom f = {} holds f is_integrable_on 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;
assume
A1: dom f = {}; then
dom f in S by MEASURE1:7; then
consider E0 be Element of S such that
A2: E0 = dom f;
for r be Real holds
E0 /\ less_dom(R_EAL f,r) in S by A1,A2; then
R_EAL f is E0-measurable; then
A3: f is E0-measurable;
M.E0 = 0 by A1,A2,VALUED_0:def 19; then
f|E0 is_integrable_on M by A2,A3,MESFUN6C:20;
hence f is_integrable_on M by A2;
end;
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL st dom f = {} holds f is_integrable_on 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: dom f = {};
set f0 = dom f --> 0;
dom f0 c= X & rng f0 c= REAL; then
reconsider f0 as PartFunc of X,REAL by RELSET_1:4;
dom (R_EAL f0) = dom f0 by MESFUNC5:def 7; then
A2: R_EAL f0 = f by A1;
dom f0 = dom f; then
f0 is_integrable_on M by A1,Th1;
hence f is_integrable_on M by A2;
end;
::$N generalization \cite{MEASUR13}:3
theorem Th3:
for n,i,j,k be non zero Nat, X be n-element FinSequence,
X1 be j-element FinSequence, X2 be k-element FinSequence
st i <= j & j <= k & X1 = X|j & X2 = X|k holds
(ProdFinSeq X1).i = (ProdFinSeq X2).i
proof
let n,i,j,k be non zero Nat, X be n-element FinSequence,
X1 be j-element FinSequence, X2 be k-element FinSequence;
assume that
A1: i <= j and
A2: j <= k and
A3: X1 = X|j and
A4: X2 = X|k;
defpred P[non zero Nat] means
$1 <= j implies (ProdFinSeq X1).$1 = (ProdFinSeq X2).$1;
A5: P[1]
proof
assume
A6: 1 <= j;
(ProdFinSeq X1).1 = X1.1 by MEASUR13:def 3; then
A7: (ProdFinSeq X1).1 = X.1 by A3,A6,FINSEQ_3:112;
(ProdFinSeq X2).1 = X2.1 by MEASUR13:def 3;
hence (ProdFinSeq X1).1 = (ProdFinSeq X2).1
by A4,A7,A6,A2,XXREAL_0:2,FINSEQ_3:112;
end;
A8: for m be non zero Nat st P[m] holds P[m+1]
proof
let m be non zero Nat;
assume
A9: P[m];
assume
A10: m+1 <= j; then
A11: m < j by NAT_1:13; then
A12: m < k by A2,XXREAL_0:2;
A13: X1.(m+1) = X.(m+1) & X2.(m+1) = X.(m+1)
by A2,A3,A4,A10,FINSEQ_3:112,XXREAL_0:2;
(ProdFinSeq X1).(m+1) = [: (ProdFinSeq X1).m,X1.(m+1) :]
by A11,MEASUR13:def 3;
hence (ProdFinSeq X1).(m+1) = (ProdFinSeq X2).(m+1)
by A13,A9,A10,A12,NAT_1:13,MEASUR13:def 3;
end;
for m be non zero Nat holds P[m] from NAT_1:sch 10(A5,A8);
hence thesis by A1;
end;
::$N generalization \cite{MEASUR13}:6
theorem Th4:
for n be non zero Nat, D be (n+1)-element FinSequence,
D1 be n-element FinSequence st D1 = D|n holds
CarProduct D = [: CarProduct D1,D.(n+1) :]
proof
let n be non zero Nat, D be (n+1)-element FinSequence,
D1 be n-element FinSequence;
assume
A1: D1 = D|n;
defpred P[non zero Nat] means
$1 <= n implies (ProdFinSeq D).$1 = (ProdFinSeq D1).$1;
A2: P[1]
proof
assume 1 <= n; then
D.1 = D1.1 by A1,FINSEQ_3:112; then
(ProdFinSeq D).1 = D1.1 by MEASUR13:def 3;
hence (ProdFinSeq D).1 = (ProdFinSeq D1).1 by MEASUR13:def 3;
end;
A3: for k be non zero Nat st P[k] holds P[k+1]
proof
let k be non zero Nat;
assume
A4: P[k];
assume
A5: k+1 <= n; then
A6: k < n by NAT_1:13;
A7: D.(k+1) = D1.(k+1) by A1,A5,FINSEQ_3:112;
k < n+1 by A6,NAT_1:13; then
(ProdFinSeq D).(k+1) = [: (ProdFinSeq D).k,D.(k+1) :]
by MEASUR13:def 3;
hence (ProdFinSeq D).(k+1) = (ProdFinSeq D1).(k+1)
by A6,A7,A4,MEASUR13:def 3;
end;
A8: for k be non zero Nat holds P[k] from NAT_1:sch 10(A2,A3);
n < n+1 by NAT_1:13; then
CarProduct D = [: (ProdFinSeq D).n,D.(n+1) :] by MEASUR13:def 3;
hence CarProduct D = [: CarProduct D1,D.(n+1) :] by A8;
end;
Lm1:
for I,J be Subset of REAL, f be PartFunc of [:RNS_Real,RNS_Real:],RNS_Real,
g be PartFunc of [:REAL,REAL:],REAL st J is empty & [:I,J:] = dom f & f = g
holds Integral2(L-Meas,|.R_EAL g.|) |I is PartFunc of REAL,REAL
& Integral2(L-Meas,R_EAL g) |I is PartFunc of REAL,REAL
proof
let I,J be Subset of REAL,
f be PartFunc of [:RNS_Real,RNS_Real:],RNS_Real,
g be PartFunc of [:REAL,REAL:],REAL;
assume that
A1: J is empty and
A2: [:I,J:] = dom f and
A3: f = g;
set Rg =R_EAL g;
set F = Integral2(L-Meas,|.Rg.|);
reconsider FI = F|I as PartFunc of REAL,ExtREAL by PARTFUN1:11;
A4: dom F = REAL by FUNCT_2:def 1;
now let y be object;
assume y in rng FI; then
consider x be Element of REAL such that
A5: x in dom FI & y = FI.x by PARTFUN1:3;
reconsider Pg = ProjPMap1(|.Rg.|,x) as PartFunc of REAL,REAL
by MESFUN16:30;
A6: (Integral2(L-Meas,|.Rg.|)).x
= Integral(L-Meas,ProjPMap1(|.Rg.|,x)) by MESFUN12:def 8;
x in dom F /\ I by A5,RELAT_1:61; then
x in I by XBOOLE_0:def 4; then
dom ProjPMap1(|.Rg.|,x) = J by A2,A3,MESFUN16:27; then
(Integral2(L-Meas,|.Rg.|)).x = 0 by A1,A6,MESFUN16:1; then
(Integral2(L-Meas,|.Rg.|)).x in REAL by XREAL_0:def 1;
hence y in REAL by A5,A4,FUNCT_1:49;
end; then
rng FI c= REAL & dom FI c= REAL;
hence Integral2(L-Meas,|.R_EAL g.|) |I is PartFunc of REAL,REAL
by RELSET_1:4;
set G = Integral2(L-Meas,Rg);
reconsider GI = G|I as PartFunc of REAL,ExtREAL by PARTFUN1:11;
A7:dom G = REAL by FUNCT_2:def 1;
now let y be object;
assume y in rng GI; then
consider x be Element of REAL such that
A8: x in dom GI & y= GI.x by PARTFUN1:3;
reconsider Pg = ProjPMap1(Rg,x) as PartFunc of REAL,REAL
by MESFUN16:30;
A9: (Integral2(L-Meas,R_EAL g)).x
= Integral(L-Meas,ProjPMap1(R_EAL g,x)) by MESFUN12:def 8;
x in dom G /\ I by A8,RELAT_1:61; then
x in I by XBOOLE_0:def 4; then
dom ProjPMap1(R_EAL g,x) = J by A2,A3,MESFUN16:27; then
(Integral2(L-Meas,R_EAL g)).x = 0 by A1,A9,MESFUN16:1; then
(Integral2(L-Meas,Rg)).x in REAL by XREAL_0:def 1;
hence y in REAL by A8,A7,FUNCT_1:49;
end; then
rng GI c= REAL & dom GI c= REAL;
hence Integral2(L-Meas,R_EAL g) |I is PartFunc of REAL,REAL by RELSET_1:4;
end;
::$N generalization \cite{MESFUN16}:51
theorem
for I be Subset of REAL, J be closed_interval Subset of REAL,
f be PartFunc of [:RNS_Real,RNS_Real:],RNS_Real,
g be PartFunc of [:REAL,REAL:],REAL
st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g holds
Integral2(L-Meas,|.R_EAL g.|) |I is PartFunc of REAL,REAL
& Integral2(L-Meas,R_EAL g) |I is PartFunc of REAL,REAL
proof
let I be Subset of REAL, J be closed_interval Subset of REAL,
f be PartFunc of [:RNS_Real,RNS_Real:],RNS_Real,
g be PartFunc of [:REAL,REAL:],REAL;
assume that
A1: [:I,J:] = dom f and
A2: f is_continuous_on [:I,J:] and
A3: f = g;
per cases;
suppose J is non empty; then
reconsider J1 = J as non empty closed_interval Subset of REAL;
[:I,J1:] = dom f & f is_continuous_on [:I,J1:] by A1,A2;
hence thesis by A3,MESFUN16:51;
end;
suppose J is empty;
hence thesis by A1,A3,Lm1;
end;
end;
::$N generalization \cite{MEASUR15}:51
theorem Th6:
for n be non zero Nat, D be n-element FinSequence st not D is non-empty
holds CarProduct D = {}
proof
let n be non zero Nat, D be n-element FinSequence;
assume not D is non-empty; then
consider i be object such that
A1: i in dom D & D.i = {};
reconsider i as Nat by A1;
A2: dom D = Seg n by FINSEQ_1:89; then
A3: 1 <= i & i <= n by A1,FINSEQ_1:1;
reconsider i as non zero Nat by A2,A1,FINSEQ_1:1;
defpred P[non zero Nat] means
i <= $1 & $1 <= n implies (ProdFinSeq D).$1 = {};
A4: P[1]
proof
assume i <= 1 & 1 <= n; then
i = 1 by A3,XXREAL_0:1;
hence (ProdFinSeq D).1 = {} by A1,MEASUR13:def 3;
end;
A5: for k be non zero Nat st P[k] holds P[k+1]
proof
let k be non zero Nat;
assume
A6: P[k];
assume
A7: i <= k+1 & k+1 <= n; then
A8: k < n by NAT_1:13;
per cases;
suppose
A9: i = k+1;
(ProdFinSeq D).(k+1) = [: (ProdFinSeq D).k,D.(k+1) :]
by A8,MEASUR13:def 3;
hence (ProdFinSeq D).(k+1) = {} by A1,A9;
end;
suppose i <> k+1; then
i < k+1 by A7,XXREAL_0:1; then
(ProdFinSeq D).(k+1) = [: {},D.(k+1) :] by A6,A8,NAT_1:13,MEASUR13:def 3;
hence (ProdFinSeq D).(k+1) = {};
end;
end;
for k be non zero Nat holds P[k] from NAT_1:sch 10(A4,A5);
hence CarProduct D = {} by A3;
end;
::$N generalization \cite{MEASUR15}:6
theorem Th7:
for n be non zero Nat, X be n-element FinSequence, x be object
holds x in CarProduct X iff
ex px be n-element FinSequence st px in product X & x = PtCarProduct px
proof
let n be non zero Nat, X be n-element FinSequence, x be object;
per cases;
suppose X is non-empty; then
reconsider X1=X as non-empty n-element FinSequence;
x in CarProduct X1 iff
ex px be n-element FinSequence st px in product X1 & x = PtCarProduct px
by MEASUR15:6;
hence thesis;
end;
suppose not X is non-empty;
hence thesis by Th6,CARD_3:9;
end;
end;
::$N generalization \cite{MEASUR15}:39
theorem Th8:
for n be non zero Nat, D be n-element FinSequence st
for i be Nat st i in Seg n holds D.i is Element of L-Field
holds CarProduct D is Element of Prod_Field(L-Field n)
proof
let n be non zero Nat, D be n-element FinSequence;
assume
A1: for i be Nat st i in Seg n holds D.i is Element of L-Field;
per cases;
suppose D is non-empty; then
reconsider D1 = D as non-empty n-element FinSequence;
CarProduct D1 is Element of Prod_Field(L-Field n) by A1,MEASUR15:39;
hence thesis;
end;
suppose not D is non-empty; then
CarProduct D = {} by Th6;
hence thesis by MEASURE1:7;
end;
end;
::$N generalization \cite{MEASUR15}:41
theorem Th9:
for n be non zero Nat, D be n-element FinSequence st
for i be Nat st i in Seg n holds D.i is Interval holds
CarProduct D is Element of Prod_Field(L-Field n)
proof
let n be non zero Nat, D be n-element FinSequence;
assume
A1: for i be Nat st i in Seg n holds D.i is Interval;
now let i be Nat;
assume i in Seg n; then
D.i is Interval by A1;
hence D.i is Element of L-Field by MEASUR12:72,75;
end;
hence thesis by Th8;
end;
::$N generalization \cite{MEASUR15}:48
theorem Th10:
for n be non zero Nat, X,Y be n-element FinSequence st
for i be Nat st i in Seg n holds X.i c= Y.i holds
CarProduct X c= CarProduct Y
proof
let n be non zero Nat, X,Y be n-element FinSequence;
assume
A1: for i be Nat st i in Seg n holds X.i c= Y.i;
now let x be object;
assume x in CarProduct X; then
reconsider X1=X as non-empty n-element FinSequence by Th6;
dom X = Seg len X by FINSEQ_1:def 3; then
A2: dom X = Seg n by CARD_1:def 7;
dom Y = Seg len Y by FINSEQ_1:def 3; then
A3: dom Y = Seg n by CARD_1:def 7;
now assume not Y is non-empty; then
consider i be object such that
A4: i in dom Y & Y.i = {};
reconsider i as Nat by A4;
X1.i c= Y.i by A1,A3,A4;
hence contradiction by A2,A3,A4;
end; then
reconsider Y1=Y as non-empty n-element FinSequence;
CarProduct X1 c= CarProduct Y1 by A1,MEASUR15:48;
hence CarProduct X c= CarProduct Y;
end;
hence thesis;
end;
::$N generalization \cite{MEASUR15}:50
theorem Th11:
for n,k be non zero Nat, X be non empty set, D be n-element FinSequence st
k in Seg n & (for i be Nat st i in Seg n holds D.i is Subset of X)
holds (ProdFinSeq D).k is Subset of CarProduct(Seg k --> X)
proof
let n,k be non zero Nat, X be non empty set, D be n-element FinSequence;
assume that
A1: k in Seg n and
A2: for i be Nat st i in Seg n holds D.i is Subset of X;
defpred P[non zero Nat] means $1 in Seg n implies
(ProdFinSeq D).$1 is Subset of CarProduct(Seg $1 --> X);
A3: P[1]
proof
assume 1 in Seg n; then
A4: D.1 is Subset of X by A2;
1 in Seg 1; then
A5: (Seg 1 --> X).1 = X by FUNCOP_1:7;
(ProdFinSeq D).1 = D.1 by MEASUR13:def 3;
hence (ProdFinSeq D).1 is Subset of CarProduct(Seg 1 --> X)
by A4,A5,MEASUR13:def 3;
end;
A6: for i be non zero Nat st P[i] holds P[i+1]
proof
let i be non zero Nat;
assume
A7: P[i];
assume
A8: i+1 in Seg n; then
1 <= i+1 & i+1 <= n by FINSEQ_1:1; then
A9: 1 <= i & i < n by NAT_1:13,14;
(Seg(i+1)-->X) |i = (Seg(i+1) /\ Seg i)-->X by FUNCOP_1:12; then
A10: Seg i --> X = (Seg(i+1)-->X) |i by FINSEQ_3:18,XBOOLE_1:28;
i < i+1 & (Seg(i+1)-->X) | (i+1) = Seg(i+1)-->X by NAT_1:16; then
A11: (ProdFinSeq D).i is Subset of (ProdFinSeq(Seg(i+1)-->X)).i
by A7,A9,A10,Th3;
(Seg(i+1)-->X).(i+1) = X by FINSEQ_1:4,FUNCOP_1:7; then
A12: D.(i+1) is Subset of (Seg(i+1)-->X).(i+1) by A2,A8;
A13: (ProdFinSeq D).(i+1) = [: (ProdFinSeq D).i, D.(i+1) :]
by A9,MEASUR13:def 3;
CarProduct(Seg(i+1)-->X)
= [: (ProdFinSeq(Seg(i+1)-->X)).i,(Seg(i+1)-->X).(i+1):]
by NAT_1:16,MEASUR13:def 3;
hence (ProdFinSeq D).(i+1) is Subset of CarProduct(Seg (i+1) --> X)
by A13,A11,A12,ZFMISC_1:96;
end;
for k be non zero Nat holds P[k] from NAT_1:sch 10(A3,A6);
hence (ProdFinSeq D).k is Subset of CarProduct(Seg k --> X) by A1;
end;
::$N generalization \cite{MEASUR15}:73
theorem Th12:
for n be non zero Nat, D be n-element FinSequence st
for i be Nat st i in Seg n holds D.i c= REAL
holds product D = (CarProd(Seg n --> REAL)).:(CarProduct D)
proof
let n be non zero Nat, D be n-element FinSequence;
assume
A1: for i be Nat st i in Seg n holds D.i c= REAL;
set I = CarProd(Seg n --> RNS_Real);
A2: dom I = the carrier of CarProduct(Seg n --> RNS_Real) by FUNCT_2:def 1;
A3: CarProduct D c= the carrier of CarProduct(Seg n-->RNS_Real)
proof
per cases;
suppose D is non-empty; then
reconsider D1=D as non-empty n-element FinSequence;
CarProduct D1 c= CarProduct(Seg n-->REAL) by A1,MEASUR15:34;
hence thesis by MEASUR15:42;
end;
suppose not D is non-empty;
hence thesis by Th6;
end;
end;
for x be object holds x in product D iff x in I.:(CarProduct D)
proof
let x be object;
hereby assume
A4: x in product D; then
consider g being Function such that
A5: x = g & dom g = dom D
& for y being object st y in dom D holds g.y in D.y by CARD_3:def 5;
A6: dom D = Seg len D by FINSEQ_1:def 3; then
reconsider t=x as FinSequence by A5,FINSEQ_1:def 2;
dom D = Seg n by A6,CARD_1:def 7; then
Seg len t = Seg n by A5,FINSEQ_1:def 3; then
reconsider y = t as n-element FinSequence by FINSEQ_1:6,CARD_1:def 7;
A7: PtCarProduct y in CarProduct D by A4,Th7;
reconsider s = PtCarProduct y
as Point of CarProduct(Seg n-->RNS_Real) by A3,A4,Th7;
consider px be n-element FinSequence such that
A8: s = PtCarProduct px & I.s = px by MEASUR15:28;
px = y by A8,MEASUR15:5;
hence x in I.:(CarProduct D) by A2,A7,A8,FUNCT_1:def 6;
end;
assume x in I.:(CarProduct D); then
consider t being object such that
A9: t in dom I & t in CarProduct D & x = I.t by FUNCT_1:def 6;
reconsider s=t as Point of CarProduct(Seg n-->RNS_Real) by A9;
A10: ex px be n-element FinSequence st
s = PtCarProduct px & I.s = px by MEASUR15:28;
ex qx be n-element FinSequence st
qx in product D & t = PtCarProduct qx by A9,Th7;
hence x in product D by A9,A10,MEASUR15:5;
end; then
product D = I.:(CarProduct D) by TARSKI:2;
hence thesis by MEASUR15:70;
end;
begin :: Integrability of continuous rean $n$-variable functions
theorem Th13:
CarProduct(Seg 1 --> RNS_Real) = RNS_Real
& ElmFin(Seg 1 --> RNS_Real,1) = RNS_Real
& CarProduct(Seg 2 --> RNS_Real) = [:RNS_Real,RNS_Real:]
& ElmFin(Seg 2 --> RNS_Real,2) = RNS_Real
& CarProduct(Seg 3 --> RNS_Real) = [:RNS_Real,RNS_Real,RNS_Real:]
proof
set X = Seg 1 --> RNS_Real;
1 in Seg 1; then
X.1 = RNS_Real by FUNCOP_1:7;
hence CarProduct X = RNS_Real & ElmFin(Seg 1 --> RNS_Real,1) = RNS_Real
by MEASUR15:def 3,def 4;
set Y = Seg 2 --> RNS_Real;
A1: 1 in Seg 2 & 2 in Seg 2; then
A2: Y.1 = RNS_Real & Y.2 = RNS_Real by FUNCOP_1:7;
CarProduct SubFin(Y,1) = (ProdFinSeq Y).1 by MEASUR15:9; then
A3: CarProduct SubFin(Y,1) = RNS_Real by A2,MEASUR15:def 4;
ElmFin(Y,1+1) = RNS_Real by A2,MEASUR15:def 3;
hence CarProduct Y = [: RNS_Real,RNS_Real :] by A3,MEASUR15:10;
ElmFin(Y,2) = Y.2 by MEASUR15:def 3;
hence ElmFin(Y,2) = RNS_Real by A1,FUNCOP_1:7;
set Z = Seg 3 --> RNS_Real;
1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3; then
A4: Z.1 = RNS_Real & Z.2 = RNS_Real & Z.3 = RNS_Real by FUNCOP_1:7; then
A5: (ProdFinSeq Z).1 = RNS_Real by MEASUR15:def 4;
A6: ex Z21,Z22 be RealNormSpace st
Z21 = (ProdFinSeq Z).1 & Z22 = Z.(1+1)
& (ProdFinSeq Z).2 = [: Z21,Z22 :] by MEASUR15:def 4;
A7: CarProduct Z = [: CarProduct SubFin(Z,2),ElmFin(Z,2+1) :] by MEASUR15:10;
A8: CarProduct SubFin(Z,2) = [: RNS_Real,RNS_Real :] by A4,A5,A6,MEASUR15:9;
ElmFin(Z,3) = RNS_Real by A4,MEASUR15:def 3;
hence CarProduct Z = [: RNS_Real,RNS_Real,RNS_Real :]
by A7,A8,PRVECT_4:def 3;
end;
theorem Th14:
for n be non zero Nat,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
p be Element of CarProduct(Seg n --> REAL)
st f is_continuous_on dom f & f = g holds ProjPMap1(g,p) is continuous
proof
let n be non zero Nat,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
p be Element of CarProduct(Seg n --> REAL);
assume that
A1: f is_continuous_on dom f and
A2: f = g;
set P1 = ProjPMap1(g,p);
for y0 be Real st y0 in dom P1 holds P1 is_continuous_in y0
proof
let y0 be Real;
assume y0 in dom P1; then
A3: y0 in X-section(dom g,p) by MESFUN12:def 3;
A4: X-section(dom g,p) = {y where y is Element of REAL : [p,y] in dom g}
by MEASUR11:def 4; then
A5: ex y be Element of REAL st y = y0 & [p,y] in dom g by A3;
reconsider xx = p as Point of CarProduct(Seg n --> RNS_Real)
by MEASUR15:42;
reconsider yy0 = y0 as Point of RNS_Real by XREAL_0:def 1;
reconsider p0 = [xx,yy0] as
Point of [:CarProduct(Seg n --> RNS_Real),RNS_Real:];
for r be Real st 0 < r ex s be Real st 0 < s
& for y1 be Real st y1 in dom P1 & |. y1-y0 .| < s
holds |. P1.y1 - P1.y0 .| < r
proof
let r be Real;
assume 0 < r; then
consider s be Real such that
A6: 0 < s and
A7: for p1 be Point of [:CarProduct(Seg n --> RNS_Real),RNS_Real:]
st p1 in dom f & ||. p1-p0 .|| < s holds ||. f/.p1 - f/.p0 .|| < r
by A1,A2,A5,NFCONT_1:19;
now let y1 be Real;
assume that
A8: y1 in dom P1 and
A9: |. y1-y0 .| < s;
y1 in X-section(dom g,p) by A8,MESFUN12:def 3; then
A10: ex y be Element of REAL st y = y1 & [p,y] in dom g by A4;
reconsider yy1 = y1 as Point of RNS_Real by XREAL_0:def 1;
reconsider p1 = [xx,yy1]
as Point of [:CarProduct(Seg n --> RNS_Real),RNS_Real:];
A11: yy1-yy0 = y1-y0 by DUALSP03:4;
p1-p0 = [xx,yy1] + [-xx,-yy0] by PRVECT_3:18; then
p1-p0 = [xx-xx,yy1-yy0] by PRVECT_3:18; then
p1-p0 = [0.(CarProduct(Seg n --> RNS_Real)),yy1-yy0]
by RLVECT_1:15; then
||. p1-p0 .|| = sqrt(||. 0.(CarProduct(Seg n --> RNS_Real)) .||^2
+ ||. yy1-yy0 .||^2)
by NDIFF_8:1; then
||. p1-p0 .|| = ||. yy1-yy0 .|| by SQUARE_1:22; then
||. p1-p0 .|| = |. y1-y0 .| by A11,EUCLID:def 2; then
A12: ||. f/.p1-f/.p0 .|| < r by A9,A2,A10,A7;
P1.y1 = g.(p,y1) & P1.y0 = g.(p,y0) by A5,A10,MESFUN12:def 3; then
P1.y1 = f/.p1 & P1.y0 = f/.p0 by A2,A5,A10,PARTFUN1:def 6; then
P1.y1 - P1.y0 = f/.p1 - f/.p0 by DUALSP03:4;
hence |. P1.y1 - P1.y0 .| < r by A12,EUCLID:def 2;
end;
hence thesis by A6;
end;
hence P1 is_continuous_in y0 by FCONT_1:3;
end;
hence P1 is continuous;
end;
theorem
for X,Y,Z be non empty set, T be Function of X,Y, f be PartFunc of X,Z,
g be PartFunc of Y,Z st T is bijective & g = f*T" holds
dom g = T.:(dom f) & dom g = (.:T).(dom f)
proof
let X,Y,Z be non empty set, T be Function of X,Y,
f be PartFunc of X,Z, g be PartFunc of Y,Z;
assume
A1: T is bijective & g = f*T"; then
dom g = (T")"(dom f) by RELAT_1:147;
hence dom g = T.:(dom f) by A1,FUNCT_1:84;
hence dom g = (.:T).(dom f) by A1,MEASUR14:1;
end;
theorem Th16:
for n be non zero Nat,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
P2 be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real,
q be Element of REAL
st f is_continuous_on dom f & f = g & P2 = ProjPMap2(g,q) holds
P2 is_continuous_on dom P2
proof
let n be non zero Nat,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
P2 be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real,
q be Element of REAL;
assume that
A1: f is_continuous_on dom f and
A2: f = g and
A3: P2 = ProjPMap2(g,q);
for x0 be Point of CarProduct(Seg n --> RNS_Real) st x0 in dom P2 holds
P2 is_continuous_in x0
proof
let x0 be Point of CarProduct(Seg n --> RNS_Real);
assume
A4: x0 in dom P2; then
A5: x0 in Y-section(dom g,q) by A3,MESFUN12:def 4;
A6: Y-section(dom g,q)
= {x where x is Element of CarProduct(Seg n --> REAL) : [x,q] in dom g}
by MEASUR11:def 5; then
A7: ex x be Element of CarProduct(Seg n --> REAL)
st x = x0 & [x,q] in dom g by A5;
reconsider yy = q as Point of RNS_Real;
reconsider xx0 = x0 as Point of CarProduct(Seg n --> RNS_Real);
reconsider p0 = [xx0,yy]
as Point of [:CarProduct(Seg n --> RNS_Real),RNS_Real:];
for r be Real st 0 < r ex s be Real st 0 < s
& for x1 be Point of CarProduct(Seg n --> RNS_Real)
st x1 in dom P2 & ||. x1-x0 .|| < s
holds ||. P2/.x1 - P2/.x0 .|| < r
proof
let r be Real;
assume 0 < r; then
consider s0 be Real such that
A8: 0 < s0 and
A9: for p1 be Point of [:CarProduct(Seg n --> RNS_Real),RNS_Real:]
st p1 in dom f &
||. p1-p0 .|| < s0 holds ||. f/.p1 - f/.p0 .|| < r
by A1,A2,A7,NFCONT_1:19;
now let x1 be Point of CarProduct(Seg n --> RNS_Real);
assume that
A10: x1 in dom P2 and
A11: ||. x1-x0 .|| < s0;
x1 in Y-section(dom g,q) by A3,A10,MESFUN12:def 4; then
A12: ex x be Element of CarProduct(Seg n --> REAL)
st x = x1 & [x,q] in dom g by A6;
reconsider xx1 = x1 as Point of CarProduct(Seg n --> RNS_Real);
reconsider p1 = [xx1,yy]
as Point of [:CarProduct(Seg n --> RNS_Real),RNS_Real:];
p1-p0 = [xx1,yy] + [-xx0,-yy] by PRVECT_3:18; then
p1-p0 = [xx1-xx0,yy-yy] by PRVECT_3:18; then
p1-p0 = [xx1-xx0,0.RNS_Real] by RLVECT_1:15; then
||. p1-p0 .|| = sqrt(||. 0.RNS_Real .||^2 + ||. xx1-xx0 .||^2)
by NDIFF_8:1; then
A13: ||. p1-p0 .|| = ||. xx1-xx0 .|| by SQUARE_1:22;
P2.x1 = g.(x1,q) & P2.x0 = g.(x0,q) by A3,A7,A12,MESFUN12:def 4; then
P2.x1 = f/.p1 & P2.x0 = f/.p0 by A2,A7,A12,PARTFUN1:def 6; then
P2/.x1 = f/.p1 & P2/.x0 = f/.p0 by A4,A10,PARTFUN1:def 6;
hence ||. P2/.x1 - P2/.x0 .|| < r by A11,A2,A12,A9,A13;
end;
hence thesis by A8;
end;
hence P2 is_continuous_in x0 by A4,NFCONT_1:7;
end;
hence P2 is_continuous_on dom P2;
end;
theorem
for n be non zero Nat,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
q be Element of REAL holds
ProjPMap2(g,q)*(CarProd(Seg n --> REAL))" is PartFunc of REAL n,REAL
& dom(ProjPMap2(g,q)*(CarProd(Seg n --> REAL))")
= (CarProd(Seg n --> REAL)).:(dom ProjPMap2(g,q))
proof
let n be non zero Nat,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
q be Element of REAL;
set P2 = ProjPMap2(g,q);
A1: CarProd(Seg n --> REAL) is bijective by MEASUR14:12;
consider T be Function of
product(Seg n --> REAL),CarProduct(Seg n --> REAL) such that
A2: T is bijective &
T = (CarProd(Seg n --> REAL))" & .:T = (.:(CarProd(Seg n --> REAL)))"
by MEASUR14:12,14;
P2*T is PartFunc of REAL n,REAL by SRINGS_5:8;
hence P2*(CarProd(Seg n --> REAL))" is PartFunc of REAL n,REAL by A2;
dom(P2*(CarProd(Seg n --> REAL))") = T"(dom P2) by A2,RELAT_1:147;
hence dom(P2*(CarProd(Seg n --> REAL))")
= (CarProd(Seg n --> REAL)).:(dom P2) by A1,A2,FUNCT_1:84;
end;
theorem Th18:
for n be non zero Nat,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
p be Element of CarProduct(Seg n --> REAL)
st f is_continuous_on dom f & f = g holds ProjPMap1(|.g.|,p) is continuous
proof
let n be non zero Nat,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
p be Element of CarProduct(Seg n --> REAL);
assume that
A1: f is_continuous_on dom f and
A2: f = g;
set Y = dom ProjPMap1(g,p);
ProjPMap1(g,p) |Y is continuous by A1,A2,Th14; then
(abs ProjPMap1(g,p)) |Y is continuous by FCONT_1:21;
hence ProjPMap1(|.g.|,p) is continuous by MESFUN16:32;
end;
theorem Th19:
for n be non zero Nat,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
P2 be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real,
q be Element of REAL
st f is_continuous_on dom f & f = g & P2 = ProjPMap2(|.g.|,q) holds
P2 is_continuous_on dom P2
proof
let n be non zero Nat,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
P2 be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real,
q be Element of REAL;
assume that
A1: f is_continuous_on dom f and
A2: f = g and
A3: P2 = ProjPMap2(|.g.|,q);
reconsider P1 = ProjPMap2(g,q)
as PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real by MEASUR15:42;
A4: P1 is_continuous_on dom P1 by A1,A2,Th16;
dom P1 = dom |. ProjPMap2(g,q) .| by VALUED_1:def 11; then
A5: dom P1 = dom P2 by A3,MESFUN16:32;
for x0 be Point of CarProduct(Seg n --> RNS_Real)
st x0 in dom P2 holds P2 is_continuous_in x0
proof
let x0 be Point of CarProduct(Seg n --> RNS_Real);
assume
A6: x0 in dom P2;
reconsider yy = q as Point of RNS_Real;
reconsider p0 = [x0,yy]
as Point of [:CarProduct(Seg n --> RNS_Real),RNS_Real:];
A7: P1 is_continuous_in x0 by A4,A5,A6;
for r be Real st 0 < r ex s be Real st 0 < s
& for x1 be Point of CarProduct(Seg n --> RNS_Real)
st x1 in dom P2 & ||. x1-x0 .|| < s
holds ||. P2/.x1 - P2/.x0 .|| < r
proof
let r be Real;
assume 0 < r; then
consider s0 be Real such that
A8: 0 < s0 and
A9: for x1 be Point of CarProduct(Seg n --> RNS_Real)
st x1 in dom P1 & ||. x1-x0 .|| < s0
holds ||. P1/.x1 - P1/.x0 .|| < r by A7,NFCONT_1:7;
now let x1 be Point of CarProduct(Seg n --> RNS_Real);
assume that
A10: x1 in dom P2 and
A11: ||. x1-x0 .|| < s0;
A12: ||. P1/.x1 - P1/.x0 .|| < r by A5,A9,A10,A11;
reconsider xx1 = x1, xx0 = x0
as Element of CarProduct(Seg n --> REAL) by MEASUR15:42;
A13: xx1 in dom |. ProjPMap2(g,q) .| by A10,A3,MESFUN16:32;
A14: xx0 in dom |. ProjPMap2(g,q) .| by A6,A3,MESFUN16:32;
A15: P1/.x1 = ProjPMap2(g,q).xx1 by A5,A10,PARTFUN1:def 6;
ProjPMap2(|.g.|,q).xx1 = (|. ProjPMap2(g,q) .|).xx1 by MESFUN16:32; then
P2/.x1 = (|. ProjPMap2(g,q) .|).xx1 by A3,A10,PARTFUN1:def 6; then
P2/.x1 = |. ProjPMap2(g,q).xx1 .| by A13,VALUED_1:def 11; then
A16: P2/.x1 = ||. P1/.x1 .|| by A15,EUCLID:def 2;
A17: P1/.x0 = ProjPMap2(g,q).xx0 by A5,A6,PARTFUN1:def 6;
ProjPMap2(|.g.|,q).xx0 = (|. ProjPMap2(g,q) .|).xx0 by MESFUN16:32; then
P2/.x0 = (|. ProjPMap2(g,q) .|).xx0 by A3,A6,PARTFUN1:def 6; then
P2/.x0 = |. ProjPMap2(g,q).xx0 .| by A14,VALUED_1:def 11; then
P2/.x0 = ||. P1/.x0 .|| by A17,EUCLID:def 2; then
P2/.x1 - P2/.x0 = ||. P1/.x1 .|| - ||. P1/.x0 .||
by A16,DUALSP03:4; then
||. P2/.x1 - P2/.x0 .|| = |. ||. P1/.x1 .|| - ||. P1/.x0 .|| .|
by EUCLID:def 2; then
||. P2/.x1 - P2/.x0 .|| <= ||. P1/.x1 - P1/.x0 .|| by NORMSP_1:9;
hence ||. P2/.x1 - P2/.x0 .|| < r by A12,XXREAL_0:2;
end;
hence thesis by A8;
end;
hence P2 is_continuous_in x0 by A6,NFCONT_1:7;
end;
hence P2 is_continuous_on dom P2;
end;
theorem
for n be non zero Nat,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
q be Element of REAL holds
ProjPMap2(|.g.|,q)*(CarProd(Seg n --> REAL))" is PartFunc of REAL n,REAL
& dom(ProjPMap2(|.g.|,q)*(CarProd(Seg n --> REAL))")
= (CarProd(Seg n --> REAL)).:(dom ProjPMap2(|.g.|,q))
proof
let n be non zero Nat,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
q be Element of REAL;
set P2 = ProjPMap2(|.g.|,q);
A1: CarProd(Seg n --> REAL) is bijective by MEASUR14:12;
consider T be Function of
product(Seg n --> REAL),CarProduct(Seg n --> REAL) such that
A2: T is bijective &
T = (CarProd(Seg n --> REAL))" & .:T = (.:(CarProd(Seg n --> REAL)))"
by MEASUR14:12,14;
P2*T is PartFunc of REAL n,REAL by SRINGS_5:8;
hence P2*(CarProd(Seg n --> REAL))" is PartFunc of REAL n,REAL by A2;
dom(P2*(CarProd(Seg n --> REAL))") = T"(dom P2) by A2,RELAT_1:147;
hence dom(P2*(CarProd(Seg n --> REAL))")
= (CarProd(Seg n --> REAL)).:(dom P2) by A1,A2,FUNCT_1:84;
end;
theorem
for n be non zero Nat,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
p be Element of CarProduct(Seg n --> REAL)
st f is_uniformly_continuous_on dom f & f = g holds
ProjPMap1(g,p) is uniformly_continuous
proof
let n be non zero Nat,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
p be Element of CarProduct(Seg n --> REAL);
assume that
A1: f is_uniformly_continuous_on dom f and
A2: f = g;
set P1 = ProjPMap1(g,p);
for r be Real st 0 < r ex s be Real st 0 < s &
for y1,y2 be Real st y1 in dom P1 & y2 in dom P1 & |. y1-y2 .| < s
holds |. P1.y1 - P1.y2 .| < r
proof
let r be Real;
assume 0 < r; then
consider s be Real such that
A3: 0 < s and
A4: for p1,p2 be Point of [:CarProduct(Seg n --> RNS_Real),RNS_Real:]
st p1 in dom f & p2 in dom f & ||. p1-p2 .|| < s
holds ||. f/.p1 - f/.p2 .|| < r by A1;
now let y1,y2 be Real;
assume that
A5: y1 in dom P1 and
A6: y2 in dom P1 and
A7: |. y1-y2 .| < s;
A8: X-section(dom g,p) = {y where y is Element of REAL : [p,y] in dom g}
by MEASUR11:def 4;
A9: y1 in X-section(dom g,p) & y2 in X-section(dom g,p)
by A5,A6,MESFUN12:def 3; then
A10: ex y be Element of REAL st y = y1 & [p,y] in dom g by A8;
A11: ex y be Element of REAL st y = y2 & [p,y] in dom g by A8,A9;
reconsider xx = p as Point of CarProduct(Seg n --> RNS_Real)
by MEASUR15:42;
reconsider yy1 = y1 as Point of RNS_Real by XREAL_0:def 1;
reconsider yy2 = y2 as Point of RNS_Real by XREAL_0:def 1;
reconsider p1 = [xx,yy1], p2 = [xx,yy2]
as Point of [:CarProduct(Seg n --> RNS_Real),RNS_Real:];
A12: yy1-yy2 = y1-y2 by DUALSP03:4;
p1-p2 = [xx,yy1] + [-xx,-yy2] by PRVECT_3:18; then
p1-p2 = [xx-xx,yy1-yy2] by PRVECT_3:18; then
p1-p2 = [0.(CarProduct(Seg n --> RNS_Real)),yy1-yy2] by RLVECT_1:15; then
||. p1-p2 .|| = sqrt( ||. 0.(CarProduct(Seg n --> RNS_Real)) .||^2
+ ||. yy1-yy2 .||^2 ) by NDIFF_8:1; then
||. p1-p2 .|| = ||. yy1-yy2 .|| by SQUARE_1:22; then
||. p1-p2 .|| = |. y1-y2 .| by A12,EUCLID:def 2; then
A13: ||. f/.p1 - f/.p2 .|| < r by A4,A7,A2,A10,A11;
P1.y1 = g.(p,y1) & P1.y2 = g.(p,y2) by A10,A11,MESFUN12:def 3; then
P1.y1 = f/.p1 & P1.y2 = f/.p2 by A2,A10,A11,PARTFUN1:def 6; then
P1.y1 - P1.y2 = f/.p1 - f/.p2 by DUALSP03:4;
hence |. P1.y1 - P1.y2 .| < r by A13,EUCLID:def 2;
end;
hence thesis by A3;
end;
hence P1 is uniformly_continuous by FCONT_2:def 1;
end;
theorem
for n be non zero Nat,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
P2 be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real,
s be Element of REAL
st f is_uniformly_continuous_on dom f & f = g & P2 = ProjPMap2(g,s) holds
P2 is_uniformly_continuous_on dom P2
proof
let n be non zero Nat,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
P2 be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real,
q be Element of REAL;
assume that
A1: f is_uniformly_continuous_on dom f and
A2: f = g and
A3: P2 = ProjPMap2(g,q);
for r be Real st 0 < r ex s0 be Real st 0 < s0 &
for x1,x2 be Point of CarProduct(Seg n --> RNS_Real)
st x1 in dom P2 & x2 in dom P2 & ||. x1-x2 .|| < s0
holds ||. P2/.x1 - P2/.x2 .|| < r
proof
let r be Real;
assume 0 < r; then
consider s0 be Real such that
A4: 0 < s0 and
A5: for p1,p2 be Point of [:CarProduct(Seg n --> RNS_Real),RNS_Real:]
st p1 in dom f & p2 in dom f & ||. p1-p2 .|| < s0
holds ||. f/.p1 - f/.p2 .|| < r by A1;
now let x1,x2 be Point of CarProduct(Seg n --> RNS_Real);
assume that
A6: x1 in dom P2 and
A7: x2 in dom P2 and
A8: ||. x1-x2 .|| < s0;
A9: Y-section(dom g,q)
= {x where x is Element of CarProduct(Seg n --> REAL) : [x,q] in dom g}
by MEASUR11:def 5;
A10: x1 in Y-section(dom g,q) & x2 in Y-section(dom g,q)
by A3,A6,A7,MESFUN12:def 4; then
A11: ex x be Element of CarProduct(Seg n --> REAL) st x = x1 & [x,q] in dom g
by A9;
A12: ex x be Element of CarProduct(Seg n --> REAL) st x = x2 & [x,q] in dom g
by A9,A10;
reconsider yy = q as Point of RNS_Real;
reconsider p1 = [x1,yy], p2 = [x2,yy]
as Point of [:CarProduct(Seg n --> RNS_Real),RNS_Real:];
p1-p2 = [x1,yy] + [-x2,-yy] by PRVECT_3:18; then
p1-p2 = [x1-x2,yy-yy] by PRVECT_3:18; then
p1-p2 = [x1-x2,0.RNS_Real] by RLVECT_1:15; then
||. p1-p2 .|| = sqrt( ||. 0.RNS_Real .||^2 + ||. x1-x2 .||^2 )
by NDIFF_8:1; then
A13: ||. p1-p2 .|| = ||. x1-x2 .|| by SQUARE_1:22;
ProjPMap2(g,q).x1 = g.(x1,q) & ProjPMap2(g,q).x2 = g.(x2,q)
by A11,A12,MESFUN12:def 4; then
P2/.x1 = g.(x1,q) & P2/.x2 = g.(x2,q) by A3,A6,A7,PARTFUN1:def 6; then
P2/.x1 = f/.p1 & P2/.x2 = f/.p2 by A2,A11,A12,PARTFUN1:def 6;
hence ||. P2/.x1 - P2/.x2 .|| < r by A5,A8,A2,A11,A12,A13;
end;
hence thesis by A4;
end;
hence P2 is_uniformly_continuous_on dom P2;
end;
theorem Th23:
for n be non zero Nat,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg1 be PartFunc of REAL,REAL,
x be Element of CarProduct(Seg n --> REAL)
st f is_continuous_on dom f & f = g & Pg1 = ProjPMap1(R_EAL g,x) holds
Pg1 is continuous
proof
let n be non zero Nat,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg1 be PartFunc of REAL,REAL,
x be Element of CarProduct(Seg n --> REAL);
assume that
A1: f is_continuous_on dom f and
A2: f = g and
A3: Pg1 = ProjPMap1(R_EAL g,x);
Pg1 = R_EAL(ProjPMap1(g,x)) by A3,MESFUN16:31; then
Pg1 = ProjPMap1(g,x) by MESFUNC5:def 7;
hence thesis by A1,A2,Th14;
end;
theorem Th24:
for n be non zero Nat,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg2 be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real,
y be Element of REAL
st f is_continuous_on dom f & f = g & Pg2 = ProjPMap2(R_EAL g,y) holds
Pg2 is_continuous_on dom Pg2
proof
let n be non zero Nat,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg2 be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real,
y be Element of REAL;
assume that
A1: f is_continuous_on dom f and
A2: f = g and
A3: Pg2 = ProjPMap2(R_EAL g,y);
Pg2 = R_EAL(ProjPMap2(g,y)) by A3,MESFUN16:31;
hence thesis by A1,A2,Th16,MESFUNC5:def 7;
end;
theorem Th25:
for n be non zero Nat,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg1 be PartFunc of REAL,REAL,
x be Element of CarProduct(Seg n --> REAL)
st f is_continuous_on dom f & f = g & Pg1 = ProjPMap1(|.R_EAL g.|,x)
holds Pg1 is continuous
proof
let n be non zero Nat,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg1 be PartFunc of REAL,REAL,
x be Element of CarProduct(Seg n --> REAL);
assume that
A1: f is_continuous_on dom f and
A2: f = g and
A3: Pg1 = ProjPMap1(|.R_EAL g.|,x);
Pg1 = |. R_EAL(ProjPMap1(g,x)) .| by A3,MESFUN16:31; then
Pg1 = R_EAL abs(ProjPMap1(g,x)) by MESFUNC6:1; then
Pg1 = R_EAL ProjPMap1(|.g.|,x) by MESFUN16:32; then
Pg1 = ProjPMap1(|.g.|,x) by MESFUNC5:def 7;
hence thesis by A1,A2,Th18;
end;
theorem Th26:
for n be non zero Nat,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg2 be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real,
y be Element of REAL
st f is_continuous_on dom f & f = g & Pg2 = ProjPMap2(|.R_EAL g.|,y)
holds Pg2 is_continuous_on dom Pg2
proof
let n be non zero Nat,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg2 be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real,
y be Element of REAL;
assume that
A1: f is_continuous_on dom f and
A2: f = g and
A3: Pg2 = ProjPMap2(|.R_EAL g.|,y);
Pg2 = |. R_EAL(ProjPMap2(g,y)) .| by A3,MESFUN16:31; then
Pg2 = R_EAL abs(ProjPMap2(g,y)) by MESFUNC6:1; then
Pg2 = R_EAL ProjPMap2(|.g.|,y) by MESFUN16:32;
hence thesis by A1,A2,Th19,MESFUNC5:def 7;
end;
theorem Th27:
for n be non zero Nat, I be Subset of CarProduct(Seg n --> REAL),
J be non empty closed_interval Subset of REAL,
x be Element of CarProduct(Seg n --> REAL),
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg1 be PartFunc of REAL,REAL
st x in I & dom f = [:I,J:] & f is_continuous_on [:I,J:] & f = g
& Pg1 = ProjPMap1(R_EAL g,x)
holds Pg1|J is bounded & Pg1 is_integrable_on J
proof
let n be non zero Nat,
I be Subset of CarProduct(Seg n --> REAL),
J be non empty closed_interval Subset of REAL,
x be Element of CarProduct(Seg n --> REAL),
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg1 be PartFunc of REAL,REAL;
assume that
A1: x in I and
A2: dom f = [:I,J:] and
A3: f is_continuous_on [:I,J:] and
A4: f = g and
A5: Pg1 = ProjPMap1(R_EAL g,x);
Pg1 = R_EAL(ProjPMap1(g,x)) by A5,MESFUN16:31; then
A6: Pg1 = ProjPMap1(g,x) by MESFUNC5:def 7;
dom Pg1 = J by A1,A2,A4,A5,MESFUN16:27;
hence thesis by A6,A2,A3,A4,Th14,INTEGRA5:10,11;
end;
theorem Th28:
for n be non zero Nat, I be Subset of CarProduct(Seg n --> REAL),
J be non empty closed_interval Subset of REAL,
x be Element of CarProduct(Seg n --> REAL),
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg1 be PartFunc of REAL,REAL
st x in I & dom f = [:I,J:] & f is_continuous_on [:I,J:] & f = g
& Pg1 = ProjPMap1(|.R_EAL g.|,x)
holds Pg1|J is bounded & Pg1 is_integrable_on J
proof
let n be non zero Nat,
I be Subset of CarProduct(Seg n --> REAL),
J be non empty closed_interval Subset of REAL,
x be Element of CarProduct(Seg n --> REAL),
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg1 be PartFunc of REAL,REAL;
assume that
A1: x in I and
A2: dom f = [:I,J:] and
A3: f is_continuous_on [:I,J:] and
A4: f = g and
A5: Pg1 = ProjPMap1(|.R_EAL g.|,x);
dom Pg1 = J by A1,A2,A4,A5,MESFUN16:27;
hence thesis by A2,A3,A4,A5,Th25,INTEGRA5:10,11;
end;
theorem Th29:
for n be non zero Nat, I be Subset of CarProduct(Seg n --> REAL),
J be closed_interval Subset of REAL,
x be Element of CarProduct(Seg n --> REAL),
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg1 be PartFunc of REAL,REAL
st dom f = [:I,J:] & f is_continuous_on [:I,J:] & f = g &
Pg1 = ProjPMap1(R_EAL g,x) holds Pg1 is_integrable_on L-Meas
proof
let n be non zero Nat,
I be Subset of CarProduct(Seg n --> REAL),
J be closed_interval Subset of REAL,
x be Element of CarProduct(Seg n --> REAL),
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg1 be PartFunc of REAL,REAL;
assume that
A1: dom f = [:I,J:] and
A2: f is_continuous_on [:I,J:] and
A3: f = g and
A4: Pg1 = ProjPMap1(R_EAL g,x);
per cases;
suppose
A5: x in I; then
A6: dom Pg1 = J by A1,A3,A4,MESFUN16:27;
A7: J is Element of L-Field by MEASUR10:5,MEASUR12:75;
now assume J <> {}; then
reconsider J as non empty closed_interval Subset of REAL;
Pg1||J is bounded & Pg1 is_integrable_on J by A5,A1,A2,A3,A4,Th27;
hence Pg1 is_integrable_on L-Meas by A6,A7,MESFUN14:49;
end;
hence Pg1 is_integrable_on L-Meas by A6,Th1;
end;
suppose not x in I; then
dom Pg1 = {} by A1,A3,A4,MESFUN16:27;
hence Pg1 is_integrable_on L-Meas by Th1;
end;
end;
theorem Th30:
for n be non zero Nat, I be Subset of CarProduct(Seg n --> REAL),
J be non empty closed_interval Subset of REAL,
x be Element of CarProduct(Seg n --> REAL),
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg1 be PartFunc of REAL,REAL
st x in I & dom f = [:I,J:] & f is_continuous_on [:I,J:] & f = g
& Pg1 = ProjPMap1(R_EAL g,x) holds
integral(Pg1,J) = Integral(L-Meas,Pg1)
& integral(Pg1,J) = Integral(L-Meas,(ProjPMap1(R_EAL g,x)))
& integral(Pg1,J) = (Integral2(L-Meas,R_EAL g)).x
proof
let n be non zero Nat,
I be Subset of CarProduct(Seg n --> REAL),
J be non empty closed_interval Subset of REAL,
x be Element of CarProduct(Seg n --> REAL),
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg1 be PartFunc of REAL,REAL;
assume that
A1: x in I and
A2: dom f = [:I,J:] and
A3: f is_continuous_on [:I,J:] and
A4: f = g and
A5: Pg1 = ProjPMap1(R_EAL g,x);
A6: J is Element of L-Field by MEASUR10:5,MEASUR12:75;
A7: dom Pg1 = J by A1,A2,A4,A5,MESFUN16:27;
Pg1||J is bounded & Pg1 is_integrable_on J by A1,A2,A3,A4,A5,Th27;
hence integral(Pg1,J) = Integral(L-Meas,Pg1) by A6,A7,MESFUN14:49;
hence integral(Pg1,J) = Integral(L-Meas,ProjPMap1(R_EAL g,x))
by A5,MESFUNC5:def 7;
hence thesis by MESFUN12:def 8;
end;
theorem Th31:
for n be non zero Nat,
I be Subset of CarProduct(Seg n --> REAL),
J be closed_interval Subset of REAL,
x be Element of CarProduct(Seg n --> REAL),
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg1 be PartFunc of REAL,REAL
st dom f = [:I,J:] & f is_continuous_on [:I,J:] & f = g
& Pg1 = ProjPMap1(|.R_EAL g.|,x) holds Pg1 is_integrable_on L-Meas
proof
let n be non zero Nat,
I be Subset of CarProduct(Seg n --> REAL),
J be closed_interval Subset of REAL,
x be Element of CarProduct(Seg n --> REAL),
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg1 be PartFunc of REAL,REAL;
assume that
A1: dom f = [:I,J:] and
A2: f is_continuous_on [:I,J:] and
A3: f = g and
A4: Pg1 = ProjPMap1(|.R_EAL g.|,x);
per cases;
suppose x in I; then
A5: dom Pg1 = J by A1,A3,A4,MESFUN16:27;
A6: J is Element of L-Field by MEASUR10:5,MEASUR12:75;
now assume J <> {}; then
reconsider J as non empty closed_interval Subset of REAL;
Pg1|J is bounded & Pg1 is_integrable_on J
by A1,A2,A3,A4,A5,Th25,INTEGRA5:10,11;
hence Pg1 is_integrable_on L-Meas by A5,A6,MESFUN14:49;
end;
hence Pg1 is_integrable_on L-Meas by A5,Th1;
end;
suppose not x in I; then
dom Pg1 = {} by A1,A3,A4,MESFUN16:27;
hence Pg1 is_integrable_on L-Meas by Th1;
end;
end;
theorem Th32:
for n be non zero Nat,
I be Subset of CarProduct(Seg n --> REAL),
J be non empty closed_interval Subset of REAL,
x be Element of CarProduct(Seg n --> REAL),
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg1 be PartFunc of REAL,REAL
st x in I & dom f = [:I,J:] & f is_continuous_on [:I,J:] & f = g
& Pg1 = ProjPMap1(|.R_EAL g.|,x) holds
integral(Pg1,J) = Integral(L-Meas,Pg1)
& integral(Pg1,J) = Integral(L-Meas,(ProjPMap1(|.R_EAL g.|,x)))
& integral(Pg1,J) = (Integral2(L-Meas,|.R_EAL g.|)).x
proof
let n be non zero Nat,
I be Subset of CarProduct(Seg n --> REAL),
J be non empty closed_interval Subset of REAL,
x be Element of CarProduct(Seg n --> REAL),
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg1 be PartFunc of REAL,REAL;
assume that
A1: x in I and
A2: dom f = [:I,J:] and
A3: f is_continuous_on [:I,J:] and
A4: f = g and
A5: Pg1 = ProjPMap1(|.R_EAL g.|,x);
A6: J is Element of L-Field by MEASUR10:5,MEASUR12:75;
A7: dom Pg1 = J by A1,A2,A4,A5,MESFUN16:27;
A8: Pg1|J is bounded & Pg1 is_integrable_on J by A1,A2,A3,A4,A5,Th28; then
integral(Pg1,J) = Integral(L-Meas,Pg1) by A7,A6,MESFUN14:49; then
integral(Pg1,J) = Integral(L-Meas,ProjPMap1(|.R_EAL g.|,x))
by A5,MESFUNC5:def 7;
hence thesis by A8,A7,A6,MESFUN14:49,MESFUN12:def 8;
end;
theorem Th33:
for n be non zero Nat,
I be Subset of CarProduct(Seg n --> REAL), J be Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
E be Element of sigma measurable_rectangles(Prod_Field(L-Field n),L-Field)
st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & E = [:I,J:] holds
g is E-measurable
proof
let n be non zero Nat,
I be Subset of CarProduct(Seg n --> REAL), J be Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
E be Element of sigma measurable_rectangles(Prod_Field(L-Field n),L-Field);
assume that
A1: [:I,J:] = dom f and
A2: f is_continuous_on [:I,J:] and
A3: f = g and
A4: E = [:I,J:];
for r being Real holds E /\ (less_dom (g,r))
in sigma measurable_rectangles(Prod_Field(L-Field n),L-Field)
proof
let r be Real;
A5: less_dom(g,r) = g" ( ].-infty,r.[ ) by MESFUN16:17;
consider H be Subset of [:CarProduct(Seg n --> RNS_Real),RNS_Real:]
such that
A6: H /\ E = f" ( ].-infty,r.[ ) & H is open by A1,A2,A4,MESFUN16:24;
CarProduct(Seg(n+1) --> RNS_Real)
= [:CarProduct(Seg n --> RNS_Real),RNS_Real:] by MEASUR15:38; then
A7: H in Prod_Field(L-Field (n+1)) by A6,MEASUR15:65;
Prod_Field(L-Field(n+1))
= sigma measurable_rectangles(Prod_Field(L-Field n),L-Field)
by MEASUR14:44; then
f" ( ].-infty,r.[ ) in
sigma measurable_rectangles(Prod_Field(L-Field n),L-Field)
by A6,A7,FINSUB_1:def 2;
hence E /\ (less_dom (g,r)) in
sigma measurable_rectangles(Prod_Field(L-Field n),L-Field)
by A3,A5,FINSUB_1:def 2;
end;
hence g is E-measurable by MESFUNC6:12;
end;
theorem Th34:
for n be non zero Nat, I be Subset of CarProduct(Seg n --> REAL),
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL
st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g holds
Integral2(L-Meas,|.R_EAL g.|) is PartFunc of CarProduct(Seg n --> REAL),REAL
& Integral2(L-Meas,R_EAL g) is PartFunc of CarProduct(Seg n --> REAL),REAL
proof
let n be non zero Nat, I be Subset of CarProduct(Seg n --> REAL),
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL;
assume that
A1: [:I,J:] = dom f and
A2: f is_continuous_on [:I,J:] and
A3: f = g;
set Rg = R_EAL g;
set F = Integral2(L-Meas,|.Rg.|);
A4: dom F = CarProduct(Seg n --> REAL) by FUNCT_2:def 1;
now let y be object;
assume y in rng F; then
consider x be Element of CarProduct(Seg n --> REAL) such that
A5: x in dom F & y = F.x by PARTFUN1:3;
reconsider Pg = ProjPMap1(|.Rg.|,x) as PartFunc of REAL,REAL
by MESFUN16:30;
per cases;
suppose
A6: x in I; then
A7: dom Pg = J by A1,A3,MESFUN16:27;
per cases;
suppose J <> {}; then
reconsider J as non empty closed_interval Subset of REAL;
(Integral2(L-Meas,|.Rg.|)).x = integral(Pg,J) by A1,A2,A3,A6,Th32;
hence y in REAL by A5,XREAL_0:def 1;
end;
suppose J = {}; then
Integral(L-Meas,ProjPMap1(|.Rg.|,x)) = 0 by A7,MESFUN16:1; then
(Integral2(L-Meas,|.Rg.|)).x = 0 by MESFUN12:def 8;
hence y in REAL by A5,XREAL_0:def 1;
end;
end;
suppose not x in I; then
dom Pg = {} by A1,A3,MESFUN16:27; then
Integral(L-Meas,ProjPMap1(|.Rg.|,x)) = 0 by MESFUN16:1; then
(Integral2(L-Meas,|.Rg.|)).x = 0 by MESFUN12:def 8;
hence y in REAL by A5,XREAL_0:def 1;
end;
end; then
rng F c= REAL;
hence Integral2(L-Meas,|.R_EAL g.|)
is PartFunc of CarProduct(Seg n --> REAL),REAL by A4,RELSET_1:4;
set G = Integral2(L-Meas,Rg);
now let y be object;
assume y in rng G; then
consider x be Element of CarProduct(Seg n --> REAL) such that
A8: x in dom G & y= G.x by PARTFUN1:3;
reconsider Pg = ProjPMap1(Rg,x) as PartFunc of REAL,REAL by MESFUN16:30;
per cases;
suppose
A9: x in I; then
A10: dom Pg = J by A1,A3,MESFUN16:27;
per cases;
suppose J <> {}; then
reconsider J as non empty closed_interval Subset of REAL;
(Integral2(L-Meas,Rg)).x = integral(Pg,J) by A9,A1,A2,A3,Th30;
hence y in REAL by A8,XREAL_0:def 1;
end;
suppose J = {}; then
Integral(L-Meas,ProjPMap1(R_EAL g,x)) = 0 by A10,MESFUN16:1; then
(Integral2(L-Meas,Rg)).x = 0 by MESFUN12:def 8;
hence y in REAL by A8,XREAL_0:def 1;
end;
end;
suppose not x in I; then
dom Pg = {} by A1,A3,MESFUN16:27; then
Integral(L-Meas,ProjPMap1(R_EAL g,x)) = 0 by MESFUN16:1; then
(Integral2(L-Meas,Rg)).x = 0 by MESFUN12:def 8;
hence y in REAL by A8,XREAL_0:def 1;
end;
end; then
rng G c= REAL & dom G c= CarProduct(Seg n --> REAL);
hence Integral2(L-Meas,R_EAL g) is
PartFunc of CarProduct(Seg n --> REAL),REAL by RELSET_1:4;
end;
theorem Th35:
for n be non zero Nat, D be n-element FinSequence,
J be closed_interval Subset of REAL,
E be Subset of [:CarProduct(Seg n --> RNS_Real),RNS_Real:]
st (for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL)
& E = [:CarProduct D,J:] holds E is compact
proof
let n be non zero Nat,
D be n-element FinSequence,
J be closed_interval Subset of REAL,
E be Subset of [:CarProduct(Seg n --> RNS_Real),RNS_Real:];
assume that
A1: for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL and
A2: E = [:CarProduct D,J:];
A3: not D is non-empty implies CarProduct D = {} by Th6;
now assume D is non-empty; then
consider I be Subset of CarProduct(Seg n --> RNS_Real) such that
A4: I = CarProduct D & I is compact by A1,MEASUR15:51;
reconsider J1 = J as Subset of RNS_Real;
J1 is compact by MESFUN16:7;
hence E is compact by A2,A4,MESFUN16:8;
end;
hence thesis by A2,A3;
end;
theorem Th36:
for n be non zero Nat, E be set,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL
st f = g & E c= dom f holds
f is_uniformly_continuous_on E iff
for e be Real st 0 < e ex r be Real st 0 < r
& for x1,x2 be Point of CarProduct(Seg n --> RNS_Real), y1,y2 be Real
st [x1,y1] in E & [x2,y2] in E & ||.x2-x1.|| < r & |.y2-y1.| < r
holds |. g.([x2,y2])-g.([x1,y1]) .| < e
proof
let n be non zero Nat, E be set,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL;
assume that
A1: f = g and
A2: E c= dom f;
hereby assume
A3: f is_uniformly_continuous_on E;
thus for e be Real st 0 < e ex r be Real st 0 < r
& for x1,x2 be Point of CarProduct(Seg n --> RNS_Real), y1,y2 be Real
st [x1,y1] in E & [x2,y2] in E & ||.x2-x1.|| < r & |.y2-y1.| < r
holds |. g.([x2,y2])-g.([x1,y1]) .| < e
proof
let e be Real;
assume 0 < e; then
consider r be Real such that
A4: 0 < r
& for z1,z2 be Point of [:CarProduct(Seg n --> RNS_Real),RNS_Real:] st
z1 in E & z2 in E & ||. z1-z2 .|| < r holds ||. f/.z1-f/.z2 .|| < e
by A3;
set r1=r/2;
take r1;
thus 0< r1 by A4,XREAL_1:215;
let x1,x2 be Point of CarProduct(Seg n --> RNS_Real), y1,y2 be Real;
assume
A5: [x1,y1] in E & [x2,y2] in E & ||.x2-x1.|| < r1 & |.y2-y1.| < r1;
reconsider yy1=y1,yy2=y2 as Point of RNS_Real
by XREAL_0:def 1;
reconsider z1 = [x1,yy1], z2 = [x2,yy2]
as Point of [:CarProduct(Seg n --> RNS_Real),RNS_Real:];
-z2 = [-x2,-yy2] by PRVECT_3:18; then
A6: z1-z2 = [x1-x2,yy1-yy2] by PRVECT_3:18;
A7: yy1-yy2 = y1-y2 by DUALSP03:4;
A8: ||.x1-x2.|| = ||.x2-x1.|| by NORMSP_1:7;
||.yy1-yy2.|| = |.y1-y2.| by A7,EUCLID:def 2; then
||.yy1-yy2.|| = |.y2-y1.| by COMPLEX1:60; then
A9: ||.z1 - z2.|| <= ||.x2-x1.|| + |.y2-y1.| by A6,A8,NDIFF_9:6;
||.x2-x1.|| + |.y2-y1.| < r1 + r1 by A5,XREAL_1:8; then
||.z1 - z2.|| < r by A9,XXREAL_0:2; then
A10: ||. f/.z1-f/.z2 .|| < e by A5,A4;
A11: f/.z1 = g.([x1,y1]) by A1,A2,A5,PARTFUN1:def 6;
f/.z2 = f.z2 by A2,A5,PARTFUN1:def 6; then
f/.z1 - f/.z2 = g.([x1,y1]) -g.([x2,y2]) by A1,A11,DUALSP03:4; then
||. f/.z1-f/.z2.|| = |. g.([x1,y1]) - g.([x2,y2]) .| by EUCLID:def 2;
hence thesis by A10,COMPLEX1:60;
end;
end;
assume
A12:for e be Real st 0 < e ex r be Real st 0 < r
& for x1,x2 be Point of CarProduct(Seg n --> RNS_Real), y1,y2 be Real
st [x1,y1] in E & [x2,y2] in E & ||.x2-x1.|| < r & |.y2-y1.| < r
holds |. g.([x2,y2])-g.([x1,y1]) .| < e;
for e be Real st 0 < e holds
ex r be Real st 0 < r &
for z1,z2 be Point of [:CarProduct(Seg n --> RNS_Real),RNS_Real:]
st z1 in E & z2 in E & ||. z1-z2 .|| < r holds ||. f/.z1-f/.z2 .|| < e
proof
let e be Real;
assume 0 < e; then
consider r be Real such that
A13: 0 < r &
for x1,x2 be Point of CarProduct(Seg n --> RNS_Real), y1,y2 be Real
st [x1,y1] in E & [x2,y2] in E & ||.x2-x1.|| < r & |.y2-y1.| < r holds
|. g.([x2,y2])-g.([x1,y1]) .| < e by A12;
take r;
thus 0 < r by A13;
thus for z1,z2 be Point of [:CarProduct(Seg n --> RNS_Real),RNS_Real:]
st z1 in E & z2 in E & ||. z1-z2 .|| < r holds ||. f/.z1-f/.z2 .|| < e
proof
let z1,z2 be Point of [:CarProduct(Seg n --> RNS_Real),RNS_Real:];
assume that
A14: z1 in E & z2 in E and
A15: ||. z1-z2 .|| < r;
consider x1 be Point of CarProduct(Seg n --> RNS_Real),
yy1 be Point of RNS_Real such that
A16: z1 = [x1,yy1] by PRVECT_3:18;
consider x2 be Point of CarProduct(Seg n --> RNS_Real),
yy2 be Point of RNS_Real such that
A17: z2 = [x2,yy2] by PRVECT_3:18;
reconsider y1 = yy1, y2 = yy2 as Real;
-z2 = [-x2,-yy2] by A17,PRVECT_3:18; then
A18: z1-z2 = [x1-x2,yy1-yy2] by A16,PRVECT_3:18;
A19: yy1-yy2 = y1-y2 by DUALSP03:4;
A20: ||.x1-x2.|| = ||.x2-x1.|| by NORMSP_1:7;
||.yy1-yy2.|| = |.y1-y2.| by A19,EUCLID:def 2; then
||.yy1-yy2.|| = |.y2-y1.| by COMPLEX1:60; then
||. x2-x1 .|| <= ||. z1-z2 .|| & |. y2-y1 .| <= ||. z1-z2 .||
by A18,A20,NDIFF_8:21; then
||. x2-x1 .|| < r & |. y2-y1 .| < r by A15,XXREAL_0:2; then
A21: |. g.([x2,y2])-g.([x1,y1]) .| < e by A13,A14,A16,A17;
A22: f/.z1 = g.([x1,y1]) by A1,A2,A14,A16,PARTFUN1:def 6;
f/.z2 = f.z2 by A2,A14,PARTFUN1:def 6; then
f/.z1 - f/.z2 = g.([x1,y1]) - g.([x2,y2]) by A1,A17,A22,DUALSP03:4; then
||. f/.z1-f/.z2 .|| = |. g.([x1,y1]) - g.([x2,y2]) .| by EUCLID:def 2;
hence thesis by A21,COMPLEX1:60;
end;
end;
hence f is_uniformly_continuous_on E by A2;
end;
theorem Th37:
for n be non zero Nat, D be n-element FinSequence,
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL
st (for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL)
& f = g & f is_continuous_on [:CarProduct D,J:]
holds
for e be Real st 0 < e ex r be Real st 0 < r
& for x1,x2 be Point of CarProduct(Seg n --> RNS_Real), y1,y2 be Real
st [x1,y1] in [:CarProduct D,J:] & [x2,y2] in [:CarProduct D,J:]
& ||.x2-x1.|| < r & |.y2-y1.| < r
holds |. g.([x2,y2])-g.([x1,y1]) .| < e
proof
let n be non zero Nat, D be n-element FinSequence,
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL;
assume that
A1: for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL and
A2: f = g and
A3: f is_continuous_on [:CarProduct D,J:];
for i be Nat st i in Seg n holds D.i is Subset of REAL by A1; then
A4: CarProduct D is Subset of CarProduct(Seg n --> REAL)
by FINSEQ_1:3,Th11;
ex I be Subset of CarProduct(Seg n --> RNS_Real) st
I = CarProduct D & I is compact
proof
now assume not D is non-empty; then
A5: CarProduct D = {} by Th6;
reconsider I = CarProduct D
as Subset of CarProduct(Seg n --> RNS_Real) by A4,MEASUR15:42;
I is compact by A5;
hence thesis;
end;
hence thesis by A1,MEASUR15:51;
end; then
consider I be Subset of CarProduct(Seg n --> RNS_Real) such that
A6: I = CarProduct D & I is compact;
reconsider J1 = J as Subset of RNS_Real;
A7: J1 is compact by MESFUN16:7;
reconsider E = [:CarProduct D,J1:] as
Subset of [:CarProduct(Seg n --> RNS_Real),RNS_Real:] by A6,A7,MESFUN16:8;
E is compact by A1,Th35; then
f is_uniformly_continuous_on [:CarProduct D,J:] by A3,NFCONT_2:10;
hence thesis by A2,Th36;
end;
theorem Th38:
for X be set, S be RealNormSpace, f be PartFunc of S,RNS_Real,
g be PartFunc of X,REAL st f = g holds ||.f.|| = |.g.|
proof
let X be set, S be RealNormSpace,
f be PartFunc of S,RNS_Real,
g be PartFunc of X,REAL;
assume
A1: f = g;
A2: dom ||.f.|| = dom f by NORMSP_0:def 3; then
A3: dom ||.f.|| = dom |.g.| by A1,VALUED_1:def 11;
for x be object st x in dom ||.f.|| holds (||.f.||).x = (|.g.|).x
proof
let x be object;
assume
A4: x in dom ||.f.||; then
A5: (||.f.||).x = ||. f/.x .|| by NORMSP_0:def 3;
f/.x = f.x by A4,A2,PARTFUN1:def 6; then
||. f/.x .|| = |. g.x .| by A1,EUCLID:def 2;
hence (||.f.||).x = (|.g.|).x by A3,A4,A5,VALUED_1:def 11;
end;
hence ||.f.|| = |.g.| by A2,A1,VALUED_1:def 11;
end;
theorem Th39:
for n be non zero Nat, D be n-element FinSequence,
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL
st (for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL)
& f is_continuous_on [:CarProduct D,J:] & f = g
holds
for e be Real st 0 < e ex r be Real st 0 < r
& for x1,x2 be Point of CarProduct(Seg n --> RNS_Real), y1,y2 be Real
st [x1,y1] in [:CarProduct D,J:] & [x2,y2] in [:CarProduct D,J:] &
||.x2-x1.|| < r & |.y2-y1.| < r holds
|. (|.g.|).([x2,y2])-(|.g.|).([x1,y1]) .| < e
proof
let n be non zero Nat, D be n-element FinSequence,
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL;
assume that
A1: for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL and
A2: f is_continuous_on [:CarProduct D,J:] and
A3: f = g;
||.f.|| = |.g.| by A3,Th38;
hence thesis by A1,A2,MESFUN16:22,Th37;
end;
Lm2:
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
.= a2+(-b1) by A1,XXREAL_3:def 3
.= a1+(-b1) by A1,XXREAL_3:def 2;
hence thesis;
end;
theorem Th40:
for n be non zero Nat, D be n-element FinSequence,
I be Subset of CarProduct(Seg n --> RNS_Real),
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
G2 be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real
st (for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL)
& I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g
& G2 = Integral2(L-Meas,|.R_EAL g.|) |I
holds G2 is_continuous_on I
proof
let n be non zero Nat, D be n-element FinSequence,
I be Subset of CarProduct(Seg n --> RNS_Real),
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
G2 be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real;
assume that
A1: for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL and
A2: I = CarProduct D and
A3: [:I,J:] = dom f and
A4: f is_continuous_on [:I,J:] and
A5: f = g and
A6: G2 = Integral2(L-Meas,|.R_EAL g.|) |I;
consider c,d be Real such that
A7: J = [.c,d.] by MEASURE5:def 3;
set Rg = R_EAL g;
dom |.Rg.| = dom Rg by MESFUNC1:def 10; then
A8:dom |.Rg.| = [:I,J:] by A3,A5,MESFUNC5:def 7;
A9:for x be Element of CarProduct(Seg n --> REAL),
y be Element of REAL st x in I & y in J holds
(ProjPMap1(|.Rg.|,x)).y =(|.Rg.|).(x,y)
& (|.Rg.|).(x,y) = |. g.([x,y]) .| & (|.Rg.|).(x,y) = (|.g.|).([x,y])
proof
let x be Element of CarProduct(Seg n --> REAL), y be Element of REAL;
assume
A10: x in I & y in J;
hence (ProjPMap1(|.Rg.|,x)).y =(|.Rg.|).(x,y)
by A8,ZFMISC_1:87,MESFUN12:def 3;
[x,y] in dom g by A10,A3,A5,ZFMISC_1:87; then
A11: [x,y] in dom |.g.| by VALUED_1:def 11;
A12: Rg.([x,y]) = g.([x,y]) by MESFUNC5:def 7;
(|.Rg.|).(x,y) = |. Rg.([x,y]) .| by A10,A8,ZFMISC_1:87,MESFUNC1:def 10;
hence (|.Rg.|).(x,y) = |. g.([x,y]) .| by A12,EXTREAL1:12;
hence (|.Rg.|).(x,y) = (|.g.|).([x,y]) by VALUED_1:def 11,A11;
end;
A13:for e be Real st 0 < e holds ex r be Real st 0 < r
& for x1,x2 be Element of CarProduct(Seg n --> REAL),
xx1,xx2 be Point of CarProduct(Seg n --> RNS_Real)
st xx1=x1 & xx2=x2 & ||.xx2-xx1.|| < r & x1 in I
& x2 in I holds for y be Element of REAL st y in J
holds |. (ProjPMap1(|.Rg.|,x2)).y-(ProjPMap1(|.Rg.|,x1)).y .| < e
proof
let e be Real;
assume 0 < e; then
consider r be Real such that
A14: 0 < r
& for x1,x2 be Point of CarProduct(Seg n --> RNS_Real), y1,y2 be Real
st [x1,y1] in [:I,J:] & [x2,y2] in [:I,J:] &
||.x2-x1.|| < r & |.y2-y1.| < r
holds |. (|.g.|).([x2,y2])-(|.g.|).([x1,y1]) .| < e
by A1,A2,A4,A5,Th39;
A15: now let x1,x2 be Point of CarProduct(Seg n --> RNS_Real);
assume
A16: ||.x2-x1.|| < r & x1 in I & x2 in I;
hereby let y be Real;
assume y in J; then
A17: [x1,y] in [:I,J:] & [x2,y] in [:I,J:] by A16,ZFMISC_1:87;
|.y-y.| < r by A14;
hence |. (|.g.|).([x2,y])-(|.g.|).([x1,y]) .| < e by A14,A16,A17;
end;
end;
take r;
thus 0 < r by A14;
let x1,x2 be Element of CarProduct(Seg n --> REAL);
let xx1,xx2 be Point of CarProduct(Seg n --> RNS_Real);
assume that
A18: xx1=x1 & xx2=x2 and
A19: ||.xx2-xx1.|| < r & x1 in I & x2 in I;
let y be Element of REAL;
assume
A20: y in J; then
A21: |. (|.g.|).([x2,y])-(|.g.|).([x1,y]) .| < e by A15,A18,A19;
(ProjPMap1(|.Rg.|,x1)).y =(|.Rg.|).(x1,y)
& (|.Rg.|).(x1,y) = (|.g.|).([x1,y])
& (ProjPMap1(|.Rg.|,x2)).y =(|.Rg.|).(x2,y)
& (|.Rg.|).(x2,y) = (|.g.|).([x2,y]) by A9,A19,A20; then
(ProjPMap1(|.Rg.|,x2)).y-(ProjPMap1(|.Rg.|,x1)).y
= (|.g.|).([x2,y])-(|.g.|).([x1,y]) by Lm2;
hence thesis by A21,EXTREAL1:12;
end;
for i be Nat st i in Seg n holds D.i is Subset of REAL by A1; then
A22:CarProduct D is Subset of CarProduct(Seg n --> REAL)
by FINSEQ_1:3,Th11;
A23:dom(Integral2(L-Meas,|.R_EAL g.|)) = CarProduct(Seg n --> REAL)
by FUNCT_2:def 1;
per cases;
suppose
A24: c <= d; then
A25: c in J & d in J by A7; then
reconsider J as non empty closed_interval Subset of REAL;
A26: J = ['c,d'] by A7,XXREAL_1:29,INTEGRA5:def 3;
for x0 be Point of CarProduct(Seg n --> RNS_Real), r be Real
st x0 in I & 0 < r
ex s be Real st 0<s & for x1 be Point of CarProduct(Seg n --> RNS_Real)
st x1 in I & ||.x1-x0.|| < s holds ||. G2/.x1 - G2/.x0 .|| < r
proof
let xx0 be Point of CarProduct(Seg n --> RNS_Real), r be Real;
assume
A27: xx0 in I & 0 < r;
reconsider x0=xx0 as Element of CarProduct(Seg n --> REAL)
by MEASUR15:42;
reconsider Pg0 = ProjPMap1(|.Rg.|,x0)
as PartFunc of REAL,REAL by MESFUN16:30;
A28: dom Pg0 = J by A27,A2,A22,A3,A5,MESFUN16:27;
A29: Pg0| (dom Pg0) is continuous by A3,A4,A5,Th25;
A30: Pg0|J is bounded & Pg0 is_integrable_on J
by A27,A3,A4,A5,A2,A22,Th28;
A31: (Integral2(L-Meas,|.Rg.|)).x0 = integral(Pg0,J)
by A27,A3,A4,A5,A2,A22,Th32;
per cases;
suppose
A32: c = d;
consider s be Real such that
A33: 0 < s
& for x1,x2 be Element of CarProduct(Seg n --> REAL),
xx1,xx2 be Point of CarProduct(Seg n --> RNS_Real)
st xx1 = x1 & xx2 = x2 & ||.xx2-xx1.|| < s & x1 in I & x2 in I
holds for y be Element of REAL st y in J holds
|. (ProjPMap1(|.Rg.|,x2)).y-(ProjPMap1(|.Rg.|,x1)).y .| < r
by A13,A27;
for x1 be Point of CarProduct(Seg n --> RNS_Real)
st x1 in I & ||.x1-xx0.|| < s holds ||. G2/.x1-G2/.xx0 .|| < r
proof
let xx1 be Point of CarProduct(Seg n --> RNS_Real);
assume
A34: xx1 in I & ||.xx1-xx0.|| < s;
reconsider x1=xx1 as Element of CarProduct(Seg n --> REAL)
by MEASUR15:42;
reconsider Pg1 = ProjPMap1(|.Rg.|,x1) as PartFunc of REAL,REAL
by MESFUN16:30;
A35: dom Pg1 = J by A34,A3,A5,A2,A22,MESFUN16:27;
A36: Pg1| (dom Pg1) is continuous by A3,A4,A5,Th25;
A37: Pg1|J is bounded & Pg1 is_integrable_on J
by A34,A3,A4,A5,A2,A22,Th28;
(Integral2(L-Meas,|.Rg.|)).x1 = integral(Pg1,J)
by A34,A3,A4,A5,A2,A22,Th32; then
G2.xx0 = integral(Pg0,J) & G2.xx1 = integral(Pg1,J)
by A6,A27,A31,A34,FUNCT_1:49; then
G2.xx0 = integral(Pg0,c,d) & G2.xx1 = integral(Pg1,c,d)
by A7,A26,XXREAL_1:29,INTEGRA5:def 4; then
G2/.xx0 = integral(Pg0,c,d) & G2/.xx1 = integral(Pg1,c,d)
by A2,A22,A6,A23,A27,A34,PARTFUN1:def 6; then
A38: G2/.xx1 - G2/.xx0 = integral(Pg1,c,d) - integral(Pg0,c,d)
by DUALSP03:4;
A39: dom(Pg1-Pg0) = J /\ J by A28,A35,VALUED_1:12; then
A40: (Pg1-Pg0) | J is bounded & (Pg1-Pg0) is_integrable_on J
by A29,A36,INTEGRA5:10,11;
for y be Real st y in J holds |. (Pg1-Pg0).y .| <= r
proof
let y be Real;
assume
A41: y in J; then
A42: |. (ProjPMap1(|.Rg.|,x1)).y-(ProjPMap1(|.Rg.|,x0)).y .| < r
by A33,A34,A27;
A43: -(ProjPMap1(|.Rg.|,x0)).y = -Pg0.y by XXREAL_3:def 3;
(ProjPMap1(|.Rg.|,x1)).y-(ProjPMap1(|.Rg.|,x0)).y
= (ProjPMap1(|.Rg.|,x1)).y +-(ProjPMap1(|.Rg.|,x0)).y
by XXREAL_3:def 4; then
(ProjPMap1(|.Rg.|,x1)).y-(ProjPMap1(|.Rg.|,x0)).y = Pg1.y + -Pg0.y
by A43,XXREAL_3:def 2; then
(ProjPMap1(|.Rg.|,x1)).y-(ProjPMap1(|.Rg.|,x0)).y
= Pg1.y - Pg0.y; then
(ProjPMap1(|.Rg.|,x1)).y-(ProjPMap1(|.Rg.|,x0)).y = (Pg1-Pg0).y
by A39,A41,VALUED_1:13;
hence |. (Pg1-Pg0).y .| <= r by A42,EXTREAL1:12;
end; then
|. integral(Pg1-Pg0,c,d) .| <= r * (d-c)
by A24,A26,A39,A40,A25,INTEGRA6:23; then
|. integral(Pg1,c,d) - integral(Pg0,c,d) .| <= r * (d-c)
by A32,A26,A35,A37,A28,A30,INTEGRA6:12;
hence ||. G2/.xx1-G2/.xx0 .|| < r by A32,A27,A38,EUCLID:def 2;
end;
hence
ex s be Real st 0<s & for x1 be Point of CarProduct(Seg n --> RNS_Real)
st x1 in I & ||.x1-xx0.|| < s holds ||. G2/.x1-G2/.xx0.|| < r by A33;
end;
suppose c <> d; then
c < d by A24,XXREAL_0:1; then
A44: 0 < d - c by XREAL_1:50;
set r1 = r/2;
A45: 0 < r1 & r1 < r by A27,XREAL_1:215,XREAL_1:216;
consider s be Real such that
A46: 0 < s
& for x1,x2 be Element of CarProduct(Seg n --> REAL),
xx1,xx2 be Point of CarProduct(Seg n --> RNS_Real)
st xx1 = x1 & xx2 = x2 & ||.xx2-xx1.|| < s & x1 in I & x2 in I
holds for y be Element of REAL st y in J holds
|. (ProjPMap1(|.Rg.|,x2)).y-(ProjPMap1(|.Rg.|,x1)).y .| < r1/(d-c)
by A13,XREAL_1:139,A45,A44;
take s;
thus 0 < s by A46;
let xx1 be Point of CarProduct(Seg n --> RNS_Real);
assume
A47: xx1 in I & ||.xx1-xx0.|| < s;
reconsider x1=xx1 as Element of CarProduct(Seg n --> REAL)
by MEASUR15:42;
reconsider Pg1 = ProjPMap1(|.Rg.|,x1) as PartFunc of REAL,REAL
by MESFUN16:30;
A48: dom Pg1 = J by A47,A3,A5,A2,A22,MESFUN16:27;
A49: Pg1| (dom Pg1) is continuous by A3,A4,A5,Th25;
A50: Pg1|J is bounded & Pg1 is_integrable_on J
by A47,A3,A4,A5,A2,A22,Th28;
(Integral2(L-Meas,|.Rg.|)).x1 = integral(Pg1,J)
by A47,A3,A4,A5,A2,A22,Th32; then
G2.xx0 = integral(Pg0,J) & G2.xx1 = integral(Pg1,J)
by A6,A27,A31,A47,FUNCT_1:49; then
G2.xx0 = integral(Pg0,c,d) & G2.xx1 = integral(Pg1,c,d)
by A7,A26,XXREAL_1:29,INTEGRA5:def 4; then
G2/.xx0 = integral(Pg0,c,d) & G2/.xx1 = integral(Pg1,c,d)
by A2,A22,A6,A23,A27,A47,PARTFUN1:def 6; then
G2/.xx1 - G2/.xx0 = integral(Pg1,c,d) - integral(Pg0,c,d)
by DUALSP03:4; then
G2/.xx1 - G2/.xx0 = integral(Pg1-Pg0,c,d)
by A24,A26,A48,A50,A28,A30,INTEGRA6:12; then
A51: ||. G2/.xx1-G2/.xx0 .|| = |. integral(Pg1-Pg0,c,d) .| by EUCLID:def 2;
A52: dom(Pg1-Pg0) = J /\ J by A28,A48,VALUED_1:12; then
A53: (Pg1-Pg0) |J is bounded & (Pg1-Pg0) is_integrable_on J
by A29,A49,INTEGRA5:10,11;
for y be Real st y in J holds |. (Pg1-Pg0).y .| <= r1 / (d-c)
proof
let y be Real;
assume
A54: y in J; then
A55: |. (ProjPMap1(|.Rg.|,x1)).y-(ProjPMap1(|.Rg.|,x0)).y .| < r1/(d-c)
by A46,A47,A27;
A56: -(ProjPMap1(|.Rg.|,x0)).y = -Pg0.y by XXREAL_3:def 3;
(ProjPMap1(|.Rg.|,x1)).y-(ProjPMap1(|.Rg.|,x0)).y
= (ProjPMap1(|.Rg.|,x1)).y +-(ProjPMap1(|.Rg.|,x0)).y
by XXREAL_3:def 4; then
(ProjPMap1(|.Rg.|,x1)).y-(ProjPMap1(|.Rg.|,x0)).y = Pg1.y + -Pg0.y
by A56,XXREAL_3:def 2; then
(ProjPMap1(|.Rg.|,x1)).y-(ProjPMap1(|.Rg.|,x0)).y = Pg1.y - Pg0.y; then
(ProjPMap1(|.Rg.|,x1)).y-(ProjPMap1(|.Rg.|,x0)).y = (Pg1-Pg0).y
by A52,A54,VALUED_1:13;
hence thesis by A55,EXTREAL1:12;
end; then
|. integral(Pg1-Pg0,c,d) .| <= (r1/(d-c)) * (d-c)
by A24,A26,A52,A53,A25,INTEGRA6:23; then
|. integral(Pg1-Pg0,c,d) .| <= r1 by A44,XCMPLX_1:87;
hence ||. G2/.xx1-G2/.xx0 .|| < r by A51,XXREAL_0:2,A45;
end;
end;
hence G2 is_continuous_on I by A2,A22,A6,A23,NFCONT_1:19;
end;
suppose
A57: c > d;
for x0 be Point of CarProduct(Seg n --> RNS_Real), r be Real
st x0 in I & 0 < r
ex s be Real st 0<s & for x1 be Point of CarProduct(Seg n --> RNS_Real)
st x1 in I & ||.x1-x0.|| < s holds ||. G2/.x1 - G2/.x0 .|| < r
proof
let xx0 be Point of CarProduct(Seg n --> RNS_Real), r be Real;
assume
A58: xx0 in I & 0 < r;
reconsider x0=xx0 as Element of CarProduct(Seg n --> REAL)
by MEASUR15:42;
reconsider Pg0 = ProjPMap1(|.Rg.|,x0)
as PartFunc of REAL,REAL by MESFUN16:30;
dom Pg0 = J by A2,A3,A5,A22,A58,MESFUN16:27; then
Integral(L-Meas,ProjPMap1(|.R_EAL g.|,x0)) = 0
by A57,A7,XXREAL_1:29,MESFUN16:1; then
A59: (Integral2(L-Meas,|.Rg.|)).x0 = 0 by MESFUN12:def 8;
consider s be Real such that
A60: 0 < s
& for x1,x2 be Element of CarProduct(Seg n --> REAL),
xx1,xx2 be Point of CarProduct(Seg n --> RNS_Real)
st xx1 = x1 & xx2 = x2 & ||.xx2-xx1.|| < s & x1 in I & x2 in I
holds for y be Element of REAL st y in J holds
|. (ProjPMap1(|.Rg.|,x2)).y-(ProjPMap1(|.Rg.|,x1)).y .| < r
by A13,A58;
for x1 be Point of CarProduct(Seg n --> RNS_Real)
st x1 in I & ||.x1-xx0.|| < s holds ||. G2/.x1-G2/.xx0 .|| < r
proof
let xx1 be Point of CarProduct(Seg n --> RNS_Real);
assume
A61: xx1 in I & ||.xx1-xx0.|| < s;
reconsider x1=xx1 as Element of CarProduct(Seg n --> REAL)
by MEASUR15:42;
reconsider Pg1 = ProjPMap1(|.Rg.|,x1) as PartFunc of REAL,REAL
by MESFUN16:30;
dom Pg1 = J by A3,A5,A2,A22,A61,MESFUN16:27; then
Integral(L-Meas,ProjPMap1(|.R_EAL g.|,x1)) = 0
by A57,A7,XXREAL_1:29,MESFUN16:1; then
(Integral2(L-Meas,|.Rg.|)).x1 = 0 by MESFUN12:def 8; then
G2.xx0 = 0 & G2.xx1 = 0 by A6,A58,A59,A61,FUNCT_1:49; then
G2/.xx0 = 0 & G2/.xx1 = 0 by A2,A6,A22,A23,A58,A61,PARTFUN1:def 6; then
G2/.xx1 - G2/.xx0 = 0.RNS_Real by RLVECT_1:15;
hence ||. G2/.xx1 - G2/.xx0 .|| < r by A58;
end;
hence
ex s be Real st 0<s & for x1 be Point of CarProduct(Seg n --> RNS_Real)
st x1 in I & ||.x1-xx0.|| < s holds ||. G2/.x1-G2/.xx0.|| < r by A60;
end;
hence G2 is_continuous_on I by A2,A6,A22,A23,NFCONT_1:19;
end;
end;
theorem
for n be non zero Nat, D be n-element FinSequence,
I be Subset of CarProduct(Seg n --> RNS_Real),
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
G2 be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real
st (for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL)
& I = CarProduct D
& [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g
& G2 = Integral2(L-Meas,R_EAL g) |I holds G2 is_continuous_on I
proof
let n be non zero Nat, D be n-element FinSequence,
I be Subset of CarProduct(Seg n --> RNS_Real),
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
G2 be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real;
assume that
A1: for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL and
A2: I = CarProduct D and
A3: [:I,J:] = dom f and
A4: f is_continuous_on [:I,J:] and
A5: f = g and
A6: G2 = Integral2(L-Meas,R_EAL g) |I;
consider c,d be Real such that
A7: J = [.c,d.] by MEASURE5:def 3;
A8:for e be Real st 0 < e holds ex r be Real st 0 < r
& for x1,x2 be Point of CarProduct(Seg n --> RNS_Real)
st ||.x2-x1.|| < r & x1 in I & x2 in I
holds for y be Real st y in J holds |. g.([x2,y])-g.([x1,y]) .| < e
proof
let e be Real;
assume 0 < e; then
consider r be Real such that
A9: 0 < r
& for x1,x2 be Point of CarProduct(Seg n --> RNS_Real), y1,y2 be Real
st [x1,y1] in [:I,J:] & [x2,y2] in [:I,J:] &
||.x2-x1.|| < r & |.y2-y1.| < r holds |. g.([x2,y2])-g.([x1,y1]) .| < e
by A1,A2,A4,A5,Th37;
take r;
thus 0 < r by A9;
let x1,x2 be Point of CarProduct(Seg n --> RNS_Real);
assume
A10: ||.x2-x1.|| < r & x1 in I & x2 in I;
let y be Real;
assume y in J; then
A11: [x1,y] in [:I,J:] & [x2,y] in [:I,J:] by A10,ZFMISC_1:87;
|.y-y.| < r by A9;
hence |. g.([x2,y])-g.([x1,y]) .| < e by A9,A10,A11;
end;
set Rg = R_EAL g;
A12:dom Rg = [:I,J:] by A3,A5,MESFUNC5:def 7;
A13:for e be Real st 0 < e holds ex r be Real st 0 < r
& for x1,x2 be Element of CarProduct(Seg n --> REAL),
xx1,xx2 be Point of CarProduct(Seg n --> RNS_Real)
st xx1=x1 & xx2=x2 & ||.xx2-xx1.|| < r & x1 in I
& x2 in I holds for y be Element of REAL st y in J
holds |. (ProjPMap1(Rg,x2)).y-(ProjPMap1(Rg,x1)).y .| < e
proof
let e be Real;
assume 0 < e; then
consider r be Real such that
A14: 0 < r
& for xx1,xx2 be Point of CarProduct(Seg n --> RNS_Real)
st ||.xx2-xx1.|| < r & xx1 in I & xx2 in I holds
for y be Real st y in J holds
|. g.([xx2,y])-g.([xx1,y]) .| < e by A8;
take r;
thus 0 < r by A14;
let x1,x2 be Element of CarProduct(Seg n --> REAL);
let xx1,xx2 be Point of CarProduct(Seg n --> RNS_Real);
assume that
A15: xx1=x1 & xx2=x2 and
A16: ||.xx2-xx1.|| < r & x1 in I & x2 in I;
let y be Element of REAL;
assume
A17: y in J; then
A18: |. g.([x2,y])-g.([x1,y]) .| < e by A14,A15,A16;
(ProjPMap1(Rg,x1)).y =Rg.(x1,y) & Rg.(x1,y) = g.([x1,y])
& (ProjPMap1(Rg,x2)).y =Rg.(x2,y) & Rg.(x2,y) = g.([x2,y])
by A12,A16,A17,ZFMISC_1:87,MESFUN12:def 3,MESFUNC5:def 7; then
(ProjPMap1(Rg,x2)).y-(ProjPMap1(Rg,x1)).y = g.([x2,y])-g.([x1,y])
by Lm2;
hence thesis by A18,EXTREAL1:12;
end;
set F = Integral2(L-Meas,Rg);
A19:dom F = CarProduct(Seg n --> REAL) by FUNCT_2:def 1;
for i be Nat st i in Seg n holds D.i is Subset of REAL by A1; then
A20:CarProduct D is Subset of CarProduct(Seg n --> REAL)
by FINSEQ_1:3,Th11;
per cases;
suppose
A21: c <= d; then
A22: c in J & d in J by A7; then
reconsider J as non empty closed_interval Subset of REAL;
A23: J = ['c,d'] by A7,XXREAL_1:29,INTEGRA5:def 3;
for x0 be Point of CarProduct(Seg n --> RNS_Real),r be Real
st x0 in I & 0 < r
ex s be Real st 0<s & for x1 be Point of CarProduct(Seg n --> RNS_Real)
st x1 in I & ||.x1-x0.|| < s holds ||.G2/.x1-G2/.x0.|| < r
proof
let xx0 be Point of CarProduct(Seg n --> RNS_Real), r be Real;
assume
A24: xx0 in I & 0 < r;
reconsider x0=xx0 as Element of CarProduct(Seg n --> REAL)
by MEASUR15:42;
reconsider Pg0 = ProjPMap1(Rg,x0) as PartFunc of REAL,REAL
by MESFUN16:30;
A25: dom Pg0 = J by A24,A2,A20,A3,A5,MESFUN16:27;
A26: Pg0 is continuous by A3,A4,A5,Th23;
A27: Pg0|J is bounded & Pg0 is_integrable_on J
by A24,A3,A4,A5,A2,A20,Th27;
A28: (Integral2(L-Meas,Rg)).x0 = integral(Pg0,J)
by A24,A3,A4,A5,A2,A20,Th30;
per cases;
suppose
A29: c = d;
consider s be Real such that
A30: 0 < s
& for x1,x2 be Element of CarProduct(Seg n --> REAL),
xx1,xx2 be Point of CarProduct(Seg n --> RNS_Real)
st xx1=x1 & xx2=x2 & ||.xx2-xx1.|| < s & x1 in I & x2 in I
holds for y be Element of REAL st y in J holds
|. (ProjPMap1(Rg,x2)).y-(ProjPMap1(Rg,x1)).y .| < r by A13,A24;
for x1 be Point of CarProduct(Seg n --> RNS_Real)
st x1 in I & ||.x1-xx0.|| < s holds ||.G2/.x1-G2/.xx0 .|| < r
proof
let xx1 be Point of CarProduct(Seg n --> RNS_Real);
assume
A31: xx1 in I & ||.xx1-xx0.|| < s;
reconsider x1=xx1 as Element of CarProduct(Seg n --> REAL)
by MEASUR15:42;
reconsider Pg1 = ProjPMap1(Rg,x1) as PartFunc of REAL,REAL
by MESFUN16:30;
A32: dom Pg1 = J by A31,A3,A5,A2,A20,MESFUN16:27;
A33: Pg1 is continuous by A3,A4,A5,Th23;
A34: Pg1|J is bounded & Pg1 is_integrable_on J
by A31,A3,A4,A5,A2,A20,Th27;
(Integral2(L-Meas,Rg)).x1 = integral(Pg1,J)
by A31,A3,A4,A5,A2,A20,Th30; then
G2.xx0 = integral(Pg0,J) & G2.xx1 = integral(Pg1,J)
by A6,A24,A28,A31,FUNCT_1:49; then
G2.xx0 = integral(Pg0,c,d) & G2.xx1 = integral(Pg1,c,d)
by A7,A23,XXREAL_1:29,INTEGRA5:def 4; then
G2/.xx0 = integral(Pg0,c,d) & G2/.xx1 = integral(Pg1,c,d)
by A2,A6,A19,A20,A24,A31,PARTFUN1:def 6; then
A35: G2/.xx1 - G2/.xx0 = integral(Pg1,c,d) - integral(Pg0,c,d)
by DUALSP03:4;
A36: dom(Pg1-Pg0) = J /\ J by A25,A32,VALUED_1:12; then
A37: (Pg1-Pg0) |J is bounded & (Pg1-Pg0) is_integrable_on J
by A26,A33,INTEGRA5:10,11;
for y be Real st y in J holds |. (Pg1-Pg0).y .| <= r
proof
let y be Real;
assume
A38: y in J; then
A39: |. (ProjPMap1(Rg,x1)).y-(ProjPMap1(Rg,x0)).y .| < r
by A30,A31,A24;
A40: -(ProjPMap1(Rg,x0)).y = -Pg0.y by XXREAL_3:def 3;
(ProjPMap1(Rg,x1)).y-(ProjPMap1(Rg,x0)).y
= (ProjPMap1(Rg,x1)).y +-(ProjPMap1(Rg,x0)).y
by XXREAL_3:def 4; then
(ProjPMap1(Rg,x1)).y-(ProjPMap1(Rg,x0)).y = Pg1.y + -Pg0.y
by A40,XXREAL_3:def 2; then
(ProjPMap1(Rg,x1)).y-(ProjPMap1(Rg,x0)).y = Pg1.y - Pg0.y; then
(ProjPMap1(Rg,x1)).y-(ProjPMap1(Rg,x0)).y = (Pg1-Pg0).y
by A36,A38,VALUED_1:13;
hence |. (Pg1-Pg0).y .| <= r by A39,EXTREAL1:12;
end; then
|. integral(Pg1-Pg0,c,d) .| <= r * (d-c)
by A21,A23,A36,A37,A22,INTEGRA6:23; then
|. integral(Pg1,c,d) - integral(Pg0,c,d) .| < r
by A29,A24,A23,A32,A34,A25,A27,INTEGRA6:12;
hence ||. G2/.xx1-G2/.xx0 .|| < r by A35,EUCLID:def 2;
end;
hence
ex s be Real st 0<s & for x1 be Point of CarProduct(Seg n --> RNS_Real)
st x1 in I & ||.x1-xx0.|| < s holds ||.G2/.x1-G2/.xx0.|| < r by A30;
end;
suppose c <> d; then
c < d by A21,XXREAL_0:1; then
A41: 0 < d - c by XREAL_1:50;
set r1 = r/2;
A42: 0 < r1 & r1 < r by A24,XREAL_1:215,XREAL_1:216;
consider s be Real such that
A43: 0 < s
& for x1,x2 be Element of CarProduct(Seg n --> REAL),
xx1,xx2 be Point of CarProduct(Seg n --> RNS_Real)
st xx1 = x1 & xx2 = x2 & ||.xx2-xx1.|| < s & x1 in I & x2 in I
holds for y be Element of REAL st y in J holds
|. (ProjPMap1(Rg,x2)).y-(ProjPMap1(Rg,x1)).y .| < r1/(d-c)
by A13,XREAL_1:139,A42,A41;
take s;
thus 0 < s by A43;
let xx1 be Point of CarProduct(Seg n --> RNS_Real);
assume
A44: xx1 in I & ||.xx1-xx0.|| < s;
reconsider x1=xx1 as Element of CarProduct(Seg n --> REAL)
by MEASUR15:42;
reconsider Pg1 = ProjPMap1(Rg,x1) as PartFunc of REAL,REAL
by MESFUN16:30;
A45: dom Pg1 = J by A44,A3,A5,A2,A20,MESFUN16:27;
A46: Pg1 is continuous by A3,A4,A5,Th23;
A47: Pg1|J is bounded & Pg1 is_integrable_on J
by A44,A3,A4,A5,A2,A20,Th27;
(Integral2(L-Meas,Rg)).x1 = integral(Pg1,J)
by A44,A3,A4,A5,A2,A20,Th30; then
G2.xx0 = integral(Pg0,J) & G2.xx1 = integral(Pg1,J)
by A6,A24,A28,A44,FUNCT_1:49; then
G2.xx0 = integral(Pg0,c,d) & G2.xx1 = integral(Pg1,c,d)
by A7,A23,XXREAL_1:29,INTEGRA5:def 4; then
G2/.xx0 = integral(Pg0,c,d) & G2/.xx1 = integral(Pg1,c,d)
by A2,A6,A19,A20,A24,A44,PARTFUN1:def 6; then
G2/.xx1 - G2/.xx0 = integral(Pg1,c,d) - integral(Pg0,c,d)
by DUALSP03:4; then
G2/.xx1 - G2/.xx0 = integral(Pg1-Pg0,c,d)
by A21,A23,A45,A47,A25,A27,INTEGRA6:12; then
A48: ||. G2/.xx1-G2/.xx0 .|| = |. integral(Pg1-Pg0,c,d) .| by EUCLID:def 2;
A49: dom(Pg1-Pg0) = J /\ J by A25,A45,VALUED_1:12; then
A50: (Pg1-Pg0) |J is bounded & (Pg1-Pg0) is_integrable_on J
by A26,A46,INTEGRA5:10,11;
for y be Real st y in J holds |. (Pg1-Pg0).y .| <= r1 / (d-c)
proof
let y be Real;
assume
A51: y in J; then
A52: |. (ProjPMap1(Rg,x1)).y-(ProjPMap1(Rg,x0)).y .| < r1/(d-c)
by A43,A44,A24;
A53: -(ProjPMap1(Rg,x0)).y = -Pg0.y by XXREAL_3:def 3;
(ProjPMap1(Rg,x1)).y-(ProjPMap1(Rg,x0)).y
= (ProjPMap1(Rg,x1)).y +-(ProjPMap1(Rg,x0)).y by XXREAL_3:def 4; then
(ProjPMap1(Rg,x1)).y-(ProjPMap1(Rg,x0)).y = Pg1.y + -Pg0.y
by A53,XXREAL_3:def 2; then
(ProjPMap1(Rg,x1)).y-(ProjPMap1(Rg,x0)).y = Pg1.y - Pg0.y; then
(ProjPMap1(Rg,x1)).y-(ProjPMap1(Rg,x0)).y = (Pg1-Pg0).y
by A49,A51,VALUED_1:13;
hence thesis by A52,EXTREAL1:12;
end; then
|. integral(Pg1-Pg0,c,d) .| <= (r1/(d-c)) * (d-c)
by A21,A23,A49,A50,A22,INTEGRA6:23; then
|. integral(Pg1-Pg0,c,d) .| <= r1 by A41,XCMPLX_1:87;
hence ||. G2/.xx1-G2/.xx0 .|| < r by A48,XXREAL_0:2,A42;
end;
end;
hence G2 is_continuous_on I by A2,A6,A19,A20,NFCONT_1:19;
end;
suppose
A54: c > d;
for x0 be Point of CarProduct(Seg n --> RNS_Real),r be Real
st x0 in I & 0 < r
ex s be Real st 0<s & for x1 be Point of CarProduct(Seg n --> RNS_Real)
st x1 in I & ||.x1-x0.|| < s holds ||.G2/.x1-G2/.x0.|| < r
proof
let xx0 be Point of CarProduct(Seg n --> RNS_Real), r be Real;
assume
A55: xx0 in I & 0 < r;
reconsider x0=xx0 as Element of CarProduct(Seg n --> REAL)
by MEASUR15:42;
reconsider Pg0 = ProjPMap1(Rg,x0) as PartFunc of REAL,REAL
by MESFUN16:30;
dom Pg0 = J by A55,A2,A20,A3,A5,MESFUN16:27; then
Integral(L-Meas,ProjPMap1(Rg,x0)) = 0
by A54,A7,XXREAL_1:29,MESFUN16:1; then
A56: (Integral2(L-Meas,Rg)).x0 = 0 by MESFUN12:def 8;
consider s be Real such that
A57: 0 < s
& for x1,x2 be Element of CarProduct(Seg n --> REAL),
xx1,xx2 be Point of CarProduct(Seg n --> RNS_Real)
st xx1=x1 & xx2=x2 & ||.xx2-xx1.|| < s & x1 in I & x2 in I
holds for y be Element of REAL st y in J holds
|. (ProjPMap1(Rg,x2)).y-(ProjPMap1(Rg,x1)).y .| < r
by A13,A55;
for x1 be Point of CarProduct(Seg n --> RNS_Real)
st x1 in I & ||.x1-xx0.|| < s holds ||.G2/.x1-G2/.xx0 .|| < r
proof
let xx1 be Point of CarProduct(Seg n --> RNS_Real);
assume
A58: xx1 in I & ||.xx1-xx0.|| < s;
reconsider x1=xx1 as Element of CarProduct(Seg n --> REAL)
by MEASUR15:42;
reconsider Pg1 = ProjPMap1(Rg,x1) as PartFunc of REAL,REAL
by MESFUN16:30;
dom Pg1 = J by A58,A3,A5,A2,A20,MESFUN16:27; then
Integral(L-Meas,ProjPMap1(Rg,x1)) = 0
by A54,A7,XXREAL_1:29,MESFUN16:1; then
(Integral2(L-Meas,Rg)).x1 = 0 by MESFUN12:def 8; then
G2.xx0 = 0 & G2.xx1 = 0 by A6,A55,A56,A58,FUNCT_1:49; then
G2/.xx0 = 0 & G2/.xx1 = 0 by A2,A6,A19,A20,A55,A58,PARTFUN1:def 6; then
G2/.xx1 - G2/.xx0 = 0.RNS_Real by RLVECT_1:15;
hence ||. G2/.xx1 - G2/.xx0 .|| < r by A55;
end;
hence
ex s be Real st 0<s & for x1 be Point of CarProduct(Seg n --> RNS_Real)
st x1 in I & ||.x1-xx0.|| < s holds ||.G2/.x1-G2/.xx0.|| < r by A57;
end;
hence G2 is_continuous_on I by A2,A6,A19,A20,NFCONT_1:19;
end;
end;
theorem Th42:
for n be non zero Nat, D be n-element FinSequence,
g be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real,
f be PartFunc of CarProduct(Seg n --> REAL),REAL st
f = g & g is_continuous_on CarProduct D & CarProduct D c= dom g
& (for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL)
holds
for e be Real st 0 < e
ex r be Real st 0 < r
& for x,y be n-element FinSequence of REAL
st PtCarProduct x in CarProduct D & PtCarProduct y in CarProduct D
& (for i be Nat st i in dom D holds
ex xi,yi be Real st xi = x.i & yi = y.i & |. xi-yi .| < r)
holds |. f.(PtCarProduct x) -f.(PtCarProduct y) .| < e
proof
let n be non zero Nat, D be n-element FinSequence,
g be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real,
f be PartFunc of CarProduct(Seg n --> REAL),REAL;
assume that
A1: f = g and
A2: g is_continuous_on CarProduct D and
A3: CarProduct D c= dom g and
A4: for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL;
set S = Seg n-->RNS_Real;
for i be Nat st i in Seg n holds D.i is Subset of REAL by A4; then
A5: CarProduct D is Subset of CarProduct(Seg n --> REAL)
by FINSEQ_1:3,Th11;
ex I be Subset of CarProduct(Seg n --> RNS_Real) st
I = CarProduct D & I is compact
proof
per cases;
suppose D is non-empty;
hence thesis by A4,MEASUR15:51;
end;
suppose not D is non-empty; then
A6: CarProduct D = {} by Th6;
reconsider I = CarProduct D
as Subset of CarProduct(Seg n --> RNS_Real) by A5,MEASUR15:42;
I is compact by A6;
hence thesis;
end;
end; then
consider E be Subset of CarProduct S such that
A7: E = CarProduct D & E is compact;
A8: g is_uniformly_continuous_on E by A2,A7,NFCONT_2:10;
let e be Real;
assume 0 < e; then
consider r0 be Real such that
A9: 0 < r0
& for z1,z2 be Point of CarProduct S st z1 in E & z2 in E
& ||.z1 - z2.|| < r0 holds ||. g/.z1 - g/.z2 .|| < e by A8;
set r1 = r0/2;
set r = r1/n;
A10: 0 < r1 by A9,XREAL_1:215;
A11: r1 < r0 by A9,XREAL_1:216;
r*r*n*1 <= r*r*n*n by A9,NAT_1:14,XREAL_1:64; then
r*r*n <= (r*n)*(r*n); then
r*r*n <= r1*(r*n) by XCMPLX_1:87; then
r*r*n <= r1*r1 by XCMPLX_1:87; then
sqrt((r*r)*n) <= sqrt(r1^2) by A9,SQUARE_1:26; then
sqrt((r*r)*n) <= r1 by A9,SQUARE_1:22; then
A12:sqrt((r*r)*n) < r0 by A11,XXREAL_0:2;
take r;
thus 0 < r by A10,XREAL_1:139;
let x,y be n-element FinSequence of REAL;
assume
A13:PtCarProduct x in CarProduct D & PtCarProduct y in CarProduct D
& for i be Nat st i in dom D holds
ex xi,yi be Real st xi = x.i & yi = y.i & |.xi-yi.| < r;
len D = n by CARD_1:def 7; then
A14:dom D = Seg n by FINSEQ_1:def 3;
reconsider z1 = PtCarProduct x, z2 = PtCarProduct y
as Point of CarProduct S by A5,A13,MEASUR15:42;
g/.z1 = g.z1 & g/.z2 = g.z2 by A13,A3,PARTFUN1:def 6; then
g/.z1 - g/.z2 = f.(PtCarProduct x) - f.(PtCarProduct y)
by A1,DUALSP03:4; then
A15: ||.g/.z1 - g/.z2 .|| = |.f.(PtCarProduct x) - f.(PtCarProduct y).|
by EUCLID:def 2;
reconsider m = n-1 as Nat by NAT_1:14,21;
consider pxy be (m+1)-element FinSequence such that
A16:z1-z2 = PtCarProduct pxy by MEASUR15:24;
consider nrxy be Element of REAL (m+1) such that
A18:( for i be non zero Nat st i <= (m+1) holds
ex pxyi be Point of ElmFin(S,i) st pxyi=pxy.i & nrxy.i =||.pxyi.|| )
& ||. z1-z2 .|| = |.nrxy.| by A16,MEASUR15:26;
for i being Nat st i in dom nrxy holds 0 <= nrxy.i & nrxy.i <= r
proof
let i be Nat;
assume i in dom nrxy; then
A19: i in Seg len nrxy by FINSEQ_1:def 3; then
A20: i in Seg (m+1) by CARD_1:def 7; then
A21: 1 <= i & i <= m+1 by FINSEQ_1:1;
reconsider i1=i as non zero Nat by A19,FINSEQ_1:1;
consider pxyi be Point of ElmFin(S,i1) such that
A22: pxyi = pxy.i & nrxy.i = ||.pxyi.|| by A18,A21;
thus 0 <= nrxy.i by A22;
consider pxi,pyi be Point of ElmFin(S,i1) such that
A23: pxi=x.i & pyi=y.i & pxi-pyi = pxy.i by A21,A16,MEASUR15:25;
S.i = RNS_Real by A20,FUNCOP_1:7; then
A24: ElmFin(S,i1) = RNS_Real by A21,MEASUR15:def 3; then
A25: pxyi = x.i-y.i by A22,A23,DUALSP03:4;
ex xi,yi be Real st xi = x.i & yi = y.i & |.xi-yi.| < r by A13,A14,A20;
hence nrxy.i <=r by A25,A22,A24,EUCLID:def 2;
end; then
|.nrxy.| <= sqrt((r*r)*(len nrxy)) by LOPBAN11:10; then
|.nrxy.| <= sqrt((r*r)*(m+1)) by CARD_1:def 7; then
|.nrxy.| < r0 by XXREAL_0:2,A12;
hence |. f.(PtCarProduct x) - f.(PtCarProduct y) .| < e
by A7,A13,A9,A15,A18;
end;
theorem Th43:
for n be non zero Nat, D be n-element FinSequence,
f be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real,
g be PartFunc of CarProduct(Seg n --> REAL),REAL
st f = g
& ( for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL )
& f is_continuous_on CarProduct D & dom f = CarProduct D
holds g is_integrable_on Prod_Measure(L-Meas n)
proof
defpred P[non zero Nat] means
for D be $1-element FinSequence,
f be PartFunc of CarProduct(Seg $1--> RNS_Real),RNS_Real,
g be PartFunc of CarProduct(Seg $1 --> REAL),REAL
st f = g
& (for i be Nat st i in Seg $1 holds D.i is closed_interval Subset of REAL)
& f is_continuous_on CarProduct D & dom f = CarProduct D
holds g is_integrable_on Prod_Measure(L-Meas $1);
A1: P[1]
proof
let D be 1-element FinSequence,
f be PartFunc of CarProduct(Seg 1 --> RNS_Real),RNS_Real,
g be PartFunc of CarProduct(Seg 1 --> REAL),REAL;
assume that
A2: f = g and
A3: for i be Nat st i in Seg 1 holds D.i is closed_interval Subset of REAL and
A4: f is_continuous_on CarProduct D and
A5: dom f = CarProduct D;
1 in Seg 1; then
reconsider I = D.1 as closed_interval Subset of REAL by A3;
reconsider f0 = f as PartFunc of RNS_Real,RNS_Real by Th13;
reconsider g0 = g as PartFunc of REAL,REAL by MEASUR14:37;
A6: CarProduct D = I by MEASUR13:def 3;
A7: I is Element of L-Field by MEASUR12:72,75;
now let x0,r be Real;
assume
A8: x0 in I & 0 < r;
reconsider p = x0 as Point of RNS_Real by XREAL_0:def 1;
reconsider pt = p as Point of CarProduct(Seg 1 --> RNS_Real) by Th13;
f|I is_continuous_in pt by A4,A6,A8; then
consider s be Real such that
A9: 0 < s
& for p1 be Point of RNS_Real st p1 in dom(f0|I) & ||. p1-p .|| < s
holds ||. (f0|I)/.p1 - (f0|I)/.p .|| < r by A8,Th13,NFCONT_1:7;
take s;
thus 0 < s by A9;
hereby let x1 be Real;
assume
A10: x1 in I & |. x1-x0 .| < s;
reconsider p1 = x1 as Point of RNS_Real by XREAL_0:def 1;
p1 - p = x1 - x0 by DUALSP03:4; then
||. p1 - p .|| = |. x1 - x0 .| by EUCLID:def 2; then
A11: ||. (f0|I)/.p1 - (f0|I)/.p .|| < r by A5,A6,A9,A10;
A12: (f0|I)/.p1 = g0.x1 by A2,A5,A6,A10,PARTFUN1:def 6;
(f0|I)/.p = g0.x0 by A2,A5,A6,A8,PARTFUN1:def 6; then
(f0|I)/.p1 - (f0|I)/.p = g0.x1 - g0.x0 by A12,DUALSP03:4;
hence |. g0.x1 - g0.x0 .| < r by A11,EUCLID:def 2;
end;
end; then
A13: g0|I is continuous by A2,A5,A6,FCONT_1:14;
per cases;
suppose I <> {}; then
reconsider I as non empty closed_interval Subset of REAL;
g0||I is bounded & g0 is_integrable_on I by A2,A5,A6,A13,INTEGRA5:10,11;
hence g is_integrable_on Prod_Measure(L-Meas 1)
by A2,A5,A6,A7,MESFUN14:49,MEASUR14:37,41,45;
end;
suppose I = {};
hence g is_integrable_on Prod_Measure(L-Meas 1)
by A2,A5,Th1,MEASUR13:def 3;
end;
end;
A14:for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A15: P[n];
let D be (n+1)-element FinSequence,
f be PartFunc of CarProduct(Seg (n+1) --> RNS_Real),RNS_Real,
g be PartFunc of CarProduct(Seg (n+1) --> REAL),REAL;
assume that
A16: f = g and
A17: for i be Nat st i in Seg (n+1) holds
D.i is closed_interval Subset of REAL and
A18: f is_continuous_on CarProduct D and
A19: dom f = CarProduct D;
reconsider f0 = f
as PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real
by MEASUR15:38;
A20: f0 is_continuous_on dom f0 by A18,A19,MEASUR15:38;
A21: CarProduct(Seg (n+1) --> REAL)
= [:CarProduct(Seg n --> REAL),REAL:] by MEASUR15:38;
reconsider g0 = g
as PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL by MEASUR15:38;
set Rg0 = R_EAL g0;
for i be Nat st i in Seg (n+1) holds D.i is Interval by A17; then
reconsider E = CarProduct D
as Element of Prod_Field(L-Field (n+1)) by Th9;
A22: g is E-measurable & dom g = E
& for e be Real st 0 < e
ex r be Real
st 0 < r
& for x,y be (n+1)-element FinSequence of REAL
st PtCarProduct x in CarProduct D & PtCarProduct y in CarProduct D
& for i be Nat st i in dom D holds
ex xi,yi be Real st xi = x.i & yi = y.i & |.xi-yi.| < r
holds |. g.(PtCarProduct x) -g.(PtCarProduct y) .| < e
by A16,A17,A18,A19,Th42,MEASUR15:66;
A23: D.(n+1) is closed_interval Subset of REAL by A17,FINSEQ_1:4; then
consider s,t be Real such that
A24: D.(n+1) = [. s,t .] by MEASURE5:def 3;
per cases;
suppose
s <= t; then
A25: [.s,t.] = ['s,t'] by INTEGRA5:def 3;
reconsider J = ['s,t'] as Element of L-Field by MEASUR10:5,MEASUR12:75;
reconsider D1 = D|n as n-element FinSequence;
A26: CarProduct D = [: CarProduct D1,[.s,t .] :] by A24,Th4;
A27: for i be Nat st i in Seg n holds D1.i c= (Seg n-->REAL).i
proof
let i be Nat;
assume
A28: i in Seg n; then
A29: i <= n by FINSEQ_1:1;
Seg n c=Seg (n+1) by NAT_1:11,FINSEQ_1:5; then
D.i is closed_interval Subset of REAL by A17,A28; then
D.i c= REAL; then
D1.i c= REAL by A29,FINSEQ_3:112;
hence D1.i c= (Seg n-->REAL).i by A28,FUNCOP_1:7;
end; then
A30: CarProduct D1 is Subset of CarProduct(Seg n --> REAL) by Th10;
A31: dom Rg0 = [:CarProduct D1,[.s,t .]:] by A26,A16,A19,MESFUNC5:def 7; then
A32: dom |.Rg0.| = [:CarProduct D1,[.s,t .]:] by MESFUNC1:def 10;
A33: for x be Element of CarProduct(Seg n --> REAL)
st x in CarProduct(Seg n --> REAL) \ CarProduct D1
holds dom ProjPMap1(|.Rg0.|,x) = {}
& (Integral2(L-Meas,|.Rg0.|)).x = 0
proof
let x be Element of CarProduct(Seg n --> REAL);
assume x in CarProduct(Seg n --> REAL) \ CarProduct D1; then
not x in CarProduct D1 by XBOOLE_0:def 5;
hence dom ProjPMap1(|.Rg0.|,x) = {} by A30,A32,MESFUN16:25; then
Integral(L-Meas,ProjPMap1(|.Rg0.|,x)) = 0 by MESFUN16:1;
hence (Integral2(L-Meas,|.Rg0.|)).x = 0 by MESFUN12:def 8;
end;
A34: for x be Element of CarProduct(Seg n --> REAL), y be Element of REAL
st x in CarProduct D1 & y in [.s,t.]
holds (ProjPMap1(|.Rg0.|,x)).y = (|.Rg0.|).(x,y)
& (|.Rg0.|).(x,y) = |. g.([x,y]) .| & (|.Rg0.|).(x,y) = (|.g.|).([x,y])
proof
let x be Element of CarProduct(Seg n --> REAL),
y be Element of REAL;
assume
A35: x in CarProduct D1 & y in [.s,t.];
hence (ProjPMap1(|.Rg0.|,x)).y = (|.Rg0.|).(x,y)
by A32,ZFMISC_1:87,MESFUN12:def 3;
[x,y] in dom g by A35,A26,A16,A19,ZFMISC_1:87; then
A36: [x,y] in dom |.g.| by VALUED_1:def 11;
A37: Rg0.([x,y]) = g.([x,y]) by MESFUNC5:def 7;
(|.Rg0.|).(x,y) = |. Rg0.([x,y]) .|
by A35,A32,ZFMISC_1:87,MESFUNC1:def 10;
hence (|.Rg0.|).(x,y) = |. g.([x,y]) .| by A37,EXTREAL1:12;
hence (|.Rg0.|).(x,y) = (|.g.|).([x,y]) by VALUED_1:def 11,A36;
end;
A38: for x be Element of CarProduct(Seg n --> REAL) st x in CarProduct D1
holds 0 <= Integral2 (L-Meas,|.Rg0.|).x
proof
let x be Element of CarProduct(Seg n --> REAL);
assume
A39: x in CarProduct D1;
reconsider Pg = ProjPMap1(|.Rg0.|,x) as PartFunc of REAL,REAL
by MESFUN16:30;
A40: dom Pg = ['s,t'] by A25,A39,A30,A32,MESFUN16:25; then
A41: Pg|| ['s,t'] is bounded & Pg is_integrable_on ['s,t']
by A16,A20,Th25,INTEGRA5:10,11;
A42: integral(Pg,s,t) = Integral(L-Meas,Pg| [.s,t.])
by A40,A25,A41,XXREAL_1:29,MESFUN14:50; then
integral(Pg,s,t) = Integral(L-Meas,ProjPMap1(|.Rg0.|,x))
by A40,A25,MESFUNC5:def 7; then
A43: Integral2(L-Meas,|.Rg0.|).x = integral(Pg,s,t) by MESFUN12:def 8;
A44: Pg = R_EAL(Pg| [.s,t.]) by A25,A40,MESFUNC5:def 7;
[.s,t.] is Element of L-Field by MEASUR10:5,MEASUR12:75; then
Pg| [.s,t.] is_integrable_on L-Meas by A40,A25,A41,MESFUN14:49; then
ex A be Element of L-Field st
A = dom R_EAL(Pg| [.s,t.]) & R_EAL(Pg| [.s,t.]) is A-measurable
by MESFUNC5:def 17; then
A45: J = dom (Pg| [.s,t.]) & Pg| [.s,t.] is J -measurable
by A40,A44,MESFUNC5:def 7;
for y being object st y in dom (Pg| [.s,t.]) holds 0 <= (Pg| [.s,t.]).y
proof
let y being object;
assume
A46: y in dom (Pg| [.s,t.]); then
reconsider y1=y as Element of REAL;
(ProjPMap1(|.Rg0.|,x)).y = (|.Rg0.|). (x,y1)
& (|.Rg0.|). (x,y1) = |. g.([x,y1]) .| by A39,A25,A40,A46,A34;
hence 0 <= (Pg| [.s,t.]).y by A25,A40;
end;
hence 0 <= Integral2 (L-Meas,|.Rg0.|).x by A42,A43,A45,MESFUNC6:52,84;
end;
set G2 = Integral2(L-Meas,|.Rg0.|);
A47: dom G2 = CarProduct(Seg n --> REAL) by FUNCT_2:def 1; then
A48: dom (G2| CarProduct D1) = CarProduct D1 by A27,Th10,RELAT_1:62;
reconsider G2I = G2| CarProduct D1
as PartFunc of CarProduct(Seg n --> REAL),ExtREAL;
now let y be object;
assume y in rng G2I; then
consider x be object such that
A49: x in dom G2I & y = G2I.x by FUNCT_1:def 3;
reconsider x as Element of CarProduct(Seg n --> REAL) by A49;
reconsider Pg = ProjPMap1(|.Rg0.|,x) as PartFunc of REAL,REAL
by MESFUN16:30;
A50: dom Pg = ['s,t'] by A25,A49,A48,A32,MESFUN16:25; then
A51: Pg|| ['s,t'] is bounded by A16,A20,Th25,INTEGRA5:10;
Pg is_integrable_on ['s,t'] by A16,A20,A50,Th25,INTEGRA5:11; then
integral(Pg,s,t) = Integral(L-Meas,Pg| [.s,t.])
by A50,A25,A51,XXREAL_1:29,MESFUN14:50; then
integral(Pg,s,t) = Integral(L-Meas,ProjPMap1(|.Rg0.|,x))
by A50,A25,MESFUNC5:def 7; then
Integral2(L-Meas,|.Rg0.|).x = integral(Pg,s,t) by MESFUN12:def 8; then
(Integral2 (L-Meas,|.Rg0.|)).x in REAL by XREAL_0:def 1;
hence y in REAL by A49,A48,FUNCT_1:49;
end; then
rng G2I c= REAL & dom G2I c= CarProduct(Seg n --> REAL); then
reconsider G = G2I as PartFunc of CarProduct(Seg n --> REAL),REAL
by RELSET_1:4;
A52: dom G = CarProduct D1 by A47,A27,Th10,RELAT_1:62;
reconsider GG = G as PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real
by MEASUR15:42;
A53: for i be Nat st i in Seg n holds D1.i is closed_interval Subset of REAL
proof
let i be Nat;
assume
A54: i in Seg n; then
i <= n by FINSEQ_1:1; then
A55: D1.i = D.i by FINSEQ_3:112;
Seg n c= Seg(n+1) by FINSEQ_3:18;
hence D1.i is closed_interval Subset of REAL by A54,A55,A17;
end;
CarProduct D1 is Subset of CarProduct(Seg n --> RNS_Real)
by A30,MEASUR15:42; then
GG is_continuous_on CarProduct D1
by A16,A19,A20,A26,A23,A24,A53,Th40; then
G is_integrable_on Prod_Measure(L-Meas n) by A15,A53,RELAT_1:62; then
A56: G2I is_integrable_on Prod_Measure(L-Meas n) by MESFUNC5:def 7; then
A57: Integral(Prod_Measure(L-Meas n),G2I) < +infty by MESFUNC5:96;
A58: for i be Nat st i in Seg n holds D1.i is Interval by A53; then
reconsider AB = CarProduct D1 as Element of Prod_Field(L-Field n)
by Th9;
CarProduct(Seg n --> REAL) in Prod_Field(L-Field n) by PROB_1:5; then
reconsider NAB = CarProduct(Seg n --> REAL) \ AB
as Element of Prod_Field(L-Field n) by PROB_1:6;
A59: AB \/ NAB = CarProduct(Seg n --> REAL) by XBOOLE_1:45;
A60: AB /\ NAB = {} by XBOOLE_1:85,XBOOLE_0:def 7;
A61: for r being Element of CarProduct(Seg n --> REAL) holds 0. <= G2.r
proof
let r being Element of CarProduct(Seg n --> REAL);
r in AB or r in NAB by A59,XBOOLE_0:def 3;
hence 0 <= G2.r by A33,A38;
end; then
A62: G2 is nonnegative;
reconsider H = CarProduct(Seg n --> REAL)
as Element of Prod_Field(L-Field n) by PROB_1:5;
A63: dom G2 = H by FUNCT_2:def 1;
for r being Real holds H /\ less_dom(G2,r) in Prod_Field(L-Field n)
proof
let r being Real;
A64: ex H0 being Element of Prod_Field(L-Field n) st
H0 = dom G2I & G2I is H0 -measurable by A56,MESFUNC5:def 17;
per cases;
suppose
A65: r <= 0;
now assume less_dom (G2,r) <> {}; then
consider x be object such that
A66: x in less_dom (G2,r) by XBOOLE_0:def 1;
x in dom G2 & G2.x < r by A66,MESFUNC1:def 11;
hence contradiction by A61,A65;
end;
hence H /\ less_dom(G2,r) in Prod_Field(L-Field n) by PROB_1:4;
end;
suppose
A67: 0 < r;
A68: for z be object holds
z in less_dom(G2,r) iff z in less_dom (G2I,r) \/ NAB
proof
let z be object;
hereby assume
A69: z in less_dom(G2,r); then
A70: z in dom G2 & G2.z < r by MESFUNC1:def 11;
A71: z in AB or z in NAB by A59,A69,XBOOLE_0:def 3;
now assume
A72: z in AB; then
G2I.z < r by FUNCT_1:49,A70; then
z in less_dom (G2I,r) by A72,A52,MESFUNC1:def 11;
hence z in less_dom (G2I,r) \/ NAB by XBOOLE_0:def 3;
end;
hence z in less_dom (G2I,r) \/ NAB by A71,XBOOLE_0:def 3;
end;
assume z in less_dom (G2I,r) \/ NAB; then
per cases by XBOOLE_0:def 3;
suppose
A73: z in less_dom (G2I,r); then
z in dom G2I & G2I.z < r by MESFUNC1:def 11; then
G2.z < r by A52,FUNCT_1:49;
hence z in less_dom(G2,r) by A63,A73,MESFUNC1:def 11;
end;
suppose
A74: z in NAB; then
reconsider x=z as Element of CarProduct(Seg n --> REAL);
G2.x = 0 by A74,A33;
hence z in less_dom(G2,r) by A63,A67,MESFUNC1:def 11;
end;
end;
A75: H /\ less_dom (G2,r) = (AB \/ NAB) /\ less_dom (G2,r) by XBOOLE_1:45
.= (AB \/ NAB) /\ (less_dom (G2I,r) \/ NAB ) by A68,TARSKI:2
.= AB /\ (less_dom (G2I,r) \/ NAB )
\/ NAB /\ (less_dom (G2I,r) \/ NAB ) by XBOOLE_1:23;
AB /\ (less_dom (G2I,r) \/ NAB)
= AB /\ less_dom (G2I,r) \/ {} by A60,XBOOLE_1:23; then
A76: AB /\ (less_dom (G2I,r) \/ NAB) in Prod_Field(L-Field n) by A64,A47;
A77: less_dom (G2I,r) c= AB by MESFUNC1:def 11,A52;
NAB /\ (less_dom (G2I,r) \/ NAB)
= (NAB /\ less_dom (G2I,r)) \/ (NAB /\ NAB) by XBOOLE_1:23; then
NAB /\ (less_dom (G2I,r) \/ NAB) = {} \/ (NAB /\ NAB) by A77;
hence H /\ less_dom (G2,r) in Prod_Field(L-Field n)
by A75,A76,PROB_1:3;
end;
end; then
A78: G2 is H -measurable;
reconsider G2J = G2|NAB
as PartFunc of CarProduct(Seg n --> REAL),ExtREAL by PARTFUN1:11;
G2| (AB \/ NAB) = G2 by A59; then
A79: Integral(Prod_Measure(L-Meas n),G2)
= Integral(Prod_Measure(L-Meas n),G2I)
+ Integral(Prod_Measure(L-Meas n),G2J)
by A63,A78,A62,XBOOLE_1:79,MESFUNC5:91;
for x being object st x in dom G2J holds G2J.x = 0
proof
let x being object;
assume
A80: x in dom G2J; then
reconsider r=x as Element of CarProduct(Seg n --> REAL);
(Integral2(L-Meas,|.Rg0.|)).r = 0 by A80,A33,A47;
hence thesis by FUNCT_1:49,A80,A47;
end; then
Integral(Prod_Measure(L-Meas n),G2J)
= 0 * ((Prod_Measure(L-Meas n)). (dom G2J)) by A47,MEASUR10:27; then
A81: Integral(Prod_Measure(L-Meas n),Integral2(L-Meas,|.Rg0.|)) < +infty
by A57,A79,XXREAL_3:4;
CarProduct D1 is Element of Prod_Field(L-Field n) by A58,Th9; then
CarProduct D1 in Prod_Field(L-Field n) & [.s,t.] in L-Field
by MEASUR10:5,MEASUR12:75; then
A82: [: CarProduct D1,[.s,t .] :]
in measurable_rectangles(Prod_Field(L-Field n),L-Field);
measurable_rectangles(Prod_Field(L-Field n),L-Field)
c= sigma measurable_rectangles(Prod_Field(L-Field n),L-Field)
by PROB_1:def 9; then
reconsider E0 = [:CarProduct(D1),[.s,t .]:] as Element of
sigma measurable_rectangles(Prod_Field(L-Field n),L-Field) by A82;
A83: Prod_Field(L-Field (n+1))
= sigma measurable_rectangles(Prod_Field(L-Field n),L-Field)
by MEASUR14:44; then
reconsider Rg0 as E0-measurable PartFunc of
[: CarProduct(Seg n --> REAL),REAL:],ExtREAL by A22,A21,A26;
Prod_Measure(L-Meas n) is sigma_finite by MEASUR15:36; then
Rg0 is_integrable_on Prod_Measure(Prod_Measure(L-Meas n),L-Meas)
by A31,MESFUN16:5,A81,MESFUN13:11;
hence g is_integrable_on Prod_Measure(L-Meas(n+1))
by A21,A83,MEASUR14:48;
end;
suppose s > t; then
A84: D.(n+1) = {} by A24,XXREAL_1:29;
n < n+1 by NAT_1:13; then
(ProdFinSeq D).(n+1) = [:(ProdFinSeq D).n,D.(n+1):]
by MEASUR13:def 3; then
CarProduct D = {} by A84;
hence g is_integrable_on Prod_Measure(L-Meas (n+1)) by A16,A19,Th1;
end;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A1,A14);
hence thesis;
end;
theorem Th44:
for n be non zero Nat, D be n-element FinSequence,
J be Subset of REAL, y be Element of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL
st (for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL)
& y in J & dom f = [:CarProduct D,J:] & f is_continuous_on [:CarProduct D,J:]
& f = g
holds dom ProjPMap2(R_EAL g,y) = CarProduct D
& ProjPMap2(R_EAL g,y) is_integrable_on Prod_Measure(L-Meas n)
proof
let n be non zero Nat,
D be n-element FinSequence,
J be Subset of REAL,
y be Element of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL;
assume that
A1: for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL and
A2: y in J and
A3: dom f = [:CarProduct D,J:] and
A4: f is_continuous_on [:CarProduct D,J:] and
A5: f = g;
reconsider RPg2 = ProjPMap2(R_EAL g,y)
as PartFunc of CarProduct(Seg n --> REAL),REAL by MESFUN16:30;
ProjPMap2(R_EAL g,y)
is PartFunc of CarProduct(Seg n --> REAL),REAL by MESFUN16:30; then
reconsider Pg2 = ProjPMap2(R_EAL g,y)
as PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real by MEASUR15:42;
for i be Nat st i in Seg n holds D.i is Subset of REAL by A1; then
A6: CarProduct D is Subset of CarProduct(Seg n --> REAL)
by FINSEQ_1:3,Th11; then
dom Pg2 = CarProduct D by A2,A3,A5,MESFUN16:28; then
RPg2 is_integrable_on Prod_Measure(L-Meas n) by A1,A3,A4,A5,Th24,Th43;
hence thesis by A6,A2,A3,A5,MESFUN16:28,MESFUNC5:def 7;
end;
theorem Th45:
for n be non zero Nat, D be n-element FinSequence,
J be Subset of REAL, y be Element of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg2 be PartFunc of CarProduct(Seg n --> REAL),REAL
st (for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL)
& y in J & dom f = [:CarProduct D,J:] & f is_continuous_on [:CarProduct D,J:]
& f = g & Pg2 = ProjPMap2(R_EAL g,y)
holds Pg2 is_integrable_on Prod_Measure(L-Meas n)
& Integral(Prod_Measure(L-Meas n),ProjPMap2(R_EAL g,y))
= (Integral1(Prod_Measure(L-Meas n),R_EAL g)).y
proof
let n be non zero Nat, D be n-element FinSequence,
J be Subset of REAL, y be Element of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg2 be PartFunc of CarProduct(Seg n --> REAL),REAL;
assume that
A1: for i be Nat st i in Seg n
holds D.i is closed_interval Subset of REAL and
A2: y in J and
A3: dom f = [:CarProduct D,J:] and
A4: f is_continuous_on [:CarProduct D,J:] and
A5: f = g and
A6: Pg2 = ProjPMap2(R_EAL g,y);
R_EAL Pg2 = ProjPMap2(R_EAL g,y) by A6,MESFUNC5:def 7;
hence Pg2 is_integrable_on Prod_Measure(L-Meas n) by A1,A2,A3,A4,A5,Th44;
thus thesis by MESFUN12:def 7;
end;
theorem Th46:
for n be non zero Nat, D be n-element FinSequence, J be Subset of REAL,
y be Element of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL
st (for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL)
& y in J & dom f = [:CarProduct D,J:] & f is_continuous_on [:CarProduct D,J:]
& f = g
holds dom ProjPMap2(|.R_EAL g.|,y) = CarProduct D
& ProjPMap2(|.R_EAL g.|,y) is_integrable_on Prod_Measure(L-Meas n)
proof
let n be non zero Nat, D be n-element FinSequence,
J be Subset of REAL,
y be Element of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL;
assume that
A1: for i be Nat st i in Seg n
holds D.i is closed_interval Subset of REAL and
A2: y in J and
A3: dom f = [:CarProduct D,J:] and
A4: f is_continuous_on [:CarProduct D,J:] and
A5: f = g;
reconsider RPg2 = ProjPMap2(|.R_EAL g.|,y)
as PartFunc of CarProduct(Seg n --> REAL),REAL by MESFUN16:30;
ProjPMap2(|.R_EAL g.|,y)
is PartFunc of CarProduct(Seg n --> REAL),REAL by MESFUN16:30; then
reconsider Pg2 = ProjPMap2(|.R_EAL g.|,y)
as PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real by MEASUR15:42;
for i be Nat st i in Seg n holds D.i is Subset of REAL by A1; then
A6: CarProduct D is Subset of CarProduct(Seg n --> REAL)
by FINSEQ_1:3,Th11; then
dom Pg2 = CarProduct D by A2,A3,A5,MESFUN16:28; then
RPg2 is_integrable_on Prod_Measure(L-Meas n) by A1,A3,A4,A5,Th26,Th43;
hence thesis by A2,A3,A5,A6,MESFUNC5:def 7,MESFUN16:28;
end;
theorem Th47:
for n be non zero Nat, D be n-element FinSequence, J be Subset of REAL,
y be Element of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
E be Element of Prod_Field(L-Field n)
st (for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL)
& y in J & dom f = [:CarProduct D,J:] & f is_continuous_on [:CarProduct D,J:]
& f = g & E = CarProduct D holds ProjPMap2(|.R_EAL g.|,y) is E-measurable
proof
let n be non zero Nat, D be n-element FinSequence,
J be Subset of REAL,
y be Element of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
E be Element of Prod_Field(L-Field n);
assume that
A1: for i be Nat st i in Seg n
holds D.i is closed_interval Subset of REAL and
A2: y in J and
A3: dom f = [:CarProduct D,J:] and
A4: f is_continuous_on [:CarProduct D,J:] and
A5: f = g and
A6: E = CarProduct D;
A7: dom ProjPMap2(|.R_EAL g.|,y) = CarProduct D
& ProjPMap2(|.R_EAL g.|,y) is_integrable_on Prod_Measure(L-Meas n)
by A1,A2,A3,A4,A5,Th46; then
ex A be Element of Prod_Field(L-Field n)
st A = dom ProjPMap2(|.R_EAL g.|,y)
& ProjPMap2(|.R_EAL g.|,y) is A-measurable by MESFUNC5:def 17;
hence ProjPMap2(|.R_EAL g.|,y) is E-measurable by A6,A7;
end;
theorem Th48:
for n be non zero Nat, D be n-element FinSequence, J be Subset of REAL,
y be Element of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg2 be PartFunc of CarProduct(Seg n --> REAL),REAL
st (for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL)
& y in J & dom f = [:CarProduct D,J:] & f is_continuous_on [:CarProduct D,J:]
& f = g & Pg2 = ProjPMap2(|.R_EAL g.|,y)
holds Pg2 is_integrable_on Prod_Measure(L-Meas n)
& Integral(Prod_Measure(L-Meas n),ProjPMap2(|.R_EAL g.|,y))
= (Integral1(Prod_Measure(L-Meas n),|.R_EAL g.|)).y
proof
let n be non zero Nat, D be n-element FinSequence,
J be Subset of REAL,
y be Element of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
Pg2 be PartFunc of CarProduct(Seg n --> REAL),REAL;
assume that
A1: for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL and
A2: y in J and
A3: dom f = [:CarProduct D,J:] and
A4: f is_continuous_on [:CarProduct D,J:] and
A5: f = g and
A6: Pg2 = ProjPMap2(|.R_EAL g.|,y);
R_EAL Pg2 = ProjPMap2(|.R_EAL g.|,y) by A6,MESFUNC5:def 7;
hence Pg2 is_integrable_on Prod_Measure(L-Meas n) by A1,A2,A3,A4,A5,Th46;
thus thesis by MESFUN12:def 7;
end;
theorem Th49:
for n be non zero Nat, D be n-element FinSequence,
I be Subset of CarProduct(Seg n --> RNS_Real), J be Interval
st (for i be Nat st i in Seg n holds D.i is Interval) & I = CarProduct D
holds [:I,J:] is Subset of [:CarProduct(Seg n --> RNS_Real),RNS_Real:]
& [:I,J:] in sigma measurable_rectangles(Prod_Field(L-Field n),L-Field)
proof
let n be non zero Nat, D be n-element FinSequence,
I be Subset of CarProduct(Seg n --> RNS_Real),
J be Interval;
assume that
A1: for i be Nat st i in Seg n holds D.i is Interval and
A2: I = CarProduct D;
I is Element of Prod_Field(L-Field n) by A1,A2,Th9; then
I in Prod_Field(L-Field n) & J in L-Field
by MEASUR10:5,MEASUR12:75; then
A3: [:I,J:] in measurable_rectangles(Prod_Field(L-Field n),L-Field);
reconsider J1 = J as Subset of RNS_Real;
A4: [:I,J:] = [:I,J1:];
measurable_rectangles(Prod_Field(L-Field n),L-Field)
c= sigma measurable_rectangles(Prod_Field(L-Field n),L-Field)
by PROB_1:def 9;
hence thesis by A3,A4;
end;
theorem Th50:
for n be non zero Nat, D be n-element FinSequence, J be Subset of REAL,
f being PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL
st (for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL)
& [:CarProduct D,J:] = dom f & f is_continuous_on [:CarProduct D,J:]
& f = g holds
Integral1(Prod_Measure(L-Meas n),|.R_EAL g.|) |J is PartFunc of REAL,REAL
& Integral1(Prod_Measure(L-Meas n),R_EAL g) |J is PartFunc of REAL,REAL
proof
let n be non zero Nat, D be n-element FinSequence,
J be Subset of REAL,
f being PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL;
assume that
A1: for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL and
A2: [:CarProduct D,J:] = dom f and
A3: f is_continuous_on [:CarProduct D,J:] and
A4: f = g;
set g1 = R_EAL g;
set T = Integral1(Prod_Measure(L-Meas n),|.g1.|);
A5: dom T = REAL by FUNCT_2:def 1;
reconsider T0 = T|J as PartFunc of REAL,ExtREAL by PARTFUN1:11;
set RT = Integral1(Prod_Measure(L-Meas n),g1);
A6: dom RT = REAL by FUNCT_2:def 1;
reconsider RT0 = RT|J as PartFunc of REAL,ExtREAL by PARTFUN1:11;
now let x be object;
assume x in rng T0; then
consider y be Element of REAL such that
A7: y in dom T0 & x = T0.y by PARTFUN1:3;
reconsider Pg = ProjPMap2(|.g1.|,y)
as PartFunc of CarProduct(Seg n --> REAL),REAL by MESFUN16:30;
A8: R_EAL Pg = ProjPMap2(|.g1.|,y) by MESFUNC5:def 7;
Pg is_integrable_on Prod_Measure(L-Meas n)
by A7,A1,A5,A2,A3,A4,Th48; then
-infty < Integral(Prod_Measure(L-Meas n),Pg)
& Integral(Prod_Measure(L-Meas n),Pg) < +infty by MESFUNC6:90; then
A9: Integral(Prod_Measure(L-Meas n),Pg) in REAL by XXREAL_0:14;
(Integral1(Prod_Measure(L-Meas n),|.g1.|)).y
= Integral(Prod_Measure(L-Meas n),Pg) by A8,A7,A1,A5,A2,A3,A4,Th48;
hence x in REAL by A7,A5,A9,FUNCT_1:49;
end; then
rng T0 c= REAL & dom T0 c= REAL;
hence Integral1(Prod_Measure(L-Meas n),|.R_EAL g.|) |J
is PartFunc of REAL,REAL by RELSET_1:4;
now let x be object;
assume x in rng RT0; then
consider y be Element of REAL such that
A10: y in dom RT0 & x= RT0.y by PARTFUN1:3;
reconsider Pg = ProjPMap2(g1,y)
as PartFunc of CarProduct(Seg n --> REAL),REAL by MESFUN16:30;
A11: R_EAL Pg = ProjPMap2(g1,y) by MESFUNC5:def 7;
Pg is_integrable_on Prod_Measure(L-Meas n)
by A1,A10,A6,A2,A3,A4,Th45; then
-infty < Integral(Prod_Measure(L-Meas n),Pg)
& Integral(Prod_Measure(L-Meas n),Pg) < +infty by MESFUNC6:90; then
A12: Integral(Prod_Measure(L-Meas n),Pg) in REAL by XXREAL_0:14;
(Integral1(Prod_Measure(L-Meas n),g1)).y
= Integral(Prod_Measure(L-Meas n),Pg) by A11,A1,A10,A6,A2,A3,A4,Th45;
hence x in REAL by A10,A6,A12,FUNCT_1:49;
end; then
rng RT0 c= REAL & dom RT0 c= REAL;
hence Integral1(Prod_Measure(L-Meas n),R_EAL g) |J
is PartFunc of REAL,REAL by RELSET_1:4;
end;
theorem Th51:
for n be non zero Nat, E1 be Element of Prod_Field(L-Field n),
E2 be Element of L-Field holds
[:E1,E2:] in sigma measurable_rectangles(Prod_Field(L-Field n),L-Field)
& (Prod_Measure(L-Meas(n+1))).([:E1,E2:])
= ((Prod_Measure(L-Meas n)).E1) * (L-Meas.E2)
proof
let n be non zero Nat, E1 be Element of Prod_Field(L-Field n),
E2 be Element of L-Field;
A1: [:E1,E2:] in measurable_rectangles(Prod_Field(L-Field n),L-Field);
A2: measurable_rectangles(Prod_Field(L-Field n),L-Field)
c= sigma measurable_rectangles(Prod_Field(L-Field n),L-Field)
by PROB_1:def 9;
hence [:E1,E2:]
in sigma measurable_rectangles(Prod_Field(L-Field n),L-Field) by A1;
reconsider E = [:E1,E2:] as Element of
sigma measurable_rectangles(Prod_Field(L-Field n),L-Field)
by A1,A2;
(product_sigma_Measure(Prod_Measure(L-Meas n),L-Meas)).E
= (Prod_Measure(L-Meas n)).E1 * (L-Meas.E2) by MEASUR11:16; then
Prod_Measure(Prod_Measure(L-Meas n),L-Meas).E
= (Prod_Measure(L-Meas n)).E1 * (L-Meas.E2) by MESFUN12:def 9;
hence (Prod_Measure(L-Meas(n+1))).([:E1,E2:])
= ((Prod_Measure(L-Meas n)).E1) * (L-Meas.E2) by MEASUR14:48;
end;
theorem Th52:
for n be non zero Nat, D be n-element FinSequence
st for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL
ex r be Real, E be Element of Prod_Field(L-Field n) st
E = CarProduct D & (Prod_Measure(L-Meas n)).E = r & 0 <= r
proof
let n be non zero Nat;
defpred P[non zero Nat] means
for D be $1-element FinSequence st
for i be Nat st i in Seg $1 holds
D.i is closed_interval Subset of REAL
ex r be Real, E be Element of Prod_Field(L-Field $1) st
E = CarProduct D & (Prod_Measure(L-Meas $1)).E = r & 0 <= r;
A1: P[1]
proof
let D be 1-element FinSequence;
assume
A2: for i be Nat st i in Seg 1 holds D.i is closed_interval Subset of REAL;
A3: 1 in Seg 1;
A4: CarProduct D = D.1 by MEASUR13:def 3; then
A5: CarProduct D is closed_interval Subset of REAL by A2,A3; then
reconsider E = CarProduct D as Element of Prod_Field(L-Field 1)
by MEASUR14:41;
per cases;
suppose
A6: D.1 <> {};
consider a,b be Real such that
A7: E = [.a,b.] by A5,MEASURE5:def 3;
A8: a <= b by A7,A4,A6,XXREAL_1:29;
set r = b-a;
take r,E;
thus E = CarProduct D;
thus (Prod_Measure(L-Meas 1)).E = r by A7,A8,MESFUN14:5,MEASUR14:45;
thus 0 <= r by A7,A4,A6,XXREAL_1:29,XREAL_1:48;
end;
suppose
A9: D.1 = {};
reconsider E = {} as Element of Prod_Field(L-Field 1) by MEASURE1:7;
set r = 0;
take r,E;
thus E = CarProduct D by A9,MEASUR13:def 3;
thus (Prod_Measure(L-Meas 1)).E = r by VALUED_0:def 19;
thus 0 <= r;
end;
end;
A10: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A11: P[n];
let D be (n+1)-element FinSequence;
assume
A12: for i be Nat st i in Seg (n+1) holds
D.i is closed_interval Subset of REAL;
reconsider D1=D|n as n-element FinSequence;
for i be Nat st i in Seg n holds D1.i is closed_interval Subset of REAL
proof
let i be Nat;
assume
A13: i in Seg n;
A14: Seg n c= Seg(n+1) by FINSEQ_3:18;
D1.i = D.i by A13,FUNCT_1:49;
hence D1.i is closed_interval Subset of REAL by A12,A13,A14;
end; then
consider r1 be Real, E1 be Element of Prod_Field(L-Field n)
such that
A15: E1 = CarProduct D1 & (Prod_Measure(L-Meas n)).E1 = r1 & 0 <= r1 by A11;
for i be Nat st i in Seg(n+1) holds D.i is Interval by A12; then
reconsider E = CarProduct D as Element of Prod_Field(L-Field(n+1))
by Th9;
A16: D.(n+1) is closed_interval Subset of REAL by A12,FINSEQ_1:4; then
reconsider E2 = D.(n+1) as Element of L-Field by MEASUR12:72,75;
consider a,b be Real such that
A17: D.(n+1) = [.a,b.] by A16,MEASURE5:def 3;
CarProduct D = [: CarProduct D1,D.(n+1) :] by Th4; then
A18: (Prod_Measure(L-Meas(n+1))).E
= (Prod_Measure(L-Meas n)).E1 * (L-Meas.E2) by A15,Th51;
per cases;
suppose D.(n+1) = {}; then
A19: L-Meas.E2 = 0 by VALUED_0:def 19;
take r = 0;
take E;
thus E = CarProduct D;
thus (Prod_Measure(L-Meas(n+1))).E = r by A18,A19;
thus 0 <= r;
end;
suppose
A20: D.(n+1) <> {}; then
a <= b by A17,XXREAL_1:29; then
A21: L-Meas.E2 = b-a by A17,MESFUN14:5;
take r = r1 * (b-a);
take E;
thus E = CarProduct D;
thus (Prod_Measure(L-Meas(n+1))).E = r by A18,A15,A21,XXREAL_3:def 5;
b-a >= 0 by A17,A20,XREAL_1:48,XXREAL_1:29;
hence 0 <= r by A15;
end;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A1,A10);
hence thesis;
end;
theorem Th53:
for n be non zero Nat, D be n-element FinSequence,
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
G1 be PartFunc of REAL,REAL
st (for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL)
& [:CarProduct D,J:] = dom f & f is_continuous_on [:CarProduct D,J:]
& f = g & G1 = Integral1(Prod_Measure(L-Meas n),|.R_EAL g.|) |J
holds G1 is continuous
proof
let n be non zero Nat,
D be n-element FinSequence,
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
G1 be PartFunc of REAL,REAL;
assume that
A1: for i be Nat st i in Seg n
holds D.i is closed_interval Subset of REAL and
A2: [:CarProduct D,J:] = dom f and
A3: f is_continuous_on [:CarProduct D,J:] and
A4: f = g and
A5: G1 = Integral1(Prod_Measure(L-Meas n),|.R_EAL g.|) |J;
A6: for e be Real st 0 < e holds ex r be Real st 0 < r
& for y1,y2 be Real st |.y2-y1.| < r & y1 in J & y2 in J
holds for x be Point of CarProduct(Seg n --> RNS_Real)
st x in CarProduct D holds
|. (|.g.|).([x,y2])-(|.g.|).([x,y1]) .| < e
proof
let e be Real;
assume 0 < e; then
consider r be Real such that
A7: 0 < r
& for x1,x2 be Point of CarProduct(Seg n --> RNS_Real), y1,y2 be Real
st [x1,y1] in [:CarProduct D,J:] & [x2,y2] in [:CarProduct D,J:]
& ||.x2-x1.|| < r & |.y2-y1.| < r holds
|. (|.g.|).([x2,y2])-(|.g.|).([x1,y1]) .| < e by A1,A3,A4,Th39;
take r ;
thus 0 < r by A7;
let y1,y2 be Real;
assume
A8: |.y2-y1.| < r & y1 in J & y2 in J;
let x be Point of CarProduct(Seg n --> RNS_Real);
assume x in CarProduct D; then
A9: [x,y1] in [:CarProduct D,J:] & [x,y2] in [:CarProduct D,J:]
by A8,ZFMISC_1:87;
x-x=0.(CarProduct(Seg n --> RNS_Real)) by RLVECT_1:15; then
||.x-x.|| < r by A7;
hence |. (|.g.|).([x,y2])-(|.g.|).([x,y1]) .| < e by A7,A8,A9;
end;
set Rg =R_EAL g;
dom |.Rg.| = dom Rg by MESFUNC1:def 10; then
A10:dom |.Rg.| = [:CarProduct D,J:] by A2,A4,MESFUNC5:def 7;
A11:for x be Element of CarProduct(Seg n --> REAL), y be Element of REAL
st x in CarProduct D & y in J holds
(ProjPMap2(|.Rg.|,y)).x =(|.Rg.|).(x,y)
& (|.Rg.|).(x,y) = |. g.([x,y]) .| & (|.Rg.|).(x,y) = (|.g.|).([x,y])
proof
let x be Element of CarProduct(Seg n --> REAL), y be Element of REAL;
assume
A12: x in CarProduct D & y in J;
hence (ProjPMap2(|.Rg.|,y)).x =(|.Rg.|).(x,y)
by A10,ZFMISC_1:87,MESFUN12:def 4;
[x,y] in dom g by A12,A2,A4,ZFMISC_1:87; then
A13: [x,y] in dom |.g.| by VALUED_1:def 11;
A14: Rg.([x,y]) = g.([x,y]) by MESFUNC5:def 7;
(|.Rg.|).(x,y) = |. Rg.([x,y]) .|
by A12,A10,ZFMISC_1:87,MESFUNC1:def 10;
hence (|.Rg.|).(x,y) = |.g.([x,y]).| by A14,EXTREAL1:12;
hence (|.Rg.|).(x,y) = (|.g.|).([x,y]) by VALUED_1:def 11,A13;
end;
A15:for e be Real st 0 < e holds ex r be Real st 0 < r
& for y1,y2 be Element of REAL st |.y2-y1.| < r & y1 in J
& y2 in J holds for x be Element of CarProduct(Seg n --> REAL)
st x in CarProduct D
holds |. (ProjPMap2(|.Rg.|,y2)).x-(ProjPMap2(|.Rg.|,y1)).x .| < e
proof
let e be Real;
assume 0 < e; then
consider r be Real such that
A16: 0 < r
& for y1,y2 be Real st |.y2-y1.| < r & y1 in J & y2 in J
holds for x be Point of CarProduct(Seg n --> RNS_Real)
st x in CarProduct D holds
|. (|.g.|).([x,y2])-(|.g.|).([x,y1]) .| < e by A6;
take r;
thus 0 < r by A16;
let y1,y2 be Element of REAL;
assume
A17: |.y2-y1.| < r & y1 in J & y2 in J;
let x be Element of CarProduct(Seg n --> REAL);
assume
A18: x in CarProduct D;
x is Point of CarProduct(Seg n --> RNS_Real) by MEASUR15:42; then
A19: |. (|.g.|).([x,y2])-(|.g.|).([x,y1]) .| < e by A16,A17,A18;
(ProjPMap2(|.Rg.|,y1)).x =(|.Rg.|).(x,y1)
& (|.Rg.|).(x,y1) = (|.g.|).([x,y1])
& (ProjPMap2(|.Rg.|,y2)).x =(|.Rg.|).(x,y2)
& (|.Rg.|).(x,y2) = (|.g.|).([x,y2]) by A11,A17,A18; then
(ProjPMap2(|.Rg.|,y2)).x-(ProjPMap2(|.Rg.|,y1)).x
= (|.g.|).([x,y2])-(|.g.|).([x,y1]) by Lm2;
hence thesis by A19,EXTREAL1:12;
end;
set T = Integral1(Prod_Measure(L-Meas n),|.Rg.|);
A20:dom T = REAL by FUNCT_2:def 1;
for y0,r be Real st y0 in J & 0 < r
ex s be Real st 0<s & for y1 be Real
st y1 in J & |.y1-y0.| < s holds |.G1.y1-G1.y0.| < r
proof
let yy0,r be Real;
assume
A21: yy0 in J & 0 < r;
reconsider y0=yy0 as Element of REAL by XREAL_0:def 1;
reconsider RPg0 = ProjPMap2(|.Rg.|,y0)
as PartFunc of CarProduct(Seg n --> REAL),REAL by MESFUN16:30;
reconsider Pg0 = RPg0
as PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real by MEASUR15:42;
for i be Nat st i in Seg n holds D.i is Subset of REAL by A1; then
A22: CarProduct D is Subset of CarProduct(Seg n --> REAL)
by FINSEQ_1:3,Th11; then
A23: dom Pg0 = CarProduct D by A21,A2,A4,MESFUN16:28;
A24: RPg0 is_integrable_on Prod_Measure(L-Meas n)
by A1,A23,A2,A3,A4,Th26,Th43;
A25: R_EAL RPg0 = ProjPMap2(|.R_EAL g.|,y0) by MESFUNC5:def 7;
RPg0 = ProjPMap2(|.R_EAL g.|,y0); then
A26: (Integral1(Prod_Measure(L-Meas n),|.R_EAL g.|)).y0
= Integral(Prod_Measure(L-Meas n),ProjPMap2(|.R_EAL g.|,y0))
by A1,A21,A2,A3,A4,Th48;
consider r0 be Real, E1 be Element of Prod_Field(L-Field n) such that
A27: E1 = CarProduct D & (Prod_Measure(L-Meas n)).E1 = r0 & 0 <= r0
by A1,Th52;
per cases;
suppose A28: r0 = 0;
consider s be Real such that
A29: 0 < s
& for y1,y2 be Element of REAL st |.y2-y1.| < s & y1 in J & y2 in J
holds for x be Element of CarProduct(Seg n --> REAL)
st x in CarProduct D holds
|. (ProjPMap2(|.Rg.|,y2)).x-(ProjPMap2(|.Rg.|,y1)).x .| < r
by A15,A21;
for y1 be Real st y1 in J & |.y1-y0.| < s holds |.G1.y1-G1.yy0 .| < r
proof
let yy1 be Real;
assume
A30: yy1 in J & |.yy1-y0.| < s;
reconsider y1=yy1 as Element of REAL by XREAL_0:def 1;
reconsider RPg1 = ProjPMap2(|.Rg.|,y1)
as PartFunc of CarProduct(Seg n --> REAL),REAL by MESFUN16:30;
reconsider Pg1 = RPg1
as PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real by MEASUR15:42;
A31: dom Pg1 = CarProduct D by A22,A30,A2,A4,MESFUN16:28;
A32: R_EAL RPg1 = ProjPMap2(|.R_EAL g.|,y1) by MESFUNC5:def 7;
RPg1 = ProjPMap2(|.R_EAL g.|,y1); then
(Integral1(Prod_Measure(L-Meas n),|.Rg.|)).y1
= Integral(Prod_Measure(L-Meas n),ProjPMap2(|.R_EAL g.|,y1))
by A1,A30,A2,A3,A4,Th48; then
A33: G1.yy0 = Integral(Prod_Measure(L-Meas n),RPg0)
& G1.yy1 = Integral(Prod_Measure(L-Meas n),RPg1)
by A25,A32,A5,A21,A26,A30,FUNCT_1:49;
A34: -(G1.yy0) = -Integral(Prod_Measure(L-Meas n),RPg0)
by A33,XXREAL_3:def 3;
A35: RPg1 is_integrable_on Prod_Measure(L-Meas n)
by A1,A31,A2,A3,A4,Th26,Th43; then
A36: RPg1-RPg0 is_integrable_on Prod_Measure(L-Meas n)
by A24,MESFUN6C:34;
A37: dom(RPg1-RPg0) = CarProduct D /\ CarProduct D
by A23,A31,VALUED_1:12; then
A38: dom(R_EAL(RPg1-RPg0)) = E1 by A27,MESFUNC5:def 7;
A39: (Prod_Measure(L-Meas n)).E1 < +infty by A27,XREAL_0:def 1,XXREAL_0:9;
for x be Element of CarProduct(Seg n --> REAL)
st x in E1 holds
-r <= (R_EAL (RPg1-RPg0)).x & (R_EAL (RPg1-RPg0)).x <= r
proof
let x be Element of CarProduct(Seg n --> REAL);
assume
A40: x in E1; then
A41: |. (ProjPMap2(|.Rg.|,y1)).x-(ProjPMap2(|.Rg.|,y0)).x .| < r
by A27,A29,A30,A21;
(ProjPMap2(|.Rg.|,y1)).x-(ProjPMap2(|.Rg.|,y0)).x
= RPg1.x - RPg0.x by Lm2; then
(ProjPMap2(|.Rg.|,y1)).x-(ProjPMap2(|.Rg.|,y0)).x = (RPg1-RPg0).x
by A27,A37,A40,VALUED_1:13; then
|. (RPg1-RPg0).x .| <= r by A41,EXTREAL1:12; then
-r <= (RPg1-RPg0).x & (RPg1-RPg0).x <= r by ABSVALUE:5;
hence -r <= (R_EAL (RPg1-RPg0)).x & (R_EAL (RPg1-RPg0)).x <= r
by MESFUNC5:def 7;
end; then
(-r)*(Prod_Measure(L-Meas n)).E1
<= Integral(Prod_Measure(L-Meas n),(R_EAL(RPg1-RPg0)) |E1)
& Integral(Prod_Measure(L-Meas n),(R_EAL(RPg1-RPg0)) |E1)
<= r * (Prod_Measure(L-Meas n)).E1 by A38,A36,A39,MESFUNC7:26; then
A42: 0 <= Integral(Prod_Measure(L-Meas n),(R_EAL(RPg1-RPg0)))
& Integral(Prod_Measure(L-Meas n),(R_EAL(RPg1-RPg0))) <= 0
by A28,A27,A38;
A43: (-1)(#)RPg0 = -RPg0 by VALUED_1:def 6;
A44: (-1) (#) RPg0 is_integrable_on Prod_Measure(L-Meas n)
& Integral(Prod_Measure(L-Meas n),(-1)(#)RPg0)
= (-1)*Integral(Prod_Measure(L-Meas n),RPg0) by A24,MESFUNC6:102; then
A45: (-RPg0) is_integrable_on Prod_Measure(L-Meas n)
& Integral(Prod_Measure(L-Meas n),-RPg0)
= -Integral(Prod_Measure(L-Meas n),RPg0) by A43,XXREAL_3:91;
A46: dom(-RPg0) = E1 by A27,A23,A43,VALUED_1:def 5;
A47: RPg1+(-RPg0) = RPg1 - RPg0 by VALUED_1:def 9;
ex E be Element of Prod_Field(L-Field n) st
E = dom RPg1 /\ dom(-RPg0)
& Integral(Prod_Measure(L-Meas n),RPg1+(-RPg0))
= Integral(Prod_Measure(L-Meas n),RPg1|E)
+ Integral(Prod_Measure(L-Meas n),(-RPg0) |E)
by A35,A43,A44,MESFUNC6:101; then
Integral(Prod_Measure(L-Meas n),RPg1-RPg0)
= G1.yy1 + - G1.yy0 by A33,A34,A27,A31,A46,A47,A45,XXREAL_3:def 2;
hence |. G1.yy1-G1.yy0 .| < r by A21,A42;
end;
hence ex s be Real st 0<s & for y1 be Real
st y1 in J & |.y1-yy0.| < s holds |.G1.y1-G1.yy0.| < r by A29;
end;
suppose A48: r0 <> 0;
set r1=r/2;
A49: 0 < r1 & r1 < r by A21,XREAL_1:215,XREAL_1:216; then
consider s be Real such that
A50: 0 < s
& for y1,y2 be Element of REAL st |.y2-y1.| < s & y1 in J & y2 in J
holds for x be Element of CarProduct(Seg n --> REAL)
st x in CarProduct D holds
|. (ProjPMap2(|.Rg.|,y2)).x-(ProjPMap2(|.Rg.|,y1)).x .| < r1/ r0
by A15,A48,A27,XREAL_1:139;
take s;
thus 0 < s by A50;
let yy1 be Real;
assume
A51: yy1 in J & |.yy1-yy0.| < s;
reconsider y1=yy1 as Element of REAL by XREAL_0:def 1;
reconsider RPg1 = ProjPMap2(|.Rg.|,y1)
as PartFunc of CarProduct(Seg n --> REAL),REAL by MESFUN16:30;
reconsider Pg1 = RPg1
as PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real by MEASUR15:42;
A52: dom Pg1 = CarProduct D by A22,A51,A2,A4,MESFUN16:28; then
A53: RPg1 is_integrable_on Prod_Measure(L-Meas n) by A1,A2,A3,A4,Th26,Th43;
A54: R_EAL RPg1 = ProjPMap2(|.R_EAL g.|,y1) by MESFUNC5:def 7;
RPg1 = ProjPMap2(|.R_EAL g.|,y1); then
(Integral1(Prod_Measure(L-Meas n),|.Rg.|)).y1
= Integral(Prod_Measure(L-Meas n),ProjPMap2(|.R_EAL g.|,y1))
by A1,A51,A2,A3,A4,Th48; then
A55: G1.yy0 = Integral(Prod_Measure(L-Meas n),RPg0)
& G1.yy1 = Integral(Prod_Measure(L-Meas n),RPg1)
by A25,A54,A5,A21,A26,A51,FUNCT_1:49;
A56: -(G1.yy0) = -Integral(Prod_Measure(L-Meas n),RPg0) by A55,XXREAL_3:def 3;
A57: RPg1-RPg0 is_integrable_on Prod_Measure(L-Meas n) by A24,A53,MESFUN6C:34;
A58: dom(RPg1-RPg0) = CarProduct D /\ CarProduct D
by A23,A52,VALUED_1:12; then
A59: dom(R_EAL(RPg1-RPg0)) = E1 by A27,MESFUNC5:def 7;
A60: (Prod_Measure(L-Meas n)).E1 < +infty by A27,XXREAL_0:9,XREAL_0:def 1;
for x be Element of CarProduct(Seg n --> REAL) st x in E1 holds
-(r1/r0) <= (R_EAL (RPg1-RPg0)).x & (R_EAL (RPg1-RPg0)).x <= r1/r0
proof
let x be Element of CarProduct(Seg n --> REAL);
assume
A61: x in E1; then
A62: |. (ProjPMap2(|.Rg.|,y1)).x-(ProjPMap2(|.Rg.|,y0)).x .| < r1/ r0
by A27,A50,A51,A21;
(ProjPMap2(|.Rg.|,y1)).x-(ProjPMap2(|.Rg.|,y0)).x
= RPg1.x - RPg0.x by Lm2; then
(ProjPMap2(|.Rg.|,y1)).x-(ProjPMap2(|.Rg.|,y0)).x = (RPg1-RPg0).x
by A27,A58,A61,VALUED_1:13; then
|. (RPg1-RPg0).x .| <= r1/r0 by A62,EXTREAL1:12; then
-(r1/r0) <= (RPg1-RPg0).x & (RPg1-RPg0).x <= r1/r0 by ABSVALUE:5;
hence -(r1/r0) <= (R_EAL (RPg1-RPg0)).x
& (R_EAL (RPg1-RPg0)).x <= r1/r0 by MESFUNC5:def 7;
end; then
A63: (-r1/r0)*(Prod_Measure(L-Meas n)).E1
<= Integral(Prod_Measure(L-Meas n),(R_EAL(RPg1-RPg0)) |E1)
& Integral(Prod_Measure(L-Meas n),(R_EAL(RPg1-RPg0)) |E1)
<= (r1/r0) * (Prod_Measure(L-Meas n)).E1
by A59,A57,A60,MESFUNC7:26;
A64: (-r1/r0)*r0 = -r1/r0*r0;
(r1/r0)*r0 = r1 by A48,XCMPLX_1:87; then
A65: -r1 <= Integral(Prod_Measure(L-Meas n),(R_EAL(RPg1-RPg0)))
& Integral(Prod_Measure(L-Meas n),(R_EAL(RPg1-RPg0))) <= r1
by A63,A64,A59,A27,XXREAL_3:def 5;
A66: (-1)(#)RPg0 = -RPg0 by VALUED_1:def 6;
A67: (-1) (#) RPg0 is_integrable_on Prod_Measure(L-Meas n)
& Integral(Prod_Measure(L-Meas n),(-1)(#)RPg0)
= (-1)*Integral(Prod_Measure(L-Meas n),RPg0) by A24,MESFUNC6:102; then
A68: (-RPg0) is_integrable_on Prod_Measure(L-Meas n)
& Integral(Prod_Measure(L-Meas n),-RPg0)
= -Integral(Prod_Measure(L-Meas n),RPg0) by A66,XXREAL_3:91;
A69: dom(-RPg0) = E1 by A27,A23,A66,VALUED_1:def 5;
A70: RPg1+(-RPg0) = RPg1 - RPg0 by VALUED_1:def 9;
ex E be Element of Prod_Field(L-Field n) st
E = dom RPg1 /\ dom(-RPg0)
& Integral(Prod_Measure(L-Meas n),RPg1+(-RPg0))
= Integral(Prod_Measure(L-Meas n),RPg1|E)
+ Integral(Prod_Measure(L-Meas n),(-RPg0) |E)
by A53,A66,A67,MESFUNC6:101; then
Integral(Prod_Measure(L-Meas n),RPg1-RPg0)
= G1.yy1 + - G1.yy0 by A27,A52,A69,A70,A55,A56,A68,XXREAL_3:def 2; then
|. G1.yy1 - G1.yy0 .| <= r1 by A65,ABSVALUE:5;
hence |. G1.yy1-G1.yy0 .| < r by XXREAL_0:2,A49;
end;
end; then
G1|J is continuous by A5,A20,FCONT_1:14;
hence G1 is continuous by A5;
end;
theorem Th54:
for n be non zero Nat, D be n-element FinSequence,
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
G1 be PartFunc of REAL,REAL
st (for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL)
& [:CarProduct D,J:] = dom f & f is_continuous_on [:CarProduct D,J:] & f = g
& G1 = Integral1(Prod_Measure(L-Meas n),R_EAL g) |J
holds G1 is continuous
proof
let n be non zero Nat, D be n-element FinSequence,
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
G1 be PartFunc of REAL,REAL;
assume that
A1: for i be Nat st i in Seg n
holds D.i is closed_interval Subset of REAL and
A2: [:CarProduct D,J:] = dom f and
A3: f is_continuous_on [:CarProduct D,J:] and
A4: f = g and
A5: G1 = Integral1(Prod_Measure(L-Meas n),R_EAL g) |J;
set I = CarProduct D;
A6:for e be Real st 0 < e holds ex r be Real st 0 < r
& for y1,y2 be Real st |.y2-y1.| < r & y1 in J & y2 in J
holds for x be Point of CarProduct(Seg n --> RNS_Real) st x in I holds
|. g.([x,y2]) - g.([x,y1]) .| < e
proof
let e be Real;
assume 0 < e; then
consider r be Real such that
A7: 0 < r
& for x1,x2 be Point of CarProduct(Seg n --> RNS_Real), y1,y2 be Real
st [x1,y1] in [:I,J:] & [x2,y2] in [:I,J:] &
||.x2-x1.|| < r & |.y2-y1.| < r
holds |. g.([x2,y2]) - g.([x1,y1]) .| < e by A3,A4,A1,Th37;
take r ;
thus 0 < r by A7;
let y1,y2 be Real;
assume
A8: |.y2-y1.| < r & y1 in J & y2 in J;
let x be Point of CarProduct(Seg n --> RNS_Real);
assume x in I; then
A9: [x,y1] in [:I,J:] & [x,y2] in [:I,J:] by A8,ZFMISC_1:87;
x-x=0.(CarProduct(Seg n --> RNS_Real)) by RLVECT_1:15; then
||.x-x.|| < r by A7;
hence |. g.([x,y2]) - g.([x,y1]) .| < e by A7,A8,A9;
end;
set Rg =R_EAL g;
A10:dom Rg = [:I,J:] by A2,A4,MESFUNC5:def 7;
A11:for e be Real st 0 < e holds ex r be Real st 0 < r
& for y1,y2 be Element of REAL st |.y2-y1.| < r & y1 in J
& y2 in J holds for x be Element of CarProduct(Seg n --> REAL)
st x in I
holds |. (ProjPMap2(Rg,y2)).x-(ProjPMap2(Rg,y1)).x .| < e
proof
let e be Real;
assume 0 < e; then
consider r be Real such that
A12: 0 < r
& for y1,y2 be Real st |.y2-y1.| < r & y1 in J & y2 in J
holds for x be Point of CarProduct(Seg n --> RNS_Real)
st x in I holds
|. g.([x,y2]) - g.([x,y1]) .| < e by A6;
take r;
thus 0 < r by A12;
let y1,y2 be Element of REAL;
assume
A13: |.y2-y1.| < r & y1 in J & y2 in J;
let x be Element of CarProduct(Seg n --> REAL);
assume
A14: x in I;
x is Point of CarProduct(Seg n --> RNS_Real) by MEASUR15:42; then
A15: |. g.([x,y2]) - g.([x,y1]) .| < e by A12,A13,A14;
(ProjPMap2(Rg,y1)).x = Rg.(x,y1) & Rg.(x,y1) = g.([x,y1])
& (ProjPMap2(Rg,y2)).x = Rg.(x,y2) & Rg.(x,y2) = g.([x,y2])
by A13,A14,A10,ZFMISC_1:87,MESFUN12:def 4,MESFUNC5:def 7; then
(ProjPMap2(Rg,y2)).x-(ProjPMap2(Rg,y1)).x
= g.([x,y2]) - g.([x,y1]) by Lm2;
hence thesis by A15,EXTREAL1:12;
end;
set T = Integral1(Prod_Measure(L-Meas n),Rg);
A16:dom T = REAL by FUNCT_2:def 1;
for y0,r be Real st y0 in J & 0 < r
ex s be Real st 0<s & for y1 be Real
st y1 in J & |.y1-y0.| < s holds |.G1.y1-G1.y0.| < r
proof
let yy0,r be Real;
assume
A17: yy0 in J & 0 < r;
reconsider y0=yy0 as Element of REAL by XREAL_0:def 1;
reconsider RPg0 = ProjPMap2(Rg,y0)
as PartFunc of CarProduct(Seg n --> REAL),REAL by MESFUN16:30;
reconsider Pg0 = RPg0
as PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real by MEASUR15:42;
for i be Nat st i in Seg n holds D.i is Subset of REAL by A1; then
A18: CarProduct D is Subset of CarProduct(Seg n --> REAL)
by FINSEQ_1:3,Th11; then
A19: dom Pg0 = I by A17,A2,A4,MESFUN16:28;
A20: RPg0 is_integrable_on Prod_Measure(L-Meas n)
by A1,A19,A2,A3,A4,Th24,Th43;
A21: R_EAL RPg0 = ProjPMap2(R_EAL g,y0) by MESFUNC5:def 7;
RPg0 = ProjPMap2(R_EAL g,y0); then
A22: (Integral1(Prod_Measure(L-Meas n),Rg)).y0
= Integral(Prod_Measure(L-Meas n),ProjPMap2(R_EAL g,y0))
by A1,A17,A2,A3,A4,Th45;
consider r0 be Real, E1 be Element of Prod_Field(L-Field n) such that
A23: E1 = CarProduct D & (Prod_Measure(L-Meas n)).E1 = r0 & 0 <= r0
by A1,Th52;
per cases;
suppose A24: r0 = 0;
consider s be Real such that
A25: 0 < s
& for y1,y2 be Element of REAL st |.y2-y1.| < s & y1 in J & y2 in J
holds for x be Element of CarProduct(Seg n --> REAL)
st x in I holds
|. (ProjPMap2(Rg,y2)).x-(ProjPMap2(Rg,y1)).x .| < r
by A11,A17;
for y1 be Real st y1 in J & |.y1-y0.| < s holds |.G1.y1-G1.yy0 .| < r
proof
let yy1 be Real;
assume
A26: yy1 in J & |.yy1-y0.| < s;
reconsider y1=yy1 as Element of REAL by XREAL_0:def 1;
reconsider RPg1 = ProjPMap2(Rg,y1)
as PartFunc of CarProduct(Seg n --> REAL),REAL by MESFUN16:30;
reconsider Pg1 = RPg1
as PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real by MEASUR15:42;
A27: dom Pg1 = I by A18,A26,A2,A4,MESFUN16:28;
A28: RPg1 is_integrable_on Prod_Measure(L-Meas n)
by A1,A27,A2,A3,A4,Th24,Th43;
A29: R_EAL RPg1 = ProjPMap2(R_EAL g,y1) by MESFUNC5:def 7;
RPg1 = ProjPMap2(R_EAL g,y1); then
(Integral1(Prod_Measure(L-Meas n),Rg)).y1
= Integral(Prod_Measure(L-Meas n),ProjPMap2(R_EAL g,y1))
by A1,A26,A2,A3,A4,Th45; then
A30: G1.yy0 = Integral(Prod_Measure(L-Meas n),RPg0)
& G1.yy1 = Integral(Prod_Measure(L-Meas n),RPg1)
by A21,A29,A5,A17,A22,A26,FUNCT_1:49;
A31: -(G1.yy0) = -Integral(Prod_Measure(L-Meas n),RPg0)
by A30,XXREAL_3:def 3;
A32: dom(RPg1-RPg0) = I /\ I by A19,A27,VALUED_1:12;
A33: RPg1-RPg0 is_integrable_on Prod_Measure(L-Meas n)
by A20,A28,MESFUN6C:34;
A34: dom(R_EAL(RPg1-RPg0)) = E1 by A23,A32,MESFUNC5:def 7;
A35: (Prod_Measure(L-Meas n)).E1 < +infty by A23,XREAL_0:def 1,XXREAL_0:9;
for x be Element of CarProduct(Seg n --> REAL)
st x in E1 holds
-r <= (R_EAL(RPg1-RPg0)).x & (R_EAL(RPg1-RPg0)).x <= r
proof
let x be Element of CarProduct(Seg n --> REAL);
assume
A36: x in E1; then
A37: |. (ProjPMap2(Rg,y1)).x-(ProjPMap2(Rg,y0)).x .| < r by A23,A25,A26,A17;
(ProjPMap2(Rg,y1)).x-(ProjPMap2(Rg,y0)).x = RPg1.x - RPg0.x
by Lm2; then
(ProjPMap2(Rg,y1)).x-(ProjPMap2(Rg,y0)).x = (RPg1-RPg0).x
by A23,A32,A36,VALUED_1:13; then
|. (RPg1-RPg0).x .| <= r by A37,EXTREAL1:12; then
-r <= (RPg1-RPg0).x & (RPg1-RPg0).x <= r by ABSVALUE:5;
hence -r <= (R_EAL(RPg1-RPg0)).x & (R_EAL(RPg1-RPg0)).x <= r
by MESFUNC5:def 7;
end; then
(-r)*(Prod_Measure(L-Meas n)).E1
<= Integral(Prod_Measure(L-Meas n),(R_EAL(RPg1-RPg0)) |E1)
& Integral(Prod_Measure(L-Meas n),(R_EAL(RPg1-RPg0)) |E1)
<= r * (Prod_Measure(L-Meas n)).E1 by A34,A33,A35,MESFUNC7:26; then
A38: 0 <= Integral(Prod_Measure(L-Meas n),(R_EAL(RPg1-RPg0)))
& Integral(Prod_Measure(L-Meas n),(R_EAL(RPg1-RPg0))) <= 0 by A24,A23,A34;
A39: (-1)(#)RPg0 = -RPg0 by VALUED_1:def 6;
A40: (-1) (#) RPg0 is_integrable_on Prod_Measure(L-Meas n)
& Integral(Prod_Measure(L-Meas n),(-1)(#)RPg0)
= (-1)*Integral(Prod_Measure(L-Meas n),RPg0) by A20,MESFUNC6:102; then
A41: (-RPg0) is_integrable_on Prod_Measure(L-Meas n)
& Integral(Prod_Measure(L-Meas n),-RPg0)
= -Integral(Prod_Measure(L-Meas n),RPg0) by A39,XXREAL_3:91;
A42: dom(-RPg0) = E1 by A23,A19,A39,VALUED_1:def 5;
A43: RPg1+(-RPg0) = RPg1 - RPg0 by VALUED_1:def 9;
ex E be Element of Prod_Field(L-Field n) st
E = dom RPg1 /\ dom(-RPg0)
& Integral(Prod_Measure(L-Meas n),RPg1+(-RPg0))
= Integral(Prod_Measure(L-Meas n),RPg1|E)
+ Integral(Prod_Measure(L-Meas n),(-RPg0) |E)
by A28,A40,A39,MESFUNC6:101; then
Integral(Prod_Measure(L-Meas n),RPg1-RPg0)
= G1.yy1 + - G1.yy0 by A23,A27,A42,A43,A30,A31,A41,XXREAL_3:def 2;
hence |. G1.yy1-G1.yy0 .| < r by A17,A38;
end;
hence ex s be Real st 0<s & for y1 be Real
st y1 in J & |.y1-yy0.| < s holds |.G1.y1-G1.yy0.| < r by A25;
end;
suppose
A44: r0 <> 0;
set r1=r/2;
A45: 0 < r1 & r1 < r by A17,XREAL_1:215,XREAL_1:216; then
consider s be Real such that
A46: 0 < s
& for y1,y2 be Element of REAL st |.y2-y1.| < s & y1 in J & y2 in J
holds for x be Element of CarProduct(Seg n --> REAL)
st x in I holds
|. (ProjPMap2(Rg,y2)).x-(ProjPMap2(Rg,y1)).x .| < r1/r0
by A11,A23,A44,XREAL_1:139;
take s;
thus 0 < s by A46;
let yy1 be Real;
assume
A47: yy1 in J & |.yy1-yy0.| < s;
reconsider y1=yy1 as Element of REAL by XREAL_0:def 1;
reconsider RPg1 = ProjPMap2(Rg,y1)
as PartFunc of CarProduct(Seg n --> REAL),REAL by MESFUN16:30;
reconsider Pg1 = RPg1
as PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real by MEASUR15:42;
A48: dom Pg1 = I by A18,A47,A2,A4,MESFUN16:28; then
A49: RPg1 is_integrable_on Prod_Measure(L-Meas n) by A1,A2,A3,A4,Th24,Th43;
A50: R_EAL RPg1 = ProjPMap2(R_EAL g,y1) by MESFUNC5:def 7;
RPg1 = ProjPMap2(R_EAL g,y1); then
(Integral1(Prod_Measure(L-Meas n),Rg)).y1
= Integral(Prod_Measure(L-Meas n),ProjPMap2(R_EAL g,y1))
by A1,A47,A2,A3,A4,Th45; then
A51: G1.yy0 = Integral(Prod_Measure(L-Meas n),RPg0)
& G1.yy1 = Integral(Prod_Measure(L-Meas n),RPg1)
by A21,A50,A5,A17,A22,A47,FUNCT_1:49;
A52: -(G1.yy0) = -Integral(Prod_Measure(L-Meas n),RPg0) by A51,XXREAL_3:def 3;
A53: RPg1-RPg0 is_integrable_on Prod_Measure(L-Meas n) by A20,A49,MESFUN6C:34;
A54: dom(RPg1-RPg0) = I /\ I by A19,A48,VALUED_1:12; then
A55: dom(R_EAL(RPg1-RPg0)) = E1 by A23,MESFUNC5:def 7;
A56: (Prod_Measure(L-Meas n)).E1 < +infty by A23,XREAL_0:def 1,XXREAL_0:9;
for x be Element of CarProduct(Seg n --> REAL) st x in E1 holds
-(r1/r0) <= (R_EAL(RPg1-RPg0)).x & (R_EAL(RPg1-RPg0)).x <= r1/r0
proof
let x be Element of CarProduct(Seg n --> REAL);
assume
A57: x in E1; then
A58: |. (ProjPMap2(Rg,y1)).x-(ProjPMap2(Rg,y0)).x .| < r1/r0
by A23,A46,A47,A17;
(ProjPMap2(Rg,y1)).x-(ProjPMap2(Rg,y0)).x = RPg1.x - RPg0.x
by Lm2; then
(ProjPMap2(Rg,y1)).x-(ProjPMap2(Rg,y0)).x = (RPg1-RPg0).x
by A23,A54,A57,VALUED_1:13; then
|. (RPg1-RPg0).x .| <= r1/r0 by A58,EXTREAL1:12; then
-(r1/r0) <= (RPg1-RPg0).x & (RPg1-RPg0).x <= r1/r0 by ABSVALUE:5;
hence -(r1/r0) <= (R_EAL(RPg1-RPg0)).x
& (R_EAL(RPg1-RPg0)).x <= (r1/r0) by MESFUNC5:def 7;
end; then
A59: (-r1/r0)*(Prod_Measure(L-Meas n)).E1
<= Integral(Prod_Measure(L-Meas n),(R_EAL(RPg1-RPg0)) |E1)
& Integral(Prod_Measure(L-Meas n),(R_EAL(RPg1-RPg0)) |E1)
<= (r1/r0) * (Prod_Measure(L-Meas n)).E1 by A55,A53,A56,MESFUNC7:26;
A60: (-r1/r0)*r0 = -r1/r0*r0 .= -r1 by A44,XCMPLX_1:87;
(r1/r0)*r0 = r1 by A44,XCMPLX_1:87; then
A61: -r1 <= Integral(Prod_Measure(L-Meas n),(R_EAL(RPg1-RPg0)))
& Integral(Prod_Measure(L-Meas n),(R_EAL(RPg1-RPg0))) <= r1
by A59,A60,A55,A23,XXREAL_3:def 5;
A62: (-1)(#)RPg0 = -RPg0 by VALUED_1:def 6;
A63: (-1) (#) RPg0 is_integrable_on Prod_Measure(L-Meas n)
& Integral(Prod_Measure(L-Meas n),(-1)(#)RPg0)
= (-1)*Integral(Prod_Measure(L-Meas n),RPg0) by A20,MESFUNC6:102; then
A64: (-RPg0) is_integrable_on Prod_Measure(L-Meas n)
& Integral(Prod_Measure(L-Meas n),-RPg0)
= -Integral(Prod_Measure(L-Meas n),RPg0) by A62,XXREAL_3:91;
A65: dom(-RPg0) = E1 by A23,A19,A62,VALUED_1:def 5;
A66: RPg1+(-RPg0) = RPg1 - RPg0 by VALUED_1:def 9;
ex E be Element of Prod_Field(L-Field n) st
E = dom RPg1 /\ dom(-RPg0)
& Integral(Prod_Measure(L-Meas n),RPg1+(-RPg0))
= Integral(Prod_Measure(L-Meas n),RPg1|E)
+ Integral(Prod_Measure(L-Meas n),(-RPg0) |E)
by A49,A63,A62,MESFUNC6:101; then
Integral(Prod_Measure(L-Meas n),RPg1-RPg0)
= G1.yy1 + - G1.yy0 by A23,A48,A65,A66,A51,A52,A64,XXREAL_3:def 2; then
|. G1.yy1 - G1.yy0 .| <= r1 by A61,ABSVALUE:5;
hence |. G1.yy1-G1.yy0 .| < r by XXREAL_0:2,A45;
end;
end; then
G1|J is continuous by A5,A16,FCONT_1:14;
hence G1 is continuous by A5;
end;
Lm3:
for n be non zero Nat, D be n-element FinSequence,
I be Subset of CarProduct(Seg n --> RNS_Real),
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL
st (for i be Nat st i in Seg n
holds D.i is closed_interval Subset of REAL)
& I = CarProduct D
& [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g
holds
g is_integrable_on Prod_Measure(Prod_Measure(L-Meas n),L-Meas)
& (for x being Element of CarProduct(Seg n --> REAL)
holds Integral2(L-Meas,|.R_EAL g.|).x < +infty)
& (for U being Element of Prod_Field(L-Field n)
holds Integral2(L-Meas,R_EAL g) is U-measurable)
& Integral2(L-Meas,R_EAL g) is_integrable_on Prod_Measure(L-Meas n)
& Integral(Prod_Measure(Prod_Measure(L-Meas n),L-Meas),g)
= Integral(Prod_Measure(L-Meas n),Integral2(L-Meas,R_EAL g))
proof
let n be non zero Nat, D be n-element FinSequence,
I be Subset of CarProduct(Seg n --> RNS_Real),
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL;
assume that
A1: for i be Nat st i in Seg n
holds D.i is closed_interval Subset of REAL and
A2: I = CarProduct D and
A3: [:I,J:] = dom f and
A4: f is_continuous_on [:I,J:] and
A5: f = g;
A6: ex I1 be Subset of CarProduct(Seg n --> RNS_Real) st
I1 = CarProduct D & I1 is compact
proof
per cases;
suppose D is non-empty; then
reconsider D1 = D as non-empty n-element FinSequence;
for i be Nat st i in Seg n holds
D1.i is closed_interval Subset of REAL by A1;
hence thesis by MEASUR15:51;
end;
suppose
A7: not D is non-empty; then
A8: CarProduct D = {} by Th6;
CarProduct D c= the carrier of CarProduct(Seg n --> RNS_Real)
by A7,Th6; then
reconsider I1 = CarProduct D
as Subset of CarProduct(Seg n --> RNS_Real);
I1 is compact by A8;
hence thesis;
end;
end;
reconsider J1 = J as Subset of RNS_Real;
A9: J1 is compact by MESFUN16:7;
reconsider E = [:CarProduct D,J1:] as
Subset of [:CarProduct(Seg n --> RNS_Real),RNS_Real:] by A6,A9,MESFUN16:8;
A10: for i be Nat st i in Seg n holds D.i is Interval by A1; then
reconsider E as Element of
sigma measurable_rectangles(Prod_Field(L-Field n),L-Field)
by A2,Th49;
for i be Nat st i in Seg n holds D.i is Subset of REAL by A1; then
A11:I is Subset of CarProduct(Seg n --> REAL)
by A2,FINSEQ_1:3,Th11; then
A12:g is E-measurable by A2,A3,A4,A5,Th33;
set Rg =R_EAL g;
A13:dom g = dom Rg by MESFUNC5:def 7; then
A14:dom |.Rg.| = [:I,J:] by A3,A5,MESFUNC1:def 10;
A15:for x be Element of CarProduct(Seg n --> REAL)
st x in CarProduct(Seg n --> REAL) \ I holds
(Integral2(L-Meas,|.Rg.|)).x = 0
proof
let x be Element of CarProduct(Seg n --> REAL);
assume x in CarProduct(Seg n --> REAL) \ I; then
not x in I by XBOOLE_0:def 5; then
dom ProjPMap1(|.Rg.|,x) = {} by A3,A5,A11,MESFUN16:27; then
Integral(L-Meas,ProjPMap1(|.Rg.|,x)) = 0 by MESFUN16:1;
hence (Integral2(L-Meas,|.Rg.|)).x = 0 by MESFUN12:def 8;
end;
A16:for x be Element of CarProduct(Seg n --> REAL),
y be Element of REAL st x in I & y in J holds
(ProjPMap1(|.Rg.|,x)).y =(|.Rg.|).(x,y)
& (|.Rg.|).(x,y) = |. g.([x,y]) .| & (|.Rg.|).(x,y) = (|.g.|).([x,y])
proof
let x be Element of CarProduct(Seg n --> REAL),y be Element of REAL;
assume
A17: x in I & y in J;
hence (ProjPMap1(|.Rg.|,x)).y =(|.Rg.|).(x,y)
by A14,ZFMISC_1:87,MESFUN12:def 3;
[x,y] in dom g by A17,A3,A5,ZFMISC_1:87; then
A18: [x,y] in dom |.g.| by VALUED_1:def 11;
A19: Rg.([x,y]) = g.([x,y]) by MESFUNC5:def 7;
(|.Rg.|).(x,y) = |. Rg.([x,y]) .|
by A17,A14,ZFMISC_1:87,MESFUNC1:def 10;
hence (|.Rg.|).(x,y) = |. g.([x,y]) .| by A19,EXTREAL1:12;
hence (|.Rg.|).(x,y) = (|.g.|).([x,y]) by VALUED_1:def 11,A18;
end;
A20:for x be Element of CarProduct(Seg n --> REAL)
st x in I holds 0 <= Integral2(L-Meas,|.Rg.|).x
proof
let x be Element of CarProduct(Seg n --> REAL);
assume
A21: x in I;
reconsider CD = J as Element of L-Field by MEASUR10:5,MEASUR12:75;
reconsider Pg = ProjPMap1(|.Rg.|,x)
as PartFunc of REAL,REAL by MESFUN16:30;
A22: dom Pg = J by A21,A3,A11,A5,MESFUN16:27;
Pg is_integrable_on L-Meas by A3,A4,A5,A11,Th31; then
consider E be Element of L-Field such that
A23: E = dom(R_EAL Pg) & R_EAL Pg is E-measurable by MESFUNC5:def 17;
E = dom Pg & R_EAL Pg is E-measurable by A23,MESFUNC5:def 7; then
A24: Pg is CD-measurable by A22;
R_EAL Pg = ProjPMap1(|.R_EAL g.|,x) by MESFUNC5:def 7; then
A25: (Integral2(L-Meas,|.Rg.|)).x = Integral(L-Meas,Pg) by MESFUN12:def 8;
for y being object st y in dom(Pg|J) holds 0 <= (Pg|J).y
proof
let y be object;
assume
A26: y in dom(Pg|J); then
y in dom Pg /\ J by RELAT_1:61; then
reconsider y as Element of REAL;
(ProjPMap1(|.Rg.|,x)).y = (|.Rg.|).(x,y)
& (|.Rg.|).(x,y) = |. g.([x,y]) .| by A21,A26,A16;
hence thesis by A22;
end;
hence thesis by A22,A24,A25,MESFUNC6:52,84;
end;
set F = Integral2(L-Meas,|.Rg.|);
F is PartFunc of CarProduct(Seg n --> REAL),REAL
by A3,A4,A5,A11,Th34; then
reconsider G = F|I as PartFunc of CarProduct(Seg n --> REAL),REAL
by PARTFUN1:11;
reconsider G2 = G as PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real
by MEASUR15:42;
reconsider H = CarProduct(Seg n --> REAL)
as Element of Prod_Field(L-Field n) by PROB_1:5;
A27:I is Element of Prod_Field(L-Field n) by A2,A10,Th9;
reconsider NI = H \ I as Subset of CarProduct(Seg n --> RNS_Real)
by MEASUR15:42;
A28:NI is Element of Prod_Field(L-Field n) by A27,PROB_1:6;
set F0 = F|I;
set F1 = F|NI;
A29:dom F = CarProduct(Seg n --> REAL) by FUNCT_2:def 1; then
A30:dom(F|I) = I & dom(F|NI) = NI by A11;
G2 is_continuous_on I by A1,A2,A3,A4,A5,Th40; then
G is_integrable_on Prod_Measure(L-Meas n) by A1,A2,A11,A29,Th43; then
A31:F0 is_integrable_on Prod_Measure(L-Meas n) by MESFUNC5:def 7; then
A32:Integral(Prod_Measure(L-Meas n),F0) < +infty by MESFUNC5:96;
A33:I \/ NI = CarProduct(Seg n --> REAL) by A11,XBOOLE_1:45; then
A34:F| (I \/ NI) = F;
A35:I /\ NI = {} by XBOOLE_1:85,XBOOLE_0:def 7;
A36:for r being Element of CarProduct(Seg n --> REAL) holds 0 <= F.r
proof
let r being Element of CarProduct(Seg n --> REAL);
r in I or r in NI by A33,XBOOLE_0:def 3;
hence 0 <= F.r by A20,A15;
end; then
A37:F is nonnegative;
for r being Real holds H /\ (less_dom(F,r)) in Prod_Field(L-Field n)
proof
let r be Real;
consider H0 being Element of Prod_Field(L-Field n) such that
A38: H0 = dom F0 & F0 is H0 -measurable by A31,MESFUNC5:def 17;
per cases;
suppose
A39: r <= 0;
less_dom (F,r) = {}
proof
assume less_dom (F,r) <> {}; then
consider x be object such that
A40: x in less_dom(F,r) by XBOOLE_0:def 1;
x in dom F & F.x < r by MESFUNC1:def 11,A40;
hence contradiction by A36,A39;
end;
hence H /\ (less_dom (F,r)) in Prod_Field(L-Field n) by PROB_1:4;
end;
suppose
A41: 0 < r;
for z be object holds z in less_dom(F,r) iff z in less_dom(F0,r) \/ NI
proof
let z be object;
hereby assume
A42: z in less_dom(F,r); then
A43: z in dom F & F.z < r by MESFUNC1:def 11;
reconsider x=z as Element of CarProduct(Seg n --> REAL) by A42;
per cases by A42,A33,XBOOLE_0:def 3;
suppose
A44: z in I; then
F0.z < r by FUNCT_1:49,A43; then
z in less_dom (F0,r) by A44,A30,MESFUNC1:def 11;
hence z in less_dom (F0,r) \/ NI by XBOOLE_0:def 3;
end;
suppose z in NI;
hence z in less_dom (F0,r) \/ NI by XBOOLE_0:def 3;
end;
end;
assume z in less_dom (F0,r) \/ NI; then
per cases by XBOOLE_0:def 3;
suppose
A45: z in less_dom (F0,r); then
z in dom F0 & F0.z < r by MESFUNC1:def 11; then
A46: F.z < r by FUNCT_1:49;
dom F = CarProduct(Seg n --> REAL) by FUNCT_2:def 1;
hence z in less_dom (F,r) by A45,A46,MESFUNC1:def 11;
end;
suppose
A47: z in NI; then
reconsider x=z as Element of CarProduct(Seg n --> REAL);
A48: F.x < r by A41,A47,A15;
dom F = CarProduct(Seg n --> REAL) by FUNCT_2:def 1;
hence z in less_dom (F,r) by A48,MESFUNC1:def 11;
end;
end; then
less_dom(F,r) = less_dom (F0,r) \/ NI by TARSKI:2; then
A49: H /\ less_dom(F,r) = I /\ (less_dom (F0,r) \/ NI)
\/ NI /\ (less_dom (F0,r) \/ NI) by A33,XBOOLE_1:23;
I /\ (less_dom (F0,r) \/ NI)
= I /\ less_dom (F0,r) \/ {} by A35,XBOOLE_1:23; then
A50: I /\ (less_dom (F0,r) \/ NI) in Prod_Field(L-Field n) by A27,A29,A38;
A51: less_dom(F0,r) c= I by A30,MESFUNC1:def 11;
NI /\ (less_dom (F0,r) \/ NI)
= (NI /\ less_dom(F0,r)) \/ (NI /\ NI) by XBOOLE_1:23; then
NI /\ (less_dom (F0,r) \/ NI)
= {} \/ (NI /\ NI) by A51;
hence H /\ less_dom (F,r) in Prod_Field(L-Field n)
by A28,A49,A50,PROB_1:3;
end;
end; then
F is H -measurable; then
A52:Integral(Prod_Measure(L-Meas n),F)
= Integral(Prod_Measure(L-Meas n),F0)
+ Integral(Prod_Measure(L-Meas n),F1)
by A29,A27,A28,A34,A37,MESFUNC5:91,XBOOLE_1:79;
A53: Prod_Measure(L-Meas n) is sigma_finite by MEASUR15:36;
for x being object st x in dom F1 holds F1.x = 0
proof
let x be object;
assume A54: x in dom F1; then
reconsider r=x as Element of CarProduct(Seg n --> REAL) by A29;
(Integral2(L-Meas,|.Rg.|)).r = 0 by A54,A15;
hence thesis by A54,FUNCT_1:49;
end; then
Integral(Prod_Measure(L-Meas n),F1)
= 0 * (Prod_Measure(L-Meas n)).(dom F1)
by A27,A29,PROB_1:6,MEASUR10:27; then
Integral(Prod_Measure(L-Meas n),F0) = Integral(Prod_Measure(L-Meas n),F)
by A52,XXREAL_3:4; then
A55:R_EAL g is_integrable_on Prod_Measure(Prod_Measure(L-Meas n),L-Meas)
by A12,A2,A3,A5,A13,A32,MESFUN16:5,A53,MESFUN13:11;
for x being Element of CarProduct(Seg n --> REAL)
holds Integral2(L-Meas,|.Rg.|).x < +infty
proof
let x be Element of CarProduct(Seg n --> REAL);
per cases by A33,XBOOLE_0:def 3;
suppose
A56: x in I; then
Integral2(L-Meas,|.Rg.|).x = G.x by FUNCT_1:49; then
Integral2(L-Meas,|.Rg.|).x in rng G by A30,A56,FUNCT_1:3;
hence Integral2(L-Meas,|.Rg.|).x < +infty by XXREAL_0:9;
end;
suppose x in NI;
hence Integral2(L-Meas,|.Rg.|).x < +infty by A15;
end;
end;
hence thesis by A53,A55,MESFUN16:5,MESFUN13:32;
end;
Lm4:
for n be non zero Nat, D be n-element FinSequence,
I be Subset of CarProduct(Seg n --> RNS_Real),
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL
st (for i be Nat st i in Seg n
holds D.i is closed_interval Subset of REAL)
& I = CarProduct D
& [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g
holds
g is_integrable_on Prod_Measure(Prod_Measure(L-Meas n),L-Meas)
& (for y being Element of REAL
holds Integral1(Prod_Measure(L-Meas n),|.R_EAL g.|).y < +infty)
& (for V being Element of L-Field
holds Integral1(Prod_Measure(L-Meas n),R_EAL g) is V-measurable)
& Integral1(Prod_Measure(L-Meas n),R_EAL g) is_integrable_on L-Meas
& Integral(Prod_Measure(Prod_Measure(L-Meas n),L-Meas),g)
= Integral(L-Meas,Integral1(Prod_Measure(L-Meas n),R_EAL g))
proof
let n be non zero Nat, D be n-element FinSequence,
I be Subset of CarProduct(Seg n --> RNS_Real),
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL;
assume that
A1: for i be Nat st i in Seg n
holds D.i is closed_interval Subset of REAL and
A2: I = CarProduct D and
A3: [:I,J:] = dom f and
A4: f is_continuous_on [:I,J:] and
A5: f = g;
A6: ex I1 be Subset of CarProduct(Seg n --> RNS_Real) st
I1 = CarProduct D & I1 is compact
proof
per cases;
suppose D is non-empty; then
reconsider D1 = D as non-empty n-element FinSequence;
for i be Nat st i in Seg n holds
D1.i is closed_interval Subset of REAL by A1;
hence thesis by MEASUR15:51;
end;
suppose
A7: not D is non-empty; then
A8: CarProduct D = {} by Th6;
CarProduct D c= the carrier of CarProduct(Seg n --> RNS_Real)
by A7,Th6; then
reconsider I1 = CarProduct D
as Subset of CarProduct(Seg n --> RNS_Real);
I1 is compact by A8;
hence thesis;
end;
end;
reconsider J1 = J as Subset of RNS_Real;
J1 is compact by MESFUN16:7; then
reconsider E = [:CarProduct D,J1:] as
Subset of [:CarProduct(Seg n --> RNS_Real),RNS_Real:] by A6,MESFUN16:8;
for i be Nat st i in Seg n holds D.i is Interval by A1; then
reconsider E as Element of
sigma measurable_rectangles(Prod_Field(L-Field n),L-Field)
by A2,Th49;
for i be Nat st i in Seg n holds D.i is Subset of REAL by A1; then
A9: I is Subset of CarProduct(Seg n --> REAL)
by A2,FINSEQ_1:3,Th11; then
A10: g is E-measurable by A2,A3,A4,A5,Th33;
set Rg =R_EAL g;
dom g = dom Rg by MESFUNC5:def 7; then
A11: dom |.Rg.| = [:I,J:] by A3,A5,MESFUNC1:def 10;
A12: for y be Element of REAL st y in REAL\J holds
(Integral1(Prod_Measure(L-Meas n),|.Rg.|)).y = 0
proof
let y be Element of REAL;
assume y in REAL \ J; then
not y in J by XBOOLE_0:def 5; then
A13: dom ProjPMap2(|.Rg.|,y) = {} by A3,A5,A9,MESFUN16:28;
(Integral1(Prod_Measure(L-Meas n),|.Rg.|)).y
= Integral(Prod_Measure(L-Meas n),(ProjPMap2(|.Rg.|,y)))
by MESFUN12:def 7;
hence (Integral1(Prod_Measure(L-Meas n),|.Rg.|)).y = 0 by A13,MESFUN16:1;
end;
A14:for x be Element of CarProduct(Seg n --> REAL),
y be Element of REAL st x in I & y in J holds
(ProjPMap2(|.Rg.|,y)).x =(|.Rg.|).(x,y)
& (|.Rg.|).(x,y) = |. g.([x,y]) .| & (|.Rg.|).(x,y) = (|.g.|).([x,y])
proof
let x be Element of CarProduct(Seg n --> REAL), y be Element of REAL;
assume that
A15: x in I and
A16: y in J;
thus (ProjPMap2(|.Rg.|,y)).x =(|.Rg.|).(x,y)
by A11,A15,A16,ZFMISC_1:87,MESFUN12:def 4;
[x,y] in dom g by A15,A3,A5,A16,ZFMISC_1:87; then
A17: [x,y] in dom |.g.| by VALUED_1:def 11;
A18: Rg.([x,y]) = g.([x,y]) by MESFUNC5:def 7;
(|.Rg.|).(x,y) = |. Rg.([x,y]) .|
by A15,A11,A16,ZFMISC_1:87,MESFUNC1:def 10;
hence (|.Rg.|).(x,y) = |.g.([x,y]).| by A18,EXTREAL1:12;
hence (|.Rg.|).(x,y) = (|.g.|).([x,y]) by VALUED_1:def 11,A17;
end;
A19:for y be Element of REAL
st y in J holds 0 <= Integral1(Prod_Measure(L-Meas n),|.Rg.|).y
proof
let y be Element of REAL;
assume
A20: y in J;
for i be Nat st i in Seg n holds D.i is Interval by A1; then
reconsider AB = I as Element of Prod_Field(L-Field n)
by A2,Th9;
reconsider Pg = ProjPMap2(|.Rg.|,y)
as PartFunc of CarProduct(Seg n --> REAL),REAL by MESFUN16:30;
A21: ProjPMap2(|.Rg.|,y) = R_EAL Pg by MESFUNC5:def 7;
A22: dom Pg = I by A20,A3,A9,A5,MESFUN16:28;
A23: Pg is AB-measurable by A21,A1,A20,A3,A2,A4,A5,Th47;
A24: Integral(Prod_Measure(L-Meas n),Pg)
= (Integral1(Prod_Measure(L-Meas n),|.Rg.|)).y
by A1,A20,A2,A3,A4,A5,A21,Th48;
for x being object st x in dom(Pg|I) holds 0 <= (Pg|I).x
proof
let x be object;
assume
A25: x in dom(Pg|I); then
reconsider x as Element of CarProduct(Seg n --> REAL) by A22;
(ProjPMap2(|.Rg.|,y)).x = (|.Rg.|).(x,y)
& (|.Rg.|).(x,y) = |. g.([x,y]) .| by A20,A25,A14;
hence thesis by A22;
end;
hence thesis by A22,A23,A24,MESFUNC6:52,84;
end;
set T = Integral1(Prod_Measure(L-Meas n),|.Rg.|);
reconsider S = T|J as PartFunc of REAL,REAL
by A1,A2,A3,A4,A5,Th50;
A26:J is Element of L-Field by MEASUR10:5,MEASUR12:75;
reconsider H = REAL as Element of L-Field by PROB_1:5;
set NJ = H \ J;
reconsider T0 = T|J as PartFunc of REAL,ExtREAL by PARTFUN1:11;
reconsider T1 = T|NJ as PartFunc of REAL,ExtREAL by PARTFUN1:11;
A27:dom T = REAL by FUNCT_2:def 1;
A28:dom(T|J) = J & dom(T|NJ) = NJ by FUNCT_2:def 1;
S is_integrable_on L-Meas
proof
per cases;
suppose J is non empty; then
reconsider J1 = J as non empty closed_interval Subset of REAL;
S||J1 is bounded & S is_integrable_on J1
by A28,A1,A2,A3,A4,A5,Th53,INTEGRA5:10,11;
hence S is_integrable_on L-Meas by A26,A28,MESFUN14:49;
end;
suppose
A29: J is empty;
reconsider E = {} as Element of L-Field by MEASURE1:7;
A30: E = dom(R_EAL S) by A28,A29,MESFUNC5:def 7;
for x be Element of REAL st x in dom(R_EAL S) holds (R_EAL S).x = 0
by A28,A29,MESFUNC5:def 7;
hence S is_integrable_on L-Meas by A30,LPSPACE1:22;
end;
end; then
A31:T0 is_integrable_on L-Meas by MESFUNC5:def 7; then
A32:Integral(L-Meas,T0) < +infty by MESFUNC5:96;
A33: NJ is Element of L-Field by A26,PROB_1:6;
A34:J \/ NJ = REAL by XBOOLE_1:45; then
A35:T| (J \/ NJ) = T;
A36:J /\ NJ = {} by XBOOLE_1:85,XBOOLE_0:def 7;
A37:for r being Element of REAL holds 0 <= T.r
proof
let r be Element of REAL;
r in J or r in NJ by A34,XBOOLE_0:def 3;
hence 0 <= T.r by A19,A12;
end; then
A38:T is nonnegative;
for r being Real holds H /\ (less_dom(T,r)) in L-Field
proof
let r be Real;
consider H0 being Element of L-Field such that
A39: H0 = dom T0 & T0 is H0 -measurable by A31,MESFUNC5:def 17;
per cases;
suppose
A40: r <= 0;
less_dom (T,r) = {}
proof
assume less_dom (T,r) <> {}; then
consider y be object such that
A41: y in less_dom(T,r) by XBOOLE_0:def 1;
y in dom T & T.y < r by MESFUNC1:def 11,A41;
hence contradiction by A37,A40;
end;
hence H /\ (less_dom (T,r)) in L-Field by PROB_1:4;
end;
suppose
A42: 0 < r;
for z be object holds z in less_dom (T,r) iff z in less_dom (T0,r) \/ NJ
proof
let z be object;
hereby assume
A43: z in less_dom (T,r); then
A44: z in dom T & T.z < r by MESFUNC1:def 11;
reconsider y=z as Element of REAL by A43;
per cases by A43,A34,XBOOLE_0:def 3;
suppose
A45: z in J; then
T0.z < r by FUNCT_1:49,A44; then
z in less_dom (T0,r) by A45,A28,MESFUNC1:def 11;
hence z in less_dom (T0,r) \/ NJ by XBOOLE_0:def 3;
end;
suppose z in NJ;
hence z in less_dom (T0,r) \/ NJ by XBOOLE_0:def 3;
end;
end;
assume z in less_dom (T0,r) \/ NJ; then
per cases by XBOOLE_0:def 3;
suppose
A46: z in less_dom (T0,r); then
z in dom T0 & T0.z < r by MESFUNC1:def 11; then
A47: T.z < r by A28,FUNCT_1:49;
dom T = REAL by FUNCT_2:def 1;
hence z in less_dom (T,r) by A46,A47,MESFUNC1:def 11;
end;
suppose
A48: z in NJ; then
reconsider y=z as Element of REAL;
A49: T.y < r by A42,A48,A12;
dom T = REAL by FUNCT_2:def 1;
hence z in less_dom (T,r) by A49,MESFUNC1:def 11;
end;
end; then
less_dom(T,r) = less_dom (T0,r) \/ NJ by TARSKI:2; then
A50: H /\ less_dom(T,r) = J /\ (less_dom (T0,r) \/ NJ)
\/ NJ /\ (less_dom (T0,r) \/ NJ) by A34,XBOOLE_1:23;
J /\ (less_dom (T0,r) \/ NJ)
= J /\ less_dom (T0,r) \/ {} by A36,XBOOLE_1:23; then
A51: J /\ (less_dom (T0,r) \/ NJ) in L-Field by A27,A39;
A52: less_dom(T0,r) c= J by A28,MESFUNC1:def 11;
NJ /\ (less_dom (T0,r) \/ NJ)
= (NJ /\ less_dom(T0,r)) \/ (NJ /\ NJ) by XBOOLE_1:23; then
NJ /\ (less_dom (T0,r) \/ NJ)
= {} \/ (NJ /\ NJ) by A52;
hence H /\ less_dom (T,r) in L-Field by A33,A50,A51,PROB_1:3;
end;
end; then
T is H-measurable; then
A53:Integral(L-Meas,T) = Integral(L-Meas,T0) + Integral(L-Meas,T1)
by A27,A26,A33,A35,A38,MESFUNC5:91,XBOOLE_1:79;
A54: Prod_Measure(L-Meas n) is sigma_finite by MEASUR15:36;
A55: E = dom (R_EAL g) by A2,A3,A5,MESFUNC5:def 7;
for y being object st y in dom T1 holds T1.y = 0
proof
let y be object;
assume A56: y in dom T1; then
reconsider r=y as Element of REAL;
A57: y in dom T & y in NJ by A56,RELAT_1:57;
(Integral1(Prod_Measure(L-Meas n),|.Rg.|)).r = 0 by A56,A12,RELAT_1:57;
hence thesis by A57,FUNCT_1:49;
end; then
Integral(L-Meas,T1) = 0 * (L-Meas.(dom T1))
by A27,A26,PROB_1:6,MEASUR10:27; then
Integral(L-Meas,T0) = Integral(L-Meas,T) by A53,XXREAL_3:4; then
A58:R_EAL g is_integrable_on Prod_Measure(Prod_Measure(L-Meas n),L-Meas)
by A32,A54,A55,MESFUN13:10,A10,MESFUN16:5;
for y being Element of REAL
holds Integral1(Prod_Measure(L-Meas n),|.Rg.|).y < +infty
proof
let y be Element of REAL;
per cases by A34,XBOOLE_0:def 3;
suppose
A59: y in J; then
Integral1(Prod_Measure(L-Meas n),|.Rg.|).y = S.y by FUNCT_1:49; then
Integral1(Prod_Measure(L-Meas n),|.Rg.|).y in rng S by A28,A59,FUNCT_1:3;
hence Integral1(Prod_Measure(L-Meas n),|.Rg.|).y < +infty by XXREAL_0:9;
end;
suppose y in NJ;
hence Integral1(Prod_Measure(L-Meas n),|.Rg.|).y < +infty by A12;
end;
end;
hence thesis by A54,A58,MESFUN16:5,MESFUN13:33;
end;
theorem
for n be non zero Nat, D be n-element FinSequence,
I be Subset of CarProduct(Seg n --> RNS_Real),
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL
st (for i be Nat st i in Seg n
holds D.i is closed_interval Subset of REAL)
& I = CarProduct D
& [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g
holds
g is_integrable_on Prod_Measure(Prod_Measure(L-Meas n),L-Meas)
& (for x being Element of CarProduct(Seg n --> REAL)
holds Integral2(L-Meas,|.R_EAL g.|).x < +infty)
& (for y being Element of REAL
holds Integral1(Prod_Measure(L-Meas n),|.R_EAL g.|).y < +infty)
& (for U being Element of Prod_Field(L-Field n)
holds Integral2(L-Meas,R_EAL g) is U-measurable)
& (for V being Element of L-Field
holds Integral1(Prod_Measure(L-Meas n),R_EAL g) is V-measurable)
& Integral2(L-Meas,R_EAL g) is_integrable_on Prod_Measure(L-Meas n)
& Integral1(Prod_Measure(L-Meas n),R_EAL g) is_integrable_on L-Meas
& Integral(Prod_Measure(Prod_Measure(L-Meas n),L-Meas),g)
= Integral(Prod_Measure(L-Meas n),Integral2(L-Meas,R_EAL g))
& Integral(Prod_Measure(Prod_Measure(L-Meas n),L-Meas),g)
= Integral(L-Meas,Integral1(Prod_Measure(L-Meas n),R_EAL g))
by Lm3,Lm4;
theorem Th56:
for n be non zero Nat, D be (n+1)-element FinSequence,
f be PartFunc of CarProduct(Seg(n+1) --> RNS_Real),RNS_Real,
g be PartFunc of CarProduct(Seg(n+1) --> REAL),REAL,
g0 be PartFunc of [:CarProduct(Seg n-->REAL),REAL:],REAL
st f = g & g0 = g
& (for i be Nat st i in Seg(n+1) holds D.i is closed_interval Subset of REAL)
& f is_continuous_on CarProduct D & dom f = CarProduct D holds
Integral2(L-Meas,R_EAL g0) is_integrable_on Prod_Measure(L-Meas n)
& Integral(Prod_Measure(L-Meas (n+1)),g)
= Integral(Prod_Measure(Prod_Measure(L-Meas n),L-Meas),g0)
proof
let n be non zero Nat, D be (n+1)-element FinSequence,
f be PartFunc of CarProduct(Seg(n+1) --> RNS_Real),RNS_Real,
g be PartFunc of CarProduct(Seg(n+1) --> REAL),REAL,
g0 be PartFunc of [:CarProduct(Seg n-->REAL),REAL:],REAL;
assume that
A1: f = g and
A2:g0 = g and
A3: for i be Nat st i in Seg (n+1)
holds D.i is closed_interval Subset of REAL and
A4: f is_continuous_on CarProduct D and
A5: dom f = CarProduct D;
reconsider f0 = g0
as PartFunc of [:CarProduct(Seg n--> RNS_Real),RNS_Real:],RNS_Real
by MEASUR15:42;
reconsider Dn = D|n as n-element FinSequence;
A6:n < n+1 by NAT_1:13;
A7: Seg n c= Seg (n+1) by FINSEQ_3:18;
A8: for i be Nat st i in Seg n holds
Dn.i is closed_interval Subset of REAL
proof
let i be Nat;
assume
A9: i in Seg n; then
Dn.i = D.i by FUNCT_1:49;
hence Dn.i is closed_interval Subset of REAL by A3,A9,A7;
end;
for i be Nat st i in Seg n holds Dn.i is Subset of REAL by A8; then
CarProduct Dn is Subset of CarProduct(Seg n --> REAL)
by FINSEQ_1:3,Th11; then
reconsider D0 = CarProduct Dn as Subset of CarProduct(Seg n --> RNS_Real)
by MEASUR15:42;
reconsider D1 = D.(n+1) as closed_interval Subset of REAL
by A3,A6,FINSEQ_3:11;
A10: [:CarProduct(Seg n --> RNS_Real),RNS_Real:]
= CarProduct(Seg(n+1) --> RNS_Real) by MEASUR15:38;
CarProduct D = [:D0,D1:] by Th4;
hence Integral2(L-Meas,R_EAL g0) is_integrable_on Prod_Measure(L-Meas n)
by A8,A1,A2,A5,A4,A10,Lm3;
A11: [:CarProduct(Seg n --> REAL),REAL:] = CarProduct(Seg(n+1) --> REAL)
by MEASUR15:38;
Prod_Field(L-Field (n+1))
= sigma measurable_rectangles(Prod_Field(L-Field n),L-Field)
by MEASUR14:44;
hence thesis by A2,A11,MEASUR14:48;
end;
theorem
for n be non zero Nat, D be n-element FinSequence,
I be Subset of CarProduct(Seg n --> RNS_Real),
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
G2 be PartFunc of CarProduct(Seg n --> REAL),REAL
st (for i be Nat st i in Seg n
holds D.i is closed_interval Subset of REAL)
& I = CarProduct D
& [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g
& G2 = Integral2(L-Meas,R_EAL g) | (CarProduct D) holds
Integral(Prod_Measure(Prod_Measure(L-Meas n),L-Meas),R_EAL g)
= Integral(Prod_Measure(L-Meas n),G2)
proof
let n be non zero Nat, D be n-element FinSequence,
I be Subset of CarProduct(Seg n --> RNS_Real),
J be closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
G2 be PartFunc of CarProduct(Seg n --> REAL),REAL;
assume that
A1: for i be Nat st i in Seg n
holds D.i is closed_interval Subset of REAL and
A2: I = CarProduct D and
A3: [:I,J:] = dom f and
A4: f is_continuous_on [:I,J:] and
A5: f = g and
A6: G2 = Integral2(L-Meas,R_EAL g) | (CarProduct D);
set Rg =R_EAL g;
set RG2 = Integral2(L-Meas,Rg);
for i be Nat st i in Seg n holds D.i is Subset of REAL by A1; then
reconsider I0 = CarProduct D
as Subset of CarProduct(Seg n --> REAL) by FINSEQ_1:3,Th11;
set NI = CarProduct(Seg n --> REAL) \ I0;
reconsider F0 = RG2|I0, F1 = RG2|NI
as PartFunc of CarProduct(Seg n --> REAL),ExtREAL by PARTFUN1:11;
reconsider GG2 = G2
as PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real by MEASUR15:42;
A7: dom RG2 = CarProduct(Seg n --> REAL) by FUNCT_2:def 1;
for i be Nat st i in Seg n holds D.i is Interval by A1; then
A8: I0 is Element of Prod_Field(L-Field n) by Th9;
CarProduct(Seg n --> REAL) in Prod_Field(L-Field n) by PROB_1:5; then
A9: NI is Element of Prod_Field(L-Field n) by A8,PROB_1:6;
A10:Integral(Prod_Measure(Prod_Measure(L-Meas n),L-Meas),g)
= Integral(Prod_Measure(L-Meas n),Integral2(L-Meas,R_EAL g))
by A1,A2,A4,A3,A5,Lm3;
I0 \/ NI = CarProduct(Seg n --> REAL) by XBOOLE_1:45; then
A11:RG2| (I0 \/ NI) = RG2;
A12:F0 = R_EAL G2 by A6,MESFUNC5:def 7;
RG2 is_integrable_on Prod_Measure(L-Meas n) by A1,A2,A4,A5,A3,Lm3; then
A13:Integral(Prod_Measure(L-Meas n),RG2)
= Integral(Prod_Measure(L-Meas n),F0)
+ Integral(Prod_Measure(L-Meas n),F1)
by A8,A9,A11,XBOOLE_1:85,MESFUNC5:98;
for x being Element of CarProduct(Seg n --> REAL)
st x in dom F1 holds F1.x = 0
proof
let x be Element of CarProduct(Seg n --> REAL);
assume
A14: x in dom F1; then
not x in I0 by A7,XBOOLE_0:def 5; then
A15: dom ProjPMap1(Rg,x) = {} by A2,A3,A5,MESFUN16:27;
(Integral2(L-Meas,Rg)).x = Integral(L-Meas,(ProjPMap1(Rg,x)))
by MESFUN12:def 8; then
(Integral2(L-Meas,Rg)).x = 0 by A15,MESFUN16:1;
hence thesis by A7,A14,FUNCT_1:49;
end; then
Integral(Prod_Measure(L-Meas n),F1) = 0 by A9,A7,MESFUN12:57;
hence thesis by A12,A10,A13,XXREAL_3:4;
end;
theorem
for n be non zero Nat, D be n-element FinSequence,
I be Subset of CarProduct(Seg n --> RNS_Real),
J be non empty closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
G1 be PartFunc of REAL,REAL
st (for i be Nat st i in Seg n
holds D.i is closed_interval Subset of REAL)
& I = CarProduct D
& [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g
& G1 = Integral1(Prod_Measure(L-Meas n),R_EAL g) |J holds
Integral(Prod_Measure(Prod_Measure(L-Meas n),L-Meas),R_EAL g)
= integral(G1,J)
proof
let n be non zero Nat, D be n-element FinSequence,
I be Subset of CarProduct(Seg n --> RNS_Real),
J be non empty closed_interval Subset of REAL,
f be PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real,
g be PartFunc of [:CarProduct(Seg n --> REAL),REAL:],REAL,
G1 be PartFunc of REAL,REAL;
assume that
A1: for i be Nat st i in Seg n
holds D.i is closed_interval Subset of REAL and
A2: I = CarProduct D and
A3: [:I,J:] = dom f and
A4: f is_continuous_on [:I,J:] and
A5: f = g and
A6: G1 = Integral1(Prod_Measure(L-Meas n),R_EAL g) |J;
set Rg =R_EAL g;
set NJ = REAL \ J;
set RG1 = Integral1(Prod_Measure(L-Meas n),Rg);
reconsider F0 = RG1|J, F1 = RG1|NJ
as PartFunc of REAL,ExtREAL by PARTFUN1:11;
A7: dom RG1 = REAL by FUNCT_2:def 1;
A8: dom(RG1|J) = J by FUNCT_2:def 1;
A9:J is Element of L-Field by MEASUR10:5,MEASUR12:75;
G1|J is bounded & G1 is_integrable_on J
by A8,A1,A2,A3,A4,A5,A6,Th54,INTEGRA5:10,11; then
A10:Integral(L-Meas,G1|J) = integral(G1,J) by A6,A9,A8,MESFUN14:49;
REAL in L-Field by PROB_1:5; then
A11: NJ is Element of L-Field by A9,PROB_1:6;
A12:Integral(Prod_Measure(Prod_Measure(L-Meas n),L-Meas),g)
= Integral(L-Meas,Integral1(Prod_Measure(L-Meas n),R_EAL g))
by A1,A2,A4,A3,A5,Lm4;
J \/ NJ = REAL by XBOOLE_1:45; then
A13:RG1| (J \/ NJ) = RG1;
RG1 is_integrable_on L-Meas by A1,A2,A4,A3,A5,Lm4; then
A14:Integral(L-Meas,RG1) = Integral(L-Meas,F0) + Integral(L-Meas,F1)
by A9,A11,A13,XBOOLE_1:85,MESFUNC5:98;
for i be Nat st i in Seg n holds D.i is Subset of REAL by A1; then
A15:CarProduct D is Subset of CarProduct(Seg n --> REAL)
by FINSEQ_1:3,Th11;
for y being Element of REAL st y in dom F1 holds F1.y = 0
proof
let y be Element of REAL;
assume
A16: y in dom F1; then
not y in J by A7,XBOOLE_0:def 5; then
A17: dom ProjPMap2(Rg,y) = {} by A15,A2,A3,A5,MESFUN16:28;
(Integral1(Prod_Measure(L-Meas n),Rg)).y
= Integral(Prod_Measure(L-Meas n),(ProjPMap2(Rg,y)))
by MESFUN12:def 7; then
(Integral1(Prod_Measure(L-Meas n),Rg)).y = 0 by A17,MESFUN16:1;
hence thesis by A7,A16,FUNCT_1:49;
end; then
Integral(L-Meas,F1) = 0 by A11,A7,MESFUN12:57; then
Integral(Prod_Measure(Prod_Measure(L-Meas n),L-Meas),Rg)
= Integral(L-Meas,F0)
by A12,A14,XXREAL_3:4;
hence thesis by A6,A10,MESFUNC5:def 7;
end;
begin :: Integrability of continuous functions on $n$-dimensional real normed spaces
theorem
for n be non zero Nat, f be PartFunc of product(Seg n--> RNS_Real),RNS_Real
holds f*(CarProd(Seg n --> RNS_Real))
is PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real;
theorem Th60:
for n be non zero Nat, D be n-element FinSequence,
f be PartFunc of product(Seg n --> RNS_Real),RNS_Real
st (for i be Nat st i in Seg n holds D.i is Subset of REAL)
& f is_continuous_on dom f & dom f = product D
holds f*(CarProd(Seg n --> RNS_Real)) is_continuous_on CarProduct D
proof
let n be non zero Nat, D be n-element FinSequence,
f be PartFunc of product(Seg n--> RNS_Real),RNS_Real;
assume that
A1: for i be Nat st i in Seg n holds D.i is Subset of REAL and
A2: f is_continuous_on dom f and
A3: dom f = product D;
set I = CarProd(Seg n --> RNS_Real);
set I0 = CarProd(Seg n --> REAL);
consider CX be non-empty n-element FinSequence such that
A4: CX = carr (Seg n --> RNS_Real)
& CarProduct CX = the carrier of CarProduct(Seg n --> RNS_Real)
& I = CarProd CX
& I is bijective by MEASUR15:def 7;
A5: dom I = the carrier of CarProduct(Seg n --> RNS_Real)
by FUNCT_2:def 1;
n |-> RNS_Real = Seg n --> RNS_Real by FINSEQ_2:def 2; then
the carrier of product (Seg n --> RNS_Real)
= the carrier of (REAL-NS n) by LOPBAN15:11; then
the carrier of product (Seg n --> RNS_Real)
= REAL n by REAL_NS1:def 4; then
rng I = REAL n by A4,FUNCT_2:def 3; then
dom (I") = REAL n
& rng (I") = the carrier of CarProduct(Seg n--> RNS_Real)
by A4,A5,FUNCT_1:33; then
reconsider J = I" as Function of REAL n,the carrier of
CarProduct(Seg n --> RNS_Real) by FUNCT_2:1;
reconsider F = f*I
as PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real;
reconsider G = F
as PartFunc of CarProduct(Seg n --> REAL),REAL by MEASUR15:42;
reconsider H = (R_EAL G)*J as PartFunc of REAL n,ExtREAL;
CarProduct D is Subset of CarProduct(Seg n --> REAL)
by A1,FINSEQ_1:3,Th11; then
CarProduct D c= CarProduct(Seg n -->REAL); then
A6: CarProduct D c= the carrier of CarProduct(Seg n-->RNS_Real) by MEASUR15:42;
for x be object holds x in product D iff x in I.:CarProduct D
proof
let x be object;
hereby assume
A7: x in product D; then
consider g being Function such that
A8: x = g & dom g = dom D
& for y being object st y in dom D holds g.y in D.y by CARD_3:def 5;
A9: dom D = Seg len D by FINSEQ_1:def 3; then
A10: dom D = Seg n by CARD_1:def 7;
reconsider t=x as FinSequence by A8,A9,FINSEQ_1:def 2;
Seg len t = Seg n by A8,A10,FINSEQ_1:def 3; then
reconsider y = t as n-element FinSequence by CARD_1:def 7,FINSEQ_1:6;
A11: PtCarProduct y in CarProduct D by A7,Th7;
reconsider s = PtCarProduct y
as Point of CarProduct(Seg n-->RNS_Real) by A6,A7,Th7;
consider px be n-element FinSequence such that
A12: s = PtCarProduct px & I.s = px by MEASUR15:28;
px = x by A12,MEASUR15:5;
hence x in I.:CarProduct D by A5,A11,A12,FUNCT_1:def 6;
end;
assume x in I.:CarProduct D; then
consider t being object such that
A13: t in dom I & t in CarProduct D & x = I.t by FUNCT_1:def 6;
reconsider s = t as Point of CarProduct(Seg n-->RNS_Real) by A13;
consider px be n-element FinSequence such that
A14: s = PtCarProduct px & I.s = px by MEASUR15:28;
ex qx be n-element FinSequence st
qx in product D & t = PtCarProduct qx by A13,Th7;
hence x in product D by A13,A14,MEASUR15:5;
end; then
A15:product D = I.:(CarProduct D) by TARSKI:2;
A16:CarProduct D c= dom I by FUNCT_2:def 1,A6;
dom F = I" (product D) by A3,RELAT_1:147; then
A17:dom F = CarProduct(D) by A15,FUNCT_1:94,A4,A16;
for x0 be Point of CarProduct(Seg n-->RNS_Real), r be Real
st x0 in CarProduct D & 0 < r
ex s be Real st 0<s
& for x1 be Point of CarProduct(Seg n-->RNS_Real)
st x1 in CarProduct D & ||. x1- x0 .|| < s
holds ||. F/.x1 - F/.x0.|| < r
proof
let x0 be Point of CarProduct(Seg n-->RNS_Real), r be Real;
assume that
A18: x0 in CarProduct D and
A19: 0 < r;
reconsider y0 = I.x0 as Point of product (Seg n-->RNS_Real);
A20: y0 in product D by A5,A15,A18,FUNCT_1:def 6; then
consider s be Real such that
A21: 0 < s
& for y1 be Point of product(Seg n-->RNS_Real)
st y1 in product D & ||. y1- y0 .|| < s
holds ||. f/.y1 - f/.y0.|| < r by A2,A3,A19,NFCONT_1:19;
take s;
thus 0 < s by A21;
let x1 be Point of CarProduct(Seg n-->RNS_Real);
assume that
A22: x1 in CarProduct D and
A23: ||. x1- x0 .|| < s;
reconsider y1 = I.x1 as Point of product (Seg n-->RNS_Real);
A24: y1 in product D by A5,A15,A22,FUNCT_1:def 6;
A25: -1 is Element of REAL by XREAL_0:def 1;
y1- y0 = y1+(-1)*y0 by RLVECT_1:16; then
y1- y0 = I.x1 + I.((-1)*x0) by A25,MEASUR15:30; then
y1- y0 = I.(x1+(-1)*x0 ) by MEASUR15:29; then
y1- y0 = I.(x1-x0) by RLVECT_1:16; then
||. x1- x0 .|| = ||. y1- y0 .|| by MEASUR15:31; then
A26: ||. f/.y1 - f/.y0.|| < r by A21,A23,A24;
F/.x1 = F.x1 by A17,PARTFUN1:def 6,A22; then
F/.x1 = f.(I.x1) by A5,FUNCT_1:13; then
A27: F/.x1 = f/.y1 by A3,A24,PARTFUN1:def 6;
F/.x0 = F.x0 by A17,PARTFUN1:def 6,A18; then
F/.x0 = f.(I.x0) by A5,FUNCT_1:13;
hence thesis by A26,A27,A3,A20,PARTFUN1:def 6;
end;
hence thesis by A17,NFCONT_1:19;
end;
theorem Th61:
for n be non zero Nat holds
REAL-NS n = product(Seg n --> RNS_Real)
& REAL n = the carrier of product(Seg n --> RNS_Real)
& REAL n = product(Seg n --> REAL)
proof
let n be non zero Nat;
A1: n |-> RNS_Real = Seg n-->RNS_Real by FINSEQ_2:def 2;
hence REAL-NS n = product(Seg n --> RNS_Real) by LOPBAN15:11;
the carrier of product (Seg n-->RNS_Real)
= the carrier of (REAL-NS n) by A1,LOPBAN15:11;
hence REAL n = the carrier of product(Seg n --> RNS_Real)
by REAL_NS1:def 4;
product(Seg n--> REAL) = n-tuples_on REAL by SRINGS_5:10;
hence product(Seg n--> REAL) = REAL n by EUCLID:def 1;
end;
theorem Th62:
for n be non zero Nat, D be n-element FinSequence,
f be PartFunc of REAL-NS n,RNS_Real
st (for i be Nat st i in Seg n holds D.i is Subset of REAL)
& f is_continuous_on dom f & dom f = product D
holds f*(CarProd(Seg n --> RNS_Real)) is_continuous_on CarProduct D
proof
let n be non zero Nat, D be n-element FinSequence,
f be PartFunc of REAL-NS n,RNS_Real;
assume that
A1: for i be Nat st i in Seg n holds D.i is Subset of REAL and
A2: f is_continuous_on dom f and
A3: dom f = product D;
reconsider f1=f as PartFunc of product(Seg n-->RNS_Real),RNS_Real
by Th61;
f1 is_continuous_on dom f1 by A2,Th61;
hence thesis by A1,A3,Th60;
end;
theorem
for n be non zero Nat, D be n-element FinSequence,
f be PartFunc of REAL-NS n,RNS_Real, g be PartFunc of REAL n,REAL,
G be PartFunc of CarProduct(Seg n --> REAL),REAL
st (for i be Nat st i in Seg n
holds D.i is closed_interval Subset of REAL)
& f is_continuous_on product D & dom f = product D
& g = f & G = f*CarProd(Seg n --> REAL) holds
G is_integrable_on Prod_Measure(L-Meas n)
& g is_integrable_on XL-Meas n
& Integral(XL-Meas n,g) = Integral(Prod_Measure(L-Meas n),G)
proof
let n be non zero Nat, D be n-element FinSequence,
f be PartFunc of REAL-NS n,RNS_Real, g be PartFunc of REAL n,REAL,
G be PartFunc of CarProduct(Seg n --> REAL),REAL;
assume that
A1: for i be Nat st i in Seg n
holds D.i is closed_interval Subset of REAL and
A2: f is_continuous_on product D and
A3: dom f = product D and
A4: g = f and
A5: G = f*CarProd(Seg n --> REAL);
set I = CarProd(Seg n --> RNS_Real);
consider CX be non-empty n-element FinSequence such that
A6: CX = carr(Seg n--> RNS_Real)
& CarProduct CX = the carrier of CarProduct(Seg n--> RNS_Real)
& I = CarProd CX
& I is bijective by MEASUR15:def 7;
A7: REAL-NS n = product(Seg n-->RNS_Real) by Th61; then
A8: the carrier of (REAL-NS n) = REAL n by Th61; then
A9: rng I = REAL n by A6,A7,FUNCT_2:def 3;
A10: dom I = the carrier of CarProduct(Seg n --> RNS_Real)
by FUNCT_2:def 1; then
dom (I") = REAL n
& rng (I") = the carrier of CarProduct(Seg n--> RNS_Real)
by A6,A9,FUNCT_1:33; then
reconsider J = I" as Function of REAL n,the carrier of
CarProduct(Seg n --> RNS_Real) by FUNCT_2:1;
reconsider H = (R_EAL G)*J as PartFunc of REAL n,ExtREAL;
A11:I = CarProd(Seg n --> REAL) by MEASUR15:70;
H = G*J by MESFUNC5:def 7; then
H = f*(I*I") by A5,A11,RELAT_1:36; then
H = f * id (rng I) by A6,FUNCT_1:39; then
A12:H = f by A8,A9,FUNCT_2:17;
reconsider F = f*I
as PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real;
for i be Nat st i in Seg n holds D.i is Subset of REAL by A1; then
A13:F is_continuous_on CarProduct D by A2,A3,Th62;
A14: for i be Nat st i in Seg n holds D.i c= REAL
proof
let i be Nat;
assume i in Seg n; then
D.i is Subset of REAL by A1;
hence thesis;
end;
CarProduct D c= CarProduct(Seg n -->REAL)
proof
per cases;
suppose D is non-empty; then
reconsider D1 = D as non-empty n-element FinSequence;
CarProduct D1 c= CarProduct(Seg n --> REAL) by A14,MEASUR15:34;
hence thesis;
end;
suppose not D is non-empty;
hence thesis by Th6;
end;
end; then
A15:CarProduct D c= dom I by A10,MEASUR15:42;
A16:product D = I.:(CarProduct D) by A14,A11,Th12;
dom F = I" (dom f) by RELAT_1:147;
hence
A17: G is_integrable_on Prod_Measure(L-Meas n)
by A1,A3,A5,A6,A11,A16,A15,A13,Th43,FUNCT_1:94; then
H is_integrable_on XL-Meas n by A11,MEASUR14:55;
hence g is_integrable_on XL-Meas n by A4,A12,MESFUNC5:def 7;
ex A being Element of Prod_Field(L-Field n)
st (A = dom R_EAL G & R_EAL G is A -measurable)
by A17,MESFUNC5:def 17;
hence Integral(XL-Meas n,g) = Integral(Prod_Measure(L-Meas n),G)
by A4,A12,A11,MESFUNC5:def 7,MEASUR14:54;
end;
theorem
for n be non zero Nat, D be (n+1)-element FinSequence,
f be PartFunc of REAL-NS(n+1),RNS_Real,
G be PartFunc of CarProduct(Seg (n+1) --> REAL),REAL,
g0 be PartFunc of [:CarProduct(Seg n-->REAL),REAL:],REAL
st ( for i be Nat st i in Seg (n+1)
holds D.i is closed_interval Subset of REAL)
& f is_continuous_on product D & dom f = product D
& G = f*CarProd(Seg (n+1) --> REAL) & g0 = G
holds
(for x being Element of CarProduct(Seg n-->REAL)
holds Integral2(L-Meas,|.R_EAL g0.|).x < +infty)
& (for x being Element of CarProduct(Seg n-->REAL)
holds ProjPMap1(R_EAL g0,x) is_integrable_on L-Meas)
& (for U being Element of Prod_Field(L-Field n)
holds Integral2(L-Meas,R_EAL g0) is U-measurable)
& Integral2(L-Meas,R_EAL g0) is_integrable_on Prod_Measure(L-Meas n)
& Integral(Prod_Measure(L-Meas (n+1)),G)
= Integral(Prod_Measure(L-Meas n),Integral2(L-Meas,R_EAL g0))
proof
let n be non zero Nat, D be (n+1)-element FinSequence,
f be PartFunc of REAL-NS(n+1),RNS_Real,
G be PartFunc of CarProduct(Seg (n+1) --> REAL),REAL,
g0 be PartFunc of [:CarProduct(Seg n-->REAL),REAL:],REAL;
assume that
A1: for i be Nat st i in Seg (n+1)
holds D.i is closed_interval Subset of REAL and
A2: f is_continuous_on product D and
A3: dom f = product D and
A4: G = f*CarProd(Seg (n+1) --> REAL) and
A5: g0 = G;
set I = CarProd(Seg (n+1) --> RNS_Real);
set I0 = CarProd(Seg (n+1) --> REAL);
A6: ex CX be non-empty (n+1)-element FinSequence st
CX = carr (Seg (n+1)--> RNS_Real)
& CarProduct CX = the carrier of CarProduct(Seg (n+1)--> RNS_Real)
& I = CarProd CX & I is bijective by MEASUR15:def 7;
A7:I = CarProd(Seg (n+1) --> REAL) by MEASUR15:70;
A8:for i be Nat st i in Seg (n+1) holds D.i c= REAL
proof
let i be Nat;
assume i in Seg (n+1); then
D.i is Subset of REAL by A1;
hence thesis;
end;
for i be Nat st i in Seg (n+1) holds D.i c= (Seg(n+1)-->REAL).i
proof
let i be Nat;
assume
A9: i in Seg(n+1); then
A10: D.i is Subset of REAL by A1;
(Seg(n+1)-->REAL).i = REAL by A9,FUNCOP_1:7;
hence thesis by A10;
end; then
CarProduct D c= CarProduct(Seg (n+1) -->REAL) by Th10; then
CarProduct D c= the carrier of CarProduct(Seg (n+1)-->RNS_Real)
by MEASUR15:42; then
A11:CarProduct D c= dom I by FUNCT_2:def 1;
reconsider D1 = D|n as n-element FinSequence;
for i be Nat st i in Seg n holds D1.i c= (Seg n-->REAL).i
proof
let i be Nat;
assume
A12: i in Seg n; then
A13: i <= n by FINSEQ_1:1;
A14: Seg n c= Seg(n+1) by FINSEQ_3:18;
D1.i = D.i by A13,FINSEQ_3:112; then
A15: D1.i is Subset of REAL by A1,A12,A14;
(Seg n-->REAL).i = REAL by A12,FUNCOP_1:7;
hence D1.i c= (Seg n-->REAL).i by A15;
end; then
A16: CarProduct D1 is Subset of CarProduct(Seg n --> REAL) by Th10; then
reconsider I1 = CarProduct D1 as Subset of CarProduct(Seg n --> RNS_Real)
by MEASUR15:42;
reconsider J1 = D.(n+1) as closed_interval Subset of REAL
by A1,FINSEQ_1:4;
reconsider f0 = f*I
as PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real
by MEASUR15:38;
A17:for i be Nat st i in Seg (n+1) holds D.i is Subset of REAL by A1; then
A18:f*I is_continuous_on CarProduct D by A2,A3,Th62;
A19:CarProduct D = [: CarProduct D1,D.(n+1) :] by Th4;
dom(f*I) = I" (product D) by A3,RELAT_1:147; then
dom(f*I) = I"(I.:(CarProduct D)) by A8,A7,Th12; then
A20:dom(f*I) = CarProduct D by A6,A11,FUNCT_1:94; then
A21:dom f0 = [:I1,J1:] by Th4;
A22:CarProduct(Seg(n+1) --> RNS_Real)
= [:CarProduct(Seg n--> RNS_Real),RNS_Real:] by MEASUR15:38;
A23:for i be Nat st i in Seg n holds D1.i is closed_interval Subset of REAL
proof
let i be Nat;
assume
A24: i in Seg n; then
i <= n by FINSEQ_1:1; then
A25: D1.i = D.i by FINSEQ_3:112;
Seg n c= Seg(n+1) by FINSEQ_3:18;
hence D1.i is closed_interval Subset of REAL by A1,A24,A25;
end;
hence for x being Element of CarProduct(Seg n --> REAL)
holds Integral2(L-Meas,|.R_EAL g0.|).x < +infty
by A5,A4,A7,A18,A22,A21,A19,Lm3;
thus for x being Element of CarProduct(Seg n-->REAL)
holds ProjPMap1(R_EAL g0,x) is_integrable_on L-Meas
proof
let x be Element of CarProduct(Seg n --> REAL);
reconsider Pg1 = ProjPMap1(R_EAL g0,x) as PartFunc of REAL,REAL
by MESFUN16:30;
Pg1 is_integrable_on L-Meas
by A16,A5,A4,A7,A21,A17,A2,A3,A22,A19,Th29,Th62;
hence ProjPMap1(R_EAL g0,x) is_integrable_on L-Meas by MESFUNC5:def 7;
end;
Integral(Prod_Measure(L-Meas(n+1)),G)
= Integral(Prod_Measure(Prod_Measure(L-Meas n),L-Meas),g0)
by A1,A5,A4,A7,A20,A18,Th56;
hence thesis by A5,A4,A7,A21,A18,A22,A19,A23,Lm3;
end;
theorem
for n be non zero Nat, D be (n+1)-element FinSequence,
D1 be n-element FinSequence, f be PartFunc of REAL-NS(n+1),RNS_Real,
G be PartFunc of CarProduct(Seg (n+1) --> REAL),REAL,
g0 be PartFunc of [:CarProduct(Seg n-->REAL),REAL:],REAL,
Dk1 be non empty closed_interval Subset of REAL,
x be Element of CarProduct(Seg n --> REAL),
Pg be PartFunc of REAL,REAL
st D1 = D|n & ( for i be Nat st i in Seg (n+1) holds D.i is Subset of REAL)
& f is_continuous_on product D & dom f = product D
& G = f*CarProd(Seg (n+1) --> REAL) & g0 = G
& Dk1 = D.(n+1) & x in CarProduct D1 & Pg = ProjPMap1(|.R_EAL g0.|,x)
holds dom ProjPMap1(|.R_EAL g0.|,x) = D.(n+1)
& Pg|Dk1 is continuous & Pg|Dk1 is bounded & Pg is_integrable_on Dk1
& ProjPMap1(|.R_EAL g0.|,x) is_integrable_on L-Meas
& Integral(L-Meas,(ProjPMap1(|.R_EAL g0.|,x))) = integral(Pg,Dk1)
& (Integral2(L-Meas,|.R_EAL g0.|)).x = integral(Pg,Dk1)
proof
let n be non zero Nat, D be (n+1)-element FinSequence,
D1 be n-element FinSequence,
f be PartFunc of REAL-NS(n+1),RNS_Real,
G be PartFunc of CarProduct(Seg (n+1) --> REAL),REAL,
g0 be PartFunc of [:CarProduct(Seg n-->REAL),REAL:],REAL,
Dk1 be non empty closed_interval Subset of REAL,
x be Element of CarProduct(Seg n --> REAL),
Pg be PartFunc of REAL,REAL;
assume that
A1: D1 = D|n and
A2: for i be Nat st i in Seg (n+1) holds D.i is Subset of REAL and
A3: f is_continuous_on product D and
A4: dom f = product D and
A5: G = f*CarProd(Seg (n+1) --> REAL) and
A6: g0 = G and
A7: Dk1 = D.(n+1) and
A8: x in CarProduct D1 and
A9: Pg = ProjPMap1(|.R_EAL g0.|,x);
set I = CarProd(Seg (n+1) --> RNS_Real);
set I0 = CarProd(Seg (n+1) --> REAL);
A10: ex CX be non-empty (n+1)-element FinSequence st
CX = carr (Seg (n+1)--> RNS_Real)
& CarProduct CX = the carrier of CarProduct(Seg (n+1)--> RNS_Real)
& I = CarProd CX
& I is bijective by MEASUR15:def 7;
A11:I = CarProd(Seg (n+1) --> REAL) by MEASUR15:70;
A12:for i be Nat st i in Seg (n+1) holds D.i c= REAL
proof
let i be Nat;
assume i in Seg (n+1); then
D.i is Subset of REAL by A2;
hence thesis;
end;
for i be Nat st i in Seg (n+1) holds D.i c= (Seg(n+1)-->REAL).i
proof
let i be Nat;
assume
A13: i in Seg(n+1); then
D.i is Subset of REAL by A2; then
D.i c= REAL;
hence thesis by A13,FUNCOP_1:7;
end; then
CarProduct D c= CarProduct(Seg (n+1) -->REAL) by Th10; then
CarProduct D c= the carrier of CarProduct(Seg (n+1)-->RNS_Real)
by MEASUR15:42; then
A14:CarProduct D c= dom I by FUNCT_2:def 1;
dom (f*I) = I" (product D) by A4,RELAT_1:147; then
dom (f*I) = I"(I.:(CarProduct D)) by A12,A11,Th12; then
A15:dom (f*I) = CarProduct D by A10,A14,FUNCT_1:94;
A16:f*I is_continuous_on CarProduct D by A2,A3,A4,Th62;
for i be Nat st i in Seg n holds D1.i is Subset of REAL
proof
let i be Nat;
assume
A17: i in Seg n; then
i <= n by FINSEQ_1:1; then
A18: D1.i = D.i by A1,FINSEQ_3:112;
Seg n c= Seg(n+1) by FINSEQ_3:18;
hence D1.i is Subset of REAL by A2,A17,A18;
end; then
A19: CarProduct D1 is Subset of CarProduct(Seg n-->REAL)
by FINSEQ_1:3,Th11; then
reconsider I1 = CarProduct D1
as Subset of CarProduct(Seg n --> RNS_Real) by MEASUR15:42;
reconsider f0 = f*I
as PartFunc of [:CarProduct(Seg n --> RNS_Real),RNS_Real:],RNS_Real
by MEASUR15:38;
A20:dom f0 = [:I1,Dk1:] by A15,A7,A1,Th4;
hence dom ProjPMap1(|.R_EAL g0.|,x) = D.(n+1)
by A19,A5,A6,A11,A7,A8,MESFUN16:27;
A21:f0 is_continuous_on dom f0 by A16,A15,MEASUR15:38; then
Pg is continuous by A5,A6,A11,A9,Th25;
hence Pg|Dk1 is continuous;
thus Pg|Dk1 is bounded & Pg is_integrable_on Dk1
by A19,A5,A6,A11,A8,A20,A21,A9,Th28;
Pg is_integrable_on L-Meas by A19,A5,A6,A11,A20,A21,A9,Th31;
hence ProjPMap1(|.R_EAL g0.|,x) is_integrable_on L-Meas
by A9,MESFUNC5:def 7;
thus Integral(L-Meas,(ProjPMap1(|.R_EAL g0.|,x))) = integral(Pg,Dk1)
& (Integral2(L-Meas,|.R_EAL g0.|)).x = integral(Pg,Dk1)
by A19,A5,A6,A8,A9,A11,A20,A21,Th32;
end;