:: Absolutely Integrable Functions
:: by Noboru Endou
::
:: Received April 30, 2022
:: Copyright (c) 2022-2025 Association of Mizar Users

Th1: for seq being without-infty ExtREAL_sequence holds Partial_Sums seq is without-infty ExtREAL_sequence

proof end;

Th2: for seq being without+infty ExtREAL_sequence holds Partial_Sums seq is without+infty ExtREAL_sequence

proof end;

registration

let seq be without-infty ExtREAL_sequence;

cluster Partial_Sums seq -> without-infty ;

correctness
coherence
Partial_Sums seq is without-infty ;
by Th1;

end;

registration

let seq be without+infty ExtREAL_sequence;

cluster Partial_Sums seq -> without+infty ;

correctness
coherence
Partial_Sums seq is without+infty ;
by Th2;

end;

theorem Th3: :: MESFUN15:1

for f1 being without-infty ExtREAL_sequence
for f2 being without+infty ExtREAL_sequence holds
( Partial_Sums (f1 - f2) = (Partial_Sums f1) - (Partial_Sums f2) & Partial_Sums (f2 - f1) = (Partial_Sums f2) - (Partial_Sums f1) )

proof end;

theorem Th4: :: MESFUN15:2

for X, A being set
for f being PartFunc of X,REAL st f is nonpositive holds
f | A is nonpositive

proof end;

theorem Th5: :: MESFUN15:3

for X being set
for f being PartFunc of X,REAL st f is nonpositive holds
- f is nonnegative

proof end;

theorem Th6: :: MESFUN15:4

for f being PartFunc of REAL,REAL
for a being Real st f is_left_convergent_in a & f is non-decreasing holds
for x being Real st x in dom f & x < a holds
f . x <= lim_left (f,a)

proof end;

theorem :: MESFUN15:5

for f being PartFunc of REAL,REAL
for a being Real st f is_left_convergent_in a & f is non-increasing holds
for x being Real st x in dom f & x < a holds
f . x >= lim_left (f,a)

proof end;

theorem :: MESFUN15:6

for f being PartFunc of REAL,REAL
for a being Real st f is_right_convergent_in a & f is non-decreasing holds
for x being Real st x in dom f & a < x holds
f . x >= lim_right (f,a)

proof end;

theorem Th9: :: MESFUN15:7

for f being PartFunc of REAL,REAL
for a being Real st f is_right_convergent_in a & f is non-increasing holds
for x being Real st x in dom f & a < x holds
f . x <= lim_right (f,a)

proof end;

theorem Th10: :: MESFUN15:8

for f being PartFunc of REAL,REAL
for a being Real st f is convergent_in-infty & f is non-increasing holds
for x being Real st x in dom f holds
f . x <= lim_in-infty f

proof end;

theorem Th11: :: MESFUN15:9

for f being PartFunc of REAL,REAL
for a being Real st f is convergent_in+infty & f is non-decreasing holds
for x being Real st x in dom f holds
f . x <= lim_in+infty f

proof end;

theorem Th12: :: MESFUN15:10

for a, b being Real
for f being PartFunc of REAL,REAL st a <= b & [.a,b.] c= dom f & f | [.a,b.] is bounded & f | [.a,b.] is nonnegative holds
integral (f,a,b) >= 0

proof end;

theorem Th13: :: MESFUN15:11

for a, b being Real
for f being PartFunc of REAL,REAL st a <= b & [.a,b.] c= dom f & f | [.a,b.] is bounded & f is_integrable_on ['a,b'] & f | [.a,b.] is nonpositive holds
integral (f,a,b) <= 0

proof end;

theorem Th14: :: MESFUN15:12

for a, b, c, d being Real
for f being PartFunc of REAL,REAL st c <= d & [.c,d.] c= [.a,b.] & [.a,b.] c= dom f & f | [.a,b.] is bounded & f is_integrable_on ['a,b'] & f | [.a,b.] is nonnegative holds
integral (f,c,d) <= integral (f,a,b)

proof end;

theorem :: MESFUN15:13

