MEASURE8: The Hopf Extension Theorem of Measure

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

begin

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 seq1, seq2, seq 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 NAT -defined F -valued Function-like V27( NAT ) quasi_total disjoint_valued for Element of bool [:NAT,F:];

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;

proof end;

end;

:: deftheorem Def1 defines FinSequence MEASURE8:def 1 :

registration

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

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

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 Function of NAT,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;

proof end;

end;

:: deftheorem Def2 defines Set_Sequence MEASURE8:def 2 :

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);

proof end;

end;

:: deftheorem Def3 defines Covering MEASURE8:def 3 :

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 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 -> Function of NAT,(Funcs (NAT,(bool X))) means :Def4: :: MEASURE8:def 4
for n being Nat holds it . n is Covering of Sets . n,F;

proof end;

end;

:: deftheorem Def4 defines Covering MEASURE8:def 4 :

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);

proof end;

proof end;

end;

:: deftheorem Def5 defines vol MEASURE8:def 5 :

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 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)));

proof end;

proof end;

end;

:: deftheorem Def6 defines Volume MEASURE8:def 6 :

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)) );

proof end;

proof end;

end;

:: deftheorem Def7 defines Svc MEASURE8:def 7 :

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 ;

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));

proof end;

proof end;

end;

:: deftheorem Def8 defines C_Meas MEASURE8:def 8 :

definition

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

correctness by FUNCTOR1:2, NAGATA_2:2;

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

proof end;

proof end;

end;

:: deftheorem Def10 defines On MEASURE8:def 10 :

theorem Th6: :: MEASURE8:6

for X being set
for F being Field_Subset of X
for M being Measure of F
for k being Element of 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 by Th14;

end;

begin

definition

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

attr M is completely-additive means :Def11: :: 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 Def11 defines completely-additive MEASURE8:def 11 :

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 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 by Th22;

end;

theorem Th23: :: MEASURE8:23

for F, G being Function of NAT,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 :Def12: :: MEASURE8:def 12
for A being set st A in F holds
M . A = m . A;

end;

:: deftheorem Def12 defines is_extension_of MEASURE8:def 12 :

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;