INTEGRA2: Scalar Multiple of Riemann Definite Integral

:: Scalar Multiple of Riemann Definite Integral
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received December 7, 1999
:: Copyright (c) 1999-2021 Association of Mizar Users

theorem :: INTEGRA2:1

for A being non empty closed_interval Subset of REAL
for x being Real holds
( x in A iff ( lower_bound A <= x & x <= upper_bound A ) )

proof end;

LM: for p being FinSequence of REAL st ( for n being Nat st n in dom p & n + 1 in dom p holds
p . n <= p . (n + 1) ) holds
for i, j being Nat st i in dom p & j in dom p & i <= j holds
p . i <= p . j

proof end;

definition

let IT be FinSequence of REAL ;

redefine attr IT is non-decreasing means :Def1: :: INTEGRA2:def 1
for n being Nat st n in dom IT & n + 1 in dom IT holds
IT . n <= IT . (n + 1);

compatibility

proof end;

end;

:: deftheorem Def1 defines non-decreasing INTEGRA2:def 1 :

registration

cluster Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued non-decreasing V56() FinSequence-like FinSubsequence-like for FinSequence of REAL ;

existence

proof end;

end;

theorem :: INTEGRA2:2

for p being non-decreasing FinSequence of REAL
for i, j being Nat st i in dom p & j in dom p & i <= j holds
p . i <= p . j

proof end;

theorem :: INTEGRA2:3

for p being FinSequence of REAL ex q being non-decreasing FinSequence of REAL st p,q are_fiberwise_equipotent

proof end;

theorem :: INTEGRA2:4

for D being non empty set
for f being FinSequence of D
for k1, k2, k3 being Nat st 1 <= k1 & k3 <= len f & k1 <= k2 & k2 < k3 holds
(mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3)) = mid (f,k1,k3)

proof end;

definition

let A be real-membered set ;
let x be Real;
:: original: **
redefine func x ** A -> Subset of REAL;
coherence by MEMBERED:3;

end;

theorem :: INTEGRA2:5

for X, Y being non empty set
for f being PartFunc of X,REAL st f | X is bounded_above & Y c= X holds
(f | Y) | Y is bounded_above

proof end;

theorem :: INTEGRA2:6

for X, Y being non empty set
for f being PartFunc of X,REAL st f | X is bounded_below & Y c= X holds
(f | Y) | Y is bounded_below

proof end;

theorem :: INTEGRA2:7

for X being real-membered set
for a being Real holds
( X is empty iff a ** X is empty ) ;

theorem Th8: :: INTEGRA2:8

for r being Real
for X being Subset of REAL holds r ** X = { (r * x) where x is Real : x in X }

proof end;

theorem :: INTEGRA2:9

for r being Real
for X being non empty Subset of REAL st X is bounded_above & 0 <= r holds
r ** X is bounded_above

proof end;

theorem :: INTEGRA2:10

for r being Real
for X being non empty Subset of REAL st X is bounded_above & r <= 0 holds
r ** X is bounded_below

proof end;

theorem :: INTEGRA2:11

for r being Real
for X being non empty Subset of REAL st X is bounded_below & 0 <= r holds
r ** X is bounded_below

proof end;

theorem :: INTEGRA2:12

for r being Real
for X being non empty Subset of REAL st X is bounded_below & r <= 0 holds
r ** X is bounded_above

proof end;

theorem Th13: :: INTEGRA2:13

for r being Real
for X being non empty Subset of REAL st X is bounded_above & 0 <= r holds
upper_bound (r ** X) = r * (upper_bound X)

proof end;

theorem Th14: :: INTEGRA2:14

for r being Real
for X being non empty Subset of REAL st X is bounded_above & r <= 0 holds
lower_bound (r ** X) = r * (upper_bound X)

proof end;

theorem Th15: :: INTEGRA2:15

for r being Real
for X being non empty Subset of REAL st X is bounded_below & 0 <= r holds
lower_bound (r ** X) = r * (lower_bound X)

proof end;

theorem Th16: :: INTEGRA2:16

for r being Real
for X being non empty Subset of REAL st X is bounded_below & r <= 0 holds
upper_bound (r ** X) = r * (lower_bound X)

proof end;

theorem Th17: :: INTEGRA2:17

