:: Antiderivatives and Integration
:: by Noboru Endou
::
:: Received June 30, 2023
:: Copyright (c) 2023-2025 Association of Mizar Users

registration

cluster open_interval -> open for Element of K19(REAL);

coherence
for b₁ being Subset of REAL st b₁ is open_interval holds
b₁ is open

proof end;

end;

theorem Th1: :: INTEGR26:1

for I being Interval st inf I in I holds
inf I = lower_bound I

proof end;

theorem Th2: :: INTEGR26:2

for I being interval Subset of REAL st sup I in I holds
sup I = upper_bound I

proof end;

theorem Th3: :: INTEGR26:3

for a, b being Real
for I being Interval st a in I & b in I holds
[.a,b.] c= I

proof end;

theorem Th4: :: INTEGR26:4

for f being PartFunc of REAL,REAL
for a, b being Real st a < b & [.a,b.[ c= dom f & f | [.a,b.[ is continuous & f is_differentiable_on ].a,b.[ & f `| ].a,b.[ is_right_convergent_in a holds
( f is_right_differentiable_in a & Rdiff (f,a) = lim_right ((f `| ].a,b.[),a) )

proof end;

theorem Th5: :: INTEGR26:5

for f being PartFunc of REAL,REAL
for a, b being Real st a < b & ].a,b.] c= dom f & f | ].a,b.] is continuous & f is_differentiable_on ].a,b.[ & f `| ].a,b.[ is_left_convergent_in b holds
( f is_left_differentiable_in b & Ldiff (f,b) = lim_left ((f `| ].a,b.[),b) )

proof end;

theorem Th6: :: INTEGR26:6

for a, b, x being Real
for f being PartFunc of REAL,REAL
for I being Interval st inf I <= a & b <= sup I & I c= dom f & f | I is continuous & x in ].a,b.[ holds
f is_continuous_in x

proof end;

theorem :: INTEGR26:7

for X being open Subset of REAL
for f, F being PartFunc of REAL,REAL st X c= dom f & f | X is continuous holds
for x being Real st x in X holds
f is_continuous_in x

proof end;

theorem Th8: :: INTEGR26:8

for a, b, x being Real
for f being PartFunc of REAL,REAL st a <= x & x < b & ].a,b.[ c= dom f & f is_right_convergent_in x holds
( f | ].a,b.[ is_right_convergent_in x & lim_right ((f | ].a,b.[),x) = lim_right (f,x) )

proof end;

theorem Th9: :: INTEGR26:9

for a, b, x being Real
for f being PartFunc of REAL,REAL st a < x & x <= b & ].a,b.[ c= dom f & f is_left_convergent_in x holds
( f | ].a,b.[ is_left_convergent_in x & lim_left ((f | ].a,b.[),x) = lim_left (f,x) )

proof end;

theorem Th10: :: INTEGR26:10

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

proof end;

theorem Th11: :: INTEGR26:11

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

proof end;

theorem Th12: :: INTEGR26:12

for x being Real
for f being PartFunc of REAL,REAL
for I being non empty Interval
for X being Subset of REAL st I c= X & x in I & x <> sup I holds
( f is_right_differentiable_in x iff f | X is_right_differentiable_in x )

proof end;

theorem Th13: :: INTEGR26:13

for x being Real
for f being PartFunc of REAL,REAL
for I being non empty Interval
for X being Subset of REAL st I c= X & x in I & x <> inf I holds
( f is_left_differentiable_in x iff f | X is_left_differentiable_in x )

proof end;

theorem Th14: :: INTEGR26:14

for f being PartFunc of REAL,REAL
for I being open Subset of REAL
for X being Subset of REAL st I c= X holds
( f is_differentiable_on I iff f | X is_differentiable_on I )

proof end;

theorem Th15: :: INTEGR26:15

for f being PartFunc of REAL,REAL
for I being non empty Interval
for X being Subset of REAL st I c= X holds
( f is_differentiable_on_interval I iff f | X is_differentiable_on_interval I )

proof end;

theorem Th16: :: INTEGR26:16

for f being PartFunc of REAL,REAL
for I being non empty Interval
for X being Subset of REAL st I c= X & f is_differentiable_on_interval I holds
f `\ I = (f | X) `\ I

proof end;

theorem Th17: :: INTEGR26:17

for f being PartFunc of REAL,REAL
for I, J being non empty Interval st f is_differentiable_on_interval I & J c= I & inf J < sup J holds
(f `\ I) | J = f `\ J

proof end;

theorem Th18: :: INTEGR26:18

for a, b being R_eal st a < b holds
ex c being Real st
( a < c & c < b )

proof end;

theorem Th19: :: INTEGR26:19

for p, q being R_eal
for f being PartFunc of REAL,REAL st f is_differentiable_on ].p,q.[ & ( for x being Real st x in ].p,q.[ holds
diff (f,x) = 0 ) holds
f | ].p,q.[ is constant

proof end;

theorem Th20: :: INTEGR26:20

for p, q being R_eal
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on ].p,q.[ & f2 is_differentiable_on ].p,q.[ & ( for x being Real st x in ].p,q.[ holds
diff (f1,x) = diff (f2,x) ) holds
( (f1 - f2) | ].p,q.[ is constant & ex r being Real st
for x being Real st x in ].p,q.[ holds
f1 . x = (f2 . x) + r )

proof end;

theorem :: INTEGR26:21

for p, q being R_eal
for f being PartFunc of REAL,REAL st f is_differentiable_on ].p,q.[ & ( for x being Real st x in ].p,q.[ holds
0 < diff (f,x) ) holds
f | ].p,q.[ is increasing

proof end;

theorem :: INTEGR26:22

for p, q being R_eal
for f being PartFunc of REAL,REAL st f is_differentiable_on ].p,q.[ & ( for x being Real st x in ].p,q.[ holds
diff (f,x) < 0 ) holds
f | ].p,q.[ is decreasing

proof end;

theorem :: INTEGR26:23

for p, q being R_eal
for f being PartFunc of REAL,REAL st f is_differentiable_on ].p,q.[ & ( for x being Real st x in ].p,q.[ holds
0 <= diff (f,x) ) holds
f | ].p,q.[ is non-decreasing

proof end;

theorem :: INTEGR26:24

for p, q being R_eal
for f being PartFunc of REAL,REAL st f is_differentiable_on ].p,q.[ & ( for x being Real st x in ].p,q.[ holds
diff (f,x) <= 0 ) holds
f | ].p,q.[ is non-increasing

proof end;

theorem :: INTEGR26:25

for X being open Subset of REAL
for x0 being Real
for f being PartFunc of REAL,REAL st x0 in X & f is_differentiable_on X holds
diff (f,x0) = diff ((f | X),x0)

proof end;

theorem Th26: :: INTEGR26:26

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

proof end;

theorem Th27: :: INTEGR26:27

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) ) holds
( F is_differentiable_on ].a,b.[ & F `| ].a,b.[ = f | ].a,b.[ )

proof end;

definition

let f, F be PartFunc of REAL,REAL;
let I be non empty Interval;

pred F is_antiderivative_of f,I means :Def1: :: INTEGR26:def 1
( F is_differentiable_on_interval I & F `\ I = f | I );

