MESFUN16: Integral of Continuous Functions of Two Variables

:: Integral of Continuous Functions of Two Variables
:: by Noboru Endou and Yasunari Shidama
::
:: Received December 18, 2023
:: Copyright (c) 2023-2025 Association of Mizar Users

theorem Th1: :: MESFUN16:1

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st dom f = {} holds
Integral (M,f) = 0

proof end;

theorem :: MESFUN16:2

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st dom f = {} holds
Integral (M,f) = 0

proof end;

theorem Th3: :: MESFUN16:3

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S st M is sigma_finite holds
COM M is sigma_finite

proof end;

theorem Th4: :: MESFUN16:4

B-Meas is sigma_finite

proof end;

theorem Th5: :: MESFUN16:5

L-Meas is sigma_finite by Th4, Th3, MEASUR12:def 11, MEASUR12:def 12;

theorem :: MESFUN16:6

Prod_Measure (L-Meas,L-Meas) is sigma_finite by Th5, MEASUR13:27;

theorem Th7: :: MESFUN16:7

for I being closed_interval Subset of REAL
for E being Subset of RNS_Real st I = E holds
E is compact

proof end;

definition

let S1, S2 be RealNormSpace;
let D1 be Subset of S1;
let D2 be Subset of S2;
:: original: [:
redefine func [:D1,D2:] -> Subset of [:S1,S2:];
coherence

proof end;

end;

theorem Th8: :: MESFUN16:8

for P, Q being RealNormSpace
for E being Subset of P
for F being Subset of Q st E is compact & F is compact holds
( [:E,F:] is Subset of [:P,Q:] & [:E,F:] is compact )

proof end;

theorem Th9: :: MESFUN16:9

for I, J being closed_interval Subset of REAL
for E being Subset of [:RNS_Real,RNS_Real:] st E = [:I,J:] holds
E is compact

proof end;

theorem Th10: :: MESFUN16:10

for E being set
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL st f = g & E c= dom f holds
( f is_uniformly_continuous_on E iff for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2, y1, y2 being 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 end;

theorem Th11: :: MESFUN16:11

for I, J being Interval holds
( [:I,J:] is Subset of [:RNS_Real,RNS_Real:] & [:I,J:] in sigma (measurable_rectangles (L-Field,L-Field)) )

proof end;

theorem Th12: :: MESFUN16:12

for z being Point of RNS_Real
for x, r being Real st x = z holds
Ball (z,r) = ].(x - r),(x + r).[

proof end;

theorem Th13: :: MESFUN16:13

for z being Point of [:RNS_Real,RNS_Real:]
for r being Real st 0 < r holds
ex s, x, y being Real st
( 0 < s & s < r & z = [x,y] & [:].(x - s),(x + s).[,].(y - s),(y + s).[:] c= Ball (z,r) )

proof end;

Lm1: for x, a being Real ex r being Real st
( 0 < r & x in ].(a - r),(a + r).[ )

proof end;

Lm2: for x, a, b being Real st a <= b holds
].(x - a),(x + a).[ c= ].(x - b),(x + b).[

proof end;

theorem Th14: :: MESFUN16:14

for A being Subset of [:RNS_Real,RNS_Real:] st ( for a, b being Real st [a,b] in A holds
ex Rx being real-membered set st
( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } ) ) holds
ex F being Function of A,REAL st
for a, b being Real st [a,b] in A holds
ex Rx being real-membered set st
( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } & F . [a,b] = (upper_bound Rx) / 2 )

proof end;

Lm3: for A being set st A c= [:REAL,REAL:] & A /\ [:RAT,RAT:] <> {} holds
ex p being sequence of [:REAL,REAL:] st rng p = A /\ [:RAT,RAT:]

proof end;

theorem Th15: :: MESFUN16:15

for A being Subset of [:RNS_Real,RNS_Real:] st A is open holds
A in sigma (measurable_rectangles (L-Field,L-Field))

proof end;

theorem :: MESFUN16:16

for H being Subset of RNS_Real
for I being open_interval Subset of REAL st H = I holds
H is open

proof end;

theorem Th17: :: MESFUN16:17

for r being Real
for X being set
for g being PartFunc of X,REAL holds less_dom (g,r) = g " ].-infty,r.[

proof end;

theorem Th18: :: MESFUN16:18

for I, J being closed_interval Subset of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL st f is_continuous_on [:I,J:] & f = g holds
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2, y1, y2 being 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 ) )