for a, b, c, d being Real
for f being PartFunc of REAL,REAL st c <= d & [.c,d.] c= [.a,b.] & [.a,b.] c= dom f & f | [.a,b.] is bounded & f is_integrable_on ['a,b'] & f | [.a,b.] is nonpositive holds
integral (f,c,d) >= integral (f,a,b)

proof end;

theorem Th16: :: MESFUN15:14

for X being non empty set
for f being PartFunc of X,REAL
for E being set holds (R_EAL f) | E = R_EAL (f | E)

proof end;

Lm1: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A being Element of S
for E being SetSequence of S st f is nonnegative & f is A -measurable & A = dom f & E is disjoint_valued & A = Union E holds
ex I being nonnegative ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(f | (E . n))) ) & I is summable & Integral (M,f) = Sum I )

proof end;

theorem Th17: :: MESFUN15:15

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A being Element of S
for E being SetSequence of S st f is A -measurable & A = dom f & E is disjoint_valued & A = Union E & ( integral+ (M,(max+ f)) < +infty or integral+ (M,(max- f)) < +infty ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(f | (E . n))) ) & I is summable & Integral (M,f) = Sum I )

proof end;

Lm2: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A, B being Element of S st dom f = A \/ B & f is A \/ B -measurable & A misses B & ( integral+ (M,(max+ f)) < +infty or integral+ (M,(max- f)) < +infty ) holds
Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

proof end;

theorem Th18: :: MESFUN15:16

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A, B being Element of S st A \/ B c= dom f & f is A \/ B -measurable & A misses B & ( integral+ (M,(max+ (f | (A \/ B)))) < +infty or integral+ (M,(max- (f | (A \/ B)))) < +infty ) holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

proof end;

theorem Th19: :: MESFUN15:17

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A being Element of S
for E being SetSequence of S st f is A -measurable & A = dom f & E is non-descending & lim E c= A & M . (A \ (lim E)) = 0 & ( integral+ (M,(max+ f)) < +infty or integral+ (M,(max- f)) < +infty ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(f | ((Partial_Union E) . n))) ) & I is convergent & Integral (M,f) = lim I )

proof end;

theorem Th20: :: MESFUN15:18

for X, Y being non empty set
for A being set
for F being sequence of X
for G being sequence of Y st ( for n being Element of NAT holds G . n = A /\ (F . n) ) holds
union (rng G) = A /\ (union (rng F))

proof end;

theorem Th21: :: MESFUN15:19

for X being non empty set
for S being SigmaField of X
for E being sequence of S
for f being PartFunc of X,ExtREAL st ( for n being Nat holds f is E . n -measurable ) holds
f is Union E -measurable

proof end;

Lm3: for a, b being Real
for E being sequence of (bool REAL) st a < b & ( for n being Nat holds E . n = [.a,(b - ((b - a) / (n + 1))).] ) holds
( E is non-descending & E is convergent & Union E = [.a,b.[ )

proof end;

theorem Th22: :: MESFUN15:20

for a, b being Real
for n being Nat st a < b holds
( a <= b - ((b - a) / (n + 1)) & b - ((b - a) / (n + 1)) < b & a < a + ((b - a) / (n + 1)) & a + ((b - a) / (n + 1)) <= b )

proof end;

theorem Th23: :: MESFUN15:21

for a, b being Real st a < b holds
ex E being SetSequence of L-Field st
( ( for n being Nat holds
( E . n = [.a,(b - ((b - a) / (n + 1))).] & E . n c= [.a,b.[ & E . n is non empty closed_interval Subset of REAL ) ) & E is non-descending & E is convergent & Union E = [.a,b.[ )

proof end;

Lm4: for a, b being Real
for E being sequence of (bool REAL) st a < b & ( for n being Nat holds E . n = [.(a + ((b - a) / (n + 1))),b.] ) holds
( E is non-descending & E is convergent & Union E = ].a,b.] )

proof end;

theorem Th24: :: MESFUN15:22

for a, b being Real st a < b holds
ex E being SetSequence of L-Field st
( ( for n being Nat holds
( E . n = [.(a + ((b - a) / (n + 1))),b.] & E . n c= ].a,b.] & E . n is non empty closed_interval Subset of REAL ) ) & E is non-descending & E is convergent & Union E = ].a,b.] )

