:: Integral of Measurable Function
:: by Noboru Endou and Yasunari Shidama
::
:: Received May 24, 2006
:: Copyright (c) 2006 Association of Mizar Users
theorem Th1: :: MESFUNC5:1
theorem Th2: :: MESFUNC5:2
theorem Th3: :: MESFUNC5:3
theorem Th4: :: MESFUNC5:4
theorem Th5: :: MESFUNC5:5
theorem :: MESFUNC5:6
theorem Th7: :: MESFUNC5:7
theorem Th8: :: MESFUNC5:8
theorem Th9: :: MESFUNC5:9
theorem Th10: :: MESFUNC5:10
theorem Th11: :: MESFUNC5:11
theorem :: MESFUNC5:12
theorem Th13: :: MESFUNC5:13
:: deftheorem Def1 defines nonpositive MESFUNC5:def 1 :
:: deftheorem Def2 defines nonpositive MESFUNC5:def 2 :
theorem Th14: :: MESFUNC5:14
theorem Th15: :: MESFUNC5:15
:: deftheorem Def3 defines without-infty MESFUNC5:def 3 :
:: deftheorem Def4 defines without+infty MESFUNC5:def 4 :
:: deftheorem Def5 defines without-infty MESFUNC5:def 5 :
:: deftheorem Def6 defines without+infty MESFUNC5:def 6 :
theorem Th16: :: MESFUNC5:16
theorem Th17: :: MESFUNC5:17
theorem Th18: :: MESFUNC5:18
theorem Th19: :: MESFUNC5:19
theorem Th20: :: MESFUNC5:20
theorem Th21: :: MESFUNC5:21
theorem Th22: :: MESFUNC5:22
theorem :: MESFUNC5:23
theorem Th24: :: MESFUNC5:24
:: deftheorem defines R_EAL MESFUNC5:def 7 :
theorem Th25: :: MESFUNC5:25
theorem Th26: :: MESFUNC5:26
theorem Th27: :: MESFUNC5:27
Lm1:
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 holds
( max+ f is nonnegative & max- f is nonnegative & |.f.| is nonnegative )
theorem Th28: :: MESFUNC5:28
theorem Th29: :: MESFUNC5:29
theorem Th30: :: MESFUNC5:30
theorem Th31: :: MESFUNC5:31
theorem Th32: :: MESFUNC5:32
theorem Th33: :: MESFUNC5:33
theorem Th34: :: MESFUNC5:34
theorem Th35: :: MESFUNC5:35
theorem Th36: :: MESFUNC5:36
theorem Th37: :: MESFUNC5:37
Lm2:
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X, ExtREAL
for A being Element of S st f is nonnegative & g is nonnegative & f is_measurable_on A & g is_measurable_on A holds
( dom (f + g) = (dom f) /\ (dom g) & f + g is_measurable_on A )
by Th22, Th37;
theorem :: MESFUNC5:38
theorem Th39: :: MESFUNC5:39
theorem Th40: :: MESFUNC5:40
theorem Th41: :: MESFUNC5:41
theorem Th42: :: MESFUNC5:42
theorem Th43: :: MESFUNC5:43
Lm3:
for Y being set
for p being FinSequence st ( for i being Nat st i in dom p holds
p . i in Y ) holds
p is FinSequence of Y
Lm4:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X, ExtREAL st f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f holds
( f + g is_simple_func_in S & dom (f + g) <> {} )
theorem Th44: :: MESFUNC5:44
theorem Th45: :: MESFUNC5:45
theorem Th46: :: MESFUNC5:46
theorem Th47: :: MESFUNC5:47
theorem Th48: :: MESFUNC5:48
theorem Th49: :: MESFUNC5:49
theorem Th50: :: MESFUNC5:50
theorem Th51: :: MESFUNC5:51
Lm5:
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
for r being Real st dom f in S & ( for x being set st x in dom f holds
f . x = r ) holds
f is_simple_func_in S
theorem Th52: :: MESFUNC5:52
Lm6:
for X being non empty set
for S being SigmaField of X
for A being Element of S
for f being PartFunc of X, ExtREAL
for r being real number holds A /\ (less_dom f,(R_EAL r)) = less_dom (f | A),(R_EAL r)
Lm7:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of S
for f being PartFunc of X, ExtREAL holds
( f | A is_measurable_on A iff f is_measurable_on A )
Lm8:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X, ExtREAL st ex E1 being Element of S st
( E1 = dom f & f is_measurable_on E1 ) & ex E2 being Element of S st
( E2 = dom g & g is_measurable_on E2 ) & dom f = dom g holds
ex DFPG being Element of S st
( DFPG = dom (f + g) & f + g is_measurable_on DFPG )
theorem Th53: :: MESFUNC5:53
theorem Th54: :: MESFUNC5:54
theorem Th55: :: MESFUNC5:55
:: deftheorem Def8 defines convergent_to_finite_number MESFUNC5:def 8 :
:: deftheorem Def9 defines convergent_to_+infty MESFUNC5:def 9 :
:: deftheorem Def10 defines convergent_to_-infty MESFUNC5:def 10 :
theorem Th56: :: MESFUNC5:56
theorem Th57: :: MESFUNC5:57
:: deftheorem Def11 defines convergent MESFUNC5:def 11 :
:: deftheorem Def12 defines lim MESFUNC5:def 12 :
theorem Th58: :: MESFUNC5:58
theorem Th59: :: MESFUNC5:59
theorem Th60: :: MESFUNC5:60
theorem Th61: :: MESFUNC5:61
theorem Th62: :: MESFUNC5:62
theorem Th63: :: MESFUNC5:63
theorem :: MESFUNC5:64
theorem Th65: :: MESFUNC5:65
theorem Th66: :: MESFUNC5:66
Lm9:
for J being ExtREAL_sequence holds
( not J is without-infty or sup (rng J) in REAL or sup (rng J) = +infty )
theorem Th67: :: MESFUNC5:67
theorem Th68: :: MESFUNC5:68
theorem Th69: :: MESFUNC5:69
:: deftheorem Def13 defines # MESFUNC5:def 13 :
theorem Th70: :: MESFUNC5:70
:: deftheorem Def14 defines integral' MESFUNC5:def 14 :
theorem Th71: :: MESFUNC5:71
theorem Th72: :: MESFUNC5:72
theorem Th73: :: MESFUNC5:73
theorem Th74: :: MESFUNC5:74
Lm10:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X, ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & g is_simple_func_in S & dom g = dom f & g is nonnegative & ( for x being set st x in dom f holds
g . x <= f . x ) holds
( f - g is_simple_func_in S & dom (f - g) <> {} & f - g is nonnegative & integral X,S,M,f = (integral X,S,M,(f - g)) + (integral X,S,M,g) )
theorem Th75: :: MESFUNC5:75
theorem Th76: :: MESFUNC5:76
theorem Th77: :: MESFUNC5:77
theorem Th78: :: MESFUNC5:78
theorem Th79: :: MESFUNC5:79
theorem Th80: :: MESFUNC5:80
theorem Th81: :: MESFUNC5:81
theorem Th82: :: MESFUNC5:82
definition
let X be non
empty set ;
let S be
SigmaField of
X;
let M be
sigma_Measure of
S;
let f be
PartFunc of
X,
ExtREAL ;
assume that A1:
ex
A being
Element of
S st
(
A = dom f &
f is_measurable_on A )
and A2:
f is
nonnegative
;
func integral+ M,
f -> Element of
ExtREAL means :
Def15:
:: MESFUNC5:def 15
ex
F being
Functional_Sequence of
X,
ExtREAL ex
K being
ExtREAL_sequence st
( ( for
n being
Nat holds
(
F . n is_simple_func_in S &
dom (F . n) = dom f ) ) & ( for
n being
Nat holds
F . n is
nonnegative ) & ( for
n,
m being
Nat st
n <= m holds
for
x being
Element of
X st
x in dom f holds
(F . n) . x <= (F . m) . x ) & ( for
x being
Element of
X st
x in dom f holds
(
F # x is
convergent &
lim (F # x) = f . x ) ) & ( for
n being
Nat holds
K . n = integral' M,
(F . n) ) &
K is
convergent &
it = lim K );
existence
ex b1 being Element of ExtREAL ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' M,(F . n) ) & K is convergent & b1 = lim K )
uniqueness
for b1, b2 being Element of ExtREAL st ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' M,(F . n) ) & K is convergent & b1 = lim K ) & ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' M,(F . n) ) & K is convergent & b2 = lim K ) holds
b1 = b2
end;
:: deftheorem Def15 defines integral+ MESFUNC5:def 15 :
theorem Th83: :: MESFUNC5:83
Lm11:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X, ExtREAL st ex A being Element of S st
( A = dom f & A = dom g & f is_measurable_on A & g is_measurable_on A ) & f is nonnegative & g is nonnegative holds
integral+ M,(f + g) = (integral+ M,f) + (integral+ M,g)
theorem Th84: :: MESFUNC5:84
theorem Th85: :: MESFUNC5:85
theorem Th86: :: MESFUNC5:86
theorem Th87: :: MESFUNC5:87
theorem Th88: :: MESFUNC5:88
theorem Th89: :: MESFUNC5:89
theorem Th90: :: MESFUNC5:90
theorem Th91: :: MESFUNC5:91
theorem Th92: :: MESFUNC5:92
theorem Th93: :: MESFUNC5:93
:: deftheorem defines Integral MESFUNC5:def 16 :
theorem Th94: :: MESFUNC5:94
theorem :: MESFUNC5:95
theorem :: MESFUNC5:96
theorem :: MESFUNC5:97
theorem :: MESFUNC5:98
theorem :: MESFUNC5:99
theorem :: MESFUNC5:100
theorem Th101: :: MESFUNC5:101
:: deftheorem Def17 defines is_integrable_on MESFUNC5:def 17 :
theorem Th102: :: MESFUNC5:102
theorem Th103: :: MESFUNC5:103
theorem Th104: :: MESFUNC5:104
theorem :: MESFUNC5:105
theorem Th106: :: MESFUNC5:106
theorem :: MESFUNC5:107
theorem Th108: :: MESFUNC5:108
theorem Th109: :: MESFUNC5:109
theorem Th110: :: MESFUNC5:110
theorem Th111: :: MESFUNC5:111
theorem Th112: :: MESFUNC5:112
theorem Th113: :: MESFUNC5:113
Lm12:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X, ExtREAL st ex E0 being Element of S st
( dom (f + g) = E0 & f + g is_measurable_on E0 ) & f is_integrable_on M & g is_integrable_on M holds
f + g is_integrable_on M
theorem Th114: :: MESFUNC5:114
Lm13:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X, ExtREAL st f is_integrable_on M & g is_integrable_on M & dom f = dom g holds
ex E, NFG, NFPG being Element of S st
( E c= dom f & NFG c= dom f & E = (dom f) \ NFG & f | E is real-valued & E = dom (f | E) & f | E is_measurable_on E & f | E is_integrable_on M & Integral M,f = Integral M,(f | E) & E c= dom g & NFG c= dom g & E = (dom g) \ NFG & g | E is real-valued & E = dom (g | E) & g | E is_measurable_on E & g | E is_integrable_on M & Integral M,g = Integral M,(g | E) & E c= dom (f + g) & NFPG c= dom (f + g) & E = (dom (f + g)) \ NFPG & M . NFG = 0 & M . NFPG = 0 & E = dom ((f + g) | E) & (f + g) | E is_measurable_on E & (f + g) | E is_integrable_on M & (f + g) | E = (f | E) + (g | E) & Integral M,((f + g) | E) = (Integral M,(f | E)) + (Integral M,(g | E)) )
Lm14:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X, ExtREAL st f is_integrable_on M & g is_integrable_on M & dom f = dom g holds
( f + g is_integrable_on M & Integral M,(f + g) = (Integral M,f) + (Integral M,g) )
theorem :: MESFUNC5:115
theorem Th116: :: MESFUNC5:116
:: deftheorem defines Integral_on MESFUNC5:def 18 :
theorem :: MESFUNC5:117
theorem :: MESFUNC5:118