:: by Keiichi Miyajima and Yasunari Shidama

::

:: Received May 5, 2009

:: Copyright (c) 2009-2012 Association of Mizar Users

begin

definition

let A be non empty closed_interval Subset of REAL;

let f be Function of A,REAL;

let D be Division of A;

existence

ex b_{1} being FinSequence of REAL st

( len b_{1} = len D & ( for i being Nat st i in dom D holds

ex r being Element of REAL st

( r in rng (f | (divset (D,i))) & b_{1} . i = r * (vol (divset (D,i))) ) ) );

end;
let f be Function of A,REAL;

let D be Division of A;

mode middle_volume of f,D -> FinSequence of REAL means :Def1: :: INTEGR15:def 1

( len it = len D & ( for i being Nat st i in dom D holds

ex r being Element of REAL st

( r in rng (f | (divset (D,i))) & it . i = r * (vol (divset (D,i))) ) ) );

correctness ( len it = len D & ( for i being Nat st i in dom D holds

ex r being Element of REAL st

( r in rng (f | (divset (D,i))) & it . i = r * (vol (divset (D,i))) ) ) );

existence

ex b

( len b

ex r being Element of REAL st

( r in rng (f | (divset (D,i))) & b

proof end;

:: deftheorem Def1 defines middle_volume INTEGR15:def 1 :

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A

for b_{4} being FinSequence of REAL holds

( b_{4} is middle_volume of f,D iff ( len b_{4} = len D & ( for i being Nat st i in dom D holds

ex r being Element of REAL st

( r in rng (f | (divset (D,i))) & b_{4} . i = r * (vol (divset (D,i))) ) ) ) );

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A

for b

( b

ex r being Element of REAL st

( r in rng (f | (divset (D,i))) & b

Lm1: for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A

for F being middle_volume of f,D

for i being Nat st f | A is bounded_below & i in dom D holds

(lower_volume (f,D)) . i <= F . i

proof end;

Lm2: for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A

for e being Real st f | A is bounded_below & 0 < e holds

ex F being middle_volume of f,D st

for i being Nat st i in dom D holds

( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e )

proof end;

Lm3: for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A

for e being Real st f | A is bounded_above & 0 < e holds

ex F being middle_volume of f,D st

for i being Nat st i in dom D holds

( F . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < F . i )

proof end;

Lm4: for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A

for F being middle_volume of f,D

for i being Nat st f | A is bounded_above & i in dom D holds

F . i <= (upper_volume (f,D)) . i

proof end;

definition

let A be non empty closed_interval Subset of REAL;

let f be Function of A,REAL;

let D be Division of A;

let F be middle_volume of f,D;

correctness

coherence

Sum F is Real;

;

end;
let f be Function of A,REAL;

let D be Division of A;

let F be middle_volume of f,D;

correctness

coherence

Sum F is Real;

;

:: deftheorem defines middle_sum INTEGR15:def 2 :

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A

for F being middle_volume of f,D holds middle_sum (f,F) = Sum F;

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A

for F being middle_volume of f,D holds middle_sum (f,F) = Sum F;

theorem Th1: :: INTEGR15:1

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A

for F being middle_volume of f,D st f | A is bounded_below holds

lower_sum (f,D) <= middle_sum (f,F)

for f being Function of A,REAL

for D being Division of A

for F being middle_volume of f,D st f | A is bounded_below holds

lower_sum (f,D) <= middle_sum (f,F)

proof end;

theorem Th2: :: INTEGR15:2

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A

for F being middle_volume of f,D st f | A is bounded_above holds

middle_sum (f,F) <= upper_sum (f,D)

for f being Function of A,REAL

for D being Division of A

for F being middle_volume of f,D st f | A is bounded_above holds

middle_sum (f,F) <= upper_sum (f,D)

proof end;

theorem Th3: :: INTEGR15:3

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A

for e being Real st f | A is bounded_below & 0 < e holds

ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e

for f being Function of A,REAL

for D being Division of A

for e being Real st f | A is bounded_below & 0 < e holds

ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e

proof end;

theorem Th4: :: INTEGR15:4

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A

for e being Real st f | A is bounded_above & 0 < e holds

ex F being middle_volume of f,D st (upper_sum (f,D)) - e <= middle_sum (f,F)

for f being Function of A,REAL

for D being Division of A

for e being Real st f | A is bounded_above & 0 < e holds

ex F being middle_volume of f,D st (upper_sum (f,D)) - e <= middle_sum (f,F)

proof end;

definition

let A be non empty closed_interval Subset of REAL;

let f be Function of A,REAL;

let T be DivSequence of A;

existence

ex b_{1} being Function of NAT,(REAL *) st

for k being Element of NAT holds b_{1} . k is middle_volume of f,T . k;

end;
let f be Function of A,REAL;

let T be DivSequence of A;

mode middle_volume_Sequence of f,T -> Function of NAT,(REAL *) means :Def3: :: INTEGR15:def 3

for k being Element of NAT holds it . k is middle_volume of f,T . k;

correctness for k being Element of NAT holds it . k is middle_volume of f,T . k;

existence

ex b

for k being Element of NAT holds b

proof end;

:: deftheorem Def3 defines middle_volume_Sequence INTEGR15:def 3 :

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for T being DivSequence of A

for b_{4} being Function of NAT,(REAL *) holds

( b_{4} is middle_volume_Sequence of f,T iff for k being Element of NAT holds b_{4} . k is middle_volume of f,T . k );

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for T being DivSequence of A

for b

( b

definition

let A be non empty closed_interval Subset of REAL;

let f be Function of A,REAL;

let T be DivSequence of A;

let S be middle_volume_Sequence of f,T;

let k be Element of NAT ;

:: original: .

redefine func S . k -> middle_volume of f,T . k;

coherence

S . k is middle_volume of f,T . k by Def3;

end;
let f be Function of A,REAL;

let T be DivSequence of A;

let S be middle_volume_Sequence of f,T;

let k be Element of NAT ;

:: original: .

redefine func S . k -> middle_volume of f,T . k;

coherence

S . k is middle_volume of f,T . k by Def3;

definition

let A be non empty closed_interval Subset of REAL;

let f be Function of A,REAL;

let T be DivSequence of A;

let S be middle_volume_Sequence of f,T;

ex b_{1} being Real_Sequence st

for i being Element of NAT holds b_{1} . i = middle_sum (f,(S . i))

for b_{1}, b_{2} being Real_Sequence st ( for i being Element of NAT holds b_{1} . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds b_{2} . i = middle_sum (f,(S . i)) ) holds

b_{1} = b_{2}

end;
let f be Function of A,REAL;

let T be DivSequence of A;

let S be middle_volume_Sequence of f,T;

func middle_sum (f,S) -> Real_Sequence means :Def4: :: INTEGR15:def 4

for i being Element of NAT holds it . i = middle_sum (f,(S . i));

existence for i being Element of NAT holds it . i = middle_sum (f,(S . i));

ex b

for i being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines middle_sum INTEGR15:def 4 :

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for T being DivSequence of A

for S being middle_volume_Sequence of f,T

for b_{5} being Real_Sequence holds

( b_{5} = middle_sum (f,S) iff for i being Element of NAT holds b_{5} . i = middle_sum (f,(S . i)) );

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for T being DivSequence of A

for S being middle_volume_Sequence of f,T

for b

( b

theorem Th5: :: INTEGR15:5

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for T being DivSequence of A

for S being middle_volume_Sequence of f,T

for i being Element of NAT st f | A is bounded_below holds

(lower_sum (f,T)) . i <= (middle_sum (f,S)) . i

for f being Function of A,REAL

for T being DivSequence of A

for S being middle_volume_Sequence of f,T

for i being Element of NAT st f | A is bounded_below holds

(lower_sum (f,T)) . i <= (middle_sum (f,S)) . i

proof end;

theorem Th6: :: INTEGR15:6

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for T being DivSequence of A

for S being middle_volume_Sequence of f,T

for i being Element of NAT st f | A is bounded_above holds

(middle_sum (f,S)) . i <= (upper_sum (f,T)) . i

for f being Function of A,REAL

for T being DivSequence of A

for S being middle_volume_Sequence of f,T

for i being Element of NAT st f | A is bounded_above holds

(middle_sum (f,S)) . i <= (upper_sum (f,T)) . i

proof end;

theorem Th7: :: INTEGR15:7

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for T being DivSequence of A

for e being Element of REAL st 0 < e & f | A is bounded_below holds

ex S being middle_volume_Sequence of f,T st

for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e

for f being Function of A,REAL

for T being DivSequence of A

for e being Element of REAL st 0 < e & f | A is bounded_below holds

ex S being middle_volume_Sequence of f,T st

for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e

proof end;

theorem Th8: :: INTEGR15:8

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for T being DivSequence of A

for e being Element of REAL st 0 < e & f | A is bounded_above holds

ex S being middle_volume_Sequence of f,T st

for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i

for f being Function of A,REAL

for T being DivSequence of A

for e being Element of REAL st 0 < e & f | A is bounded_above holds

ex S being middle_volume_Sequence of f,T st

for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i

proof end;

Lm5: for p, q, r being Real_Sequence st p is convergent & r is convergent & lim p = lim r & ( for i being Element of NAT holds p . i <= q . i ) & ( for i being Element of NAT holds q . i <= r . i ) holds

( q is convergent & lim p = lim q & lim r = lim q )

proof end;

theorem Th9: :: INTEGR15:9

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )

for f being Function of A,REAL

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )

proof end;

theorem Th10: :: INTEGR15:10

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL st f is bounded holds

( f is integrable iff ex I being Real st

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )

for f being Function of A,REAL st f is bounded holds

( f is integrable iff ex I being Real st

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )

proof end;

definition

let n be Element of NAT ;

let A be non empty closed_interval Subset of REAL;

let f be Function of A,(REAL n);

let D be Division of A;

existence

ex b_{1} being FinSequence of REAL n st

( len b_{1} = len D & ( for i being Nat st i in dom D holds

ex r being Element of REAL n st

( r in rng (f | (divset (D,i))) & b_{1} . i = (vol (divset (D,i))) * r ) ) );

end;
let A be non empty closed_interval Subset of REAL;

let f be Function of A,(REAL n);

let D be Division of A;

mode middle_volume of f,D -> FinSequence of REAL n means :Def5: :: INTEGR15:def 5

( len it = len D & ( for i being Nat st i in dom D holds

ex r being Element of REAL n st

( r in rng (f | (divset (D,i))) & it . i = (vol (divset (D,i))) * r ) ) );

correctness ( len it = len D & ( for i being Nat st i in dom D holds

ex r being Element of REAL n st

( r in rng (f | (divset (D,i))) & it . i = (vol (divset (D,i))) * r ) ) );

existence

ex b

( len b

ex r being Element of REAL n st

( r in rng (f | (divset (D,i))) & b

proof end;

:: deftheorem Def5 defines middle_volume INTEGR15:def 5 :

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n)

for D being Division of A

for b_{5} being FinSequence of REAL n holds

( b_{5} is middle_volume of f,D iff ( len b_{5} = len D & ( for i being Nat st i in dom D holds

ex r being Element of REAL n st

( r in rng (f | (divset (D,i))) & b_{5} . i = (vol (divset (D,i))) * r ) ) ) );

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n)

for D being Division of A

for b

( b

ex r being Element of REAL n st

( r in rng (f | (divset (D,i))) & b

definition

let n be Element of NAT ;

let A be non empty closed_interval Subset of REAL;

let f be Function of A,(REAL n);

let D be Division of A;

let F be middle_volume of f,D;

ex b_{1} being Element of REAL n st

for i being Element of NAT st i in Seg n holds

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & b_{1} . i = Sum Fi )

for b_{1}, b_{2} being Element of REAL n st ( for i being Element of NAT st i in Seg n holds

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & b_{1} . i = Sum Fi ) ) & ( for i being Element of NAT st i in Seg n holds

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & b_{2} . i = Sum Fi ) ) holds

b_{1} = b_{2}

end;
let A be non empty closed_interval Subset of REAL;

let f be Function of A,(REAL n);

let D be Division of A;

let F be middle_volume of f,D;

func middle_sum (f,F) -> Element of REAL n means :Def6: :: INTEGR15:def 6

for i being Element of NAT st i in Seg n holds

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & it . i = Sum Fi );

existence for i being Element of NAT st i in Seg n holds

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & it . i = Sum Fi );

ex b

for i being Element of NAT st i in Seg n holds

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & b

proof end;

uniqueness for b

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & b

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & b

b

proof end;

:: deftheorem Def6 defines middle_sum INTEGR15:def 6 :

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n)