proof end;

theorem Th19: :: MESFUN16:19

for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL st f = g holds
||.f.|| = |.g.|

proof end;

theorem :: MESFUN16:20

for X being non empty set
for g being PartFunc of X,REAL
for A being Subset of X holds |.(g | A).| = |.g.| | A

proof end;

theorem Th21: :: MESFUN16:21

for S being RealNormSpace
for x0 being Point of S
for f, g being PartFunc of S,RNS_Real st f is_continuous_in x0 & g = ||.f.|| holds
g is_continuous_in x0

proof end;

theorem Th22: :: MESFUN16:22

for X being set
for S being RealNormSpace
for f, g being PartFunc of S,RNS_Real st f is_continuous_on X & g = ||.f.|| holds
g is_continuous_on X

proof end;

theorem Th23: :: MESFUN16:23

proof end;

theorem Th24: :: MESFUN16:24

for r being Real
for S being RealNormSpace
for E being Subset of S
for f being PartFunc of S,RNS_Real st f is_continuous_on E & dom f = E holds
ex H being Subset of S st
( H /\ E = f " ].-infty,r.[ & H is open )

proof end;

theorem Th25: :: MESFUN16:25

for X, Y, Z being non empty set
for A being Subset of X
for B being Subset of Y
for x being Element of X
for f being PartFunc of [:X,Y:],Z st dom f = [:A,B:] holds
( ( x in A implies dom (ProjPMap1 (f,x)) = B ) & ( not x in A implies dom (ProjPMap1 (f,x)) = {} ) )

proof end;

theorem Th26: :: MESFUN16:26

for X, Y, Z being non empty set
for A being Subset of X
for B being Subset of Y
for y being Element of Y
for f being PartFunc of [:X,Y:],Z st dom f = [:A,B:] holds
( ( y in B implies dom (ProjPMap2 (f,y)) = A ) & ( not y in B implies dom (ProjPMap2 (f,y)) = {} ) )

proof end;

theorem Th27: :: MESFUN16:27

for X, Y being non empty set
for A being Subset of X
for B being Subset of Y
for x being Element of X
for f being PartFunc of [:X,Y:],REAL st dom f = [:A,B:] holds
( ( x in A implies ( dom (ProjPMap1 ((R_EAL f),x)) = B & dom (ProjPMap1 (|.(R_EAL f).|,x)) = B ) ) & ( not x in A implies ( dom (ProjPMap1 ((R_EAL f),x)) = {} & dom (ProjPMap1 (|.(R_EAL f).|,x)) = {} ) ) )

proof end;

theorem Th28: :: MESFUN16:28

for X, Y being non empty set
for A being Subset of X
for B being Subset of Y
for y being Element of Y
for f being PartFunc of [:X,Y:],REAL st dom f = [:A,B:] holds
( ( y in B implies ( dom (ProjPMap2 ((R_EAL f),y)) = A & dom (ProjPMap2 (|.(R_EAL f).|,y)) = A ) ) & ( not y in B implies ( dom (ProjPMap2 ((R_EAL f),y)) = {} & dom (ProjPMap2 (|.(R_EAL f).|,y)) = {} ) ) )

proof end;

theorem Th29: :: MESFUN16:29

for X, Y being non empty set
for Z being set
for f being PartFunc of [:X,Y:],Z
for x being Element of X
for y being Element of Y holds
( rng (ProjPMap1 (f,x)) c= rng f & rng (ProjPMap2 (f,y)) c= rng f )

proof end;

theorem Th30: :: MESFUN16:30

for X, Y being non empty set
for f being PartFunc of [:X,Y:],REAL
for x being Element of X
for y being Element of Y holds
( ProjPMap1 ((R_EAL f),x) is PartFunc of Y,REAL & ProjPMap1 (|.(R_EAL f).|,x) is PartFunc of Y,REAL & ProjPMap2 ((R_EAL f),y) is PartFunc of X,REAL & ProjPMap2 (|.(R_EAL f).|,y) is PartFunc of X,REAL )

proof end;

theorem Th31: :: MESFUN16:31

proof end;

theorem Th32: :: MESFUN16:32

for X, Y being non empty set
for f being PartFunc of [:X,Y:],REAL
for x being Element of X
for y being Element of Y holds
( ProjPMap1 (|.f.|,x) = |.(ProjPMap1 (f,x)).| & ProjPMap2 (|.f.|,y) = |.(ProjPMap2 (f,y)).| )

proof end;

theorem Th33: :: MESFUN16:33

for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL
for t being Element of REAL st f is_continuous_on dom f & f = g holds
( ProjPMap1 (g,t) is continuous & ProjPMap2 (g,t) is continuous )

proof end;

theorem Th34: :: MESFUN16:34

for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL
for t being Element of REAL st f is_continuous_on dom f & f = g holds
( ProjPMap1 (|.g.|,t) is continuous & ProjPMap2 (|.g.|,t) is continuous )

proof end;

theorem :: MESFUN16:35

for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL
for t being Element of REAL st f is_uniformly_continuous_on dom f & f = g holds
( ProjPMap1 (g,t) is uniformly_continuous & ProjPMap2 (g,t) is uniformly_continuous )

proof end;

theorem Th36: :: MESFUN16:36

for x being Element of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL
for Pg1 being PartFunc of REAL,REAL st f is_continuous_on dom f & f = g & Pg1 = ProjPMap1 ((R_EAL g),x) holds
Pg1 is continuous

proof end;

theorem Th37: :: MESFUN16:37

for y being Element of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL
for Pg2 being PartFunc of REAL,REAL st f is_continuous_on dom f & f = g & Pg2 = ProjPMap2 ((R_EAL g),y) holds
Pg2 is continuous

proof end;

theorem Th38: :: MESFUN16:38

proof end;

theorem Th39: :: MESFUN16:39

for y being Element of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL
for p2 being PartFunc of REAL,REAL st f is_continuous_on dom f & f = g & p2 = ProjPMap2 (|.(R_EAL g).|,y) holds
p2 is continuous

proof end;

theorem Th40: :: MESFUN16:40

for I being Subset of REAL
for J being non empty closed_interval Subset of REAL
for x being Element of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL
for Pg1 being 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 end;

theorem Th41: :: MESFUN16:41

proof end;

theorem Th42: :: MESFUN16:42

for I being non empty closed_interval Subset of REAL
for J being Subset of REAL
for y being Element of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL
for Pg2 being PartFunc of REAL,REAL st y in J & dom f = [:I,J:] & f is_continuous_on [:I,J:] & f = g & Pg2 = ProjPMap2 ((R_EAL g),y) holds
( Pg2 | I is bounded & Pg2 is_integrable_on I )

proof end;

theorem Th43: :: MESFUN16:43

proof end;

theorem Th44: :: MESFUN16:44

for I being Subset of REAL
for J being non empty closed_interval Subset of REAL
for x being Element of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL
for Pg1 being 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 end;

theorem Th45: :: MESFUN16:45

for I being Subset of REAL
for J being non empty closed_interval Subset of REAL
for x being Element of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL
for Pg1 being PartFunc of REAL,REAL
for E being Element of L-Field st x in I & dom f = [:I,J:] & f is_continuous_on [:I,J:] & f = g & Pg1 = ProjPMap1 (|.(R_EAL g).|,x) & E = J holds
Pg1 is E -measurable

proof end;

theorem Th46: :: MESFUN16:46

for I being Subset of REAL
for J being non empty closed_interval Subset of REAL
for x being Element of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL
for Pg1 being 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 is_integrable_on L-Meas & 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 end;

theorem Th47: :: MESFUN16:47

for I being non empty closed_interval Subset of REAL
for J being Subset of REAL
for y being Element of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL
for Pg2 being PartFunc of REAL,REAL st y in J & dom f = [:I,J:] & f is_continuous_on [:I,J:] & f = g & Pg2 = ProjPMap2 (|.(R_EAL g).|,y) holds
( Pg2 | I is bounded & Pg2 is_integrable_on I )

proof end;

theorem Th48: :: MESFUN16:48

for I being non empty closed_interval Subset of REAL
for J being Subset of REAL
for y being Element of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL
for Pg2 being PartFunc of REAL,REAL
for E being Element of L-Field st y in J & dom f = [:I,J:] & f is_continuous_on [:I,J:] & f = g & Pg2 = ProjPMap2 (|.(R_EAL g).|,y) & E = I holds
Pg2 is E -measurable

proof end;

theorem Th49: :: MESFUN16:49

for I being non empty closed_interval Subset of REAL
for J being Subset of REAL
for y being Element of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL
for Pg2 being PartFunc of REAL,REAL st y in J & dom f = [:I,J:] & f is_continuous_on [:I,J:] & f = g & Pg2 = ProjPMap2 (|.(R_EAL g).|,y) holds
( Pg2 is_integrable_on L-Meas & integral (Pg2,I) = Integral (L-Meas,Pg2) & integral (Pg2,I) = Integral (L-Meas,(ProjPMap2 (|.(R_EAL g).|,y))) & integral (Pg2,I) = (Integral1 (L-Meas,|.(R_EAL g).|)) . y )

proof end;

theorem Th50: :: MESFUN16:50

for I, J being non empty closed_interval Subset of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL
for E being Element of sigma (measurable_rectangles (L-Field,L-Field)) st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & E = [:I,J:] holds
g is E -measurable

proof end;

theorem Th51: :: MESFUN16:51

for I being Subset of REAL
for J being non empty closed_interval Subset of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being 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 end;

theorem Th52: :: MESFUN16:52

for I, J being non empty closed_interval Subset of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL
for G2 being PartFunc of REAL,REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,|.(R_EAL g).|)) | I holds
G2 is continuous

