:: Construction of Measure from Semialgebra of Sets
:: by Noboru Endou
::
:: Received August 14, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users

theorem Th52: :: MEASURE9:1

for K being Relation st rng K is empty-membered holds
union (rng K) = {}

proof end;

theorem :: MEASURE9:2

for K being Function holds
( rng K is empty-membered iff for x being object holds K . x = {} )

proof end;

definition

let D be set ;
let F be FinSequenceSet of D;
let f be FinSequence of F;
let n be Nat;
:: original: .
redefine func f . n -> FinSequence of D;
correctness
coherence
f . n is FinSequence of D;

proof end;

end;

definition

let D be set ;
let Y be FinSequenceSet of D;
let F be FinSequence of Y;

func Length F -> FinSequence of NAT means :Def1: :: MEASURE9:def 1
( dom it = dom F & ( for n being Nat st n in dom it holds
it . n = len (F . n) ) );

existence
ex b₁ being FinSequence of NAT st
( dom b₁ = dom F & ( for n being Nat st n in dom b₁ holds
b₁ . n = len (F . n) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of NAT st dom b₁ = dom F & ( for n being Nat st n in dom b₁ holds
b₁ . n = len (F . n) ) & dom b₂ = dom F & ( for n being Nat st n in dom b₂ holds
b₂ . n = len (F . n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Length MEASURE9:def 1 :
for D being set
for Y being FinSequenceSet of D
for F being FinSequence of Y
for b₄ being FinSequence of NAT holds
( b₄ = Length F iff ( dom b₄ = dom F & ( for n being Nat st n in dom b₄ holds
b₄ . n = len (F . n) ) ) );

theorem :: MEASURE9:3

for D being set
for Y being FinSequenceSet of D
for F being FinSequence of Y st ( for n being Nat st n in dom F holds
F . n = <*> D ) holds
Sum (Length F) = 0

proof end;

theorem Th2: :: MEASURE9:4

for D being set
for Y being FinSequenceSet of D
for F being FinSequence of Y
for k being Nat st k < len F holds
Length (F | (k + 1)) = (Length (F | k)) ^ <*(len (F . (k + 1)))*>

proof end;

theorem Th3: :: MEASURE9:5

for D being set
for Y being FinSequenceSet of D
for F being FinSequence of Y
for n being Nat st 1 <= n & n <= Sum (Length F) holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) )

proof end;

RFINSEQlm3: for n being Nat
for D being set
for f being FinSequence of D st len f <= n holds
f | n = f

proof end;

RFINSEQ6: for D being set
for f being FinSequence of D
for n, m being Nat st n in dom f & m in Seg n holds
( (f | n) . m = f . m & m in dom f )

proof end;

RFINSEQ8: for D being set
for f being FinSequence of D
for n being Nat holds (f | n) ^ (f /^ n) = f

proof end;

theorem Th4: :: MEASURE9:6

for D being set
for Y being FinSequenceSet of D
for F1, F2 being FinSequence of Y holds Length (F1 ^ F2) = (Length F1) ^ (Length F2)

proof end;

theorem Th5: :: MEASURE9:7

for D being set
for Y being FinSequenceSet of D
for F being FinSequence of Y
for k1, k2 being Nat st k1 <= k2 holds
Sum (Length (F | k1)) <= Sum (Length (F | k2))

proof end;

theorem Th6: :: MEASURE9:8

for D being set
for Y being FinSequenceSet of D
for F being FinSequence of Y
for m1, m2, k1, k2 being Nat st 1 <= m1 & 1 <= m2 & m1 + (Sum (Length (F | k1))) = m2 + (Sum (Length (F | k2))) & m1 + (Sum (Length (F | k1))) <= Sum (Length (F | (k1 + 1))) & m2 + (Sum (Length (F | k2))) <= Sum (Length (F | (k2 + 1))) holds
( m1 = m2 & k1 = k2 )

proof end;

definition

let D be non empty set ;
let Y be FinSequenceSet of D;
let F be FinSequence of Y;

func joined_FinSeq F -> FinSequence of D means :Def2: :: MEASURE9:def 2
( len it = Sum (Length F) & ( for n being Nat st n in dom it holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) & it . n = (F . (k + 1)) . m ) ) );