for D being Division of A

for F being middle_volume of f,D

for b_{6} being Element of REAL n holds

( b_{6} = middle_sum (f,F) iff for i being Element of NAT st i in Seg n holds

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & b_{6} . i = Sum Fi ) );

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n)

for D being Division of A

for F being middle_volume of f,D

for b

( b

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & b

definition

let n be Element of NAT ;

let A be non empty closed_interval Subset of REAL;

let f be Function of A,(REAL n);

let T be DivSequence of A;

existence

ex b_{1} being Function of NAT,((REAL n) *) st

for k being Element of NAT holds b_{1} . k is middle_volume of f,T . k;

end;
let A be non empty closed_interval Subset of REAL;

let f be Function of A,(REAL n);

let T be DivSequence of A;

mode middle_volume_Sequence of f,T -> Function of NAT,((REAL n) *) means :Def7: :: INTEGR15:def 7

for k being Element of NAT holds it . k is middle_volume of f,T . k;

correctness for k being Element of NAT holds it . k is middle_volume of f,T . k;

existence

ex b

for k being Element of NAT holds b

proof end;

:: deftheorem Def7 defines middle_volume_Sequence INTEGR15:def 7 :

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n)

for T being DivSequence of A

for b_{5} being Function of NAT,((REAL n) *) holds