end;

:: deftheorem Def1 defines is_antiderivative_of INTEGR26:def 1 :
for f, F being PartFunc of REAL,REAL
for I being non empty Interval holds
( F is_antiderivative_of f,I iff ( F is_differentiable_on_interval I & F `\ I = f | I ) );

theorem :: INTEGR26:28

for f, F, g, G being PartFunc of REAL,REAL
for I being non empty Interval st F is_antiderivative_of f,I & G is_antiderivative_of g,I holds
( F + G is_antiderivative_of f + g,I & F - G is_antiderivative_of f - g,I )

proof end;

theorem :: INTEGR26:29

for f, F being PartFunc of REAL,REAL
for I being non empty Interval
for r being Real st F is_antiderivative_of f,I holds
r (#) F is_antiderivative_of r (#) f,I

proof end;

theorem :: INTEGR26:30

for f, g, F, G being PartFunc of REAL,REAL
for I being non empty Interval st F is_antiderivative_of f,I & G is_antiderivative_of g,I holds
F (#) G is_antiderivative_of (f (#) G) + (F (#) g),I

proof end;

theorem :: INTEGR26:31

for f, g, F, G being PartFunc of REAL,REAL
for I being non empty Interval st F is_antiderivative_of f,I & G is_antiderivative_of g,I & ( for x being set st x in I holds
G . x <> 0 ) holds
F / G is_antiderivative_of ((f (#) G) - (F (#) g)) / (G (#) G),I

proof end;

theorem Th32: :: INTEGR26:32

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) ) holds
for x being Real st x in ].a,b.[ holds
( F is_differentiable_in x & diff (F,x) = f . x )

proof end;

theorem Th33: :: INTEGR26:33

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 bounded & f is_integrable_on ['a,b'] & [.a,b.] = dom F & ( for x being Real st x in [.a,b.] holds
F . x = integral (f,a,x) ) holds
F is Lipschitzian

proof end;

theorem Th34: :: INTEGR26:34

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) ) holds
( F `| ].a,b.[ is_right_convergent_in a & F `| ].a,b.[ is_left_convergent_in b )

proof end;

theorem Th35: :: INTEGR26:35

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) ) holds
( F is_right_differentiable_in a & Rdiff (F,a) = lim_right ((F `| ].a,b.[),a) )

proof end;

