:: by Keiichi Miyajima , Takahiro Kato and Yasunari Shidama

::

:: Received May 20, 2010

:: Copyright (c) 2010-2018 Association of Mizar Users

definition

let X be RealNormSpace;

let A be non empty closed_interval Subset of REAL;

let f be Function of A, the carrier of X;

let D be Division of A;

existence

ex b_{1} being FinSequence of X st

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

ex c being Point of X st

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

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

let f be Function of A, the carrier of X;

let D be Division of A;

mode middle_volume of f,D -> FinSequence of X means :Def1: :: INTEGR18:def 1

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

ex c being Point of X st

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

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

ex c being Point of X st

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

existence

ex b

( len b

ex c being Point of X st

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

proof end;

:: deftheorem Def1 defines middle_volume INTEGR18:def 1 :

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f being Function of A, the carrier of X

for D being Division of A

for b_{5} being FinSequence of X 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 c being Point of X st

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

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f being Function of A, the carrier of X

for D being Division of A

for b

( b

ex c being Point of X st

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

definition

let X be RealNormSpace;

let A be non empty closed_interval Subset of REAL;

let f be Function of A, the carrier of X;

let D be Division of A;

let F be middle_volume of f,D;

coherence

Sum F is Point of X ;

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

let f be Function of A, the carrier of X;

let D be Division of A;

let F be middle_volume of f,D;

coherence

Sum F is Point of X ;

:: deftheorem defines middle_sum INTEGR18:def 2 :

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f being Function of A, the carrier of X

for D being Division of A

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

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f being Function of A, the carrier of X

for D being Division of A

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

definition

let X be RealNormSpace;

let A be non empty closed_interval Subset of REAL;

let f be Function of A, the carrier of X;

let T be DivSequence of A;

existence

ex b_{1} being sequence of ( the carrier of X *) 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, the carrier of X;

let T be DivSequence of A;

mode middle_volume_Sequence of f,T -> sequence of ( the carrier of X *) means :Def3: :: INTEGR18: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 INTEGR18:def 3 :

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f being Function of A, the carrier of X

for T being DivSequence of A

for b_{5} being sequence of ( the carrier of X *) 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 X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f being Function of A, the carrier of X

for T being DivSequence of A

for b

( b

definition

let X be RealNormSpace;

let A be non empty closed_interval Subset of REAL;

let f be Function of A, the carrier of X;

let T be DivSequence of A;

let S be middle_volume_Sequence of f,T;

let k be Nat;

:: original: .

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

coherence

S . 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, the carrier of X;

let T be DivSequence of A;

let S be middle_volume_Sequence of f,T;

let k be Nat;

:: original: .

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

coherence

S . k is middle_volume of f,T . k

proof end;

definition

let X be RealNormSpace;

let A be non empty closed_interval Subset of REAL;

let f be Function of A, the carrier of X;

let T be DivSequence of A;

let S be middle_volume_Sequence of f,T;

ex b_{1} being sequence of X st

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

for b_{1}, b_{2} being sequence of X st ( for i being Nat holds b_{1} . i = middle_sum (f,(S . i)) ) & ( for i being 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, the carrier of X;

let T be DivSequence of A;

let S be middle_volume_Sequence of f,T;

func middle_sum (f,S) -> sequence of X means :Def4: :: INTEGR18:def 4

for i being Nat holds it . i = middle_sum (f,(S . i));

existence for i being Nat holds it . i = middle_sum (f,(S . i));

ex b

for i being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines middle_sum INTEGR18:def 4 :

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f being Function of A, the carrier of X

for T being DivSequence of A

for S being middle_volume_Sequence of f,T

for b_{6} being sequence of X holds

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

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f being Function of A, the carrier of X

for T being DivSequence of A

for S being middle_volume_Sequence of f,T

for b

( b

definition

let X be RealNormSpace;

let A be non empty closed_interval Subset of REAL;

let f be Function of A, the carrier of X;

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

let f be Function of A, the carrier of X;

attr f is integrable means :: INTEGR18:def 5

ex I being Point of X 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 );

ex I being Point of X 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 );

:: deftheorem defines integrable INTEGR18:def 5 :

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f being Function of A, the carrier of X holds

( f is integrable iff ex I being Point of X 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 X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f being Function of A, the carrier of X holds

( f is integrable iff ex I being Point of X 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 ) );

theorem Th1: :: INTEGR18:1

for X being RealNormSpace

for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 + R2 holds

Sum R3 = (Sum R1) + (Sum R2)

for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 + R2 holds

Sum R3 = (Sum R1) + (Sum R2)

proof end;

theorem :: INTEGR18:2

for X being RealNormSpace

for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 - R2 holds

Sum R3 = (Sum R1) - (Sum R2)

for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 - R2 holds

Sum R3 = (Sum R1) - (Sum R2)

proof end;

theorem Th3: :: INTEGR18:3

for X being RealNormSpace

for R1, R2 being FinSequence of X

for a being Real st R2 = a (#) R1 holds

Sum R2 = a * (Sum R1)

for R1, R2 being FinSequence of X

for a being Real st R2 = a (#) R1 holds

Sum R2 = a * (Sum R1)

proof end;

definition

let X be RealNormSpace;

let A be non empty closed_interval Subset of REAL;

let f be Function of A, the carrier of X;

assume A1: f is integrable ;

ex b_{1} being Point of X 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)) = b_{1} )
by A1;

uniqueness

for b_{1}, b_{2} being Point of X 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)) = b_{1} ) ) & ( 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)) = b_{2} ) ) holds

