:: MEASURE3 semantic presentation

theorem Th1: :: MEASURE3:1

for b₁ being R_eal st -infty <' b₁ & b₁ <' +infty holds
b₁ is Real

proof end;

theorem Th2: :: MEASURE3:2

for b₁ being R_eal st not b₁ = -infty & not b₁ = +infty holds
b₁ is Real

proof end;

theorem Th3: :: MEASURE3:3

for b₁, b₂ being Function of NAT , ExtREAL st ( for b₃ being Nat holds (Ser b₁) . b₃ <=' (Ser b₂) . b₃ ) holds
SUM b₁ <=' SUM b₂

proof end;

theorem Th4: :: MEASURE3:4

for b₁, b₂ being Function of NAT , ExtREAL st ( for b₃ being Nat holds (Ser b₁) . b₃ = (Ser b₂) . b₃ ) holds
SUM b₁ = SUM b₂

proof end;

notation

let c₁ be set ;
let c₂ be sigma_Field_Subset of c₁;
synonym N_Sub_fam of c₂ for N_Measure_fam of c₂;

end;

definition

let c₁ be set ;
let c₂ be sigma_Field_Subset of c₁;
let c₃ be Function of NAT ,c₂;
redefine func rng as rng c₃ -> N_Measure_fam of a₂;
coherence

proof end;

end;

theorem Th5: :: MEASURE3:5

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂
for b₄ being Function of NAT ,b₂
for b₅ being Element of b₂ st meet (rng b₄) c= b₅ & ( for b₆ being Element of NAT holds b₅ c= b₄ . b₆ ) holds
b₃ . b₅ = b₃ . (meet (rng b₄))

proof end;

theorem Th6: :: MEASURE3:6

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃, b₄ being Function of NAT ,b₂ st b₃ . 0 = {} & ( for b₅ being Element of NAT holds
( b₃ . (b₅ + 1) = (b₄ . 0) \ (b₄ . b₅) & b₄ . (b₅ + 1) c= b₄ . b₅ ) ) holds
union (rng b₃) = (b₄ . 0) \ (meet (rng b₄))

proof end;

theorem Th7: :: MEASURE3:7

proof end;

theorem Th8: :: MEASURE3:8

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂
for b₄, b₅ being Function of NAT ,b₂ st b₃ . (b₅ . 0) <' +infty & b₄ . 0 = {} & ( for b₆ being Element of NAT holds
( b₄ . (b₆ + 1) = (b₅ . 0) \ (b₅ . b₆) & b₅ . (b₆ + 1) c= b₅ . b₆ ) ) holds
b₃ . (meet (rng b₅)) = (b₃ . (b₅ . 0)) - (b₃ . (union (rng b₄)))

proof end;

theorem Th9: :: MEASURE3:9

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂
for b₄, b₅ being Function of NAT ,b₂ st b₃ . (b₅ . 0) <' +infty & b₄ . 0 = {} & ( for b₆ being Element of NAT holds
( b₄ . (b₆ + 1) = (b₅ . 0) \ (b₅ . b₆) & b₅ . (b₆ + 1) c= b₅ . b₆ ) ) holds
b₃ . (union (rng b₄)) = (b₃ . (b₅ . 0)) - (b₃ . (meet (rng b₅)))

proof end;

theorem Th10: :: MEASURE3:10

proof end;

theorem Th11: :: MEASURE3:11

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂
for b₄, b₅ being Function of NAT ,b₂ st b₃ . (b₅ . 0) <' +infty & b₄ . 0 = {} & ( for b₆ being Element of NAT holds
( b₄ . (b₆ + 1) = (b₅ . 0) \ (b₅ . b₆) & b₅ . (b₆ + 1) c= b₅ . b₆ ) ) holds
( sup (rng (b₃ * b₄)) is Real & b₃ . (b₅ . 0) is Real & inf (rng (b₃ * b₅)) is Real )

proof end;

theorem Th12: :: MEASURE3:12

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂
for b₄, b₅ being Function of NAT ,b₂ st b₃ . (b₅ . 0) <' +infty & b₄ . 0 = {} & ( for b₆ being Element of NAT holds
( b₄ . (b₆ + 1) = (b₅ . 0) \ (b₅ . b₆) & b₅ . (b₆ + 1) c= b₅ . b₆ ) ) holds
sup (rng (b₃ * b₄)) = (b₃ . (b₅ . 0)) - (inf (rng (b₃ * b₅)))

proof end;

theorem Th13: :: MEASURE3:13

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂
for b₄, b₅ being Function of NAT ,b₂ st b₃ . (b₅ . 0) <' +infty & b₄ . 0 = {} & ( for b₆ being Element of NAT holds
( b₄ . (b₆ + 1) = (b₅ . 0) \ (b₅ . b₆) & b₅ . (b₆ + 1) c= b₅ . b₆ ) ) holds
inf (rng (b₃ * b₅)) = (b₃ . (b₅ . 0)) - (sup (rng (b₃ * b₄)))

proof end;

theorem Th14: :: MEASURE3:14

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂
for b₄ being Function of NAT ,b₂ st ( for b₅ being Element of NAT holds b₄ . (b₅ + 1) c= b₄ . b₅ ) & b₃ . (b₄ . 0) <' +infty holds
b₃ . (meet (rng b₄)) = inf (rng (b₃ * b₄))

proof end;