proof end;

Lm5: for a being Real
for E being sequence of (bool REAL) st ( for n being Nat holds E . n = [.a,(a + n).] ) holds
( E is non-descending & E is convergent & Union E = [.a,+infty.[ )

proof end;

theorem Th25: :: MESFUN15:23

for a being Real ex E being SetSequence of L-Field st
( ( for n being Nat holds E . n = [.a,(a + n).] ) & E is non-descending & E is convergent & Union E = [.a,+infty.[ )

proof end;

Lm6: for a being Real
for E being sequence of (bool REAL) st ( for n being Nat holds E . n = [.(a - n),a.] ) holds
( E is non-descending & E is convergent & Union E = ].-infty,a.] )

proof end;

theorem Th26: :: MESFUN15:24

for a being Real ex E being SetSequence of L-Field st
( ( for n being Nat holds E . n = [.(a - n),a.] ) & E is non-descending & E is convergent & Union E = ].-infty,a.] )

proof end;

theorem Th27: :: MESFUN15:25

for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for A being thin of M holds A in COM (S,M)

proof end;

theorem Th28: :: MESFUN15:26

for r being Real holds {r} in L-Field

proof end;

theorem Th29: :: MESFUN15:27

for X being non empty set
for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,ExtREAL st E = {} holds
f is E -measurable

proof end;

theorem Th30: :: MESFUN15:28

for X being non empty set
for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st E = {} holds
f is E -measurable

proof end;

theorem Th31: :: MESFUN15:29

for r being Real
for E being Element of L-Field
for f being PartFunc of REAL,ExtREAL st E = {r} holds
f is E -measurable

proof end;

theorem :: MESFUN15:30

for r being Real
for E being Element of L-Field
for f being PartFunc of REAL,REAL st E = {r} holds
f is E -measurable

proof end;

theorem Th33: :: MESFUN15:31

for a, b being Real
for f being PartFunc of REAL,REAL st [.a,b.[ c= dom f & f is_right_improper_integrable_on a,b holds
for E being Element of L-Field st E c= [.a,b.[ holds
f is E -measurable

proof end;

theorem Th34: :: MESFUN15:32

for a, b being Real
for f being PartFunc of REAL,REAL st ].a,b.] c= dom f & f is_left_improper_integrable_on a,b holds
for E being Element of L-Field st E c= ].a,b.] holds
f is E -measurable

proof end;

theorem Th35: :: MESFUN15:33

for a, b being Real
for f being PartFunc of REAL,REAL st ].a,b.[ c= dom f & f is_improper_integrable_on a,b holds
for E being Element of L-Field st E c= ].a,b.[ holds
f is E -measurable

proof end;

theorem Th36: :: MESFUN15:34

for a being Real
for f being PartFunc of REAL,REAL st [.a,+infty.[ c= dom f & f is_+infty_improper_integrable_on a holds
for E being Element of L-Field st E c= [.a,+infty.[ holds
f is E -measurable

proof end;

theorem Th37: :: MESFUN15:35

for a being Real
for f being PartFunc of REAL,REAL st ].-infty,a.] c= dom f & f is_-infty_improper_integrable_on a holds
for E being Element of L-Field st E c= ].-infty,a.] holds
f is E -measurable

proof end;

theorem Th38: :: MESFUN15:36

for f being PartFunc of REAL,REAL st dom f = REAL & f is_improper_integrable_on_REAL holds
for E being Element of L-Field holds f is E -measurable

proof end;

theorem Th39: :: MESFUN15:37

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A being Element of S st A = dom f & f is A -measurable holds
Integral (M,(- f)) = - (Integral (M,f))

proof end;

theorem Th40: :: MESFUN15:38

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A c= B holds
Integral (M,(f | A)) >= Integral (M,(f | B))

proof end;

Lm7: for f being PartFunc of REAL,REAL
for a, b being Real
for A being non empty Subset of REAL st ].a,b.] c= dom f & A = ].a,b.] & f is_left_improper_integrable_on a,b & f | A is nonnegative & not f is_left_ext_Riemann_integrable_on a,b holds
( left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & Integral (L-Meas,(f | A)) = +infty )