existence
ex b₁ being FinSequence of D st
( len b₁ = Sum (Length F) & ( for n being Nat st n in dom b₁ holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) & b₁ . n = (F . (k + 1)) . m ) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of D st len b₁ = Sum (Length F) & ( for n being Nat st n in dom b₁ holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) & b₁ . n = (F . (k + 1)) . m ) ) & len b₂ = Sum (Length F) & ( for n being Nat st n in dom b₂ holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) & b₂ . n = (F . (k + 1)) . m ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines joined_FinSeq MEASURE9:def 2 :
for D being non empty set
for Y being FinSequenceSet of D
for F being FinSequence of Y
for b₄ being FinSequence of D holds
( b₄ = joined_FinSeq F iff ( len b₄ = Sum (Length F) & ( for n being Nat st n in dom b₄ holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) & b₄ . n = (F . (k + 1)) . m ) ) ) );

definition

let D be set ;
let Y be FinSequenceSet of D;
let s be sequence of Y;

func Length s -> sequence of NAT means :Def3: :: MEASURE9:def 3
for n being Nat holds it . n = len (s . n);

existence
ex b₁ being sequence of NAT st
for n being Nat holds b₁ . n = len (s . n)

proof end;

uniqueness
for b₁, b₂ being sequence of NAT st ( for n being Nat holds b₁ . n = len (s . n) ) & ( for n being Nat holds b₂ . n = len (s . n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Length MEASURE9:def 3 :
for D being set
for Y being FinSequenceSet of D
for s being sequence of Y
for b₄ being sequence of NAT holds
( b₄ = Length s iff for n being Nat holds b₄ . n = len (s . n) );

definition

let s be sequence of NAT;
:: original: Partial_Sums
redefine func Partial_Sums s -> sequence of NAT;
correctness
coherence
Partial_Sums s is sequence of NAT;

proof end;

end;

registration

let D be non empty set ;

cluster non empty with_non-empty_element for FinSequenceSet of D;

existence
ex b₁ being FinSequenceSet of D st
( not b₁ is empty & b₁ is with_non-empty_element )

proof end;

end;

theorem Th7: :: MEASURE9:9

for D being non empty set
for Y being non empty with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y
for n being Nat holds
( len (s . n) >= 1 & n < (Partial_Sums (Length s)) . n & (Partial_Sums (Length s)) . n < (Partial_Sums (Length s)) . (n + 1) )

proof end;

theorem Th8: :: MEASURE9:10

for D being non empty set
for Y being non empty with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y
for n being Nat ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n )

proof end;

theorem Th9: :: MEASURE9:11

for D being non empty set
for Y being non empty with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y holds Partial_Sums (Length s) is increasing

proof end;

theorem Th10: :: MEASURE9:12

for D being non empty set
for Y being non empty with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y
for m1, m2, k1, k2 being Nat st m1 in dom (s . k1) & m2 in dom (s . k2) & (((Partial_Sums (Length s)) . k1) - (len (s . k1))) + m1 = (((Partial_Sums (Length s)) . k2) - (len (s . k2))) + m2 holds
( m1 = m2 & k1 = k2 )

proof end;

theorem Th11: :: MEASURE9:13

for D being non empty set
for Y being with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y ex N being increasing sequence of NAT st
for k being Nat holds N . k = ((Partial_Sums (Length s)) . k) - 1

proof end;

definition

let D be non empty set ;
let Y be with_non-empty_element FinSequenceSet of D;
let s be non-empty sequence of Y;

func joined_seq s -> sequence of D means :Def4: :: MEASURE9:def 4
for n being Nat ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & it . n = (s . k) . m );

existence
ex b₁ being sequence of D st
for n being Nat ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & b₁ . n = (s . k) . m )

proof end;

uniqueness
for b₁, b₂ being sequence of D st ( for n being Nat ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & b₁ . n = (s . k) . m ) ) & ( for n being Nat ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & b₂ . n = (s . k) . m ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines joined_seq MEASURE9:def 4 :
for D being non empty set
for Y being with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y
for b₄ being sequence of D holds
( b₄ = joined_seq s iff for n being Nat ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & b₄ . n = (s . k) . m ) );

theorem :: MEASURE9:14

for D being non empty set
for Y being with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y
for s1 being sequence of D st ( for n being Nat holds s1 . n = (joined_seq s) . (((Partial_Sums (Length s)) . n) - 1) ) holds
s1 is subsequence of joined_seq s

proof end;

theorem Th13: :: MEASURE9:15