proof end;

theorem Th53: :: MESFUN16:53

proof end;

Lm4: for I, J being non empty closed_interval Subset of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g holds
( g is_integrable_on Prod_Measure (L-Meas,L-Meas) & ( for x being Element of REAL holds (Integral2 (L-Meas,|.(R_EAL g).|)) . x < +infty ) & ( for U being Element of L-Field holds Integral2 (L-Meas,(R_EAL g)) is U -measurable ) & Integral2 (L-Meas,(R_EAL g)) is_integrable_on L-Meas & Integral ((Prod_Measure (L-Meas,L-Meas)),g) = Integral (L-Meas,(Integral2 (L-Meas,(R_EAL g)))) )

proof end;

theorem Th54: :: MESFUN16:54

for I, J being non empty closed_interval Subset of REAL
for g being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for f being PartFunc of [:REAL,REAL:],REAL st [:I,J:] = dom g & g is_continuous_on [:I,J:] & g = f holds
( (Integral1 (L-Meas,|.(R_EAL f).|)) | J is PartFunc of REAL,REAL & (Integral1 (L-Meas,(R_EAL f))) | J is PartFunc of REAL,REAL )

proof end;

theorem Th55: :: MESFUN16:55

for I, J being non empty closed_interval Subset of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL
for G1 being PartFunc of REAL,REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G1 = (Integral1 (L-Meas,|.(R_EAL g).|)) | J holds
G1 is continuous

