:: The Hopf Extension Theorem of Measure
:: by Noboru Endou , Hiroyuki Okazaki and Yasunari Shidama
::
:: Copyright (c) 2009-2021 Association of Mizar Users

theorem Th1: :: MEASURE8:1
for seq being ExtREAL_sequence holds Ser seq = Partial_Sums seq
proof end;

:: In the theorem below, the notion "summable" means in MESFUNC9, not in SUPINF_2
theorem Th2: :: MEASURE8:2
for seq being ExtREAL_sequence st seq is nonnegative holds
( seq is summable & SUM seq = Sum seq )
proof end;

theorem Th3: :: MEASURE8:3
for seq, seq1, seq2 being ExtREAL_sequence st seq1 is nonnegative & seq2 is nonnegative & ( for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) ) holds
( seq is nonnegative & SUM seq = (SUM seq1) + (SUM seq2) & Sum seq = (Sum seq1) + (Sum seq2) )
proof end;

registration
let X be set ;
let F be Field_Subset of X;
existence
ex b1 being sequence of F st b1 is disjoint_valued
proof end;
end;

definition
let X be set ;
let F be Field_Subset of X;
mode FinSequence of F -> FinSequence of bool X means :Def1: :: MEASURE8:def 1
for k being Nat st k in dom it holds
it . k in F;
existence
ex b1 being FinSequence of bool X st
for k being Nat st k in dom b1 holds
b1 . k in F
proof end;
end;

:: deftheorem Def1 defines FinSequence MEASURE8:def 1 :
for X being set
for F being Field_Subset of X
for b3 being FinSequence of bool X holds
( b3 is FinSequence of F iff for k being Nat st k in dom b3 holds
b3 . k in F );

registration
let X be set ;
let F be Field_Subset of X;
existence
ex b1 being FinSequence of F st b1 is disjoint_valued
proof end;
end;

definition
let X be set ;
let F be Field_Subset of X;
mode Sep_FinSequence of F is disjoint_valued FinSequence of F;
end;

definition
let X be set ;
let F be Field_Subset of X;
mode Sep_Sequence of F is disjoint_valued sequence of F;
end;

definition
let X be set ;
let F be Field_Subset of X;
mode Set_Sequence of F -> SetSequence of X means :Def2: :: MEASURE8:def 2
for n being Nat holds it . n in F;
existence
ex b1 being SetSequence of X st
for n being Nat holds b1 . n in F
proof end;
end;

:: deftheorem Def2 defines Set_Sequence MEASURE8:def 2 :
for X being set
for F being Field_Subset of X
for b3 being SetSequence of X holds
( b3 is Set_Sequence of F iff for n being Nat holds b3 . n in F );

definition
let X be set ;
let A be Subset of X;
let F be Field_Subset of X;
mode Covering of A,F -> Set_Sequence of F means :Def3: :: MEASURE8:def 3
A c= union (rng it);
existence
ex b1 being Set_Sequence of F st A c= union (rng b1)
proof end;
end;

:: deftheorem Def3 defines Covering MEASURE8:def 3 :
for X being set
for A being Subset of X
for F being Field_Subset of X
for b4 being Set_Sequence of F holds
( b4 is Covering of A,F iff A c= union (rng b4) );

definition
let X be set ;
let F be Field_Subset of X;
let FSets be Set_Sequence of F;
let n be Nat;
:: original: .
redefine func FSets . n -> Element of F;
correctness
coherence
FSets . n is Element of F
;
by Def2;
end;

Lm1: for X being set
for F being Field_Subset of X holds NAT --> X is Set_Sequence of F

proof end;

definition
let X be set ;
let F be Field_Subset of X;
let Sets be SetSequence of X;
mode Covering of Sets,F -> sequence of (Funcs (NAT,(bool X))) means :Def4: :: MEASURE8:def 4
for n being Nat holds it . n is Covering of Sets . n,F;
existence
ex b1 being sequence of (Funcs (NAT,(bool X))) st
for n being Nat holds b1 . n is Covering of Sets . n,F
proof end;
end;

:: deftheorem Def4 defines Covering MEASURE8:def 4 :
for X being set
for F being Field_Subset of X
for Sets being SetSequence of X
for b4 being sequence of (Funcs (NAT,(bool X))) holds
( b4 is Covering of Sets,F iff for n being Nat holds b4 . n is Covering of Sets . n,F );