( b_{5} is middle_volume_Sequence of f,T iff for k being Element of NAT holds b_{5} . k is middle_volume of f,T . k );

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n)

for T being DivSequence of A

for b

( b

definition

let n be Element of NAT ;

let A be non empty closed_interval Subset of REAL;

let f be Function of A,(REAL n);

let T be DivSequence of A;

let S be middle_volume_Sequence of f,T;

let k be Element of NAT ;

:: original: .

redefine func S . k -> middle_volume of f,T . k;

coherence

S . k is middle_volume of f,T . k by Def7;

end;
let A be non empty closed_interval Subset of REAL;

let f be Function of A,(REAL n);

let T be DivSequence of A;

let S be middle_volume_Sequence of f,T;

let k be Element of NAT ;

:: original: .

redefine func S . k -> middle_volume of f,T . k;

coherence

S . k is middle_volume of f,T . k by Def7;

definition

let n be Element of NAT ;

let A be non empty closed_interval Subset of REAL;

let f be Function of A,(REAL n);

let T be DivSequence of A;

let S be middle_volume_Sequence of f,T;

ex b_{1} being sequence of (REAL-NS n) st

for i being Element of NAT holds b_{1} . i = middle_sum (f,(S . i))

for b_{1}, b_{2} being sequence of (REAL-NS n) st ( for i being Element of NAT holds b_{1} . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds b_{2} . i = middle_sum (f,(S . i)) ) holds

b_{1} = b_{2}

end;
let A be non empty closed_interval Subset of REAL;

let f be Function of A,(REAL n);

let T be DivSequence of A;

let S be middle_volume_Sequence of f,T;

func middle_sum (f,S) -> sequence of (REAL-NS n) means :Def8: :: INTEGR15:def 8

for i being Element of NAT holds it . i = middle_sum (f,(S . i));

existence for i being Element of NAT holds it . i = middle_sum (f,(S . i));

ex b

for i being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines middle_sum INTEGR15:def 8 :

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n)