b_{1} = b_{2}

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

let f be Function of A, the carrier of X;

assume A1: f is integrable ;

func integral f -> Point of X means :Def6: :: INTEGR18:def 6

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)) = it );

existence 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)) = it );

ex b

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

uniqueness

for b

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

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

b

proof end;

:: deftheorem Def6 defines integral INTEGR18:def 6 :

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f being Function of A, the carrier of X st f is integrable holds

for b_{4} being Point of X holds

( b_{4} = integral f iff 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)) = b_{4} ) );

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f being Function of A, the carrier of X st f is integrable holds

for b

( b

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

theorem Th4: :: INTEGR18:4

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for r being Real

for f, h being Function of A, the carrier of X st h = r (#) f & f is integrable holds

( h is integrable & integral h = r * (integral f) )

for A being non empty closed_interval Subset of REAL

for r being Real

for f, h being Function of A, the carrier of X st h = r (#) f & f is integrable holds

( h is integrable & integral h = r * (integral f) )

proof end;

reconsider jj = 1 as Real ;

theorem Th5: :: INTEGR18:5

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f, h being Function of A, the carrier of X st h = - f & f is integrable holds

( h is integrable & integral h = - (integral f) )

for A being non empty closed_interval Subset of REAL

for f, h being Function of A, the carrier of X st h = - f & f is integrable holds

( h is integrable & integral h = - (integral f) )

proof end;

theorem Th6: :: INTEGR18:6

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f, g, h being Function of A, the carrier of X st h = f + g & f is integrable & g is integrable holds

( h is integrable & integral h = (integral f) + (integral g) )

for A being non empty closed_interval Subset of REAL

for f, g, h being Function of A, the carrier of X st h = f + g & f is integrable & g is integrable holds

( h is integrable & integral h = (integral f) + (integral g) )

proof end;

theorem :: INTEGR18:7

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f, g, h being Function of A, the carrier of X st h = f - g & f is integrable & g is integrable holds

( h is integrable & integral h = (integral f) - (integral g) )

for A being non empty closed_interval Subset of REAL

for f, g, h being Function of A, the carrier of X st h = f - g & f is integrable & g is integrable holds

( h is integrable & integral h = (integral f) - (integral g) )

proof end;

definition

let X be RealNormSpace;

let A be non empty closed_interval Subset of REAL;

let f be PartFunc of REAL, the carrier of X;

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

let f be PartFunc of REAL, the carrier of X;

pred f is_integrable_on A means :: INTEGR18:def 7

ex g being Function of A, the carrier of X st

( g = f | A & g is integrable );

ex g being Function of A, the carrier of X st

( g = f | A & g is integrable );

:: deftheorem defines is_integrable_on INTEGR18:def 7 :

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL, the carrier of X holds

( f is_integrable_on A iff ex g being Function of A, the carrier of X st

( g = f | A & g is integrable ) );

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL, the carrier of X holds

( f is_integrable_on A iff ex g being Function of A, the carrier of X st

( g = f | A & g is integrable ) );

definition

let X be RealNormSpace;

let A be non empty closed_interval Subset of REAL;

let f be PartFunc of REAL, the carrier of X;

assume A1: A c= dom f ;

existence

ex b_{1} being Element of X ex g being Function of A, the carrier of X st

( g = f | A & b_{1} = integral g );

uniqueness

for b_{1}, b_{2} being Element of X st ex g being Function of A, the carrier of X st

( g = f | A & b_{1} = integral g ) & ex g being Function of A, the carrier of X st

( g = f | A & b_{2} = integral g ) holds

b_{1} = b_{2};

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

let f be PartFunc of REAL, the carrier of X;

assume A1: A c= dom f ;

func integral (f,A) -> Element of X means :Def8: :: INTEGR18:def 8

ex g being Function of A, the carrier of X st

( g = f | A & it = integral g );

correctness ex g being Function of A, the carrier of X st

( g = f | A & it = integral g );

existence

ex b

( g = f | A & b

uniqueness

for b

( g = f | A & b

( g = f | A & b

b

proof end;

:: deftheorem Def8 defines integral INTEGR18:def 8 :

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL, the carrier of X st A c= dom f holds

for b_{4} being Element of X holds

( b_{4} = integral (f,A) iff ex g being Function of A, the carrier of X st

( g = f | A & b_{4} = integral g ) );

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL, the carrier of X st A c= dom f holds

for b

( b

( g = f | A & b

theorem :: INTEGR18:8

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL, the carrier of X

for g being Function of A, the carrier of X 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, the carrier of X

for g being Function of A, the carrier of X st f | A = g holds

( f is_integrable_on A iff g is integrable ) ;

theorem :: INTEGR18:9

theorem Th10: :: INTEGR18:10

for X, Y being non empty set

for V being RealNormSpace

for g, f being PartFunc of X, the carrier of V

for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds

g1 + f1 = g + f

for V being RealNormSpace

for g, f being PartFunc of X, the carrier of V

for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds

g1 + f1 = g + f

proof end;

theorem :: INTEGR18:11

for X, Y being non empty set

for V being RealNormSpace

for g, f being PartFunc of X, the carrier of V

for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds

g1 - f1 = g - f

for V being RealNormSpace

for g, f being PartFunc of X, the carrier of V

for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds

g1 - f1 = g - f

proof end;

theorem Th12: :: INTEGR18:12

for r being Real

for X, Y being non empty set

for V being RealNormSpace

for g being PartFunc of X, the carrier of V

for g1 being PartFunc of Y, the carrier of V st g = g1 holds

r (#) g1 = r (#) g

for X, Y being non empty set

for V being RealNormSpace

for g being PartFunc of X, the carrier of V

for g1 being PartFunc of Y, the carrier of V st g = g1 holds

r (#) g1 = r (#) g

proof end;

theorem Th13: :: INTEGR18:13

for X being RealNormSpace

for r being Real

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL, the carrier of X st A c= dom f & f is_integrable_on A 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, the carrier of X st A c= dom f & f is_integrable_on A holds

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

proof end;

theorem Th14: :: INTEGR18:14

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f1, f2 being PartFunc of REAL, the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds

( f1 + f2 is_integrable_on 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, the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds

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

proof end;

theorem :: INTEGR18:15

for X being RealNormSpace

for A being non empty closed_interval Subset of REAL

for f1, f2 being PartFunc of REAL, the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds

( f1 - f2 is_integrable_on 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, the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds

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

proof end;

definition

let X be RealNormSpace;

let f be PartFunc of REAL, the carrier of X;

let a, b be Real;

coherence

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

consistency

for b_{1} being Element of X holds verum;

;

end;
let f be PartFunc of REAL, the carrier of X;

let a, b be Real;

func integral (f,a,b) -> Element of X equals :Def9: :: INTEGR18:def 9

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 Element of X ) & ( not a <= b implies - (integral (f,['b,a'])) is Element of X ) );

consistency

for b

;

:: deftheorem Def9 defines integral INTEGR18:def 9 :

for X being RealNormSpace

for f being PartFunc of REAL, the carrier of X

for a, b being 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 X being RealNormSpace

for f being PartFunc of REAL, the carrier of X

for a, b being 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 Th16: :: INTEGR18:16

for X being RealNormSpace

for f being PartFunc of REAL, the carrier of X

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, the carrier of X

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 Th17: :: INTEGR18:17

for X being RealNormSpace

for f being PartFunc of REAL, the carrier of X

for A being non empty closed_interval Subset of REAL st vol A = 0 & A c= dom f holds

( f is_integrable_on A & integral (f,A) = 0. X )

for f being PartFunc of REAL, the carrier of X

for A being non empty closed_interval Subset of REAL st vol A = 0 & A c= dom f holds

( f is_integrable_on A & integral (f,A) = 0. X )

proof end;

theorem :: INTEGR18:18

for X being RealNormSpace

for f being PartFunc of REAL, the carrier of X

for A being non empty closed_interval Subset of REAL

for a, b being Real st A = [.b,a.] & A c= dom f holds

- (integral (f,A)) = integral (f,a,b)

for f being PartFunc of REAL, the carrier of X

for A being non empty closed_interval Subset of REAL

for a, b being Real st A = [.b,a.] & A c= dom f holds

- (integral (f,A)) = integral (f,a,b)

proof end;