theorem Th36: :: INTEGR26:36

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) ) holds
( F is_left_differentiable_in b & Ldiff (F,b) = lim_left ((F `| ].a,b.[),b) )

proof end;

theorem Th37: :: INTEGR26:37

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) ) holds
( F is_differentiable_on_interval ['a,b'] & F `\ ['a,b'] = f | ['a,b'] )

proof end;

theorem :: INTEGR26:38

for f being PartFunc of REAL,REAL
for a, b being Real holds integral (f,b,a) = - (integral (f,a,b))

proof end;

theorem :: INTEGR26:39

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) ) holds
for x being Real st x in ].a,b.[ holds
( F is_differentiable_in x & diff (F,x) = f . x )

proof end;

Lm1: for f being PartFunc of REAL,REAL
for I being non empty Interval
for a being Real ex F being PartFunc of REAL,REAL st
( dom F = REAL & ( for x being Real st x in I holds
F . x = integral (f,a,x) ) )

proof end;

theorem :: INTEGR26:40

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

proof end;

theorem :: INTEGR26:41

for c being Real
for f, F, G being PartFunc of REAL,REAL
for I being non empty Interval st I c= dom f & F is_antiderivative_of f,I & I c= dom G & ( for x being Real st x in I holds
G . x = (F . x) + c ) holds
G is_antiderivative_of f,I

proof end;

theorem Th42: :: INTEGR26:42

for f, F being PartFunc of REAL,REAL
for I, J being non empty Interval st inf I < sup I & I c= J & F is_antiderivative_of f,J holds
F is_antiderivative_of f,I

proof end;

Lm2: for I, J being Subset of REAL st J c= I holds
].(inf J),(sup J).[ c= ].(inf I),(sup I).[

proof end;

Lm3: for I being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL
for D being Division of I st f is_differentiable_on_interval I & f `\ I is bounded holds
( lower_sum (((f `\ I) || I),D) <= (f . (upper_bound I)) - (f . (lower_bound I)) & (f . (upper_bound I)) - (f . (lower_bound I)) <= upper_sum (((f `\ I) || I),D) )

proof end;

theorem Th43: :: INTEGR26:43

for a, b being Real
for f being PartFunc of REAL,REAL
for D being Division of ['a,b'] st a < b & f is_differentiable_on_interval ['a,b'] & f `\ ['a,b'] is bounded holds
( lower_sum (((f `\ ['a,b']) || ['a,b']),D) <= (f . b) - (f . a) & (f . b) - (f . a) <= upper_sum (((f `\ ['a,b']) || ['a,b']),D) )

proof end;

Lm4: for a, b being Real
for f being PartFunc of REAL,REAL st a < b & f is_differentiable_on_interval ['a,b'] & f `\ ['a,b'] is_integrable_on ['a,b'] & f `\ ['a,b'] is bounded holds
integral ((f `\ ['a,b']),['a,b']) = (f . b) - (f . a)

proof end;

theorem :: INTEGR26:44

for f being PartFunc of REAL,REAL
for a, b being Real
for I being non empty Interval st a in I & b in I & a < b & f is_differentiable_on_interval I & f `\ I is_integrable_on ['a,b'] & f `\ I is bounded holds
( integral ((f `\ ['a,b']),a,b) = (f . b) - (f . a) & integral ((f `\ I),a,b) = (f . b) - (f . a) )

proof end;

theorem :: INTEGR26:45

for f being PartFunc of REAL,REAL
for a being Real
for I being non empty Interval st f is_differentiable_on_interval I & a in I holds
integral ((f `\ I),a,a) = 0

proof end;

Lm5: for f, F, G being PartFunc of REAL,REAL
for I being non empty open_interval Subset of REAL st F is_antiderivative_of f,I & G is_antiderivative_of f,I holds
ex c being Real st
for x being Real st x in I holds
F . x = (G . x) + c

proof end;

theorem :: INTEGR26:46

for f, F, G being PartFunc of REAL,REAL
for I being non empty Interval st F is_antiderivative_of f,I & G is_antiderivative_of f,I holds
ex c being Real st
for x being Real st x in I holds
F . x = (G . x) + c

proof end;

:: Integration by substitution

theorem :: INTEGR26:47

for a, b, p, q being Real
for f, g being PartFunc of REAL,REAL st a < b & p < q & [.a,b.] c= dom f & f | ['a,b'] is continuous & g is_differentiable_on_interval ['p,q'] & g `\ ['p,q'] is_integrable_on ['p,q'] & g `\ ['p,q'] is bounded & rng (g | ['p,q']) c= ['a,b'] & g . p = a & g . q = b holds
integral (f,a,b) = integral (((f * g) (#) (g `\ ['p,q'])),p,q)

proof end;

:: Integration by parts

theorem :: INTEGR26:48

for a, b being Real
for f, g being PartFunc of REAL,REAL st a < b & f is_differentiable_on_interval ['a,b'] & g is_differentiable_on_interval ['a,b'] & f `\ ['a,b'] is_integrable_on ['a,b'] & f `\ ['a,b'] is bounded & g `\ ['a,b'] is_integrable_on ['a,b'] & g `\ ['a,b'] is bounded holds
integral (((f `\ ['a,b']) (#) g),a,b) = (((f . b) * (g . b)) - ((f . a) * (g . a))) - (integral ((f (#) (g `\ ['a,b'])),a,b))

proof end;