proof end;

Lm8: for f being PartFunc of REAL,REAL
for a, b being Real
for A being non empty Subset of REAL st [.a,b.[ c= dom f & A = [.a,b.[ & f is_right_improper_integrable_on a,b & f | A is nonnegative & not f is_right_ext_Riemann_integrable_on a,b holds
( right_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & Integral (L-Meas,(f | A)) = +infty )

proof end;

theorem Th41: :: MESFUN15:39

for f being PartFunc of REAL,REAL
for a, b being Real
for A being non empty Subset of REAL st [.a,b.[ c= dom f & A = [.a,b.[ & f is_right_improper_integrable_on a,b & f | A is nonnegative holds
( right_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( f is_right_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) & ( not f is_right_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = +infty ) )

proof end;

theorem :: MESFUN15:40

for f being PartFunc of REAL,REAL
for a, b being Real
for A being non empty Subset of REAL st [.a,b.[ c= dom f & A = [.a,b.[ & f is_right_improper_integrable_on a,b & f | A is nonpositive holds
( right_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( f is_right_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) & ( not f is_right_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = -infty ) )

proof end;

theorem Th43: :: MESFUN15:41

for f being PartFunc of REAL,REAL
for a, b being Real
for A being non empty Subset of REAL st ].a,b.] c= dom f & A = ].a,b.] & f is_left_improper_integrable_on a,b & f | A is nonnegative holds
( left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( f is_left_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) & ( not f is_left_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = +infty ) )

proof end;

theorem :: MESFUN15:42

for f being PartFunc of REAL,REAL
for a, b being Real
for A being non empty Subset of REAL st ].a,b.] c= dom f & A = ].a,b.] & f is_left_improper_integrable_on a,b & f | A is nonpositive holds
( left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( f is_left_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) & ( not f is_left_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = -infty ) )

proof end;

theorem Th45: :: MESFUN15:43

for f being PartFunc of REAL,REAL
for a, b being Real
for A being non empty Subset of REAL st ].a,b.[ c= dom f & A = ].a,b.[ & f is_improper_integrable_on a,b & f | A is nonnegative holds
( improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( ex c being Real st
( a < c & c < b & f is_left_ext_Riemann_integrable_on a,c & f is_right_ext_Riemann_integrable_on c,b ) implies f | A is_integrable_on L-Meas ) & ( ( for c being Real st a < c & c < b & f is_left_ext_Riemann_integrable_on a,c holds
not f is_right_ext_Riemann_integrable_on c,b ) implies Integral (L-Meas,(f | A)) = +infty ) )

proof end;

theorem :: MESFUN15:44

for f being PartFunc of REAL,REAL
for a, b being Real
for A being non empty Subset of REAL st ].a,b.[ c= dom f & A = ].a,b.[ & f is_improper_integrable_on a,b & f | A is nonpositive holds
( improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( ex c being Real st
( a < c & c < b & f is_left_ext_Riemann_integrable_on a,c & f is_right_ext_Riemann_integrable_on c,b ) implies f | A is_integrable_on L-Meas ) & ( ( for c being Real st a < c & c < b & f is_left_ext_Riemann_integrable_on a,c holds
not f is_right_ext_Riemann_integrable_on c,b ) implies Integral (L-Meas,(f | A)) = -infty ) )

proof end;

Lm9: for f being PartFunc of REAL,REAL
for b being Real
for A being non empty Subset of REAL st left_closed_halfline b c= dom f & A = left_closed_halfline b & f is_-infty_improper_integrable_on b & f is nonnegative & not f is_-infty_ext_Riemann_integrable_on b holds
( improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) & Integral (L-Meas,(f | A)) = +infty )

proof end;

theorem Th47: :: MESFUN15:45

for f being PartFunc of REAL,REAL
for b being Real
for A being non empty Subset of REAL st left_closed_halfline b c= dom f & A = left_closed_halfline b & f is_-infty_improper_integrable_on b & f is nonnegative holds
( improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) & ( f is_-infty_ext_Riemann_integrable_on b implies f | A is_integrable_on L-Meas ) & ( not f is_-infty_ext_Riemann_integrable_on b implies Integral (L-Meas,(f | A)) = +infty ) )

proof end;

theorem Th48: :: MESFUN15:46

for f being PartFunc of REAL,REAL
for b being Real
for A being non empty Subset of REAL st left_closed_halfline b c= dom f & A = left_closed_halfline b & f is_-infty_improper_integrable_on b & f is nonpositive holds
( improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) & ( f is_-infty_ext_Riemann_integrable_on b implies f | A is_integrable_on L-Meas ) & ( not f is_-infty_ext_Riemann_integrable_on b implies Integral (L-Meas,(f | A)) = -infty ) )

proof end;

Lm10: for f being PartFunc of REAL,REAL
for a being Real
for A being non empty Subset of REAL st right_closed_halfline a c= dom f & A = right_closed_halfline a & f is_+infty_improper_integrable_on a & f is nonnegative & not f is_+infty_ext_Riemann_integrable_on a holds
( improper_integral_+infty (f,a) = Integral (L-Meas,(f | A)) & Integral (L-Meas,(f | A)) = +infty )

proof end;

theorem Th49: :: MESFUN15:47

for f being PartFunc of REAL,REAL
for a being Real
for A being non empty Subset of REAL st right_closed_halfline a c= dom f & A = right_closed_halfline a & f is_+infty_improper_integrable_on a & f is nonnegative holds
( improper_integral_+infty (f,a) = Integral (L-Meas,(f | A)) & ( f is_+infty_ext_Riemann_integrable_on a implies f | A is_integrable_on L-Meas ) & ( not f is_+infty_ext_Riemann_integrable_on a implies Integral (L-Meas,(f | A)) = +infty ) )

proof end;

theorem Th50: :: MESFUN15:48

for f being PartFunc of REAL,REAL
for a being Real
for A being non empty Subset of REAL st right_closed_halfline a c= dom f & A = right_closed_halfline a & f is_+infty_improper_integrable_on a & f is nonpositive holds
( improper_integral_+infty (f,a) = Integral (L-Meas,(f | A)) & ( f is_+infty_ext_Riemann_integrable_on a implies f | A is_integrable_on L-Meas ) & ( not f is_+infty_ext_Riemann_integrable_on a implies Integral (L-Meas,(f | A)) = -infty ) )

proof end;

theorem Th51: :: MESFUN15:49

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A, B being Element of S st ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative holds
integral+ (M,(f | (A \/ B))) <= (integral+ (M,(f | A))) + (integral+ (M,(f | B)))

proof end;

theorem Th52: :: MESFUN15:50

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A, B being set st A c= dom f & B c= dom f & f | A is_integrable_on M & f | B is_integrable_on M holds
f | (A \/ B) is_integrable_on M

proof end;

theorem Th53: :: MESFUN15:51

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A, B being set st A c= dom f & B c= dom f & f | A is_integrable_on M & f | B is_integrable_on M holds
f | (A \/ B) is_integrable_on M

proof end;

theorem Th54: :: MESFUN15:52

for f being PartFunc of REAL,REAL
for a being Real
for A being non empty Subset of REAL st dom f = REAL & f is_improper_integrable_on_REAL & f is nonnegative holds
( improper_integral_on_REAL f = Integral (L-Meas,f) & ( f is infty_ext_Riemann_integrable implies f is_integrable_on L-Meas ) & ( not f is infty_ext_Riemann_integrable implies Integral (L-Meas,f) = +infty ) )

proof end;

theorem :: MESFUN15:53

for f being PartFunc of REAL,REAL
for a being Real
for A being non empty Subset of REAL st dom f = REAL & f is_improper_integrable_on_REAL & f is nonpositive holds
( improper_integral_on_REAL f = Integral (L-Meas,f) & ( f is infty_ext_Riemann_integrable implies f is_integrable_on L-Meas ) & ( not f is infty_ext_Riemann_integrable implies Integral (L-Meas,f) = -infty ) )

proof end;

theorem :: MESFUN15:54

for f being PartFunc of REAL,REAL
for a, b being Real st [.a,b.[ = dom f holds
ex F being Functional_Sequence of REAL,REAL st
( ( for n being Nat holds
( dom (F . n) = dom f & ( for x being Real st x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = f . x ) & ( for x being Real st not x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = 0 ) ) ) & lim (R_EAL F) = f )

proof end;

theorem Th57: :: MESFUN15:55

for f being PartFunc of REAL,REAL
for a, b being Real st a < b & [.a,b.[ c= dom f & f is_right_improper_integrable_on a,b & abs f is_right_ext_Riemann_integrable_on a,b holds
( f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) <= right_improper_integral ((abs f),a,b) & right_improper_integral ((abs f),a,b) < +infty )

proof end;

theorem Th58: :: MESFUN15:56

for f being PartFunc of REAL,REAL
for a, b being Real st a < b & ].a,b.] c= dom f & f is_left_improper_integrable_on a,b & abs f is_left_ext_Riemann_integrable_on a,b holds
( f is_left_ext_Riemann_integrable_on a,b & left_improper_integral (f,a,b) <= left_improper_integral ((abs f),a,b) & left_improper_integral ((abs f),a,b) < +infty )

proof end;

theorem Th59: :: MESFUN15:57

for f being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st A c= dom f holds
( max+ (f || A) = max+ (f | A) & max- (f || A) = max- (f | A) )

proof end;

theorem Th60: :: MESFUN15:58

for f being PartFunc of REAL,REAL
for b being Real st left_closed_halfline b c= dom f & f is_-infty_improper_integrable_on b & abs f is_-infty_ext_Riemann_integrable_on b holds
( f is_-infty_ext_Riemann_integrable_on b & improper_integral_-infty (f,b) <= improper_integral_-infty ((abs f),b) & improper_integral_-infty ((abs f),b) < +infty )

proof end;

theorem Th61: :: MESFUN15:59

for f being PartFunc of REAL,REAL
for a being Real st right_closed_halfline a c= dom f & f is_+infty_improper_integrable_on a & abs f is_+infty_ext_Riemann_integrable_on a holds
( f is_+infty_ext_Riemann_integrable_on a & improper_integral_+infty (f,a) <= improper_integral_+infty ((abs f),a) & improper_integral_+infty ((abs f),a) < +infty )

proof end;

theorem Th62: :: MESFUN15:60

for f being PartFunc of REAL,REAL
for a, b being Real st a <= b & [.a,b.] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds
( max+ f is_integrable_on ['a,b'] & max- f is_integrable_on ['a,b'] & 2 * (integral ((max+ f),a,b)) = (integral (f,a,b)) + (integral ((abs f),a,b)) & 2 * (integral ((max- f),a,b)) = (- (integral (f,a,b))) + (integral ((abs f),a,b)) & integral (f,a,b) = (integral ((max+ f),a,b)) - (integral ((max- f),a,b)) )

proof end;

theorem Th63: :: MESFUN15:61

for f being PartFunc of REAL,REAL
for a, b being Real st a < b & ].a,b.] c= dom f & f is_left_ext_Riemann_integrable_on a,b & abs f is_left_ext_Riemann_integrable_on a,b holds
max+ f is_left_ext_Riemann_integrable_on a,b

