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

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) )

( 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

F1 . i <= F2 . i ) holds

Sum F1 <= Sum F2

proof end;

notation
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;
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;

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

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)

for C being non empty Subset of REAL holds (f + g) || C = (f || C) + (g || C)

proof 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 );

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;

correctness

coherence

integral (f || A) is Real;

;

end;
let f be PartFunc of REAL,REAL;

correctness

coherence

integral (f || A) is Real;

;

:: 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);

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

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 ;

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 ;

for f being PartFunc of REAL,REAL st f | A is bounded_below holds

(f || A) | A is bounded_below ;

theorem :: INTEGRA5:9

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

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

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) )

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))

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

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) )

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

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

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)) )

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 ;

correctness

coherence

[.a,b.] is non empty closed_interval Subset of REAL;

by A1, MEASURE5:14;

end;
assume A1: a <= b ;

correctness

coherence

[.a,b.] is non empty closed_interval Subset of REAL;

by A1, MEASURE5:14;

:: deftheorem Def3 defines [' INTEGRA5:def 3 :

for a, b being Real st a <= b holds

['a,b'] = [.a,b.];

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;

coherence

( ( a <= b implies integral (f,['a,b']) is Real ) & ( not a <= b implies - (integral (f,['b,a'])) is Real ) );

consistency

for b_{1} being Real holds verum;

;

end;
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 integral (f,['a,b']) if a <= b

otherwise - (integral (f,['b,a']));

coherence

( ( a <= b implies integral (f,['a,b']) is Real ) & ( not a <= b implies - (integral (f,['b,a'])) is Real ) );

consistency

for b

;

:: 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'])) ) );

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)

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)

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))

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;