for r being Real
for X being non empty set
for f being Function of X,REAL holds rng (r (#) f) = r ** (rng f)

proof end;

theorem Th18: :: INTEGRA2:18

for r being Real
for X, Z being non empty set
for f being PartFunc of X,REAL holds rng (r (#) (f | Z)) = r ** (rng (f | Z))

proof end;

theorem Th19: :: INTEGRA2:19

for r being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded & r >= 0 holds
(upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A)

proof end;

theorem Th20: :: INTEGRA2:20

for r being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded & r <= 0 holds
(upper_sum_set (r (#) f)) . D >= (r * (upper_bound (rng f))) * (vol A)

proof end;

theorem Th21: :: INTEGRA2:21

for r being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded & r >= 0 holds
(lower_sum_set (r (#) f)) . D <= (r * (upper_bound (rng f))) * (vol A)

proof end;

theorem Th22: :: INTEGRA2:22

for r being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded & r <= 0 holds
(lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A)

proof end;

theorem Th23: :: INTEGRA2:23

for r being Real
for i being Nat
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_above & r >= 0 holds
(upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i)

proof end;

theorem Th24: :: INTEGRA2:24

for r being Real
for i being Nat
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_above & r <= 0 holds
(lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i)

proof end;

theorem Th25: :: INTEGRA2:25

for r being Real
for i being Nat
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_below & r >= 0 holds
(lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)

proof end;

theorem Th26: :: INTEGRA2:26

for r being Real
for i being Nat
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_below & r <= 0 holds
(upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)

proof end;

theorem Th27: :: INTEGRA2:27

for r being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded_above & r >= 0 holds
upper_sum ((r (#) f),D) = r * (upper_sum (f,D))

proof end;

theorem Th28: :: INTEGRA2:28

for r being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded_above & r <= 0 holds
lower_sum ((r (#) f),D) = r * (upper_sum (f,D))

proof end;

theorem Th29: :: INTEGRA2:29

for r being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded_below & r >= 0 holds
lower_sum ((r (#) f),D) = r * (lower_sum (f,D))

proof end;

theorem Th30: :: INTEGRA2:30

for r being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded_below & r <= 0 holds
upper_sum ((r (#) f),D) = r * (lower_sum (f,D))

proof end;

theorem Th31: :: INTEGRA2:31

for r being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st f | A is bounded & f is integrable holds
( r (#) f is integrable & integral (r (#) f) = r * (integral f) )

proof end;

theorem Th32: :: INTEGRA2:32

for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st f | A is bounded & ( for x being Real st x in A holds
f . x >= 0 ) holds
integral f >= 0

proof end;

theorem Th33: :: INTEGRA2:33

for A being non empty closed_interval Subset of REAL
for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable holds
( f - g is integrable & integral (f - g) = (integral f) - (integral g) )

proof end;

theorem :: INTEGRA2:34

for A being non empty closed_interval Subset of REAL
for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable & ( for x being Real st x in A holds
f . x >= g . x ) holds
integral f >= integral g

proof end;

theorem :: INTEGRA2:35

for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st f | A is bounded holds
rng (upper_sum_set f) is bounded_below

proof end;

theorem :: INTEGRA2:36

for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st f | A is bounded holds
rng (lower_sum_set f) is bounded_above

proof end;

definition

let A be non empty closed_interval Subset of REAL;
mode DivSequence of A is sequence of (divs A);

end;

definition

let A be non empty closed_interval Subset of REAL;
let T be DivSequence of A;
let i be Nat;
:: original: .
redefine func T . i -> Division of A;
coherence

proof end;

end;

definition

let A be non empty closed_interval Subset of REAL;
let f be PartFunc of A,REAL;
let T be DivSequence of A;

func upper_sum (f,T) -> Real_Sequence means :: INTEGRA2:def 2
for i being Nat holds it . i = upper_sum (f,(T . i));

existence

proof end;

uniqueness

proof end;

func lower_sum (f,T) -> Real_Sequence means :: INTEGRA2:def 3
for i being Nat holds it . i = lower_sum (f,(T . i));

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines upper_sum INTEGRA2:def 2 :

:: deftheorem defines lower_sum INTEGRA2:def 3 :

theorem :: INTEGRA2:37

for A being non empty closed_interval Subset of REAL
for D1, D2 being Division of A st D1 <= D2 holds
for j being Nat st j in dom D2 holds
ex i being Nat st
( i in dom D1 & divset (D2,j) c= divset (D1,i) )

proof end;

theorem :: INTEGRA2:38

for A, B being non empty closed_interval Subset of REAL st A c= B holds
vol A <= vol B

proof end;

theorem :: INTEGRA2:39

for A being Subset of REAL
for a, x being Real st x in a ** A holds
ex b being Real st
( b in A & x = a * b )

proof end;

:: missing, 2008.06.10

theorem :: INTEGRA2:40

for A being non empty ext-real-membered set holds 0 ** A = {0}

proof end;