:: Lebesgue Integral of Simple Valued Function
:: by Yasunari Shidama and Noboru Endou
::
:: Received September 25, 2004
:: Copyright (c) 2004-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, FUNCT_1, ZFMISC_1, FINSEQ_1, RELAT_1, CARD_3,
ARYTM_3, SUBSET_1, XXREAL_0, TARSKI, XBOOLE_0, FINSEQ_2, ARYTM_1,
PARTFUN1, BINOP_2, ORDINAL4, CARD_1, FUNCOP_1, PROB_1, MESFUNC2, FUNCT_3,
SUPINF_2, PROB_2, MEASURE1, XXREAL_2, ORDINAL2, SUPINF_1, XREAL_0,
MESFUNC1, VALUED_0, COMPLEX1, SETFAM_1, FINSET_1, FINSOP_1, INTEGRA1,
REAL_1, MESFUNC3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, XREAL_0, FINSEQ_1,
SETFAM_1, FUNCOP_1, FINSOP_1, FUNCT_3, FINSET_1, PROB_1, PROB_2,
XXREAL_0, XXREAL_2, XXREAL_3, NAT_1, REAL_1, XCMPLX_0, SUPINF_1,
SUPINF_2, MEASURE1, FINSEQOP, FINSEQ_2, BINOP_1, BINOP_2, RVSUM_1,
EXTREAL1, MESFUNC1, MESFUNC2;
constructors PARTFUN1, BINOP_1, SETWISEO, REAL_1, NAT_1, FINSEQOP, PROB_2,
FINSOP_1, RVSUM_1, MEASURE3, MEASURE6, EXTREAL1, MESFUNC1, BINARITH,
MESFUNC2, BINOP_2, SUPINF_1, RELSET_1, NUMBERS;
registrations SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XXREAL_0,
XREAL_0, NAT_1, MEMBERED, FINSEQ_1, MEASURE1, FINSET_1, VALUED_0, CARD_1,
CARD_3, XXREAL_3, RELSET_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: Integral of Simple Valued Function
theorem :: MESFUNC3:1
for n,m be Nat, a be Function of [:Seg n,Seg m:],REAL for p,q
be FinSequence of REAL st ( dom p=Seg n & for i be Nat st i in dom p holds ex r
be FinSequence of REAL st (dom r = Seg m & p.i = Sum r & for j be Nat st j in
dom r holds r.j=a.[i,j])) & ( dom q=Seg m & for j be Nat st j in dom q holds ex
s be FinSequence of REAL st (dom s = Seg n & q.j = Sum s & for i be Nat st i in
dom s holds s.i=a.[i,j])) holds Sum p = Sum q;
theorem :: MESFUNC3:2
for F be FinSequence of ExtREAL, f be FinSequence of REAL st F=f
holds Sum(F)=Sum(f);
theorem :: MESFUNC3:3
for X be non empty set, S be SigmaField of X, f be PartFunc of X,
ExtREAL st f is_simple_func_in S holds ex F be Finite_Sep_Sequence of S, a be
FinSequence of ExtREAL st dom f = union rng F & dom F= dom a & (for n be Nat st
n in dom F for x be object st x in F.n holds f.x = a.n) &
for x be object st x in dom f
ex ax be FinSequence of ExtREAL st dom ax = dom a & for n be Nat st n
in dom ax holds ax.n=a.n*(chi(F.n,X)).x;
theorem :: MESFUNC3:4
for X be set, F be FinSequence of X holds F is disjoint_valued
iff for i,j be Nat st i in dom F & j in dom F & i <> j holds F.i misses F.j;
theorem :: MESFUNC3:5
for X be non empty set, A be set, S be SigmaField of X, F be
Finite_Sep_Sequence of S, G be FinSequence of S st dom G = dom F & for i be Nat
st i in dom G holds G.i = A /\ F.i holds G is Finite_Sep_Sequence of S;
theorem :: MESFUNC3:6
for X be non empty set, A be set, F,G be FinSequence of X st dom
G = dom F & (for i be Nat st i in dom G holds G.i = A /\ F.i) holds union rng G
= A /\ union rng F;
theorem :: MESFUNC3:7
for X be set, F be FinSequence of X, i be Nat st i in dom F holds
F.i c= union rng F & F.i /\ union rng F = F.i;
theorem :: MESFUNC3:8
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, F be Finite_Sep_Sequence of S holds dom F = dom (M*F);
theorem :: MESFUNC3:9
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, F be Finite_Sep_Sequence of S holds M.(union rng F) = Sum(M*F);
theorem :: MESFUNC3:10
for F,G be FinSequence of ExtREAL, a be R_eal st (a is real or (
for i be Nat st i in dom F holds F.i < 0.) or
for i be Nat st i in dom F holds 0. < F.i )
& dom F = dom G & for i be Nat st i in dom G holds G.i=a*F.i holds
Sum(G)=a*Sum(F);
theorem :: MESFUNC3:11
for F be FinSequence of REAL holds F is FinSequence of ExtREAL;
definition
let X be non empty set;
let S be SigmaField of X;
let f be PartFunc of X,ExtREAL;
let F be Finite_Sep_Sequence of S;
let a be FinSequence of ExtREAL;
pred F,a are_Re-presentation_of f means
:: MESFUNC3:def 1
dom f = union rng F & dom F=
dom a & for n be Nat st n in dom F
for x be object st x in F.n holds f.x=a.n;
end;
theorem :: MESFUNC3:12
for X be non empty set, S be SigmaField of X, f be PartFunc of X,
ExtREAL st f is_simple_func_in S
ex F be Finite_Sep_Sequence of S, a be
FinSequence of ExtREAL st F,a are_Re-presentation_of f;
theorem :: MESFUNC3:13
for X be non empty set, S be SigmaField of X, F be
Finite_Sep_Sequence of S holds ex G be Finite_Sep_Sequence of S st union rng F
= union rng G & for n be Nat st n in dom G holds (G.n <> {} & ex m be Nat st m
in dom F & F.m = G.n);
theorem :: MESFUNC3:14
for X be non empty set, S be SigmaField of X, f be PartFunc of X
,ExtREAL st f is_simple_func_in S & f is nonnegative
holds ex F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL st F,a
are_Re-presentation_of f & a.1=0. & for n be Nat st 2 <= n & n in dom a holds
0. < a.n & a.n < +infty;
theorem :: MESFUNC3:15
for X be non empty set, S be SigmaField of X, f be PartFunc of X,
ExtREAL, F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL, x be
Element of X st F,a are_Re-presentation_of f & x in dom f holds ex ax be
FinSequence of ExtREAL st dom ax= dom a & (for n be Nat st n in dom ax holds ax
.n=a.n*(chi(F.n,X)).x) & f.x=Sum(ax);
theorem :: MESFUNC3:16
for p be FinSequence of ExtREAL, q be FinSequence of REAL st p=q holds
Sum(p) = Sum(q);
theorem :: MESFUNC3:17
for p be FinSequence of ExtREAL st not -infty in rng p & +infty in rng p
holds Sum(p) = +infty;
definition
let X be non empty set;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,ExtREAL;
assume
f is_simple_func_in S & f is nonnegative;
func integral(M,f) -> Element of ExtREAL means
:: MESFUNC3:def 2
ex F be Finite_Sep_Sequence of S, a, x be FinSequence of ExtREAL st F,a
are_Re-presentation_of f & a.1 =0. & (for n be Nat st 2 <= n & n in dom a holds
0. < a.n & a.n < +infty ) & dom x = dom F & (for n be Nat st n in dom x holds x
.n=a.n*(M*F).n) & it=Sum(x);
end;
begin :: Additional Lemma
theorem :: MESFUNC3:18
for a be FinSequence of ExtREAL, p,N be Element of ExtREAL st N = len a &
(for n be Nat st n in dom a holds a.n = p) holds Sum(a) = N * p;