proof end;

theorem Th64: :: MESFUN15:62

for f being PartFunc of REAL,REAL
for a, b being Real st a < b & [.a,b.[ c= dom f & f is_right_ext_Riemann_integrable_on a,b & abs f is_right_ext_Riemann_integrable_on a,b holds
max+ f is_right_ext_Riemann_integrable_on a,b

proof end;

theorem Th65: :: MESFUN15:63

for f being PartFunc of REAL,REAL
for b being Real st left_closed_halfline b c= dom f & f is_-infty_ext_Riemann_integrable_on b & abs f is_-infty_ext_Riemann_integrable_on b holds
max+ f is_-infty_ext_Riemann_integrable_on b

proof end;

theorem Th66: :: MESFUN15:64

for f being PartFunc of REAL,REAL
for a being Real st right_closed_halfline a c= dom f & f is_+infty_ext_Riemann_integrable_on a & abs f is_+infty_ext_Riemann_integrable_on a holds
max+ f is_+infty_ext_Riemann_integrable_on a

proof end;

theorem Th67: :: MESFUN15:65

for f being PartFunc of REAL,REAL
for a, b being Real st a < b & ].a,b.] c= dom f & f is_left_ext_Riemann_integrable_on a,b & abs f is_left_ext_Riemann_integrable_on a,b holds
max- f is_left_ext_Riemann_integrable_on a,b