theorem Th15: :: MEASURE3:15

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being Measure of b₂
for b₄ being N_Measure_fam of b₂
for b₅ being Sep_Sequence of b₂ st b₄ = rng b₅ holds
SUM (b₃ * b₅) <=' b₃ . (union b₄)

proof end;

theorem Th16: :: MEASURE3:16

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being Measure of b₂
for b₄ being Sep_Sequence of b₂ holds SUM (b₃ * b₄) <=' b₃ . (union (rng b₄)) by Th15;

theorem Th17: :: MEASURE3:17

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being Measure of b₂ st ( for b₄ being Sep_Sequence of b₂ holds b₃ . (union (rng b₄)) <=' SUM (b₃ * b₄) ) holds
b₃ is sigma_Measure of b₂

proof end;

definition

let c₁ be set ;
let c₂ be sigma_Field_Subset of c₁;
let c₃ be sigma_Measure of c₂;
canceled;
pred c₃ is_complete c₂ means :Def2: :: MEASURE3:def 2
for b₁ being Subset of a₁
for b₂ being set st b₂ in a₂ & b₁ c= b₂ & a₃ . b₂ = 0. holds
b₁ in a₂;

end;

:: deftheorem Def1 MEASURE3:def 1 :

:: deftheorem Def2 defines is_complete MEASURE3:def 2 :

definition

let c₁ be set ;
let c₂ be sigma_Field_Subset of c₁;
let c₃ be sigma_Measure of c₂;
mode thin of c₃ -> Subset of a₁ means :Def3: :: MEASURE3:def 3
ex b₁ being set st
( b₁ in a₂ & a₄ c= b₁ & a₃ . b₁ = 0. );
existence

proof end;

end;

:: deftheorem Def3 defines thin MEASURE3:def 3 :

definition

let c₁ be set ;
let c₂ be sigma_Field_Subset of c₁;
let c₃ be sigma_Measure of c₂;
func COM c₂,c₃ -> non empty Subset-Family of a₁ means :Def4: :: MEASURE3:def 4
for b₁ being set holds
( b₁ in a₄ iff ex b₂ being set st
( b₂ in a₂ & ex b₃ being thin of a₃ st b₁ = b₂ \/ b₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines COM MEASURE3:def 4 :

definition

let c₁ be set ;
let c₂ be sigma_Field_Subset of c₁;
let c₃ be sigma_Measure of c₂;
let c₄ be Element of COM c₂,c₃;
func MeasPart c₄ -> non empty Subset-Family of a₁ means :Def5: :: MEASURE3:def 5
for b₁ being set holds
( b₁ in a₅ iff ( b₁ in a₂ & b₁ c= a₄ & a₄ \ b₁ is thin of a₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines MeasPart MEASURE3:def 5 :

theorem Th18: :: MEASURE3:18

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂
for b₄ being Function of NAT , COM b₂,b₃ ex b₅ being Function of NAT ,b₂ st
for b₆ being Element of NAT holds b₅ . b₆ in MeasPart (b₄ . b₆)

proof end;

theorem Th19: :: MEASURE3:19

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂
for b₄ being Function of NAT , COM b₂,b₃
for b₅ being Function of NAT ,b₂ ex b₆ being Function of NAT , bool b₁ st
for b₇ being Element of NAT holds b₆ . b₇ = (b₄ . b₇) \ (b₅ . b₇)

proof end;

theorem Th20: :: MEASURE3:20

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂
for b₄ being Function of NAT , bool b₁ st ( for b₅ being Element of NAT holds b₄ . b₅ is thin of b₃ ) holds
ex b₅ being Function of NAT ,b₂ st
for b₆ being Element of NAT holds
( b₄ . b₆ c= b₅ . b₆ & b₃ . (b₅ . b₆) = 0. )

proof end;

Lemma18: for b₁, b₂, b₃ being set st b₃ c= b₂ holds
b₁ \ b₃ = (b₁ \ b₂) \/ (b₁ /\ (b₂ \ b₃))

proof end;

theorem Th21: :: MEASURE3:21

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂
for b₄ being non empty Subset-Family of b₁ st ( for b₅ being set holds
( b₅ in b₄ iff ex b₆ being set st
( b₆ in b₂ & ex b₇ being thin of b₃ st b₅ = b₆ \/ b₇ ) ) ) holds
b₄ is sigma_Field_Subset of b₁

proof end;

registration

let c₁ be set ;
let c₂ be sigma_Field_Subset of c₁;
let c₃ be sigma_Measure of c₂;
cluster COM a₂,a₃ -> non empty compl-closed sigma_Field_Subset-like ;
coherence

proof end;

end;

theorem Th22: :: MEASURE3:22

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂
for b₄, b₅ being set st b₄ in b₂ & b₅ in b₂ holds
for b₆, b₇ being thin of b₃ st b₄ \/ b₆ = b₅ \/ b₇ holds
b₃ . b₄ = b₃ . b₅

proof end;

definition

let c₁ be set ;
let c₂ be sigma_Field_Subset of c₁;
let c₃ be sigma_Measure of c₂;
func COM c₃ -> sigma_Measure of COM a₂,a₃ means :Def6: :: MEASURE3:def 6
for b₁ being set st b₁ in a₂ holds
for b₂ being thin of a₃ holds a₄ . (b₁ \/ b₂) = a₃ . b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines COM MEASURE3:def 6 :

theorem Th23: :: MEASURE3:23

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂ holds COM b₃ is_complete COM b₂,b₃

proof end;