:: 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-2021 Association of Mizar Users

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*> ) & ( F2 = <*r2*> ^ F or F2 = F ^ <*r2*> ) holds
Sum (F1 - F2) = r1 - r2

proof end;

theorem Th2: :: INTEGRA5:2

for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
( len (F1 + F2) = len F1 & len (F1 - F2) = len F1 & Sum (F1 + F2) = (Sum F1) + (Sum F2) & Sum (F1 - F2) = (Sum F1) - (Sum F2) )

proof end;

theorem Th3: :: INTEGRA5:3

for F1, F2 being FinSequence of REAL st len F1 = len F2 & ( for i being Element of NAT st i in dom F1 holds
F1 . i <= F2 . i ) holds
Sum F1 <= Sum F2

proof end;

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 func f || 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

proof end;

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)

proof end;

definition

let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL,REAL;

pred f is_integrable_on A means :: INTEGRA5:def 1
f || A is integrable ;

end;

:: deftheorem 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

proof end;

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 ;

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 ;

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 ;

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 & f | A is continuous holds
f | A is bounded

proof end;

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 & f | A is continuous holds
f is_integrable_on A

proof end;

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 & f is_differentiable_on X & (f `| X) | A is bounded holds
( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) )

proof end;

:: 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 & f is_differentiable_on X & f `| X is_integrable_on A & (f `| X) | A is bounded holds
integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A))

proof end;

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 & A c= dom f holds
rng (f | A) is real-bounded

proof end;

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 & A c= dom f holds
( lower_bound (rng (f | A)) = f . (lower_bound A) & upper_bound (rng (f | A)) = f . (upper_bound A) )

proof end;

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

proof end;

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 & A c= dom f holds
f is_integrable_on A

proof end;

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 & f | A is continuous & B c= A holds
f is_integrable_on B

proof end;

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 & f is_differentiable_on X & (f `| X) | A is continuous & lower_bound A = lower_bound B & upper_bound B = lower_bound C & upper_bound C = upper_bound A holds
( B c= A & C c= A & integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) )

proof end;

definition

let a, b be Real;
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;
by A1, MEASURE5:14;

end;

:: deftheorem Def3 defines [' INTEGRA5:def 3 :
for a, b being Real st a <= b holds
['a,b'] = [.a,b.];

definition

let a, b be Real;
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 ) & ( not a <= b implies - (integral (f,['b,a'])) is Real ) );
consistency
for b₁ being Real holds verum;
;

end;

:: deftheorem Def4 defines integral INTEGRA5:def 4 :
for a, b being Real
for f being PartFunc of REAL,REAL holds
( ( a <= b implies integral (f,a,b) = integral (f,['a,b']) ) & ( 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)

proof end;

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)

proof end;

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 & g is_differentiable_on X & A c= X & f `| X is_integrable_on A & (f `| X) | A is bounded & g `| X is_integrable_on A & (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))

proof end;