proof end;

theorem Th68: :: MESFUN15:66

for f being PartFunc of REAL,REAL
for a, b being Real st a < b & [.a,b.[ c= dom f & f is_right_ext_Riemann_integrable_on a,b & abs f is_right_ext_Riemann_integrable_on a,b holds
max- f is_right_ext_Riemann_integrable_on a,b

proof end;

theorem Th69: :: MESFUN15:67

for f being PartFunc of REAL,REAL
for b being Real st left_closed_halfline b c= dom f & f is_-infty_ext_Riemann_integrable_on b & abs f is_-infty_ext_Riemann_integrable_on b holds
max- f is_-infty_ext_Riemann_integrable_on b

proof end;

theorem Th70: :: MESFUN15:68

for f being PartFunc of REAL,REAL
for a being Real st right_closed_halfline a c= dom f & f is_+infty_ext_Riemann_integrable_on a & abs f is_+infty_ext_Riemann_integrable_on a holds
max- f is_+infty_ext_Riemann_integrable_on a

proof end;

theorem Th71: :: MESFUN15:69

for f being PartFunc of REAL,REAL
for a, b being Real st ].a,b.] c= dom f & max+ f is_left_ext_Riemann_integrable_on a,b & max- f is_left_ext_Riemann_integrable_on a,b holds
( f is_left_ext_Riemann_integrable_on a,b & left_improper_integral (f,a,b) = (left_improper_integral ((max+ f),a,b)) - (left_improper_integral ((max- f),a,b)) )