proof end;

theorem Th56: :: MESFUN16:56

proof end;

Lm5: for I, J being non empty closed_interval Subset of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g holds
( g is_integrable_on Prod_Measure (L-Meas,L-Meas) & ( for y being Element of REAL holds (Integral1 (L-Meas,|.(R_EAL g).|)) . y < +infty ) & ( for V being Element of L-Field holds Integral1 (L-Meas,(R_EAL g)) is V -measurable ) & Integral1 (L-Meas,(R_EAL g)) is_integrable_on L-Meas & Integral ((Prod_Measure (L-Meas,L-Meas)),g) = Integral (L-Meas,(Integral1 (L-Meas,(R_EAL g)))) )

proof end;

theorem :: MESFUN16:57

for I, J being non empty closed_interval Subset of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g holds
( g is_integrable_on Prod_Measure (L-Meas,L-Meas) & ( for x being Element of REAL holds (Integral2 (L-Meas,|.(R_EAL g).|)) . x < +infty ) & ( for y being Element of REAL holds (Integral1 (L-Meas,|.(R_EAL g).|)) . y < +infty ) & ( for U being Element of L-Field holds Integral2 (L-Meas,(R_EAL g)) is U -measurable ) & ( for V being Element of L-Field holds Integral1 (L-Meas,(R_EAL g)) is V -measurable ) & Integral2 (L-Meas,(R_EAL g)) is_integrable_on L-Meas & Integral1 (L-Meas,(R_EAL g)) is_integrable_on L-Meas & Integral ((Prod_Measure (L-Meas,L-Meas)),g) = Integral (L-Meas,(Integral2 (L-Meas,(R_EAL g)))) & Integral ((Prod_Measure (L-Meas,L-Meas)),g) = Integral (L-Meas,(Integral1 (L-Meas,(R_EAL g)))) ) by Lm4, Lm5;

theorem :: MESFUN16:58

proof end;

theorem :: MESFUN16:59

proof end;