for D being non empty set
for Y being with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y
for k, m being Nat st m in dom (s . k) holds
ex n being Nat st
( n = ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 & (joined_seq s) . n = (s . k) . m )

proof end;

theorem Th14: :: MEASURE9:16

for D being non empty set
for Y being FinSequenceSet of D
for F being FinSequence of Y st ( for n, m being Nat st n <> m holds
union (rng (F . n)) misses union (rng (F . m)) ) & ( for n being Nat holds F . n is disjoint_valued ) holds
joined_FinSeq F is disjoint_valued

proof end;

theorem Th15: :: MEASURE9:17

for D being non empty set
for Y being FinSequenceSet of D
for F being FinSequence of Y holds rng (joined_FinSeq F) = union { (rng (F . n)) where n is Nat : n in dom F }

proof end;

definition

let x be ext-real number ;
:: original: <*
redefine func <*x*> -> FinSequence of ExtREAL ;
coherence
<*x*> is FinSequence of ExtREAL

proof end;

end;

definition

let e be FinSequence of ExtREAL * ;

func Sum e -> FinSequence of ExtREAL means :Def5: :: MEASURE9:def 5
( len it = len e & ( for k being Nat st k in dom it holds
it . k = Sum (e . k) ) );

existence
ex b₁ being FinSequence of ExtREAL st
( len b₁ = len e & ( for k being Nat st k in dom b₁ holds
b₁ . k = Sum (e . k) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of ExtREAL st len b₁ = len e & ( for k being Nat st k in dom b₁ holds
b₁ . k = Sum (e . k) ) & len b₂ = len e & ( for k being Nat st k in dom b₂ holds
b₂ . k = Sum (e . k) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines Sum MEASURE9:def 5 :
for e being FinSequence of ExtREAL *
for b₂ being FinSequence of ExtREAL holds
( b₂ = Sum e iff ( len b₂ = len e & ( for k being Nat st k in dom b₂ holds
b₂ . k = Sum (e . k) ) ) );

definition

let M be Matrix of ExtREAL;

func SumAll M -> Element of ExtREAL equals :: MEASURE9:def 6
Sum (Sum M);

coherence
Sum (Sum M) is Element of ExtREAL ;

end;

:: deftheorem defines SumAll MEASURE9:def 6 :
for M being Matrix of ExtREAL holds SumAll M = Sum (Sum M);

theorem Th16: :: MEASURE9:18

for M being Matrix of ExtREAL holds
( len (Sum M) = len M & ( for i being Nat st i in Seg (len M) holds
(Sum M) . i = Sum (Line (M,i)) ) )

proof end;

theorem Th17: :: MEASURE9:19

for F being FinSequence of ExtREAL st ( for i being Nat st i in dom F holds
F . i <> -infty ) holds
Sum F <> -infty

proof end;

theorem Th18: :: MEASURE9:20

for F, G, H being FinSequence of ExtREAL st not -infty in rng F & not -infty in rng G & dom F = dom G & H = F + G holds
Sum H = (Sum F) + (Sum G)

proof end;

theorem Th19: :: MEASURE9:21

for r being R_eal
for F being FinSequence of ExtREAL holds Sum (F ^ <*r*>) = (Sum F) + r

proof end;

theorem Th20: :: MEASURE9:22

for r being R_eal
for i being Nat st r is real holds
Sum (i |-> r) = i * r

proof end;

theorem Th21: :: MEASURE9:23

for M being Matrix of ExtREAL st len M = 0 holds
SumAll M = 0

proof end;

theorem Th22: :: MEASURE9:24

for m being Nat
for M being Matrix of m, 0 ,ExtREAL holds SumAll M = 0

proof end;

theorem Th23: :: MEASURE9:25

for n, m, k being Nat
for M1 being Matrix of n,k,ExtREAL
for M2 being Matrix of m,k,ExtREAL holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)

proof end;

theorem Th24: :: MEASURE9:26

for M1, M2 being Matrix of ExtREAL st ( for i being Nat st i in dom M1 holds
not -infty in rng (M1 . i) ) & ( for i being Nat st i in dom M2 holds
not -infty in rng (M2 . i) ) holds
(Sum M1) + (Sum M2) = Sum (M1 ^^ M2)

proof end;

theorem Th25: :: MEASURE9:27

for M1, M2 being Matrix of ExtREAL st len M1 = len M2 & ( for i being Nat st i in dom M1 holds
not -infty in rng (M1 . i) ) & ( for i being Nat st i in dom M2 holds
not -infty in rng (M2 . i) ) holds
(SumAll M1) + (SumAll M2) = SumAll (M1 ^^ M2)

proof end;

theorem Th26: :: MEASURE9:28

for p being FinSequence of ExtREAL st not -infty in rng p holds
SumAll <*p*> = SumAll (<*p*> @)

proof end;

theorem Th27: :: MEASURE9:29

for p being ext-real number
for M being Matrix of ExtREAL st ( for i being Nat st i in dom M holds
not p in rng (M . i) ) holds
for j being Nat st j in dom (M @) holds
not p in rng ((M @) . j)

proof end;

theorem Th28: :: MEASURE9:30

for M being Matrix of ExtREAL st ( for i being Nat st i in dom M holds
not -infty in rng (M . i) ) holds
SumAll M = SumAll (M @)

proof end;

registration

let x be object ;

cluster <*x*> -> disjoint_valued ;

correctness
coherence
<*x*> is disjoint_valued ;

proof end;

end;

theorem :: MEASURE9:31

for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for F being FinSequence of S
for G being Element of S ex H being disjoint_valued FinSequence of S st G \ (Union F) = Union H

proof end;

registration

let X be set ;
let P be with_empty_element cap-closed semi-diff-closed Subset-Family of X;

cluster Relation-like omega -defined P -valued non empty Function-like total V31( omega ,P) disjoint_valued for Element of bool [:omega,P:];

existence
ex b₁ being sequence of P st b₁ is disjoint_valued

proof end;

end;

LM: for X being set
for P being non empty Subset-Family of X holds
( P --> 0. is V224() & P --> 0. is additive & P --> 0. is zeroed )

proof end;

registration

let X be set ;
let P be non empty Subset-Family of X;

cluster Relation-like P -defined ExtREAL -valued non empty Function-like total V31(P, ExtREAL ) ext-real-valued zeroed V224() additive for Element of bool [:P,ExtREAL:];

existence
ex b₁ being Function of P,ExtREAL st
( b₁ is V224() & b₁ is additive & b₁ is zeroed )

proof end;

end;

registration

let X be set ;
let P be with_empty_element Subset-Family of X;

cluster Relation-like NAT -defined P -valued non empty Function-like total V31( NAT ,P) disjoint_valued for Element of bool [:NAT,P:];

existence
ex b₁ being Function of NAT,P st b₁ is disjoint_valued

proof end;

end;

definition

let X be set ;
let P be with_empty_element Subset-Family of X;

mode pre-Measure of P -> zeroed V224() Function of P,ExtREAL means :Def8: :: MEASURE9:def 7
( ( for F being disjoint_valued FinSequence of P st Union F in P holds
it . (Union F) = Sum (it * F) ) & ( for K being disjoint_valued Function of NAT,P st Union K in P holds
it . (Union K) <= SUM (it * K) ) );

existence
ex b₁ being zeroed V224() Function of P,ExtREAL st
( ( for F being disjoint_valued FinSequence of P st Union F in P holds
b₁ . (Union F) = Sum (b₁ * F) ) & ( for K being disjoint_valued Function of NAT,P st Union K in P holds
b₁ . (Union K) <= SUM (b₁ * K) ) )

proof end;

end;

:: deftheorem Def8 defines pre-Measure MEASURE9:def 7 :
for X being set
for P being with_empty_element Subset-Family of X
for b₃ being zeroed V224() Function of P,ExtREAL holds
( b₃ is pre-Measure of P iff ( ( for F being disjoint_valued FinSequence of P st Union F in P holds
b₃ . (Union F) = Sum (b₃ * F) ) & ( for K being disjoint_valued Function of NAT,P st Union K in P holds
b₃ . (Union K) <= SUM (b₃ * K) ) ) );

theorem :: MEASURE9:32

for X being with_empty_element set
for F being FinSequence of X ex G being Function of NAT,X st
( ( for i being Nat holds F . i = G . i ) & Union F = Union G )

proof end;

theorem :: MEASURE9:33

for X being non empty set
for F being FinSequence of X
for G being Function of NAT,X st ( for i being Nat holds F . i = G . i ) holds
( F is disjoint_valued iff G is disjoint_valued )

proof end;

theorem :: MEASURE9:34

for F being FinSequence of ExtREAL
for G being ExtREAL_sequence st ( for i being Nat holds F . i = G . i ) holds
( F is nonnegative iff G is V224() )

proof end;

LL1: ( <*+infty*> is nonnegative & <*+infty*> is V251() )

proof end;

LL2: ( <*-infty*> is nonpositive & <*-infty*> is V252() )

proof end;

registration

cluster Relation-like omega -defined ExtREAL -valued Function-like V34() FinSequence-like FinSubsequence-like ext-real-valued nonnegative for FinSequence of ExtREAL ;

existence
ex b₁ being FinSequence of ExtREAL st b₁ is nonnegative by LL1;

cluster Relation-like omega -defined ExtREAL -valued Function-like V34() FinSequence-like FinSubsequence-like ext-real-valued V251() for FinSequence of ExtREAL ;

existence
not for b₁ being FinSequence of ExtREAL holds b₁ is V251() by LL1;

cluster Relation-like omega -defined ExtREAL -valued Function-like V34() FinSequence-like FinSubsequence-like ext-real-valued nonpositive for FinSequence of ExtREAL ;

existence
ex b₁ being FinSequence of ExtREAL st b₁ is nonpositive by LL2;

cluster Relation-like omega -defined ExtREAL -valued Function-like V34() FinSequence-like FinSubsequence-like ext-real-valued V252() for FinSequence of ExtREAL ;

existence
not for b₁ being FinSequence of ExtREAL holds b₁ is V252() by LL2;

cluster nonnegative -> V251() for FinSequence of ExtREAL ;

correctness
coherence
for b₁ being FinSequence of ExtREAL st b₁ is nonnegative holds
b₁ is V251();
;

cluster nonpositive -> V252() for FinSequence of ExtREAL ;

correctness
coherence
for b₁ being FinSequence of ExtREAL st b₁ is nonpositive holds
b₁ is V252();
;

end;

registration

let X, Y be non empty set ;
let F be V251() Function of Y,ExtREAL;
let G be Function of X,Y;

cluster G * F -> V251() for Function of X,ExtREAL;

correctness
coherence
for b₁ being Function of X,ExtREAL st b₁ = F * G holds
b₁ is without-infty ;

proof end;

end;

registration

let X, Y be non empty set ;
let F be V224() Function of Y,ExtREAL;
let G be Function of X,Y;

cluster G * F -> V224() for Function of X,ExtREAL;

correctness
coherence
for b₁ being Function of X,ExtREAL st b₁ = F * G holds
b₁ is nonnegative ;
by MEASURE1:25;

end;

theorem Th33: :: MEASURE9:35

for a being R_eal holds Sum <*a*> = a

proof end;

theorem Th34: :: MEASURE9:36

for F being FinSequence of ExtREAL
for k being Nat holds
( ( F is V251() implies F | k is V251() ) & ( F is V252() implies F | k is V252() ) )

proof end;

theorem Th35: :: MEASURE9:37

for F being V251() FinSequence of ExtREAL
for G being ExtREAL_sequence st ( for i being Nat holds F . i = G . i ) holds
for i being Nat holds Sum (F | i) = (Partial_Sums G) . i

proof end;

theorem :: MEASURE9:38

for F being V251() FinSequence of ExtREAL
for G being ExtREAL_sequence st ( for i being Nat holds F . i = G . i ) holds
( G is summable & Sum F = Sum G )

proof end;

theorem :: MEASURE9:39

for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for F being disjoint_valued FinSequence of S
for R being non empty preBoolean Subset-Family of X st S c= R & Union F in R holds
for i being Nat holds Union (F | i) in R

proof end;

theorem :: MEASURE9:40

for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for P being pre-Measure of S
for F1, F2 being disjoint_valued FinSequence of S st Union F1 in S & Union F1 = Union F2 holds
P . (Union F1) = P . (Union F2) ;

theorem FStoMAT1: :: MEASURE9:41

for S being non empty cap-closed set
for F1, F2 being FinSequence of S ex Mx being Matrix of len F1, len F2,S st
for i, j being Nat st [i,j] in Indices Mx holds
Mx * (i,j) = (F1 . i) /\ (F2 . j)

proof end;

theorem Th40: :: MEASURE9:42

for X being set
for S being with_empty_element cap-closed Subset-Family of X
for F1, F2 being non empty disjoint_valued FinSequence of S
for P being zeroed V224() Function of S,ExtREAL
for Mx being Matrix of len F1, len F2,ExtREAL st Union F1 = Union F2 & ( for i, j being Nat st [i,j] in Indices Mx holds
Mx * (i,j) = P . ((F1 . i) /\ (F2 . j)) ) & ( for F being disjoint_valued FinSequence of S st Union F in S holds
P . (Union F) = Sum (P * F) ) holds
( ( for i being Nat st i <= len (P * F1) holds
(P * F1) . i = (Sum Mx) . i ) & Sum (P * F1) = SumAll Mx )

proof end;

theorem Th41: :: MEASURE9:43

for X being set
for S being with_empty_element cap-closed Subset-Family of X
for F1, F2 being non empty disjoint_valued FinSequence of S
for P being zeroed V224() Function of S,ExtREAL
for Mx being Matrix of len F1, len F2,ExtREAL st Union F1 = Union F2 & ( for i, j being Nat st [i,j] in Indices Mx holds
Mx * (i,j) = P . ((F1 . i) /\ (F2 . j)) ) & ( for F being disjoint_valued FinSequence of S st Union F in S holds
P . (Union F) = Sum (P * F) ) holds
( ( for i being Nat st i <= len (P * F2) holds
(P * F2) . i = (Sum (Mx @)) . i ) & Sum (P * F2) = SumAll (Mx @) )

proof end;

theorem Th42: :: MEASURE9:44

for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for P being pre-Measure of S
for A being set st A in Ring_generated_by S holds
for F1, F2 being disjoint_valued FinSequence of S st A = Union F1 & A = Union F2 holds
Sum (P * F1) = Sum (P * F2)

proof end;

theorem Th43: :: MEASURE9:45

for f1, f2 being FinSequence st f1 is disjoint_valued & f2 is disjoint_valued & union (rng f1) misses union (rng f2) holds
f1 ^ f2 is disjoint_valued

proof end;

theorem :: MEASURE9:46

for X being set
for P being with_empty_element semi-diff-closed Subset-Family of X
for M being pre-Measure of P
for A, B being set st A in P & B in P & A \ B in P & B c= A holds
M . A >= M . B

proof end;

theorem Th45: :: MEASURE9:47

for Y, S being non empty set
for F being PartFunc of Y,S
for M being Function of S,ExtREAL st M is V224() holds
M * F is nonnegative

proof end;

theorem Th46: :: MEASURE9:48

for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for P being pre-Measure of S ex M being zeroed V224() additive Function of (Ring_generated_by S),ExtREAL st
for A being set st A in Ring_generated_by S holds
for F being disjoint_valued FinSequence of S st A = Union F holds
M . A = Sum (P * F)

proof end;

theorem :: MEASURE9:49

for X, Y being set
for F, G being Function of NAT,(bool X) st ( for i being Nat holds G . i = (F . i) /\ Y ) & Union F = Y holds
Union G = Union F

proof end;

theorem :: MEASURE9:50

for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for P being pre-Measure of S ex M being Function of (Ring_generated_by S),ExtREAL st
( M . {} = 0 & ( for K being disjoint_valued FinSequence of S st Union K in Ring_generated_by S holds
M . (Union K) = Sum (P * K) ) )

proof end;

theorem :: MEASURE9:51

for X, Z being set
for P being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for K being disjoint_valued Function of NAT,(Ring_generated_by P) st Z = { [n,F] where n is Nat, F is disjoint_valued FinSequence of P : ( Union F = K . n & ( K . n = {} implies F = <*{}*> ) ) } holds
( proj2 Z is FinSequenceSet of P & ( for x being object holds
( x in rng K iff ex F being FinSequence of P st
( F in proj2 Z & Union F = x ) ) ) & proj2 Z is with_non-empty_elements )

proof end;

theorem :: MEASURE9:52

for X being set
for P being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for K being disjoint_valued Function of NAT,(Ring_generated_by P) st rng K is with_non-empty_element holds
ex Y being non empty FinSequenceSet of P st
( Y = { F where F is disjoint_valued FinSequence of P : ( Union F in rng K & F <> {} ) } & Y is with_non-empty_elements )

proof end;

theorem Th51: :: MEASURE9:53

for X, Z being set
for P being semialgebra_of_sets of X
for K being disjoint_valued Function of NAT,(Field_generated_by P) st Z = { [n,F] where n is Nat, F is disjoint_valued FinSequence of P : ( Union F = K . n & ( K . n = {} implies F = <*{}*> ) ) } holds
( proj2 Z is FinSequenceSet of P & ( for x being object holds
( x in rng K iff ex F being FinSequence of P st
( F in proj2 Z & Union F = x ) ) ) & proj2 Z is with_non-empty_elements )

proof end;

theorem Th54: :: MEASURE9:54

for X being set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for A being set
for F1, F2 being disjoint_valued FinSequence of S st A = Union F1 & A = Union F2 holds
Sum (P * F1) = Sum (P * F2)

proof end;

theorem Th55: :: MEASURE9:55

for X being set
for S being semialgebra_of_sets of X
for P being pre-Measure of S ex M being Measure of (Field_generated_by S) st
for A being set st A in Field_generated_by S holds
for F being disjoint_valued FinSequence of S st A = Union F holds
M . A = Sum (P * F)

proof end;

theorem :: MEASURE9:56

for F being ExtREAL_sequence
for n being Nat
for a being R_eal st ( for k being Nat holds F . k = a ) holds
(Partial_Sums F) . n = a * (n + 1)

proof end;

theorem Th57: :: MEASURE9:57

for X being non empty set
for F being sequence of X
for n being Nat holds rng (F | (Segm (n + 1))) = (rng (F | (Segm n))) \/ {(F . n)}

proof end;

theorem Th58: :: MEASURE9:58

for X being set
for S being Field_Subset of X
for M being Measure of S
for F being Sep_Sequence of S
for n being Nat holds
( union (rng (F | (Segm (n + 1)))) in S & (Partial_Sums (M * F)) . n = M . (union (rng (F | (Segm (n + 1))))) )

proof end;

theorem Th59: :: MEASURE9:59

for X being set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for M being Measure of (Field_generated_by S) st ( for A being set st A in Field_generated_by S holds
for F being disjoint_valued FinSequence of S st A = Union F holds
M . A = Sum (P * F) ) holds
M is completely-additive

proof end;

definition

let X be set ;
let S be semialgebra_of_sets of X;
let P be pre-Measure of S;

mode induced_Measure of S,P -> Measure of (Field_generated_by S) means :Def9: :: MEASURE9:def 8
for A being set st A in Field_generated_by S holds
for F being disjoint_valued FinSequence of S st A = Union F holds
it . A = Sum (P * F);

existence
ex b₁ being Measure of (Field_generated_by S) st
for A being set st A in Field_generated_by S holds
for F being disjoint_valued FinSequence of S st A = Union F holds
b₁ . A = Sum (P * F) by Th55;

end;

:: deftheorem Def9 defines induced_Measure MEASURE9:def 8 :
for X being set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for b₄ being Measure of (Field_generated_by S) holds
( b₄ is induced_Measure of S,P iff for A being set st A in Field_generated_by S holds
for F being disjoint_valued FinSequence of S st A = Union F holds
b₄ . A = Sum (P * F) );

theorem Th60: :: MEASURE9:60

for X being set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for M being induced_Measure of S,P holds M is completely-additive

proof end;

theorem Th61: :: MEASURE9:61

for X being non empty set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for M being induced_Measure of S,P holds (sigma_Meas (C_Meas M)) | (sigma (Field_generated_by S)) is sigma_Measure of (sigma (Field_generated_by S))

proof end;

definition

let X be non empty set ;
let S be semialgebra_of_sets of X;
let P be pre-Measure of S;
let M be induced_Measure of S,P;

mode induced_sigma_Measure of S,M -> sigma_Measure of (sigma (Field_generated_by S)) means :Def10: :: MEASURE9:def 9
it = (sigma_Meas (C_Meas M)) | (sigma (Field_generated_by S));

existence
ex b₁ being sigma_Measure of (sigma (Field_generated_by S)) st b₁ = (sigma_Meas (C_Meas M)) | (sigma (Field_generated_by S))

proof end;

end;

:: deftheorem Def10 defines induced_sigma_Measure MEASURE9:def 9 :
for X being non empty set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for M being induced_Measure of S,P
for b₅ being sigma_Measure of (sigma (Field_generated_by S)) holds
( b₅ is induced_sigma_Measure of S,M iff b₅ = (sigma_Meas (C_Meas M)) | (sigma (Field_generated_by S)) );

theorem :: MEASURE9:62

for X being non empty set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for m being induced_Measure of S,P
for M being induced_sigma_Measure of S,m holds M is_extension_of m

proof end;