:: MESFUNC2 semantic presentation

definition

let c₁ be non empty set ;
let c₂ be PartFunc of c₁, ExtREAL ;
pred c₂ is_finite means :Def1: :: MESFUNC2:def 1
for b₁ being Element of a₁ st b₁ in dom a₂ holds
|.(a₂ . b₁).| <' +infty ;

end;

:: deftheorem Def1 defines is_finite MESFUNC2:def 1 :

theorem Th1: :: MESFUNC2:1

for b₁ being non empty set
for b₂ being PartFunc of b₁, ExtREAL holds b₂ = 1 (#) b₂

proof end;

theorem Th2: :: MESFUNC2:2

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, ExtREAL st ( b₂ is_finite or b₃ is_finite ) holds
( dom (b₂ + b₃) = (dom b₂) /\ (dom b₃) & dom (b₂ - b₃) = (dom b₂) /\ (dom b₃) )

proof end;

theorem Th3: :: MESFUNC2:3

for b₁ being non empty set
for b₂ being sigma_Field_Subset of b₁
for b₃, b₄ being PartFunc of b₁, ExtREAL
for b₅ being Function of RAT ,b₂
for b₆ being Real
for b₇ being Element of b₂ st b₃ is_finite & b₄ is_finite & ( for b₈ being Rational holds b₅ . b₈ = (b₇ /\ (less_dom b₃,(R_EAL b₈))) /\ (b₇ /\ (less_dom b₄,(R_EAL (b₆ - b₈)))) ) holds
b₇ /\ (less_dom (b₃ + b₄),(R_EAL b₆)) = union (rng b₅)

proof end;

theorem Th4: :: MESFUNC2:4

ex b₁ being Function of NAT , RAT st
( b₁ is one-to-one & dom b₁ = NAT & rng b₁ = RAT )

proof end;

theorem Th5: :: MESFUNC2:5

for b₁, b₂, b₃ being non empty set
for b₄ being Function of b₁,b₃ st b₁,b₂ are_equipotent holds
ex b₅ being Function of b₂,b₃ st rng b₄ = rng b₅

proof end;

theorem Th6: :: MESFUNC2:6

for b₁ being non empty set
for b₂ being Real
for b₃ being sigma_Field_Subset of b₁
for b₄, b₅ being PartFunc of b₁, ExtREAL
for b₆ being Element of b₃ st b₄ is_measurable_on b₆ & b₅ is_measurable_on b₆ holds
ex b₇ being Function of RAT ,b₃ st
for b₈ being Rational holds b₇ . b₈ = (b₆ /\ (less_dom b₄,(R_EAL b₈))) /\ (b₆ /\ (less_dom b₅,(R_EAL (b₂ - b₈))))

proof end;

theorem Th7: :: MESFUNC2:7

for b₁ being non empty set
for b₂ being sigma_Field_Subset of b₁
for b₃, b₄ being PartFunc of b₁, ExtREAL
for b₅ being Element of b₂ st b₃ is_finite & b₄ is_finite & b₃ is_measurable_on b₅ & b₄ is_measurable_on b₅ holds
b₃ + b₄ is_measurable_on b₅

proof end;

theorem Th8: :: MESFUNC2:8

canceled;

theorem Th9: :: MESFUNC2:9

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, ExtREAL holds b₂ - b₃ = b₂ + (- b₃)

proof end;

theorem Th10: :: MESFUNC2:10

for b₁ being Real holds R_EAL (- b₁) = - (R_EAL b₁)

proof end;

theorem Th11: :: MESFUNC2:11

for b₁ being non empty set
for b₂ being PartFunc of b₁, ExtREAL holds - b₂ = (- 1) (#) b₂

proof end;

theorem Th12: :: MESFUNC2:12

for b₁ being non empty set
for b₂ being PartFunc of b₁, ExtREAL
for b₃ being Real st b₂ is_finite holds
b₃ (#) b₂ is_finite

proof end;

theorem Th13: :: MESFUNC2:13

proof end;

definition

let c₁ be non empty set ;
let c₂ be PartFunc of c₁, ExtREAL ;
deffunc H₁( Element of c₁) -> Element of ExtREAL = max (c₂ . a₁),0. ;
func max+ c₂ -> PartFunc of a₁, ExtREAL means :Def2: :: MESFUNC2:def 2
( dom a₃ = dom a₂ & ( for b₁ being Element of a₁ st b₁ in dom a₃ holds
a₃ . b₁ = max (a₂ . b₁),0. ) );
existence

proof end;

uniqueness

proof end;

deffunc H₂( Element of c₁) -> Element of ExtREAL = max (- (c₂ . a₁)),0. ;
func max- c₂ -> PartFunc of a₁, ExtREAL means :Def3: :: MESFUNC2:def 3
( dom a₃ = dom a₂ & ( for b₁ being Element of a₁ st b₁ in dom a₃ holds
a₃ . b₁ = max (- (a₂ . b₁)),0. ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines max+ MESFUNC2:def 2 :

:: deftheorem Def3 defines max- MESFUNC2:def 3 :

theorem Th14: :: MESFUNC2:14

for b₁ being non empty set
for b₂ being PartFunc of b₁, ExtREAL
for b₃ being Element of b₁ st b₃ in dom b₂ holds
0. <=' (max+ b₂) . b₃

proof end;

theorem Th15: :: MESFUNC2:15

for b₁ being non empty set
for b₂ being PartFunc of b₁, ExtREAL
for b₃ being Element of b₁ st b₃ in dom b₂ holds
0. <=' (max- b₂) . b₃

proof end;

theorem Th16: :: MESFUNC2:16

for b₁ being non empty set
for b₂ being PartFunc of b₁, ExtREAL holds max- b₂ = max+ (- b₂)

proof end;

theorem Th17: :: MESFUNC2:17

for b₁ being non empty set
for b₂ being PartFunc of b₁, ExtREAL
for b₃ being Element of b₁ st b₃ in dom b₂ & 0. <' (max+ b₂) . b₃ holds
(max- b₂) . b₃ = 0.

proof end;

theorem Th18: :: MESFUNC2:18

for b₁ being non empty set
for b₂ being PartFunc of b₁, ExtREAL
for b₃ being Element of b₁ st b₃ in dom b₂ & 0. <' (max- b₂) . b₃ holds
(max+ b₂) . b₃ = 0.

proof end;

theorem Th19: :: MESFUNC2:19

for b₁ being non empty set
for b₂ being PartFunc of b₁, ExtREAL holds
( dom b₂ = dom ((max+ b₂) - (max- b₂)) & dom b₂ = dom ((max+ b₂) + (max- b₂)) )

proof end;

theorem Th20: :: MESFUNC2:20

for b₁ being non empty set
for b₂ being PartFunc of b₁, ExtREAL
for b₃ being Element of b₁ st b₃ in dom b₂ holds
( ( (max+ b₂) . b₃ = b₂ . b₃ or (max+ b₂) . b₃ = 0. ) & ( (max- b₂) . b₃ = - (b₂ . b₃) or (max- b₂) . b₃ = 0. ) )

proof end;

theorem Th21: :: MESFUNC2:21

for b₁ being non empty set
for b₂ being PartFunc of b₁, ExtREAL
for b₃ being Element of b₁ st b₃ in dom b₂ & (max+ b₂) . b₃ = b₂ . b₃ holds
(max- b₂) . b₃ = 0.

proof end;

theorem Th22: :: MESFUNC2:22

for b₁ being non empty set
for b₂ being PartFunc of b₁, ExtREAL
for b₃ being Element of b₁ st b₃ in dom b₂ & (max+ b₂) . b₃ = 0. holds
(max- b₂) . b₃ = - (b₂ . b₃)

proof end;

theorem Th23: :: MESFUNC2:23

for b₁ being non empty set
for b₂ being PartFunc of b₁, ExtREAL
for b₃ being Element of b₁ st b₃ in dom b₂ & (max- b₂) . b₃ = - (b₂ . b₃) holds
(max+ b₂) . b₃ = 0.

proof end;

theorem Th24: :: MESFUNC2:24

for b₁ being non empty set
for b₂ being PartFunc of b₁, ExtREAL
for b₃ being Element of b₁ st b₃ in dom b₂ & (max- b₂) . b₃ = 0. holds
(max+ b₂) . b₃ = b₂ . b₃

proof end;

theorem Th25: :: MESFUNC2:25

for b₁ being non empty set
for b₂ being PartFunc of b₁, ExtREAL holds b₂ = (max+ b₂) - (max- b₂)

proof end;

theorem Th26: :: MESFUNC2:26

for b₁ being non empty set
for b₂ being PartFunc of b₁, ExtREAL holds |.b₂.| = (max+ b₂) + (max- b₂)

proof end;

theorem Th27: :: MESFUNC2:27

for b₁ being non empty set
for b₂ being PartFunc of b₁, ExtREAL
for b₃ being sigma_Field_Subset of b₁
for b₄ being Element of b₃ st b₂ is_measurable_on b₄ holds
max+ b₂ is_measurable_on b₄

proof end;

theorem Th28: :: MESFUNC2:28

for b₁ being non empty set
for b₂ being PartFunc of b₁, ExtREAL
for b₃ being sigma_Field_Subset of b₁
for b₄ being Element of b₃ st b₂ is_measurable_on b₄ & b₄ c= dom b₂ holds
max- b₂ is_measurable_on b₄

proof end;

theorem Th29: :: MESFUNC2:29

for b₁ being non empty set
for b₂ being sigma_Field_Subset of b₁
for b₃ being PartFunc of b₁, ExtREAL
for b₄ being Element of b₂ st b₃ is_measurable_on b₄ & b₄ c= dom b₃ holds
|.b₃.| is_measurable_on b₄

proof end;

theorem Th30: :: MESFUNC2:30

for b₁, b₂ being set holds rng (chi b₁,b₂) c= {0. ,1. }

proof end;

definition

let c₁, c₂ be set ;
redefine func chi as chi c₁,c₂ -> PartFunc of a₂, ExtREAL ;
coherence

proof end;

end;

theorem Th31: :: MESFUNC2:31

for b₁ being non empty set
for b₂ being sigma_Field_Subset of b₁
for b₃ being Element of b₂ holds chi b₃,b₁ is_finite

proof end;

theorem Th32: :: MESFUNC2:32

for b₁ being non empty set
for b₂ being sigma_Field_Subset of b₁
for b₃, b₄ being Element of b₂ holds chi b₃,b₁ is_measurable_on b₄

proof end;

registration

let c₁ be set ;
let c₂ be sigma_Field_Subset of c₁;
cluster disjoint_valued FinSequence of a₂;
existence

proof end;

end;

definition

let c₁ be set ;
let c₂ be sigma_Field_Subset of c₁;
mode Finite_Sep_Sequence of a₂ is disjoint_valued FinSequence of a₂;

end;

theorem Th33: :: MESFUNC2:33

for b₁ being non empty set
for b₂ being sigma_Field_Subset of b₁
for b₃ being Function st b₃ is Finite_Sep_Sequence of b₂ holds
ex b₄ being Sep_Sequence of b₂ st
( union (rng b₃) = union (rng b₄) & ( for b₅ being Nat st b₅ in dom b₃ holds
b₃ . b₅ = b₄ . b₅ ) & ( for b₅ being Nat st not b₅ in dom b₃ holds
b₄ . b₅ = {} ) )

proof end;

theorem Th34: :: MESFUNC2:34

for b₁ being non empty set
for b₂ being sigma_Field_Subset of b₁
for b₃ being Function st b₃ is Finite_Sep_Sequence of b₂ holds
union (rng b₃) in b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be sigma_Field_Subset of c₁;
let c₃ be PartFunc of c₁, ExtREAL ;
canceled;
pred c₃ is_simple_func_in c₂ means :Def5: :: MESFUNC2:def 5
( a₃ is_finite & ex b₁ being Finite_Sep_Sequence of a₂ st
( dom a₃ = union (rng b₁) & ( for b₂ being Nat
for b₃, b₄ being Element of a₁ st b₂ in dom b₁ & b₃ in b₁ . b₂ & b₄ in b₁ . b₂ holds
a₃ . b₃ = a₃ . b₄ ) ) );

end;

:: deftheorem Def4 MESFUNC2:def 4 :

:: deftheorem Def5 defines is_simple_func_in MESFUNC2:def 5 :

theorem Th35: :: MESFUNC2:35

for b₁ being non empty set
for b₂ being PartFunc of b₁, ExtREAL st b₂ is_finite holds
rng b₂ is Subset of REAL

proof end;

theorem Th36: :: MESFUNC2:36

for b₁ being non empty set
for b₂ being sigma_Field_Subset of b₁
for b₃ being Nat
for b₄ being Relation st b₄ is Finite_Sep_Sequence of b₂ holds
b₄ | (Seg b₃) is Finite_Sep_Sequence of b₂

proof end;

theorem Th37: :: MESFUNC2:37

for b₁ being non empty set
for b₂ being PartFunc of b₁, ExtREAL
for b₃ being sigma_Field_Subset of b₁
for b₄ being Element of b₃ st b₂ is_simple_func_in b₃ holds
b₂ is_measurable_on b₄

proof end;