INTEGRA7: Riemann Indefinite Integral of Functions of Real Variable

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 )

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 )

proof end;

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

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

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

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

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)

proof end;

definition

let X be set ;
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines IntegralFuncs INTEGRA7:def 1 :

:: deftheorem defines is_integral_of INTEGRA7:def 2 :

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 )

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

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

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

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.[

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)

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)

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 )

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)

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

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

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)

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

proof end;

theorem Th32: :: INTEGRA7:32

for a, b being Real
for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is continuous holds
ex F being PartFunc of REAL,REAL st
( ].a,b.[ c= dom F & ( for t being Real st t in ].a,b.[ holds
F . t = integral (f,a,t) ) & ( for t being Real st t in ].a,b.[ holds
( F is_differentiable_in t & diff (F,t) = f . t ) ) )

proof end;

theorem :: INTEGRA7:33

for f, P being PartFunc of REAL,REAL
for x, y, a, b, s, t being Real st x <= y & s <= t & ['s,t'] c= ].a,b.[ & ['x,y'] c= dom f & f is continuous & P is_differentiable_on ].a,b.[ & P .: ].a,b.[ is open Subset of REAL & P `| ].a,b.[ is continuous & P .: ].a,b.[ c= ].x,y.[ & ['s,t'] c= dom (f * P) holds
( f | ['x,y'] is bounded & f is_integrable_on ['x,y'] & ((f * P) (#) (P `| ].a,b.[)) | ['s,t'] is continuous & ['s,t'] c= dom ((f * P) (#) (P `| ].a,b.[)) & ((f * P) (#) (P `| ].a,b.[)) | ['s,t'] is bounded & (f * P) (#) (P `| ].a,b.[) is_integrable_on ['s,t'] & integral (((f * P) (#) (P `| ].a,b.[)),s,t) = integral (f,(P . s),(P . t)) )

proof end;