for T being DivSequence of A

for S being middle_volume_Sequence of f,T

for b_{6} being sequence of (REAL-NS n) holds

( b_{6} = middle_sum (f,S) iff for i being Element of NAT holds b_{6} . i = middle_sum (f,(S . i)) );

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n)

for T being DivSequence of A

for S being middle_volume_Sequence of f,T

for b

( b

definition

let n be Nat;

let Z be set ;

let f, g be PartFunc of Z,(REAL n);

coherence

f <++> g is PartFunc of Z,(REAL n)

f <--> g is PartFunc of Z,(REAL n)

end;
let Z be set ;

let f, g be PartFunc of Z,(REAL n);

coherence

f <++> g is PartFunc of Z,(REAL n)

proof end;

coherence f <--> g is PartFunc of Z,(REAL n)

proof end;

:: deftheorem defines + INTEGR15:def 9 :

for n being Nat

for Z being set

for f, g being PartFunc of Z,(REAL n) holds f + g = f <++> g;

for n being Nat

for Z being set

for f, g being PartFunc of Z,(REAL n) holds f + g = f <++> g;

:: deftheorem defines - INTEGR15:def 10 :

for n being Nat

for Z being set

for f, g being PartFunc of Z,(REAL n) holds f - g = f <--> g;

for n being Nat

for Z being set

for f, g being PartFunc of Z,(REAL n) holds f - g = f <--> g;

definition

let n be Nat;

let r be real number ;

let Z be set ;

let f be PartFunc of Z,(REAL n);

coherence

f [#] r is PartFunc of Z,(REAL n)

end;
let r be real number ;

let Z be set ;

let f be PartFunc of Z,(REAL n);

coherence

f [#] r is PartFunc of Z,(REAL n)

proof end;

:: deftheorem defines (#) INTEGR15:def 11 :

for n being Nat

for r being real number

for Z being set

for f being PartFunc of Z,(REAL n) holds r (#) f = f [#] r;

for n being Nat

for r being real number

for Z being set

for f being PartFunc of Z,(REAL n) holds r (#) f = f [#] r;

begin

definition

let n be Element of NAT ;

let A be non empty closed_interval Subset of REAL;

let f be Function of A,(REAL n);

end;
let A be non empty closed_interval Subset of REAL;

let f be Function of A,(REAL n);

:: deftheorem Def12 defines bounded INTEGR15:def 12 :

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n) holds

( f is bounded iff for i being Element of NAT st i in Seg n holds

(proj (i,n)) * f is bounded );

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n) holds

( f is bounded iff for i being Element of NAT st i in Seg n holds

(proj (i,n)) * f is bounded );

Lm6: for n, i being Element of NAT

for f being PartFunc of REAL,(REAL n)

for i being Element of NAT

for A being Subset of REAL holds (proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A

proof end;

definition

let n be Element of NAT ;

let A be non empty closed_interval Subset of REAL;

let f be Function of A,(REAL n);

end;
let A be non empty closed_interval Subset of REAL;

let f be Function of A,(REAL n);

attr f is integrable means :Def13: :: INTEGR15:def 13

for i being Element of NAT st i in Seg n holds

(proj (i,n)) * f is integrable ;

for i being Element of NAT st i in Seg n holds

(proj (i,n)) * f is integrable ;

:: deftheorem Def13 defines integrable INTEGR15:def 13 :

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n) holds

( f is integrable iff for i being Element of NAT st i in Seg n holds

(proj (i,n)) * f is integrable );

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n) holds

( f is integrable iff for i being Element of NAT st i in Seg n holds

(proj (i,n)) * f is integrable );

definition

let n be Element of NAT ;

let A be non empty closed_interval Subset of REAL;

let f be Function of A,(REAL n);

ex b_{1} being Element of REAL n st

( dom b_{1} = Seg n & ( for i being Element of NAT st i in Seg n holds

b_{1} . i = integral ((proj (i,n)) * f) ) )

for b_{1}, b_{2} being Element of REAL n st dom b_{1} = Seg n & ( for i being Element of NAT st i in Seg n holds

b_{1} . i = integral ((proj (i,n)) * f) ) & dom b_{2} = Seg n & ( for i being Element of NAT st i in Seg n holds

b_{2} . i = integral ((proj (i,n)) * f) ) holds

b_{1} = b_{2}

end;
let A be non empty closed_interval Subset of REAL;

let f be Function of A,(REAL n);

func integral f -> Element of REAL n means :Def14: :: INTEGR15:def 14

( dom it = Seg n & ( for i being Element of NAT st i in Seg n holds

it . i = integral ((proj (i,n)) * f) ) );

existence ( dom it = Seg n & ( for i being Element of NAT st i in Seg n holds

it . i = integral ((proj (i,n)) * f) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def14 defines integral INTEGR15:def 14 :

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n)

for b_{4} being Element of REAL n holds

( b_{4} = integral f iff ( dom b_{4} = Seg n & ( for i being Element of NAT st i in Seg n holds

b_{4} . i = integral ((proj (i,n)) * f) ) ) );

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n)

for b

( b

b

theorem Th11: :: INTEGR15:11

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n)

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )

for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n)

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )

