:: Integral of Non Positive Functions
:: by Noboru Endou
::
:: Received September 3, 2017
:: Copyright (c) 2017 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, XXREAL_0, SUBSET_1, CARD_1, ARYTM_3, ARYTM_1, RELAT_1,
NAT_1, REAL_1, CARD_3, FUNCT_1, FINSEQ_1, XBOOLE_0, TARSKI, PROB_1,
FUNCOP_1, SUPINF_2, VALUED_0, FUNCT_2, PARTFUN1, MEASURE1, ORDINAL2,
SERIES_1, MESFUNC5, SEQ_2, SEQFUNC, PBOOLE, VALUED_1, MESFUNC1, MESFUNC8,
MESFUNC2, MESFUNC3, COMPLEX1, XCMPLX_0, RFUNCT_3, INT_1, MSSUBFAM;
notations TARSKI, XBOOLE_0, SUBSET_1, XXREAL_3, XXREAL_0, XREAL_0, ORDINAL1,
NUMBERS, FUNCT_1, RELSET_1, FUNCT_2, FUNCOP_1, PARTFUN1, PROB_1, PROB_3,
NAT_1, NAT_D, VALUED_0, FINSEQ_1, SUPINF_2, SEQFUNC, MEASURE1, MESFUNC1,
MESFUNC2, MESFUNC3, MESFUNC5, MESFUNC8, DBLSEQ_3, MESFUNC9, EXTREAL1;
constructors SEQFUNC, PROB_3, MESFUNC8, MESFUNC9, EXTREAL1, SUPINF_1,
MESFUNC2, DBLSEQ_3, MEASUR11, MESFUNC3, NAT_D;
registrations ORDINAL1, XBOOLE_0, RELAT_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1,
NUMBERS, VALUED_0, MESFUNC9, RELSET_1, PARTFUN1, XXREAL_3, DBLSEQ_3,
MEASUR11, MESFUNC5;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
begin :: Preliminaries
registration
let X be non empty set, f be nonnegative PartFunc of X,ExtREAL;
cluster -f -> nonpositive;
end;
registration
let X be non empty set, f be nonpositive PartFunc of X,ExtREAL;
cluster -f -> nonnegative;
end;
theorem :: MESFUN11:1
for X be non empty set, f be nonpositive PartFunc of X,ExtREAL, E be set
holds f|E is nonpositive;
theorem :: MESFUN11:2
for X be non empty set, A be set, r be Real, f be PartFunc of X,ExtREAL
holds (r(#)f)|A = r(#)(f|A);
theorem :: MESFUN11:3
for X be non empty set, A be set, f be PartFunc of X,ExtREAL
holds -(f|A) = (-f)|A;
theorem :: MESFUN11:4
for X be non empty set, f be PartFunc of X,ExtREAL,c be Real st
f is nonpositive holds
(0 <= c implies c(#)f is nonpositive) &
(c <= 0 implies c(#)f is nonnegative);
theorem :: MESFUN11:5
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL holds
max+f is nonnegative & max-f is nonnegative &
|.f.| is nonnegative;
theorem :: MESFUN11:6
for X be non empty set, f be PartFunc of X,ExtREAL, x be object holds
f.x <= (max+f).x & f.x >= -(max-f).x;
theorem :: MESFUN11:7
for X be non empty set, f be PartFunc of X,ExtREAL,
r be positive Real holds less_dom(f,r) = less_dom(max+f,r);
theorem :: MESFUN11:8
for X be non empty set, f be PartFunc of X,ExtREAL,
r be non positive Real holds less_dom(f,r) = great_dom(max-f,-r);
theorem :: MESFUN11:9
for X be non empty set, f,g be PartFunc of X,ExtREAL,
a be ExtReal, r be Real
st r <> 0 & g = r(#)f holds eq_dom(f,a) = eq_dom(g,a*r);
theorem :: MESFUN11:10
for X be non empty set, S be SigmaField of X, f be PartFunc of X,ExtREAL,
A be Element of S st A c= dom f holds
f is_measurable_on A iff
max+f is_measurable_on A & max-f is_measurable_on A;
definition
let X be non empty set, f be Function of X,ExtREAL, r be Real;
redefine func r(#)f -> Function of X,ExtREAL;
end;
theorem :: MESFUN11:11
for X be non empty set, r be Real, f be without+infty Function of X,ExtREAL
st r >= 0 holds r(#)f is without+infty;
registration
let X be non empty set;
let f be without+infty Function of X,ExtREAL;
let r be non negative Real;
cluster r(#)f -> without+infty for Function of X,ExtREAL;
end;
theorem :: MESFUN11:12
for X be non empty set, r be Real, f be without+infty Function of X,ExtREAL
st r <= 0 holds r(#)f is without-infty;
registration
let X be non empty set;
let f be without+infty Function of X,ExtREAL;
let r be non positive Real;
cluster r(#)f -> without-infty;
end;
theorem :: MESFUN11:13
for X be non empty set, r be Real, f be without-infty Function of X,ExtREAL
st r >= 0 holds r(#)f is without-infty;
registration
let X be non empty set;
let f be without-infty Function of X,ExtREAL;
let r be non negative Real;
cluster r(#)f -> without-infty;
end;
theorem :: MESFUN11:14
for X be non empty set, r be Real, f be without-infty Function of X,ExtREAL
st r <= 0 holds r(#)f is without+infty;
registration
let X be non empty set;
let f be without-infty Function of X,ExtREAL;
let r be non positive Real;
cluster r(#)f -> without+infty;
end;
theorem :: MESFUN11:15
for X be non empty set, r be Real,
f be without-infty without+infty Function of X,ExtREAL holds
r(#)f is without-infty without+infty;
registration
let X be non empty set;
let f be without-infty without+infty Function of X,ExtREAL;
let r be Real;
cluster r(#)f -> without-infty without+infty;
end;
theorem :: MESFUN11:16
for X be non empty set, r be positive Real, f be Function of X,ExtREAL
holds f is without+infty iff r(#)f is without+infty;
theorem :: MESFUN11:17
for X be non empty set, r be negative Real, f be Function of X,ExtREAL
holds f is without+infty iff r(#)f is without-infty;
theorem :: MESFUN11:18
for X be non empty set, r be positive Real, f be Function of X,ExtREAL
holds f is without-infty iff r(#)f is without-infty;
theorem :: MESFUN11:19
for X be non empty set, r be negative Real, f be Function of X,ExtREAL
holds f is without-infty iff r(#)f is without+infty;
theorem :: MESFUN11:20
for X be non empty set, r be non zero Real, f be Function of X,ExtREAL
holds f is without-infty without+infty iff
r(#)f is without-infty without+infty;
theorem :: MESFUN11:21
for X,Y be non empty set, f be PartFunc of X,ExtREAL, r be Real
st f = Y --> r holds f is without-infty without+infty;
theorem :: MESFUN11:22
for X be non empty set, f be Function of X,ExtREAL holds
0(#)f = X --> 0
& 0(#)f is without-infty without+infty;
theorem :: MESFUN11:23
for X be non empty set, f,g be PartFunc of X,ExtREAL st
f is without-infty without+infty holds
dom(f+g)=dom f /\ dom g & dom(f-g)=dom f /\ dom g
& dom(g-f)=dom f /\ dom g;
theorem :: MESFUN11:24
for X be non empty set, f1,f2 be Function of X,ExtREAL
st f2 is without-infty without+infty holds
f1+f2 is Function of X,ExtREAL
& for x be Element of X holds (f1+f2).x = f1.x + f2.x;
theorem :: MESFUN11:25
for X be non empty set, f1,f2 be Function of X,ExtREAL
st f1 is without-infty without+infty holds
f1-f2 is Function of X,ExtREAL
& for x be Element of X holds (f1-f2).x = f1.x - f2.x;
theorem :: MESFUN11:26
for X be non empty set, f1,f2 be Function of X,ExtREAL
st f2 is without-infty without+infty holds
f1-f2 is Function of X,ExtREAL
& for x be Element of X holds (f1-f2).x = f1.x - f2.x;
theorem :: MESFUN11:27
for X,Y be non empty set, f1,f2 be PartFunc of X,ExtREAL st
dom f1 c= Y & f2 = Y --> 0 holds f1+f2 = f1 & f1-f2 = f1 & f2-f1 = -f1;
theorem :: MESFUN11:28
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f,g be PartFunc of X,ExtREAL st f is_simple_func_in S &
g is_simple_func_in S holds f+g is_simple_func_in S;
theorem :: MESFUN11:29
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f,g be PartFunc of X,ExtREAL st f is_simple_func_in S &
g is_simple_func_in S holds f-g is_simple_func_in S;
theorem :: MESFUN11:30
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 -f is_simple_func_in S;
theorem :: MESFUN11:31
for X be non empty set, f be nonnegative PartFunc of X,ExtREAL holds f = max+f;
theorem :: MESFUN11:32
for X be non empty set, f be nonpositive PartFunc of X,ExtREAL
holds f = -(max-f);
theorem :: MESFUN11:33
for C being non empty set, f being PartFunc of C,ExtREAL, c be
Real st c <= 0 holds max+(c(#)f) = (-c)(#)max-f & max-(c(#)f) = (-c)(#)max+f;
theorem :: MESFUN11:34
for X be non empty set, f be PartFunc of X,ExtREAL holds
max+f = max-(-f);
theorem :: MESFUN11:35
for X be non empty set, f be PartFunc of X,ExtREAL, r1,r2 be Real
holds r1(#)(r2(#)f) = (r1*r2)(#)f;
theorem :: MESFUN11:36
for X be non empty set, f,g be PartFunc of X,ExtREAL st f = -g holds g = -f;
definition
let X be non empty set;
let F be Functional_Sequence of X,ExtREAL;
let r be Real;
func r(#)F -> Functional_Sequence of X,ExtREAL means
:: MESFUN11:def 1
for n being Nat holds it.n = r(#)(F.n);
end;
definition
let X be non empty set;
let F be Functional_Sequence of X,ExtREAL;
func -F -> Functional_Sequence of X,ExtREAL equals
:: MESFUN11:def 2
(-1)(#)F;
end;
theorem :: MESFUN11:37
for X be non empty set, F be Functional_Sequence of X,ExtREAL, n be Nat
holds (-F).n = -(F.n);
theorem :: MESFUN11:38
for X be non empty set, F be Functional_Sequence of X,ExtREAL,
x be Element of X holds (-F)#x = -(F#x);
theorem :: MESFUN11:39
for X be non empty set, F be Functional_Sequence of X,ExtREAL,
x be Element of X holds
(F#x is convergent_to_+infty iff (-F)#x is convergent_to_-infty) &
(F#x is convergent_to_-infty iff (-F)#x is convergent_to_+infty) &
(F#x is convergent_to_finite_number
iff (-F)#x is convergent_to_finite_number) &
(F#x is convergent iff (-F)#x is convergent) &
(F#x is convergent implies lim((-F)#x) = - lim(F#x));
theorem :: MESFUN11:40
for X be non empty set, F be Functional_Sequence of X,ExtREAL
st F is with_the_same_dom holds -F is with_the_same_dom;
theorem :: MESFUN11:41
for X be non empty set, F be Functional_Sequence of X,ExtREAL
st F is additive holds -F is additive;
theorem :: MESFUN11:42
for X be non empty set, F be Functional_Sequence of X,ExtREAL, n be Nat
holds (Partial_Sums(-F)).n = (-(Partial_Sums F)).n;
theorem :: MESFUN11:43
for seq be ExtREAL_sequence, n be Nat holds
(Partial_Sums(-seq)).n = -((Partial_Sums seq).n);
theorem :: MESFUN11:44
for seq be ExtREAL_sequence holds Partial_Sums(-seq) = -(Partial_Sums seq);
theorem :: MESFUN11:45
for seq be ExtREAL_sequence st seq is summable holds -seq is summable;
theorem :: MESFUN11:46
for X be non empty set, F be Functional_Sequence of X,ExtREAL
st (for n be Nat holds F.n is without+infty) holds F is additive;
theorem :: MESFUN11:47
for X be non empty set, F be Functional_Sequence of X,ExtREAL
st (for n be Nat holds F.n is without-infty) holds F is additive;
theorem :: MESFUN11:48
for X be non empty set, F be Functional_Sequence of X,ExtREAL,
x be Element of X st F#x is summable holds
(-F)#x is summable & Sum((-F)#x) = -Sum(F#x);
theorem :: MESFUN11:49
for X be non empty set, S be SigmaField of X,
F be Functional_Sequence of X,ExtREAL st
F is additive & F is with_the_same_dom &
(for x be Element of X st x in dom(F.0) holds F#x is summable)
holds lim Partial_Sums (-F) = -(lim Partial_Sums F);
theorem :: MESFUN11:50
for X be non empty set, S be SigmaField of X,
F,G be Functional_Sequence of X,ExtREAL, E be Element of S
st E c= dom(F.0) & F is additive & F is with_the_same_dom
& (for n be Nat holds G.n = (F.n)|E)
holds lim(Partial_Sums G) = (lim(Partial_Sums F))|E;
begin :: Integral of non positive measurable functions
theorem :: MESFUN11:51
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be nonnegative PartFunc of X, ExtREAL
holds integral'(M,max-(-f)) = integral'(M,f);
theorem :: MESFUN11:52
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, A be Element of S
st A = dom f & f is_measurable_on A holds Integral(M,-f) = - Integral(M,f);
theorem :: MESFUN11:53
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be nonnegative PartFunc of X,ExtREAL, E be Element of S
st E = dom f & f is_measurable_on E
holds Integral(M,max-f) = 0 & integral+(M,max-f) = 0;
theorem :: MESFUN11:54
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, E be Element of S
st E = dom f & f is_measurable_on E holds
Integral(M,f) = Integral(M,max+f) - Integral(M,max-f);
theorem :: MESFUN11:55
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, E be Element of S
st E c= dom f & f is_measurable_on E holds
Integral(M,(-f)|E) = - Integral(M,f|E);
theorem :: MESFUN11:56
for X be non empty set, S be SigmaField of X, f be PartFunc of X,ExtREAL
st (ex A be Element of S st A = dom f & f is_measurable_on A)
& f qua ext-real-valued Function is nonpositive
ex F be Functional_Sequence of X,ExtREAL st (for n be Nat
holds F.n is_simple_func_in S & dom(F.n) = dom f) & (for n be Nat holds F.n is
nonpositive) & (for n,m be Nat st n <=m holds for x be Element of X st x in dom
f holds (F.n).x >= (F.m).x ) & for x be Element of X st x in dom f holds (F#x)
is convergent & lim(F#x) = f.x;
theorem :: MESFUN11:57
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f be nonpositive PartFunc of X,ExtREAL
st (ex A be Element of S st A = dom f & f is_measurable_on A) holds
Integral(M,f) = - integral+(M,max- f) & Integral(M,f) = - integral+(M,-f)
& Integral(M,f) = - Integral(M,-f);
theorem :: MESFUN11:58
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be nonpositive PartFunc of X,ExtREAL st f is_simple_func_in S
holds Integral(M,f) = -integral'(M,-f) & Integral(M,f) = -integral'(M,max-f);
theorem :: MESFUN11:59
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X, ExtREAL, c be Real
st f is_simple_func_in S & f is nonnegative
holds Integral(M,c(#)f) = c * integral'(M,f);
theorem :: MESFUN11:60
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X, ExtREAL, c be Real
st f is_simple_func_in S & f is nonpositive
holds Integral(M,c(#)f) = (-c) * integral'(M,-f)
& Integral(M,c(#)f) = -(c * integral'(M,-f));
theorem :: MESFUN11:61
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL st (ex A be Element of S st A = dom f & f
is_measurable_on A) & f is nonpositive holds 0 >= Integral(M,f);
theorem :: MESFUN11:62
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, A,B,E be Element of S
st E = dom f & f is_measurable_on E & f is nonpositive & A misses B
holds Integral(M,f|(A\/B)) = Integral(M,f|A)+Integral(M,f|B);
theorem :: MESFUN11:63
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, A,E be Element of S
st E = dom f & f is_measurable_on E & f is nonpositive
holds 0 >= Integral(M,f|A);
theorem :: MESFUN11:64
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, A,B,E be Element of S
st E = dom f & f is_measurable_on E & f is nonpositive & A c= B
holds Integral(M,f|A) >= Integral(M,f|B);
begin :: Convergent theorems for non positive function's integration
theorem :: MESFUN11:65
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f be PartFunc of X,ExtREAL st
E = dom f & f is_measurable_on E & f is nonpositive & M.(E /\
eq_dom(f,-infty)) <> 0 holds Integral(M,f) = -infty;
theorem :: MESFUN11:66
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f,g be PartFunc of X,ExtREAL st
E c= dom f & E c= dom g & f is_measurable_on E & g
is_measurable_on E & f is nonpositive & (for x be Element of X st x in E holds
g.x <= f.x ) holds Integral(M,g|E) <= Integral(M,f|E);
theorem :: MESFUN11:67
for X be non empty set, F be Functional_Sequence of X,ExtREAL,
S be SigmaField of X, E be Element of S, m be Nat st
F is with_the_same_dom & E = dom(F.0) &
(for n be Nat holds F.n is_measurable_on E & F.n is without+infty)
holds (Partial_Sums F).m is_measurable_on E;
theorem :: MESFUN11:68
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
F be Functional_Sequence of X,ExtREAL, E be Element of S,
I be ExtREAL_sequence, m be Nat
st E = dom(F.0) & F is additive & F is with_the_same_dom
& (for n be Nat holds
F.n is_measurable_on E & F.n is nonpositive & I.n = Integral(M,F.n))
holds Integral(M,(Partial_Sums F).m) = (Partial_Sums I).m;
theorem :: MESFUN11:69
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
F be Functional_Sequence of X,ExtREAL, E be Element of S,
f be PartFunc of X,ExtREAL
st E c= dom f & f is nonpositive & f is_measurable_on E &
(for n be Nat holds
F.n is_simple_func_in S & F.n is nonpositive & E c= dom(F.n)) &
(for x be Element of X st x in E holds F#x is summable & f.x = Sum(F#x))
holds ex I be ExtREAL_sequence st
(for n be Nat holds I.n = Integral(M,(F.n)|E)) & I is summable &
Integral(M,f|E) = Sum I;
theorem :: MESFUN11:70
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f be PartFunc of X,ExtREAL
st E c= dom f & f is nonpositive & f is_measurable_on E
holds
ex F be Functional_Sequence of X,ExtREAL st
F is additive
& (for n be Nat holds
F.n is_simple_func_in S & F.n is nonpositive & F.n is_measurable_on E)
& (for x be Element of X st x in E holds
F#x is summable & f.x = Sum(F#x))
& ex I be ExtREAL_sequence st
(for n be Nat holds I.n = Integral(M,(F.n)|E))
& I is summable
& Integral(M,f|E) = Sum I;
theorem :: MESFUN11:71
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
F be Functional_Sequence of X,ExtREAL, E be Element of S st
E = dom(F.0) & F is with_the_same_dom & (for n be Nat holds F.n
is nonpositive & F.n is_measurable_on E )
holds ex FF be sequence of
Funcs(NAT,PFuncs(X,ExtREAL)) st for n be Nat holds (for m be Nat holds (FF.n).m
is_simple_func_in S & dom((FF.n).m) = dom(F.n)) & (for m be Nat holds (FF.n).m
is nonpositive) & (for j,k be Nat st j <= k holds for x be Element of X st x in
dom(F.n) holds ((FF.n).j).x >= ((FF.n).k).x) & for x be Element of X st x in
dom(F.n) holds (FF.n)#x is convergent & lim((FF.n)#x) = (F.n).x;
theorem :: MESFUN11:72
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
F be Functional_Sequence of X,ExtREAL, E be Element of S
st E = dom(F.0) & F is additive & F is with_the_same_dom
& (for n be Nat holds F.n is_measurable_on E & F.n is nonpositive)
holds
ex I be ExtREAL_sequence st for n be Nat holds
I.n = Integral(M,F.n) & Integral(M,(Partial_Sums F).n) = (Partial_Sums I).n;
theorem :: MESFUN11:73
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
F be Functional_Sequence of X,ExtREAL, E be Element of S
st E c= dom(F.0) & F is additive & F is with_the_same_dom
& (for n be Nat holds F.n is nonpositive & F.n is_measurable_on E)
& (for x be Element of X st x in E holds F#x is summable)
holds ex I be ExtREAL_sequence st
(for n be Nat holds I.n = Integral(M,(F.n)|E))
& I is summable & Integral(M,(lim(Partial_Sums F))|E) = Sum I;
theorem :: MESFUN11:74
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
F be Functional_Sequence of X,ExtREAL, E be Element of S
st E = dom(F.0) & F.0 is nonpositive & F is with_the_same_dom
& (for n be Nat holds F.n is_measurable_on E)
& (for n,m be Nat st n <=m holds for x be Element of X st x in E
holds (F.n).x >= (F.m).x )
& (for x be Element of X st x in E holds F#x is convergent)
holds
ex I be ExtREAL_sequence st (for n be Nat holds I.n = Integral(M,F.n))
& I is convergent & Integral(M,lim F) = lim I;