:: PROB_4 semantic presentation

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

proof end;

definition

let c₁ be set ;
let c₂ be SigmaField of c₁;
let c₃ be SetSequence of c₂;
let c₄ be Nat;
redefine func . as c₃ . c₄ -> Element of a₂;
coherence by PROB_1:def 9;

end;

theorem Th1: :: PROB_4:1

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ holds rng b₃ c= b₂

proof end;

theorem Th2: :: PROB_4:2

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being Function holds
( b₃ is SetSequence of b₂ iff b₃ is Function of NAT ,b₂ )

proof end;

scheme :: PROB_4:sch 1
s1{ F₁() -> set , F₂() -> SigmaField of F₁(), F₃( set ) -> Element of F₂() } :

ex b₁ being SetSequence of F₂() st
for b₂ being Nat holds b₁ . b₂ = F₃(b₂)

proof end;

registration

let c₁ be set ;
cluster disjoint_valued Relation of NAT , bool a₁;
existence

proof end;

end;

registration

let c₁ be set ;
let c₂ be SigmaField of c₁;
cluster disjoint_valued SetSequence of a₂;
existence

proof end;

end;

theorem Th3: :: PROB_4:3

for b₁ being set
for b₂, b₃ being Subset of b₁ ex b₄ being SetSequence of b₁ st
( b₄ . 0 = b₂ & b₄ . 1 = b₃ & ( for b₅ being Nat st b₅ > 1 holds
b₄ . b₅ = {} ) )

proof end;

theorem Th4: :: PROB_4:4

for b₁ being set
for b₂ being SetSequence of b₁
for b₃, b₄ being Subset of b₁ st b₃ misses b₄ & b₂ . 0 = b₃ & b₂ . 1 = b₄ & ( for b₅ being Nat st b₅ > 1 holds
b₂ . b₅ = {} ) holds
( b₂ is disjoint_valued & Union b₂ = b₃ \/ b₄ )

proof end;

theorem Th5: :: PROB_4:5