proof end;

theorem :: INTEGR15:12

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n) st f is bounded holds

( f is integrable iff ex I being Element of REAL n st

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )

for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n) st f is bounded holds

( f is integrable iff ex I being Element of REAL n st

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )

proof end;

:: deftheorem Def15 defines bounded INTEGR15:def 15 :

for n being Element of NAT

for f being PartFunc of REAL,(REAL n) holds

( f is bounded iff for i being Element of NAT st i in Seg n holds

(proj (i,n)) * f is bounded );

for n being Element of NAT

for f being PartFunc of REAL,(REAL n) holds

( f is bounded iff for i being Element of NAT st i in Seg n holds

(proj (i,n)) * f is bounded );

definition

let n be Element of NAT ;

let A be non empty closed_interval Subset of REAL;

let f be PartFunc of REAL,(REAL n);

end;
let A be non empty closed_interval Subset of REAL;

let f be PartFunc of REAL,(REAL n);

pred f is_integrable_on A means :Def16: :: INTEGR15:def 16

for i being Element of NAT st i in Seg n holds

(proj (i,n)) * f is_integrable_on A;

for i being Element of NAT st i in Seg n holds

(proj (i,n)) * f is_integrable_on A;

:: deftheorem Def16 defines is_integrable_on INTEGR15:def 16 :

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL,(REAL n) holds

