:: Definition of Integrability for Partial Functions from REAL to REAL and Integrability for Continuous Functions
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received March 23, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

theorem Th1: :: INTEGRA5:1
for F, F1, F2 being FinSequence of REAL
for r1, r2 being Real st ( F1 = <*r1*> ^ F or F1 = F ^ <*r1*> ) &amp; ( F2 = <*r2*> ^ F or F2 = F ^ <*r2*> ) holds
Sum (F1 - F2) = r1 - r2
proofend;

theorem Th2: :: INTEGRA5:2
for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
( len (F1 + F2) = len F1 &amp; len (F1 - F2) = len F1 &amp; Sum (F1 + F2) = (Sum F1) + (Sum F2) &amp; Sum (F1 - F2) = (Sum F1) - (Sum F2) )
proofend;

theorem Th3: :: INTEGRA5:3
for F1, F2 being FinSequence of REAL st len F1 = len F2 &amp; ( for i being Element of NAT st i in dom F1 holds
F1 . i <= F2 . i ) holds
Sum F1 <= Sum F2
proofend;

begin

notation
let f be PartFunc of REAL,REAL;
let C be non empty Subset of REAL;
synonym f || C for f | C;
end;

definition
let f be PartFunc of REAL,REAL;
let C be non empty Subset of REAL;
:: original:||
redefine funcf || C ->  PartFunc of C,REAL;
correctness
coherence
f || C is PartFunc of C,REAL;
by PARTFUN1:10;
end;

theorem Th4: :: INTEGRA5:4
for f, g being PartFunc of REAL,REAL
for C being non empty Subset of REAL holds (f || C) (#) (g || C) = (f (#) g) || C
proofend;

theorem Th5: :: INTEGRA5:5
for f, g being PartFunc of REAL,REAL
for C being non empty Subset of REAL holds (f + g) || C = (f || C) + (g || C)
proofend;

definition
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL,REAL;
predf is_integrable_on A means :Def1: :: INTEGRA5:def 1
f || A is integrable ;
end;

:: deftheorem Def1 defines is_integrable_on INTEGRA5:def_1_:_
 for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL holds
( f is_integrable_on A iff f || A is integrable );

definition
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL,REAL;
func integral (f,A) ->  Real equals :: INTEGRA5:def 2
 integral (f || A);
correctness
coherence
integral (f || A) is Real;
;
end;

:: deftheorem  defines integral INTEGRA5:def_2_:_
 for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL holds integral (f,A) = integral (f || A);

theorem Th6: :: INTEGRA5:6
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st A c= dom f holds
f || A is total
proofend;

theorem :: INTEGRA5:7
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st f | A is bounded_above holds
(f || A) | A is bounded_above
proofend;

theorem :: INTEGRA5:8
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st f | A is bounded_below holds
(f || A) | A is bounded_below
proofend;

theorem :: INTEGRA5:9
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st f | A is bounded holds
(f || A) | A is bounded
proofend;

begin

theorem Th10: :: INTEGRA5:10
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st A c= dom f &amp; f | A is continuous holds
f | A is bounded
proofend;

theorem Th11: :: INTEGRA5:11
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st A c= dom f &amp; f | A is continuous holds
f is_integrable_on A
proofend;

theorem Th12: :: INTEGRA5:12
for A being non empty closed_interval Subset of REAL
for X being set
for f being PartFunc of REAL,REAL
for D being Division of A st A c= X &amp; f is_differentiable_on X &amp; (f `| X) | A is bounded holds
( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) &amp; (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) )
proofend;

:: [WP: ] Fundamental_Theorem_of_Integral_Calculus
theorem Th13: :: INTEGRA5:13
for A being non empty closed_interval Subset of REAL
for X being set
for f being PartFunc of REAL,REAL st A c= X &amp; f is_differentiable_on X &amp; f `| X is_integrable_on A &amp; (f `| X) | A is bounded holds
integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A))
proofend;

theorem Th14: :: INTEGRA5:14
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st f | A is non-decreasing &amp; A c= dom f holds
rng (f | A) is real-bounded
proofend;

theorem Th15: :: INTEGRA5:15
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st f | A is non-decreasing &amp; A c= dom f holds
( lower_bound (rng (f | A)) = f . (lower_bound A) &amp; upper_bound (rng (f | A)) = f . (upper_bound A) )
proofend;

Lm1:  for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st f | A is non-decreasing &amp; A c= dom f holds
f is_integrable_on A
proofend;

theorem :: INTEGRA5:16
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st f | A is monotone &amp; A c= dom f holds
f is_integrable_on A
proofend;

theorem :: INTEGRA5:17
for f being PartFunc of REAL,REAL
for A, B being non empty closed_interval Subset of REAL st A c= dom f &amp; f | A is continuous &amp; B c= A holds
f is_integrable_on B
proofend;

theorem :: INTEGRA5:18
for f being PartFunc of REAL,REAL
for A, B, C being non empty closed_interval Subset of REAL
for X being set st A c= X &amp; f is_differentiable_on X &amp; (f `| X) | A is continuous &amp; lower_bound A = lower_bound B &amp; upper_bound B = lower_bound C &amp; upper_bound C = upper_bound A holds
( B c= A &amp; C c= A &amp; integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) )
proofend;

definition
let a, b be real number ;
assume A1: a <= b ;
func['a,b'] ->  non empty closed_interval Subset of REAL equals :Def3: :: INTEGRA5:def 3
[.a,b.];
correctness
coherence
[.a,b.] is non empty closed_interval Subset of REAL;
proofend;
end;

:: deftheorem Def3 defines [' INTEGRA5:def_3_:_
 for a, b being real number st a <= b holds
['a,b'] = [.a,b.];

definition
let a, b be real number ;
let f be PartFunc of REAL,REAL;
func integral (f,a,b) ->  Real equals :Def4: :: INTEGRA5:def 4
 integral (f,['a,b']) if a <= b
otherwise  - (integral (f,['b,a']));
correctness
coherence
( ( a <= b implies integral (f,['a,b']) is Real ) &amp; ( not a <= b implies - (integral (f,['b,a'])) is Real ) );
consistency
for b1 being Real holds verum;
;
end;

:: deftheorem Def4 defines integral INTEGRA5:def_4_:_
 for a, b being real number
for f being PartFunc of REAL,REAL holds
( ( a <= b implies integral (f,a,b) = integral (f,['a,b']) ) &amp; ( not a <= b implies integral (f,a,b) = - (integral (f,['b,a'])) ) );

theorem :: INTEGRA5:19
for f being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.a,b.] holds
integral (f,A) = integral (f,a,b)
proofend;

theorem :: INTEGRA5:20
for f being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.b,a.] holds
- (integral (f,A)) = integral (f,a,b)
proofend;

theorem :: INTEGRA5:21
for A being non empty closed_interval Subset of REAL
for f, g being PartFunc of REAL,REAL
for X being open Subset of REAL st f is_differentiable_on X &amp; g is_differentiable_on X &amp; A c= X &amp; f `| X is_integrable_on A &amp; (f `| X) | A is bounded &amp; g `| X is_integrable_on A &amp; (g `| X) | A is bounded holds
integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A))
proofend;