:: INTEGRA5 semantic presentation

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 Nat st i in dom F1 holds
F1 . i <= F2 . i ) holds
Sum F1 <= Sum F2

proof end;

definition

let C be non empty Subset of REAL ;
let f be PartFunc of REAL , REAL ;
func f || C -> PartFunc of C, REAL equals :: INTEGRA5:def 1
f | C;
correctness by PARTFUN1:43;

end;

:: deftheorem defines || INTEGRA5:def 1 :

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 closed-interval Subset of REAL ;
let f be PartFunc of REAL , REAL ;
pred f is_integrable_on A means :Def2: :: INTEGRA5:def 2
f || A is_integrable_on A;

end;

:: deftheorem Def2 defines is_integrable_on INTEGRA5:def 2 :

definition

let A be closed-interval Subset of REAL ;
let f be PartFunc of REAL , REAL ;
func integral f,A -> Real equals :: INTEGRA5:def 3
integral (f || A);
correctness ;

end;

:: deftheorem defines integral INTEGRA5:def 3 :

theorem Th6: :: INTEGRA5:6

for A being 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 Th7: :: INTEGRA5:7

for A being closed-interval Subset of REAL
for f being PartFunc of REAL , REAL st f is_bounded_above_on A holds
f || A is_bounded_above_on A

proof end;

theorem Th8: :: INTEGRA5:8

for A being closed-interval Subset of REAL
for f being PartFunc of REAL , REAL st f is_bounded_below_on A holds
f || A is_bounded_below_on A

proof end;

theorem Th9: :: INTEGRA5:9

for A being closed-interval Subset of REAL
for f being PartFunc of REAL , REAL st f is_bounded_on A holds
f || A is_bounded_on A

proof end;

theorem Th10: :: INTEGRA5:10

for A being closed-interval Subset of REAL
for f being PartFunc of REAL , REAL st f is_continuous_on A holds
f is_bounded_on A

proof end;

theorem Th11: :: INTEGRA5:11

for A being closed-interval Subset of REAL
for f being PartFunc of REAL , REAL st f is_continuous_on A holds
f is_integrable_on A

proof end;

theorem Th12: :: INTEGRA5:12

for A being closed-interval Subset of REAL
for X being set
for f being PartFunc of REAL , REAL
for D being Element of divs A st A c= X & f is_differentiable_on X & f `| X is_bounded_on A holds
( lower_sum ((f `| X) || A),D <= (f . (sup A)) - (f . (inf A)) & (f . (sup A)) - (f . (inf A)) <= upper_sum ((f `| X) || A),D )

proof end;

theorem Th13: :: INTEGRA5:13

for A being 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 is_bounded_on A holds
integral (f `| X),A = (f . (sup A)) - (f . (inf A))

proof end;

theorem Th14: :: INTEGRA5:14

for A being closed-interval Subset of REAL
for f being PartFunc of REAL , REAL st f is_non_decreasing_on A & A c= dom f holds
rng (f | A) is bounded

proof end;

theorem Th15: :: INTEGRA5:15

for A being closed-interval Subset of REAL
for f being PartFunc of REAL , REAL st f is_non_decreasing_on A & A c= dom f holds
( inf (rng (f | A)) = f . (inf A) & sup (rng (f | A)) = f . (sup A) )

proof end;

Lm1: for A being closed-interval Subset of REAL
for f being PartFunc of REAL , REAL st f is_non_decreasing_on A & A c= dom f holds
f is_integrable_on A

proof end;

theorem :: INTEGRA5:16

for A being closed-interval Subset of REAL
for f being PartFunc of REAL , REAL st f is_monotone_on A & A c= dom f holds
f is_integrable_on A

proof end;

theorem Th17: :: INTEGRA5:17

for f being PartFunc of REAL , REAL
for A, B being closed-interval Subset of REAL st f is_continuous_on A & 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 closed-interval Subset of REAL
for X being set st A c= X & f is_differentiable_on X & f `| X is_continuous_on A & inf A = inf B & sup B = inf C & sup C = sup 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 number ;
assume A1: a <= b ;
func ['a,b'] -> closed-interval Subset of REAL equals :Def4: :: INTEGRA5:def 4
[.a,b.];
correctness

proof end;

end;

:: deftheorem Def4 defines [' INTEGRA5:def 4 :

definition

let a, b be real number ;
let f be PartFunc of REAL , REAL ;
func integral f,a,b -> Real equals :Def5: :: INTEGRA5:def 5
integral f,['a,b'] if a <= b
otherwise - (integral f,['b,a']);
correctness ;

end;

:: deftheorem Def5 defines integral INTEGRA5:def 5 :

theorem :: INTEGRA5:19

for f being PartFunc of REAL , REAL
for A being 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 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 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 is_bounded_on A & g `| X is_integrable_on A & g `| X is_bounded_on A holds
integral ((f `| X) (#) g),A = (((f . (sup A)) * (g . (sup A))) - ((f . (inf A)) * (g . (inf A)))) - (integral (f (#) (g `| X)),A)

proof end;