:: by Yasunari Shidama , Noboru Endou , Katsumi Wasaki and Katuhiko Kanazashi

::

:: Received June 6, 2007

:: Copyright (c) 2007-2019 Association of Mizar Users

theorem Th1: :: INTEGRA7:1

for a being Real

for A being non empty set

for f, g being Function of A,REAL st rng f is bounded_above & rng g is bounded_above & ( for x being set st x in A holds

|.((f . x) - (g . x)).| <= a ) holds

( (upper_bound (rng f)) - (upper_bound (rng g)) <= a & (upper_bound (rng g)) - (upper_bound (rng f)) <= a )

for A being non empty set

for f, g being Function of A,REAL st rng f is bounded_above & rng g is bounded_above & ( for x being set st x in A holds

|.((f . x) - (g . x)).| <= a ) holds

( (upper_bound (rng f)) - (upper_bound (rng g)) <= a & (upper_bound (rng g)) - (upper_bound (rng f)) <= a )

proof end;

theorem Th2: :: INTEGRA7:2

for a being Real

for A being non empty set

for f, g being Function of A,REAL st rng f is bounded_below & rng g is bounded_below & ( for x being set st x in A holds

|.((f . x) - (g . x)).| <= a ) holds

( (lower_bound (rng f)) - (lower_bound (rng g)) <= a & (lower_bound (rng g)) - (lower_bound (rng f)) <= a )

for A being non empty set

for f, g being Function of A,REAL st rng f is bounded_below & rng g is bounded_below & ( for x being set st x in A holds

|.((f . x) - (g . x)).| <= a ) holds

( (lower_bound (rng f)) - (lower_bound (rng g)) <= a & (lower_bound (rng g)) - (lower_bound (rng f)) <= a )

proof end;

theorem :: INTEGRA7:3

theorem Th4: :: INTEGRA7:4

for X being set

for f being PartFunc of REAL,REAL

for x being Real st x in X & f | X is_differentiable_in x holds

f is_differentiable_in x

for f being PartFunc of REAL,REAL

for x being Real st x in X & f | X is_differentiable_in x holds

f is_differentiable_in x

proof end;

theorem :: INTEGRA7:5

for X being set

for f being PartFunc of REAL,REAL st f | X is_differentiable_on X holds

f is_differentiable_on X

for f being PartFunc of REAL,REAL st f | X is_differentiable_on X holds

f is_differentiable_on X

proof end;

theorem Th6: :: INTEGRA7:6

for X being set

for f, g being PartFunc of REAL,REAL st f is_differentiable_on X & g is_differentiable_on X holds