( f is_integrable_on A iff for i being Element of NAT st i in Seg n holds

(proj (i,n)) * f is_integrable_on A );

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL,(REAL n) holds

( f is_integrable_on A iff for i being Element of NAT st i in Seg n holds

(proj (i,n)) * f is_integrable_on A );

definition

let n be Element of NAT ;

let A be non empty closed_interval Subset of REAL;

let f be PartFunc of REAL,(REAL n);

ex b_{1} being Element of REAL n st

( dom b_{1} = Seg n & ( for i being Element of NAT st i in Seg n holds

b_{1} . i = integral (((proj (i,n)) * f),A) ) )

for b_{1}, b_{2} being Element of REAL n st dom b_{1} = Seg n & ( for i being Element of NAT st i in Seg n holds

b_{1} . i = integral (((proj (i,n)) * f),A) ) & dom b_{2} = Seg n & ( for i being Element of NAT st i in Seg n holds

b_{2} . i = integral (((proj (i,n)) * f),A) ) holds

b_{1} = b_{2}

end;
let A be non empty closed_interval Subset of REAL;

let f be PartFunc of REAL,(REAL n);

func integral (f,A) -> Element of REAL n means :Def17: :: INTEGR15:def 17

( dom it = Seg n & ( for i being Element of NAT st i in Seg n holds

it . i = integral (((proj (i,n)) * f),A) ) );