definition
let X be set ;
let F be Field_Subset of X;
let M be Measure of F;
let FSets be Set_Sequence of F;
func vol (M,FSets) -> ExtREAL_sequence means :Def5: :: MEASURE8:def 5
for n being Nat holds it . n = M . (FSets . n);
existence
ex b1 being ExtREAL_sequence st
for n being Nat holds b1 . n = M . (FSets . n)
proof end;
uniqueness
for b1, b2 being ExtREAL_sequence st ( for n being Nat holds b1 . n = M . (FSets . n) ) & ( for n being Nat holds b2 . n = M . (FSets . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines vol MEASURE8:def 5 :
for X being set
for F being Field_Subset of X
for M being Measure of F
for FSets being Set_Sequence of F
for b5 being ExtREAL_sequence holds
( b5 = vol (M,FSets) iff for n being Nat holds b5 . n = M . (FSets . n) );

theorem Th4: :: MEASURE8:4
for X being set
for F being Field_Subset of X
for M being Measure of F
for FSets being Set_Sequence of F holds vol (M,FSets) is nonnegative
proof end;

definition
let X be set ;
let F be Field_Subset of X;
let Sets be SetSequence of X;
let Cvr be Covering of Sets,F;
let n be Nat;
:: original: .
redefine func Cvr . n -> Covering of Sets . n,F;
correctness
coherence
Cvr . n is Covering of Sets . n,F
;
by Def4;
end;

definition
let X be set ;
let F be Field_Subset of X;
let Sets be SetSequence of X;
let M be Measure of F;
let Cvr be Covering of Sets,F;
func Volume (M,Cvr) -> ExtREAL_sequence means :Def6: :: MEASURE8:def 6
for n being Nat holds it . n = SUM (vol (M,(Cvr . n)));
existence
ex b1 being ExtREAL_sequence st
for n being Nat holds b1 . n = SUM (vol (M,(Cvr . n)))
proof end;
uniqueness
for b1, b2 being ExtREAL_sequence st ( for n being Nat holds b1 . n = SUM (vol (M,(Cvr . n))) ) & ( for n being Nat holds b2 . n = SUM (vol (M,(Cvr . n))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Volume MEASURE8:def 6 :
for X being set
for F being Field_Subset of X
for Sets being SetSequence of X
for M being Measure of F
for Cvr being Covering of Sets,F
for b6 being ExtREAL_sequence holds
( b6 = Volume (M,Cvr) iff for n being Nat holds b6 . n = SUM (vol (M,(Cvr . n))) );

theorem Th5: :: MEASURE8:5
for X being set
for F being Field_Subset of X
for M being Measure of F
for Sets being SetSequence of X
for n being Nat
for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n
proof end;

definition
let X be set ;
let F be Field_Subset of X;
let M be Measure of F;
let A be Subset of X;
func Svc (M,A) -> Subset of ExtREAL means :Def7: :: MEASURE8:def 7
for x being R_eal holds
( x in it iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) );
existence
ex b1 being Subset of ExtREAL st
for x being R_eal holds
( x in b1 iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) )
proof end;
uniqueness
for b1, b2 being Subset of ExtREAL st ( for x being R_eal holds
( x in b1 iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) ) & ( for x being R_eal holds
( x in b2 iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines Svc MEASURE8:def 7 :
for X being set
for F being Field_Subset of X
for M being Measure of F
for A being Subset of X
for b5 being Subset of ExtREAL holds
( b5 = Svc (M,A) iff for x being R_eal holds
( x in b5 iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) );

registration
let X be set ;
let A be Subset of X;
let F be Field_Subset of X;
let M be Measure of F;
cluster Svc (M,A) -> non empty ;
coherence
not Svc (M,A) is empty
proof end;
end;

definition
let X be set ;
let F be Field_Subset of X;
let M be Measure of F;
func C_Meas M -> Function of (bool X),ExtREAL means :Def8: :: MEASURE8:def 8
for A being Subset of X holds it . A = inf (Svc (M,A));
existence
ex b1 being Function of (bool X),ExtREAL st
for A being Subset of X holds b1 . A = inf (Svc (M,A))
proof end;
uniqueness
for b1, b2 being Function of (bool X),ExtREAL st ( for A being Subset of X holds b1 . A = inf (Svc (M,A)) ) & ( for A being Subset of X holds b2 . A = inf (Svc (M,A)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines C_Meas MEASURE8:def 8 :
for X being set
for F being Field_Subset of X
for M being Measure of F
for b4 being Function of (bool X),ExtREAL holds
( b4 = C_Meas M iff for A being Subset of X holds b4 . A = inf (Svc (M,A)) );

definition
correctness
coherence ;
by ;
end;

:: deftheorem defines InvPairFunc MEASURE8:def 9 :

definition
let X be set ;
let F be Field_Subset of X;
let Sets be SetSequence of X;
let Cvr be Covering of Sets,F;
func On Cvr -> Covering of union (rng Sets),F means :Def10: :: MEASURE8:def 10
for n being Nat holds it . n = (Cvr . ( . n)) . ( . n);
existence
ex b1 being Covering of union (rng Sets),F st
for n being Nat holds b1 . n = (Cvr . ( . n)) . ( . n)
proof end;
uniqueness
for b1, b2 being Covering of union (rng Sets),F st ( for n being Nat holds b1 . n = (Cvr . ( . n)) . ( . n) ) & ( for n being Nat holds b2 . n = (Cvr . ( . n)) . ( . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines On MEASURE8:def 10 :
for X being set
for F being Field_Subset of X
for Sets being SetSequence of X
for Cvr being Covering of Sets,F
for b5 being Covering of union (rng Sets),F holds
( b5 = On Cvr iff for n being Nat holds b5 . n = (Cvr . ( . n)) . ( . n) );

theorem Th6: :: MEASURE8:6
for X being set
for F being Field_Subset of X
for M being Measure of F
for k being Nat ex m being Nat st
for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . k <= (Partial_Sums (Volume (M,Cvr))) . m
proof end;

theorem Th7: :: MEASURE8:7
for X being set
for F being Field_Subset of X
for M being Measure of F
for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr))
proof end;

theorem Th8: :: MEASURE8:8
for X being set
for F being Field_Subset of X
for A being Subset of X st A in F holds
(A,({} X)) followed_by ({} X) is Covering of A,F
proof end;

theorem Th9: :: MEASURE8:9
for X being set
for F being Field_Subset of X
for M being Measure of F
for A being set st A in F holds
() . A <= M . A
proof end;

theorem Th10: :: MEASURE8:10
for X being set
for F being Field_Subset of X
for M being Measure of F holds C_Meas M is nonnegative
proof end;

theorem Th11: :: MEASURE8:11
for X being set
for F being Field_Subset of X
for M being Measure of F holds () . {} = 0
proof end;

theorem Th12: :: MEASURE8:12
for X being set
for F being Field_Subset of X
for M being Measure of F
for A, B being Subset of X st A c= B holds
() . A <= () . B
proof end;

Lm2: for X being set
for F being Field_Subset of X
for M being Measure of F
for Sets being SetSequence of X st ex n being Nat st () . (Sets . n) = +infty holds
() . (union (rng Sets)) <= SUM (() * Sets)

proof end;

theorem Th13: :: MEASURE8:13
for X being set
for F being Field_Subset of X
for M being Measure of F
for Sets being SetSequence of X holds () . (union (rng Sets)) <= SUM (() * Sets)
proof end;

theorem Th14: :: MEASURE8:14
for X being set
for F being Field_Subset of X
for M being Measure of F holds C_Meas M is C_Measure of X
proof end;

definition
let X be set ;
let F be Field_Subset of X;
let M be Measure of F;
:: original: C_Meas
redefine func C_Meas M -> C_Measure of X;
correctness
coherence
C_Meas M is C_Measure of X
;
by Th14;
end;

definition
let X be set ;
let F be Field_Subset of X;
let M be Measure of F;
attr M is completely-additive means :: MEASURE8:def 11
for FSets being Sep_Sequence of F st union (rng FSets) in F holds
SUM (M * FSets) = M . (union (rng FSets));
end;

:: deftheorem defines completely-additive MEASURE8:def 11 :
for X being set
for F being Field_Subset of X
for M being Measure of F holds
( M is completely-additive iff for FSets being Sep_Sequence of F st union (rng FSets) in F holds
SUM (M * FSets) = M . (union (rng FSets)) );

theorem Th15: :: MEASURE8:15
for X being set
for F being Field_Subset of X
for FSets being Set_Sequence of F holds Partial_Union FSets is Set_Sequence of F
proof end;

theorem Th16: :: MEASURE8:16
for X being set
for F being Field_Subset of X
for FSets being Set_Sequence of F holds Partial_Diff_Union FSets is Set_Sequence of F
proof end;

theorem Th17: :: MEASURE8:17
for X being set
for F being Field_Subset of X
for A being Subset of X
for CA being Covering of A,F st A in F holds
ex FSets being Sep_Sequence of F st
( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) )
proof end;

theorem Th18: :: MEASURE8:18
for X being set
for F being Field_Subset of X
for M being Measure of F st M is completely-additive holds
for A being set st A in F holds
M . A = () . A
proof end;

theorem Th19: :: MEASURE8:19
for X being set
for A being Subset of X
for C being C_Measure of X st ( for B being Subset of X holds (C . (B /\ A)) + (C . (B /\ (X \ A))) <= C . B ) holds
A in sigma_Field C
proof end;

theorem Th20: :: MEASURE8:20
for X being set
for F being Field_Subset of X
for M being Measure of F holds F c= sigma_Field ()
proof end;

theorem Th21: :: MEASURE8:21
for X being set
for F being Field_Subset of X
for FSets being Set_Sequence of F
for M being Function of F,ExtREAL holds M * FSets is ExtREAL_sequence
proof end;

definition
let X be set ;
let F be Field_Subset of X;
let FSets be Set_Sequence of F;
let g be Function of F,ExtREAL;
:: original: *
redefine func g * FSets -> ExtREAL_sequence;
correctness
coherence
FSets * g is ExtREAL_sequence
;
by Th21;
end;

theorem Th22: :: MEASURE8:22
for X being set
for S being SigmaField of X
for SSets being SetSequence of S
for M being Function of S,ExtREAL holds M * SSets is ExtREAL_sequence
proof end;

definition
let X be set ;
let S be SigmaField of X;
let SSets be SetSequence of S;
let g be Function of S,ExtREAL;
:: original: *
redefine func g * SSets -> ExtREAL_sequence;
correctness
coherence
SSets * g is ExtREAL_sequence
;
by Th22;
end;

theorem Th23: :: MEASURE8:23
for F, G being sequence of ExtREAL
for n being Nat st ( for m being Nat st m <= n holds
F . m <= G . m ) holds
(Ser F) . n <= (Ser G) . n
proof end;

theorem Th24: :: MEASURE8:24
for X being set
for C being C_Measure of X
for seq being Sep_Sequence of () holds
( union (rng seq) in sigma_Field C & C . (union (rng seq)) = Sum (C * seq) )
proof end;

theorem :: MEASURE8:25
for X being set
for C being C_Measure of X
for seq being SetSequence of sigma_Field C holds Union seq in sigma_Field C
proof end;

theorem Th26: :: MEASURE8:26
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for SSets being SetSequence of S st SSets is non-descending holds
lim (M * SSets) = M . (lim SSets)
proof end;

theorem :: MEASURE8:27
for X being set
for F being Field_Subset of X
for M being Measure of F
for FSets being Set_Sequence of F st FSets is non-descending holds
M * FSets is non-decreasing
proof end;

theorem :: MEASURE8:28
for X being set
for F being Field_Subset of X
for M being Measure of F
for FSets being Set_Sequence of F st FSets is non-ascending holds
M * FSets is non-increasing
proof end;

theorem Th29: :: MEASURE8:29
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for SSets being SetSequence of S st SSets is non-descending holds
M * SSets is non-decreasing
proof end;

theorem Th30: :: MEASURE8:30
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for SSets being SetSequence of S st SSets is non-ascending holds
M * SSets is non-increasing
proof end;

theorem :: MEASURE8:31
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for SSets being SetSequence of S st SSets is non-ascending & M . (SSets . 0) < +infty holds
lim (M * SSets) = M . (lim SSets)
proof end;

definition
let X be set ;
let F be Field_Subset of X;
let S be SigmaField of X;
let m be Measure of F;
let M be sigma_Measure of S;
pred M is_extension_of m means :: MEASURE8:def 12
for A being set st A in F holds
M . A = m . A;
end;

:: deftheorem defines is_extension_of MEASURE8:def 12 :
for X being set
for F being Field_Subset of X
for S being SigmaField of X
for m being Measure of F
for M being sigma_Measure of S holds
( M is_extension_of m iff for A being set st A in F holds
M . A = m . A );

theorem :: MEASURE8:32
for X being non empty set
for F being Field_Subset of X
for m being Measure of F st ex M being sigma_Measure of () st M is_extension_of m holds
proof end;

theorem Th33: :: MEASURE8:33
for X being non empty set
for F being Field_Subset of X
for m being Measure of F st m is completely-additive holds
ex M being sigma_Measure of () st
( M is_extension_of m & M = (sigma_Meas ()) | () )
proof end;

theorem Th34: :: MEASURE8:34
for X being set
for F being Field_Subset of X
for M being Measure of F
for k being Nat
for FSets being Set_Sequence of F st ( for n being Nat holds M . (FSets . n) < +infty ) holds
M . ((Partial_Union FSets) . k) < +infty
proof end;

theorem :: MEASURE8:35
for X being non empty set
for F being Field_Subset of X
for m being Measure of F st m is completely-additive & ex Aseq being Set_Sequence of F st
( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) holds
for M being sigma_Measure of () st M is_extension_of m holds
M = (sigma_Meas ()) | ()
proof end;