proof end;

theorem Th72: :: MESFUN15:70

for f being PartFunc of REAL,REAL
for a, b being Real st [.a,b.[ c= dom f & max+ f is_right_ext_Riemann_integrable_on a,b & max- f is_right_ext_Riemann_integrable_on a,b holds
( f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) = (right_improper_integral ((max+ f),a,b)) - (right_improper_integral ((max- f),a,b)) )

proof end;

theorem Th73: :: MESFUN15:71

for f being PartFunc of REAL,REAL
for b being Real st left_closed_halfline b c= dom f & max+ f is_-infty_ext_Riemann_integrable_on b & max- f is_-infty_ext_Riemann_integrable_on b holds
( f is_-infty_ext_Riemann_integrable_on b & improper_integral_-infty (f,b) = (improper_integral_-infty ((max+ f),b)) - (improper_integral_-infty ((max- f),b)) )

proof end;

theorem Th74: :: MESFUN15:72

for f being PartFunc of REAL,REAL
for a being Real st right_closed_halfline a c= dom f & max+ f is_+infty_ext_Riemann_integrable_on a & max- f is_+infty_ext_Riemann_integrable_on a holds
( f is_+infty_ext_Riemann_integrable_on a & improper_integral_+infty (f,a) = (improper_integral_+infty ((max+ f),a)) - (improper_integral_+infty ((max- f),a)) )

proof end;

theorem Th75: :: MESFUN15:73

for f being PartFunc of REAL,REAL
for a, b being Real
for A being non empty Subset of REAL st ].a,b.] c= dom f & A = ].a,b.] & f is_left_improper_integrable_on a,b & abs f is_left_ext_Riemann_integrable_on a,b & f | A is nonnegative holds
( f | A is_integrable_on L-Meas & left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) )

proof end;