existence ( dom it = Seg n & ( for i being Element of NAT st i in Seg n holds

it . i = integral (((proj (i,n)) * f),A) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def17 defines integral INTEGR15:def 17 :

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL,(REAL n)

for b_{4} being Element of REAL n holds

( b_{4} = integral (f,A) iff ( dom b_{4} = Seg n & ( for i being Element of NAT st i in Seg n holds

b_{4} . i = integral (((proj (i,n)) * f),A) ) ) );

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL,(REAL n)

for b

( b

b

theorem :: INTEGR15:13

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL,(REAL n)

for g being Function of A,(REAL n) st f | A = g holds

( f is_integrable_on A iff g is integrable )

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL,(REAL n)

for g being Function of A,(REAL n) st f | A = g holds

( f is_integrable_on A iff g is integrable )

proof end;

theorem :: INTEGR15:14

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL,(REAL n)

for g being Function of A,(REAL n) st f | A = g holds

integral (f,A) = integral g

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL,(REAL n)

for g being Function of A,(REAL n) st f | A = g holds

integral (f,A) = integral g

proof end;

definition

let a, b be real number ;

let n be Element of NAT ;

let f be PartFunc of REAL,(REAL n);

ex b_{1} being Element of REAL n st

( dom b_{1} = Seg n & ( for i being Element of NAT st i in Seg n holds

b_{1} . i = integral (((proj (i,n)) * f),a,b) ) )

for b_{1}, b_{2} being Element of REAL n st dom b_{1} = Seg n & ( for i being Element of NAT st i in Seg n holds

b_{1} . i = integral (((proj (i,n)) * f),a,b) ) & dom b_{2} = Seg n & ( for i being Element of NAT st i in Seg n holds

b_{2} . i = integral (((proj (i,n)) * f),a,b) ) holds

b_{1} = b_{2}

end;
let n be Element of NAT ;

let f be PartFunc of REAL,(REAL n);

func integral (f,a,b) -> Element of REAL n means :Def18: :: INTEGR15:def 18

( dom it = Seg n & ( for i being Element of NAT st i in Seg n holds

it . i = integral (((proj (i,n)) * f),a,b) ) );

existence ( dom it = Seg n & ( for i being Element of NAT st i in Seg n holds

it . i = integral (((proj (i,n)) * f),a,b) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def18 defines integral INTEGR15:def 18 :

for a, b being real number

for n being Element of NAT

for f being PartFunc of REAL,(REAL n)

for b_{5} being Element of REAL n holds

( b_{5} = integral (f,a,b) iff ( dom b_{5} = Seg n & ( for i being Element of NAT st i in Seg n holds

b_{5} . i = integral (((proj (i,n)) * f),a,b) ) ) );

for a, b being real number

for n being Element of NAT

for f being PartFunc of REAL,(REAL n)

for b

( b

b

begin

theorem Th15: :: INTEGR15:15

for Z being set

for n, i being Element of NAT

for f1, f2 being PartFunc of Z,(REAL n) holds

( (proj (i,n)) * (f1 + f2) = ((proj (i,n)) * f1) + ((proj (i,n)) * f2) & (proj (i,n)) * (f1 - f2) = ((proj (i,n)) * f1) - ((proj (i,n)) * f2) )

for n, i being Element of NAT

for f1, f2 being PartFunc of Z,(REAL n) holds

( (proj (i,n)) * (f1 + f2) = ((proj (i,n)) * f1) + ((proj (i,n)) * f2) & (proj (i,n)) * (f1 - f2) = ((proj (i,n)) * f1) - ((proj (i,n)) * f2) )

proof end;

theorem Th16: :: INTEGR15:16

for Z being set

for n, i being Element of NAT

for r being Real

for f being PartFunc of Z,(REAL n) holds (proj (i,n)) * (r (#) f) = r (#) ((proj (i,n)) * f)

for n, i being Element of NAT

for r being Real

for f being PartFunc of Z,(REAL n) holds (proj (i,n)) * (r (#) f) = r (#) ((proj (i,n)) * f)

proof end;

theorem :: INTEGR15:17

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f1, f2 being PartFunc of REAL,(REAL n) st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & f1 | A is bounded & f2 | A is bounded holds

( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )

for A being non empty closed_interval Subset of REAL

for f1, f2 being PartFunc of REAL,(REAL n) st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & f1 | A is bounded & f2 | A is bounded holds

( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )

proof end;

theorem :: INTEGR15:18

for n being Element of NAT

for r being Real

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL,(REAL n) st A c= dom f & f is_integrable_on A & f | A is bounded holds

( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )

for r being Real

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL,(REAL n) st A c= dom f & f is_integrable_on A & f | A is bounded holds

( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )

proof end;

theorem :: INTEGR15:19

for n being Element of NAT

for f being PartFunc of REAL,(REAL n)

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 f being PartFunc of REAL,(REAL n)

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

for n being Element of NAT

for f being PartFunc of REAL,(REAL n)

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 f being PartFunc of REAL,(REAL n)

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

for n being Nat

for Z, x being set

for f, g being PartFunc of Z,(REAL n) st x in dom (f + g) holds

(f + g) /. x = (f /. x) + (g /. x)

for Z, x being set

for f, g being PartFunc of Z,(REAL n) st x in dom (f + g) holds

(f + g) /. x = (f /. x) + (g /. x)

proof end;

theorem :: INTEGR15:22

for n being Nat

for Z, x being set

for f, g being PartFunc of Z,(REAL n) st x in dom (f - g) holds

(f - g) /. x = (f /. x) - (g /. x)

for Z, x being set

for f, g being PartFunc of Z,(REAL n) st x in dom (f - g) holds

(f - g) /. x = (f /. x) - (g /. x)

proof end;

theorem :: INTEGR15:23

for n being Nat

for Z, x being set

for f being PartFunc of Z,(REAL n)

for r being real number st x in dom (r (#) f) holds

(r (#) f) /. x = r * (f /. x)

for Z, x being set

for f being PartFunc of Z,(REAL n)

for r being real number st x in dom (r (#) f) holds

(r (#) f) /. x = r * (f /. x)

proof end;