for b₁ being set
for b₂ being non empty set holds
( b₂ is SigmaField of b₁ iff ( b₂ c= bool b₁ & ( for b₃ being SetSequence of b₁ st ( for b₄ being Nat holds b₃ . b₄ in b₂ ) holds
Union b₃ in b₂ ) & ( for b₃ being Subset of b₁ st b₃ in b₂ holds
b₃ ` in b₂ ) ) )

proof end;

theorem Th6: :: PROB_4:6

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂
for b₄, b₅ being Event of b₂ holds b₃ . (b₄ \ b₅) = (b₃ . (b₄ \/ b₅)) - (b₃ . b₅)

proof end;

theorem Th7: :: PROB_4:7

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂
for b₄, b₅ being Event of b₂ st b₄ c= b₅ & b₃ . b₅ = 0 holds
b₃ . b₄ = 0

proof end;

theorem Th8: :: PROB_4:8

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂
for b₄ being Probability of b₂ holds
( ( for b₅ being Nat holds b₄ . (b₃ . b₅) = 0 ) iff b₄ . (Union b₃) = 0 )

proof end;

theorem Th9: :: PROB_4:9

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂
for b₄ being Probability of b₂ holds
( ( for b₅ being set st b₅ in rng b₃ holds
b₄ . b₅ = 0 ) iff b₄ . (union (rng b₃)) = 0 )

proof end;

definition

let c₁ be set ;
let c₂ be SigmaField of c₁;
func SF2SFS c₂ -> sigma_Field_Subset of a₁ equals :: PROB_4:def 1
a₂;
coherence by TOPGEN_4:62;

end;

:: deftheorem Def1 defines SF2SFS PROB_4:def 1 :

definition

let c₁ be set ;
let c₂ be sigma_Field_Subset of c₁;
func SFS2SF c₂ -> SigmaField of a₁ equals :: PROB_4:def 2
a₂;
coherence by TOPGEN_4:62;

end;

:: deftheorem Def2 defines SFS2SF PROB_4:def 2 :

theorem Th10: :: PROB_4:10

for b₁ being Function of NAT , REAL
for b₂ being Function of NAT , ExtREAL st b₁ = b₂ holds
Partial_Sums b₁ = Ser b₂

proof end;

theorem Th11: :: PROB_4:11

for b₁ being Function of NAT , REAL
for b₂ being Function of NAT , ExtREAL st b₁ = b₂ & b₁ is bounded_above holds
sup b₁ = sup (rng b₂)

proof end;

theorem Th12: :: PROB_4:12

for b₁ being Function of NAT , REAL
for b₂ being Function of NAT , ExtREAL st b₁ = b₂ & b₁ is bounded_below holds
inf b₁ = inf (rng b₂)

proof end;

theorem Th13: :: PROB_4:13

for b₁ being Function of NAT , REAL
for b₂ being Function of NAT , ExtREAL st b₁ = b₂ & b₁ is nonnegative & b₁ is summable holds
Sum b₁ = SUM b₂

proof end;

theorem Th14: :: PROB_4:14

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂ holds b₃ is sigma_Measure of SF2SFS b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be SigmaField of c₁;
let c₃ be Probability of c₂;
func P2M c₃ -> sigma_Measure of SF2SFS a₂ equals :: PROB_4:def 3
a₃;
coherence by Th14;

end;

:: deftheorem Def3 defines P2M PROB_4:def 3 :

theorem Th15: :: PROB_4:15

for b₁ being non empty set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂ st b₃ . b₁ = R_EAL 1 holds
b₃ is Probability of SFS2SF b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be sigma_Field_Subset of c₁;
let c₃ be sigma_Measure of c₂;
assume E17: c₃ . c₁ = R_EAL 1 ;
func M2P c₃ -> Probability of SFS2SF a₂ equals :: PROB_4:def 4
a₃;
coherence by E17, Th15;

end;

:: deftheorem Def4 defines M2P PROB_4:def 4 :

Lemma17: for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is non-decreasing holds
for b₃ being Nat holds (Partial_Union b₂) . b₃ = b₂ . b₃

proof end;

theorem Th16: :: PROB_4:16

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is non-decreasing holds
Partial_Union b₂ = b₂

proof end;

theorem Th17: :: PROB_4:17

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is non-decreasing holds
( (Partial_Diff_Union b₂) . 0 = b₂ . 0 & ( for b₃ being Nat holds (Partial_Diff_Union b₂) . (b₃ + 1) = (b₂ . (b₃ + 1)) \ (b₂ . b₃) ) )

proof end;

theorem Th18: :: PROB_4:18

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is non-decreasing holds
for b₃ being Nat holds b₂ . (b₃ + 1) = ((Partial_Diff_Union b₂) . (b₃ + 1)) \/ (b₂ . b₃)

proof end;

theorem Th19: :: PROB_4:19

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is non-decreasing holds
for b₃ being Nat holds (Partial_Diff_Union b₂) . (b₃ + 1) misses b₂ . b₃

proof end;

theorem Th20: :: PROB_4:20

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ st b₃ is non-decreasing holds
@Partial_Union b₃ = b₃

proof end;

theorem Th21: :: PROB_4:21

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ st b₃ is non-decreasing holds
( (@Partial_Diff_Union b₃) . 0 = b₃ . 0 & ( for b₄ being Nat holds (@Partial_Diff_Union b₃) . (b₄ + 1) = (b₃ . (b₄ + 1)) \ (b₃ . b₄) ) )

proof end;

theorem Th22: :: PROB_4:22

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ st b₃ is non-decreasing holds
for b₄ being Nat holds (@Partial_Diff_Union b₃) . (b₄ + 1) misses b₃ . b₄

proof end;

definition

let c₁ be non empty set ;
let c₂ be SigmaField of c₁;
let c₃ be Probability of c₂;
pred c₃ is_complete c₂ means :Def5: :: PROB_4:def 5
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 Def5 defines is_complete PROB_4:def 5 :

theorem Th23: :: PROB_4:23

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂ holds
( b₃ is_complete b₂ iff P2M b₃ is_complete SF2SFS b₂ )

proof end;

definition

let c₁ be non empty set ;
let c₂ be SigmaField of c₁;
let c₃ be Probability of c₂;
mode thin of c₃ -> Subset of a₁ means :Def6: :: PROB_4:def 6
ex b₁ being set st
( b₁ in a₂ & a₄ c= b₁ & a₃ . b₁ = 0 );
existence

proof end;

end;

:: deftheorem Def6 defines thin PROB_4:def 6 :

theorem Th24: :: PROB_4:24

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂
for b₄ being Subset of b₁ holds
( b₄ is thin of b₃ iff b₄ is thin of P2M b₃ )

proof end;

theorem Th25: :: PROB_4:25

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂ holds {} is thin of b₃

proof end;

theorem Th26: :: PROB_4:26

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability 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 non empty set ;
let c₂ be SigmaField of c₁;
let c₃ be Probability of c₂;
func COM c₂,c₃ -> non empty Subset-Family of a₁ means :Def7: :: PROB_4:def 7
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 Def7 defines COM PROB_4:def 7 :

theorem Th27: :: PROB_4:27

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂
for b₄ being thin of b₃ holds b₄ in COM b₂,b₃

proof end;

theorem Th28: :: PROB_4:28

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂ holds COM b₂,b₃ = COM (SF2SFS b₂),(P2M b₃)

proof end;

definition

let c₁ be non empty set ;
let c₂ be SigmaField of c₁;
let c₃ be Probability of c₂;
let c₄ be Element of COM c₂,c₃;
func P_COM2M_COM c₄ -> Element of COM (SF2SFS a₂),(P2M a₃) equals :: PROB_4:def 8
a₄;
correctness by Th28;

end;

:: deftheorem Def8 defines P_COM2M_COM PROB_4:def 8 :

theorem Th29: :: PROB_4:29

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂ holds b₂ c= COM b₂,b₃

proof end;

definition

let c₁ be non empty set ;
let c₂ be SigmaField of c₁;
let c₃ be Probability of c₂;
let c₄ be Element of COM c₂,c₃;
func ProbPart c₄ -> non empty Subset-Family of a₁ means :Def9: :: PROB_4:def 9
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 Def9 defines ProbPart PROB_4:def 9 :

theorem Th30: :: PROB_4:30

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂
for b₄ being Element of COM b₂,b₃ holds ProbPart b₄ = MeasPart (P_COM2M_COM b₄)

proof end;

theorem Th31: :: PROB_4:31

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂
for b₄ being Element of COM b₂,b₃
for b₅, b₆ being set st b₅ in ProbPart b₄ & b₆ in ProbPart b₄ holds
b₃ . b₅ = b₃ . b₆

proof end;

theorem Th32: :: PROB_4:32

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂
for b₄ being Function of NAT , COM b₂,b₃ ex b₅ being SetSequence of b₂ st
for b₆ being Nat holds b₅ . b₆ in ProbPart (b₄ . b₆)

proof end;

theorem Th33: :: PROB_4:33

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂
for b₄ being Function of NAT , COM b₂,b₃
for b₅ being SetSequence of b₂ ex b₆ being SetSequence of b₁ st
for b₇ being Nat holds b₆ . b₇ = (b₄ . b₇) \ (b₅ . b₇)

proof end;

theorem Th34: :: PROB_4:34

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂
for b₄ being SetSequence of b₁ st ( for b₅ being Nat holds b₄ . b₅ is thin of b₃ ) holds
ex b₅ being SetSequence of b₂ st
for b₆ being Nat holds
( b₄ . b₆ c= b₅ . b₆ & b₃ . (b₅ . b₆) = 0 )

proof end;

theorem Th35: :: PROB_4:35

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability 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 SigmaField of b₁

proof end;

definition

let c₁ be non empty set ;
let c₂ be SigmaField of c₁;
let c₃ be Probability of c₂;
redefine func COM as COM c₂,c₃ -> SigmaField of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be SigmaField of c₁;
let c₃ be Probability of c₂;
redefine mode thin as thin of c₃ -> Event of COM a₂,a₃;
coherence

proof end;

end;

theorem Th36: :: PROB_4:36

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂
for b₄ being set holds
( b₄ in COM b₂,b₃ iff ex b₅, b₆ being set st
( b₅ in b₂ & b₆ in b₂ & b₅ c= b₄ & b₄ c= b₆ & b₃ . (b₆ \ b₅) = 0 ) )

proof end;

theorem Th37: :: PROB_4:37

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂
for b₄ being non empty Subset-Family of b₁ st ( for b₅ being set holds
( b₅ in b₄ iff ex b₆, b₇ being set st
( b₆ in b₂ & b₇ in b₂ & b₆ c= b₅ & b₅ c= b₇ & b₃ . (b₇ \ b₆) = 0 ) ) ) holds
b₄ = COM b₂,b₃

proof end;

definition

let c₁ be non empty set ;
let c₂ be SigmaField of c₁;
let c₃ be Probability of c₂;
func COM c₃ -> Probability of COM a₂,a₃ means :Def10: :: PROB_4:def 10
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 Def10 defines COM PROB_4:def 10 :

theorem Th38: :: PROB_4:38

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂ holds COM b₃ = COM (P2M b₃)

proof end;

theorem Th39: :: PROB_4:39

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂ holds COM b₃ is_complete COM b₂,b₃

proof end;

theorem Th40: :: PROB_4:40

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂
for b₄ being Event of b₂ holds b₃ . b₄ = (COM b₃) . b₄

proof end;

theorem Th41: :: PROB_4:41

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂
for b₄ being thin of b₃ holds (COM b₃) . b₄ = 0

proof end;

theorem Th42: :: PROB_4:42

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂
for b₄ being Element of COM b₂,b₃
for b₅ being set st b₅ in ProbPart b₄ holds
b₃ . b₅ = (COM b₃) . b₄

proof end;