( f + g is_differentiable_on X & f - g is_differentiable_on X & f (#) g is_differentiable_on X )

for f, g being PartFunc of REAL,REAL st f is_differentiable_on X & g is_differentiable_on X holds

( f + g is_differentiable_on X & f - g is_differentiable_on X & f (#) g is_differentiable_on X )

proof end;

theorem Th7: :: INTEGRA7:7

for r being Real

for X being set

for f being PartFunc of REAL,REAL st f is_differentiable_on X holds

r (#) f is_differentiable_on X

for X being set

for f being PartFunc of REAL,REAL st f is_differentiable_on X holds

r (#) f is_differentiable_on X

proof end;

theorem Th8: :: INTEGRA7:8

for X being set

for f, g being PartFunc of REAL,REAL st ( for x being set st x in X holds

g . x <> 0 ) & f is_differentiable_on X & g is_differentiable_on X holds

f / g is_differentiable_on X

for f, g being PartFunc of REAL,REAL st ( for x being set st x in X holds

g . x <> 0 ) & f is_differentiable_on X & g is_differentiable_on X holds

f / g is_differentiable_on X

proof end;

theorem :: INTEGRA7:9

for X being set

for f being PartFunc of REAL,REAL st ( for x being set st x in X holds

f . x <> 0 ) & f is_differentiable_on X holds

f ^ is_differentiable_on X

for f being PartFunc of REAL,REAL st ( for x being set st x in X holds

f . x <> 0 ) & f is_differentiable_on X holds

f ^ is_differentiable_on X

proof end;

theorem Th10: :: INTEGRA7:10

for a, b being Real

for X being set

for F being PartFunc of REAL,REAL st a <= b & ['a,b'] c= X & F is_differentiable_on X & F `| X is_integrable_on ['a,b'] & (F `| X) | ['a,b'] is bounded holds

F . b = (integral ((F `| X),a,b)) + (F . a)

for X being set

for F being PartFunc of REAL,REAL st a <= b & ['a,b'] c= X & F is_differentiable_on X & F `| X is_integrable_on ['a,b'] & (F `| X) | ['a,b'] is bounded holds

F . b = (integral ((F `| X),a,b)) + (F . a)

proof end;

definition

let X be set ;

let f be PartFunc of REAL,REAL;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ex F being PartFunc of REAL,REAL st

( x = F & F is_differentiable_on X & F `| X = f | X ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ex F being PartFunc of REAL,REAL st

( x = F & F is_differentiable_on X & F `| X = f | X ) ) ) & ( for x being set holds

( x in b_{2} iff ex F being PartFunc of REAL,REAL st

( x = F & F is_differentiable_on X & F `| X = f | X ) ) ) holds

b_{1} = b_{2}

end;
let f be PartFunc of REAL,REAL;

func IntegralFuncs (f,X) -> set means :Def1: :: INTEGRA7:def 1

for x being set holds

( x in it iff ex F being PartFunc of REAL,REAL st

( x = F & F is_differentiable_on X & F `| X = f | X ) );

existence for x being set holds

( x in it iff ex F being PartFunc of REAL,REAL st

( x = F & F is_differentiable_on X & F `| X = f | X ) );

ex b

for x being set holds

( x in b

( x = F & F is_differentiable_on X & F `| X = f | X ) )

proof end;

uniqueness for b

( x in b

( x = F & F is_differentiable_on X & F `| X = f | X ) ) ) & ( for x being set holds

( x in b

( x = F & F is_differentiable_on X & F `| X = f | X ) ) ) holds

b

proof end;

:: deftheorem Def1 defines IntegralFuncs INTEGRA7:def 1 :

for X being set

for f being PartFunc of REAL,REAL

for b_{3} being set holds

( b_{3} = IntegralFuncs (f,X) iff for x being set holds

( x in b_{3} iff ex F being PartFunc of REAL,REAL st

( x = F & F is_differentiable_on X & F `| X = f | X ) ) );

for X being set

for f being PartFunc of REAL,REAL

for b

( b

( x in b

( x = F & F is_differentiable_on X & F `| X = f | X ) ) );

:: deftheorem defines is_integral_of INTEGRA7:def 2 :

for X being set

for F, f being PartFunc of REAL,REAL holds

( F is_integral_of f,X iff F in IntegralFuncs (f,X) );

for X being set

for F, f being PartFunc of REAL,REAL holds

( F is_integral_of f,X iff F in IntegralFuncs (f,X) );

Lm1: for X being set

for f, F being PartFunc of REAL,REAL holds

( F is_integral_of f,X iff ( F is_differentiable_on X & F `| X = f | X ) )

proof end;

theorem :: INTEGRA7:12

for X being set

for f, g, F, G being PartFunc of REAL,REAL st F is_integral_of f,X & G is_integral_of g,X holds

( F + G is_integral_of f + g,X & F - G is_integral_of f - g,X )

for f, g, F, G being PartFunc of REAL,REAL st F is_integral_of f,X & G is_integral_of g,X holds

( F + G is_integral_of f + g,X & F - G is_integral_of f - g,X )

proof end;

theorem :: INTEGRA7:13

for r being Real

for X being set

for f, F being PartFunc of REAL,REAL st F is_integral_of f,X holds

r (#) F is_integral_of r (#) f,X

for X being set

for f, F being PartFunc of REAL,REAL st F is_integral_of f,X holds

r (#) F is_integral_of r (#) f,X

proof end;

theorem :: INTEGRA7:14

for X being set

for f, g, F, G being PartFunc of REAL,REAL st F is_integral_of f,X & G is_integral_of g,X holds

F (#) G is_integral_of (f (#) G) + (F (#) g),X

for f, g, F, G being PartFunc of REAL,REAL st F is_integral_of f,X & G is_integral_of g,X holds

F (#) G is_integral_of (f (#) G) + (F (#) g),X

proof end;

theorem :: INTEGRA7:15

for X being set

for f, g, F, G being PartFunc of REAL,REAL st ( for x being set st x in X holds

G . x <> 0 ) & F is_integral_of f,X & G is_integral_of g,X holds

F / G is_integral_of ((f (#) G) - (F (#) g)) / (G (#) G),X

for f, g, F, G being PartFunc of REAL,REAL st ( for x being set st x in X holds

G . x <> 0 ) & F is_integral_of f,X & G is_integral_of g,X holds

F / G is_integral_of ((f (#) G) - (F (#) g)) / (G (#) G),X

proof end;

theorem :: INTEGRA7:16

for a, b being Real

for f, F being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f | ['a,b'] is continuous & ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = (integral (f,a,x)) + (F . a) ) holds

F is_integral_of f,].a,b.[

for f, F being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f | ['a,b'] is continuous & ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = (integral (f,a,x)) + (F . a) ) holds

F is_integral_of f,].a,b.[

proof end;

theorem :: INTEGRA7:17

for a, b being Real

for f, F being PartFunc of REAL,REAL

for x, x0 being Real st f | [.a,b.] is continuous & [.a,b.] c= dom f & x in ].a,b.[ & x0 in ].a,b.[ & F is_integral_of f,].a,b.[ holds

F . x = (integral (f,x0,x)) + (F . x0)

for f, F being PartFunc of REAL,REAL

for x, x0 being Real st f | [.a,b.] is continuous & [.a,b.] c= dom f & x in ].a,b.[ & x0 in ].a,b.[ & F is_integral_of f,].a,b.[ holds

F . x = (integral (f,x0,x)) + (F . x0)

proof end;

theorem Th18: :: INTEGRA7:18

for a, b being Real

for X being set

for f, F being PartFunc of REAL,REAL st a <= b & ['a,b'] c= X & F is_integral_of f,X & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds

F . b = (integral (f,a,b)) + (F . a)

for X being set

for f, F being PartFunc of REAL,REAL st a <= b & ['a,b'] c= X & F is_integral_of f,X & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds

F . b = (integral (f,a,b)) + (F . a)

proof end;

theorem Th19: :: INTEGRA7:19

for a, b being Real

for X being set

for f being PartFunc of REAL,REAL st a <= b & [.a,b.] c= X & X c= dom f & f | X is continuous holds

( f | ['a,b'] is continuous & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded )

for X being set

for f being PartFunc of REAL,REAL st a <= b & [.a,b.] c= X & X c= dom f & f | X is continuous holds

( f | ['a,b'] is continuous & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded )

proof end;

theorem Th20: :: INTEGRA7:20

for a, b being Real

for X being set

for f, F being PartFunc of REAL,REAL st a <= b & [.a,b.] c= X & X c= dom f & f | X is continuous & F is_integral_of f,X holds

F . b = (integral (f,a,b)) + (F . a)

for X being set

for f, F being PartFunc of REAL,REAL st a <= b & [.a,b.] c= X & X c= dom f & f | X is continuous & F is_integral_of f,X holds

F . b = (integral (f,a,b)) + (F . a)

proof end;

theorem Th21: :: INTEGRA7:21

for a, b being Real

for X being set

for f, g, F, G being PartFunc of REAL,REAL st b <= a & ['b,a'] c= X & f is_integrable_on ['b,a'] & g is_integrable_on ['b,a'] & f | ['b,a'] is bounded & g | ['b,a'] is bounded & X c= dom f & X c= dom g & F is_integral_of f,X & G is_integral_of g,X holds

((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a))

for X being set

for f, g, F, G being PartFunc of REAL,REAL st b <= a & ['b,a'] c= X & f is_integrable_on ['b,a'] & g is_integrable_on ['b,a'] & f | ['b,a'] is bounded & g | ['b,a'] is bounded & X c= dom f & X c= dom g & F is_integral_of f,X & G is_integral_of g,X holds

((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a))

proof end;

theorem :: INTEGRA7:22

for a, b being Real

for X being set

for f, g, F, G being PartFunc of REAL,REAL st b <= a & [.b,a.] c= X & X c= dom f & X c= dom g & f | X is continuous & g | X is continuous & F is_integral_of f,X & G is_integral_of g,X holds

((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a))

for X being set

for f, g, F, G being PartFunc of REAL,REAL st b <= a & [.b,a.] c= X & X c= dom f & X c= dom g & f | X is continuous & g | X is continuous & F is_integral_of f,X & G is_integral_of g,X holds

((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a))

proof end;

theorem :: INTEGRA7:30

for a, b being Real

for n being Element of NAT holds ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b)

for n being Element of NAT holds ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b)

proof end;

theorem :: INTEGRA7:31

for a, b being Real

for H being Functional_Sequence of REAL,REAL

for rseq being Real_Sequence st a < b & ( for n being Element of NAT holds

( H . n is_integrable_on ['a,b'] & (H . n) | ['a,b'] is bounded & rseq . n = integral ((H . n),a,b) ) ) & H is_unif_conv_on ['a,b'] holds

( (lim (H,['a,b'])) | ['a,b'] is bounded & lim (H,['a,b']) is_integrable_on ['a,b'] & rseq is convergent & lim rseq = integral ((lim (H,['a,b'])),a,b) )

for H being Functional_Sequence of REAL,REAL

for rseq being Real_Sequence st a < b & ( for n being Element of NAT holds

( H . n is_integrable_on ['a,b'] & (H . n) | ['a,b'] is bounded & rseq . n = integral ((H . n),a,b) ) ) & H is_unif_conv_on ['a,b'] holds

( (lim (H,['a,b'])) | ['a,b'] is bounded & lim (H,['a,b']) is_integrable_on ['a,b'] & rseq is convergent & lim rseq = integral ((lim (H,['a,b'])),a,b) )

proof end;