theorem Th76: :: MESFUN15:74

for f being PartFunc of REAL,REAL
for a, b being Real
for A being non empty Subset of REAL st [.a,b.[ c= dom f & A = [.a,b.[ & f is_right_improper_integrable_on a,b & abs f is_right_ext_Riemann_integrable_on a,b & f | A is nonnegative holds
( f | A is_integrable_on L-Meas & right_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) )

proof end;

theorem Th77: :: MESFUN15:75

for f being PartFunc of REAL,REAL
for b being Real
for A being non empty Subset of REAL st left_closed_halfline b c= dom f & A = left_closed_halfline b & f is_-infty_improper_integrable_on b & abs f is_-infty_ext_Riemann_integrable_on b & f is nonnegative holds
( f | A is_integrable_on L-Meas & improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) )

proof end;

theorem Th78: :: MESFUN15:76

for f being PartFunc of REAL,REAL
for a being Real
for A being non empty Subset of REAL st right_closed_halfline a c= dom f & A = right_closed_halfline a & f is_+infty_improper_integrable_on a & abs f is_+infty_ext_Riemann_integrable_on a & f is nonnegative holds
( f | A is_integrable_on L-Meas & improper_integral_+infty (f,a) = Integral (L-Meas,(f | A)) )

proof end;

theorem :: MESFUN15:77

for f being PartFunc of REAL,REAL
for a, b being Real st a < b & [.a,b.[ c= dom f & f is_right_improper_integrable_on a,b & abs f is_right_ext_Riemann_integrable_on a,b holds
max+ f is_right_ext_Riemann_integrable_on a,b

proof end;

theorem Th80: :: MESFUN15:78

for f being PartFunc of REAL,REAL
for a, b being Real
for A being non empty Subset of REAL st [.a,b.[ c= dom f & A = [.a,b.[ & f is_right_improper_integrable_on a,b & abs f is_right_ext_Riemann_integrable_on a,b holds
( f | A is_integrable_on L-Meas & right_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) )

proof end;

theorem Th81: :: MESFUN15:79

for f being PartFunc of REAL,REAL
for a, b being Real
for A being non empty Subset of REAL st ].a,b.] c= dom f & A = ].a,b.] & f is_left_improper_integrable_on a,b & abs f is_left_ext_Riemann_integrable_on a,b holds
( f | A is_integrable_on L-Meas & left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) )

proof end;

theorem :: MESFUN15:80

for f being PartFunc of REAL,REAL
for a, b being Real
for A being non empty Subset of REAL st ].a,b.[ c= dom f & A = ].a,b.[ & f is_improper_integrable_on a,b & ex c being Real st
( a < c & c < b & abs f is_left_ext_Riemann_integrable_on a,c & abs f is_right_ext_Riemann_integrable_on c,b ) holds
( f | A is_integrable_on L-Meas & improper_integral (f,a,b) = Integral (L-Meas,(f | A)) )

proof end;

theorem Th83: :: MESFUN15:81

for f being PartFunc of REAL,REAL
for b being Real
for A being non empty Subset of REAL st left_closed_halfline b c= dom f & A = left_closed_halfline b & f is_-infty_improper_integrable_on b & abs f is_-infty_ext_Riemann_integrable_on b holds
( f | A is_integrable_on L-Meas & improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) )

proof end;

theorem Th84: :: MESFUN15:82

for f being PartFunc of REAL,REAL
for a being Real
for A being non empty Subset of REAL st right_closed_halfline a c= dom f & A = right_closed_halfline a & f is_+infty_improper_integrable_on a & abs f is_+infty_ext_Riemann_integrable_on a holds
( f | A is_integrable_on L-Meas & improper_integral_+infty (f,a) = Integral (L-Meas,(f | A)) )

proof end;

theorem :: MESFUN15:83

for f being PartFunc of REAL,REAL st dom f = REAL & f is_improper_integrable_on_REAL & abs f is infty_ext_Riemann_integrable holds
( f is_integrable_on L-Meas & improper_integral_on_REAL f = Integral (L-Meas,f) )

proof end;