:: The Hopf Extension Theorem of Measure
:: by Noboru Endou , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received April 7, 2009
:: 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;

cluster non empty Relation-like omega -defined F -valued Function-like V30( omega ) quasi_total disjoint_valued for Element of bool [:omega,F:];

existence
ex b₁ being sequence of F st b₁ 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 b₁ being FinSequence of bool X st
for k being Nat st k in dom b₁ holds
b₁ . 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 b₃ being FinSequence of bool X holds
( b₃ is FinSequence of F iff for k being Nat st k in dom b₃ holds
b₃ . k in F );

registration

let X be set ;
let F be Field_Subset of X;

cluster Relation-like omega -defined bool X -valued Function-like FinSequence-like disjoint_valued for FinSequence of F;

existence
ex b₁ being FinSequence of F st b₁ 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 b₁ being SetSequence of X st
for n being Nat holds b₁ . 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 b₃ being SetSequence of X holds
( b₃ is Set_Sequence of F iff for n being Nat holds b₃ . 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 b₁ being Set_Sequence of F st A c= union (rng b₁)

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 b₄ being Set_Sequence of F holds
( b₄ is Covering of A,F iff A c= union (rng b₄) );

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 b₁ being sequence of (Funcs (NAT,(bool X))) st
for n being Nat holds b₁ . 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 b₄ being sequence of (Funcs (NAT,(bool X))) holds
( b₄ is Covering of Sets,F iff for n being Nat holds b₄ . 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 b₁ being ExtREAL_sequence st
for n being Nat holds b₁ . n = M . (FSets . n)

proof end;

uniqueness
for b₁, b₂ being ExtREAL_sequence st ( for n being Nat holds b₁ . n = M . (FSets . n) ) & ( for n being Nat holds b₂ . n = M . (FSets . n) ) holds
b₁ = b₂

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 b₅ being ExtREAL_sequence holds
( b₅ = vol (M,FSets) iff for n being Nat holds b₅ . 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 b₁ being ExtREAL_sequence st
for n being Nat holds b₁ . n = SUM (vol (M,(Cvr . n)))

proof end;

uniqueness
for b₁, b₂ being ExtREAL_sequence st ( for n being Nat holds b₁ . n = SUM (vol (M,(Cvr . n))) ) & ( for n being Nat holds b₂ . n = SUM (vol (M,(Cvr . n))) ) holds
b₁ = b₂

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 b₆ being ExtREAL_sequence holds
( b₆ = Volume (M,Cvr) iff for n being Nat holds b₆ . 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 b₁ being Subset of ExtREAL st
for x being R_eal holds
( x in b₁ iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) )

proof end;

uniqueness
for b₁, b₂ being Subset of ExtREAL st ( for x being R_eal holds
( x in b₁ iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) ) & ( for x being R_eal holds
( x in b₂ iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) ) holds
b₁ = b₂

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 b₅ being Subset of ExtREAL holds
( b₅ = Svc (M,A) iff for x being R_eal holds
( x in b₅ 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 b₁ being Function of (bool X),ExtREAL st
for A being Subset of X holds b₁ . A = inf (Svc (M,A))

proof end;

uniqueness
for b₁, b₂ being Function of (bool X),ExtREAL st ( for A being Subset of X holds b₁ . A = inf (Svc (M,A)) ) & ( for A being Subset of X holds b₂ . A = inf (Svc (M,A)) ) holds
b₁ = b₂

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 b₄ being Function of (bool X),ExtREAL holds
( b₄ = C_Meas M iff for A being Subset of X holds b₄ . A = inf (Svc (M,A)) );

definition

func InvPairFunc -> sequence of [:NAT,NAT:] equals :: MEASURE8:def 9
PairFunc " ;

correctness
coherence
PairFunc " is sequence of [:NAT,NAT:];
by FUNCTOR1:2, NAGATA_2:2;

end;

:: deftheorem defines InvPairFunc MEASURE8:def 9 :
InvPairFunc = PairFunc " ;

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 . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n);

existence
ex b₁ being Covering of union (rng Sets),F st
for n being Nat holds b₁ . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n)

proof end;

uniqueness
for b₁, b₂ being Covering of union (rng Sets),F st ( for n being Nat holds b₁ . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) ) & ( for n being Nat holds b₂ . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) ) holds
b₁ = b₂

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 b₅ being Covering of union (rng Sets),F holds
( b₅ = On Cvr iff for n being Nat holds b₅ . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . 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
(C_Meas M) . 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 (C_Meas M) . {} = 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
(C_Meas M) . A <= (C_Meas M) . 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 (C_Meas M) . (Sets . n) = +infty holds
(C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * 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 (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * 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 = (C_Meas M) . 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 (C_Meas M)

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 (sigma_Field C) 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 (sigma F) st M is_extension_of m holds
m is completely-additive

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 (sigma F) st
( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) )

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 (sigma F) st M is_extension_of m holds
M = (sigma_Meas (C_Meas m)) | (sigma F)

proof end;