:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama

::

:: Received December 7, 1999

:: Copyright (c) 1999-2012 Association of Mizar Users

begin

Lm1: for j being Element of NAT holds (j -' j) + 1 = 1

proof end;

Lm2: for n being Element of NAT st 1 <= n & n <= 2 & not n = 1 holds

n = 2

proof end;

definition

let A be non empty closed_interval Subset of REAL;

let D be Division of A;

correctness

coherence

max (rng (upper_volume ((chi (A,A)),D))) is Real;

by XREAL_0:def 1;

end;
let D be Division of A;

correctness

coherence

max (rng (upper_volume ((chi (A,A)),D))) is Real;

by XREAL_0:def 1;

:: deftheorem defines delta INTEGRA3:def 1 :

for A being non empty closed_interval Subset of REAL

for D being Division of A holds delta D = max (rng (upper_volume ((chi (A,A)),D)));

for A being non empty closed_interval Subset of REAL

for D being Division of A holds delta D = max (rng (upper_volume ((chi (A,A)),D)));

definition

let A be non empty closed_interval Subset of REAL;

let T be DivSequence of A;

ex b_{1} being Real_Sequence st

for i being Element of NAT holds b_{1} . i = delta (T . i)

for b_{1}, b_{2} being Real_Sequence st ( for i being Element of NAT holds b_{1} . i = delta (T . i) ) & ( for i being Element of NAT holds b_{2} . i = delta (T . i) ) holds

b_{1} = b_{2}

end;
let T be DivSequence of A;

func delta T -> Real_Sequence means :Def2: :: INTEGRA3:def 2

for i being Element of NAT holds it . i = delta (T . i);

existence for i being Element of NAT holds it . i = delta (T . i);

ex b

for i being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines delta INTEGRA3:def 2 :

for A being non empty closed_interval Subset of REAL

for T being DivSequence of A

for b_{3} being Real_Sequence holds

( b_{3} = delta T iff for i being Element of NAT holds b_{3} . i = delta (T . i) );

for A being non empty closed_interval Subset of REAL

for T being DivSequence of A

for b

( b

theorem :: INTEGRA3:1

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A st D1 <= D2 holds

delta D1 >= delta D2

for D1, D2 being Division of A st D1 <= D2 holds

delta D1 >= delta D2

proof end;

theorem Th2: :: INTEGRA3:2

for A being non empty closed_interval Subset of REAL

for D being Division of A st vol A <> 0 holds

ex i being Element of NAT st

( i in dom D & vol (divset (D,i)) > 0 )

for D being Division of A st vol A <> 0 holds

ex i being Element of NAT st

( i in dom D & vol (divset (D,i)) > 0 )

proof end;

theorem Th3: :: INTEGRA3:3

for x being Real

for A being non empty closed_interval Subset of REAL

for D being Division of A st x in A holds

ex j being Element of NAT st

( j in dom D & x in divset (D,j) )

for A being non empty closed_interval Subset of REAL

for D being Division of A st x in A holds

ex j being Element of NAT st

( j in dom D & x in divset (D,j) )

proof end;

theorem Th4: :: INTEGRA3:4

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A ex D being Division of A st

( D1 <= D & D2 <= D & rng D = (rng D1) \/ (rng D2) )

for D1, D2 being Division of A ex D being Division of A st

( D1 <= D & D2 <= D & rng D = (rng D1) \/ (rng D2) )

proof end;

theorem Th5: :: INTEGRA3:5

for A being non empty closed_interval Subset of REAL

for D1, D being Division of A st delta D1 < min (rng (upper_volume ((chi (A,A)),D))) holds

for x, y being Real

for i being Element of NAT st i in dom D1 & x in (rng D) /\ (divset (D1,i)) & y in (rng D) /\ (divset (D1,i)) holds

x = y

for D1, D being Division of A st delta D1 < min (rng (upper_volume ((chi (A,A)),D))) holds

for x, y being Real

for i being Element of NAT st i in dom D1 & x in (rng D) /\ (divset (D1,i)) & y in (rng D) /\ (divset (D1,i)) holds

x = y

proof end;

theorem Th7: :: INTEGRA3:7

for i, j being Element of NAT

for A being non empty closed_interval Subset of REAL

for D, D1 being Division of A st D <= D1 & i in dom D & j in dom D & i <= j holds

( indx (D1,D,i) <= indx (D1,D,j) & indx (D1,D,i) in dom D1 )

for A being non empty closed_interval Subset of REAL

for D, D1 being Division of A st D <= D1 & i in dom D & j in dom D & i <= j holds

( indx (D1,D,i) <= indx (D1,D,j) & indx (D1,D,i) in dom D1 )

proof end;

theorem Th8: :: INTEGRA3:8

for i, j being Element of NAT

for A being non empty closed_interval Subset of REAL

for D, D1 being Division of A st D <= D1 & i in dom D & j in dom D & i < j holds

indx (D1,D,i) < indx (D1,D,j)

for A being non empty closed_interval Subset of REAL

for D, D1 being Division of A st D <= D1 & i in dom D & j in dom D & i < j holds

indx (D1,D,i) < indx (D1,D,j)

proof end;

Lm3: for A being non empty closed_interval Subset of REAL

for g being Function of A,REAL st g | A is bounded holds

upper_bound (rng g) >= lower_bound (rng g)

proof end;

Lm4: for A, B being non empty closed_interval Subset of REAL

for f being Function of A,REAL st f | A is bounded & B c= A holds

( lower_bound (rng (f | B)) >= lower_bound (rng f) & lower_bound (rng f) <= upper_bound (rng (f | B)) & upper_bound (rng (f | B)) <= upper_bound (rng f) & lower_bound (rng (f | B)) <= upper_bound (rng f) )

proof end;

Lm5: for j being Element of NAT

for A being non empty closed_interval Subset of REAL

for D1 being Division of A st j in dom D1 holds

vol (divset (D1,j)) <= delta D1

proof end;

Lm6: for x being Real

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for j1 being Element of NAT st j1 = (len D1) - 1 & x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} holds

rng (D2 | (indx (D2,D1,j1))) = rng (D1 | j1)

proof end;

theorem Th10: :: INTEGRA3:10

for x being Real

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for g being Function of A,REAL st x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & g | A is bounded holds

(Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for g being Function of A,REAL st x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & g | A is bounded holds

(Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)

proof end;

theorem Th11: :: INTEGRA3:11

for x being Real

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for g being Function of A,REAL st x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & g | A is bounded holds

(Sum (upper_volume (g,D1))) - (Sum (upper_volume (g,D2))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for g being Function of A,REAL st x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & g | A is bounded holds

(Sum (upper_volume (g,D1))) - (Sum (upper_volume (g,D2))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)

proof end;

Lm7: for y being Real

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL st vol A <> 0 & y in rng (lower_sum_set f) holds

ex D being Division of A st

( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A )

proof end;

theorem Th12: :: INTEGRA3:12

for r being Real

for i, j being Element of NAT

for A being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D & j in dom D & i <= j & r < (mid (D,i,j)) . 1 holds

ex B being non empty closed_interval Subset of REAL st

( r = lower_bound B & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B )

for i, j being Element of NAT

for A being non empty closed_interval Subset of REAL

for D being Division of A st i in dom D & j in dom D & i <= j & r < (mid (D,i,j)) . 1 holds

ex B being non empty closed_interval Subset of REAL st

( r = lower_bound B & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B )

proof end;

Lm8: for A being non empty closed_interval Subset of REAL

for D1 being Division of A st vol A <> 0 & len D1 = 1 holds

<*(lower_bound A)*> ^ D1 is non empty increasing FinSequence of REAL

proof end;

Lm9: for A being non empty closed_interval Subset of REAL

for D2 being Division of A st lower_bound A < D2 . 1 holds

<*(lower_bound A)*> ^ D2 is non empty increasing FinSequence of REAL

proof end;

Lm10: for A being non empty closed_interval Subset of REAL

for D1 being Division of A

for f being Function of A,REAL

for MD1 being Division of A st MD1 = <*(lower_bound A)*> ^ D1 holds

( ( for i being Element of NAT st i in Seg (len D1) holds

divset (MD1,(i + 1)) = divset (D1,i) ) & upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1 & lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1 )

proof end;

Lm11: for A being non empty closed_interval Subset of REAL

for D2, MD2 being Division of A st MD2 = <*(lower_bound A)*> ^ D2 holds

vol (divset (MD2,1)) = 0

proof end;

Lm12: for A being non empty closed_interval Subset of REAL

for D1, MD1 being Division of A st MD1 = <*(lower_bound A)*> ^ D1 holds

delta MD1 = delta D1

proof end;

theorem Th13: :: INTEGRA3:13

for x being Real

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for f being Function of A,REAL st x in divset (D1,(len D1)) & vol A <> 0 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & f | A is bounded & x > lower_bound A holds

(Sum (lower_volume (f,D2))) - (Sum (lower_volume (f,D1))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for f being Function of A,REAL st x in divset (D1,(len D1)) & vol A <> 0 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & f | A is bounded & x > lower_bound A holds

(Sum (lower_volume (f,D2))) - (Sum (lower_volume (f,D1))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

proof end;

theorem Th14: :: INTEGRA3:14

for x being Real

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for f being Function of A,REAL st x in divset (D1,(len D1)) & vol A <> 0 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & f | A is bounded & x > lower_bound A holds

(Sum (upper_volume (f,D1))) - (Sum (upper_volume (f,D2))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for f being Function of A,REAL st x in divset (D1,(len D1)) & vol A <> 0 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & f | A is bounded & x > lower_bound A holds

(Sum (upper_volume (f,D1))) - (Sum (upper_volume (f,D2))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

proof end;

theorem Th15: :: INTEGRA3:15

for r being Real

for i, j being Element of NAT

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A st i in dom D1 & j in dom D1 & i <= j & D1 <= D2 & r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 holds

ex B being non empty closed_interval Subset of REAL ex MD1, MD2 being Division of B st

( r = lower_bound B & upper_bound B = MD2 . (len MD2) & upper_bound B = MD1 . (len MD1) & MD1 <= MD2 & MD1 = mid (D1,i,j) & MD2 = mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j))) )

for i, j being Element of NAT

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A st i in dom D1 & j in dom D1 & i <= j & D1 <= D2 & r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 holds

ex B being non empty closed_interval Subset of REAL ex MD1, MD2 being Division of B st

( r = lower_bound B & upper_bound B = MD2 . (len MD2) & upper_bound B = MD1 . (len MD1) & MD1 <= MD2 & MD1 = mid (D1,i,j) & MD2 = mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j))) )

proof end;

theorem Th16: :: INTEGRA3:16

for x being Real

for A being non empty closed_interval Subset of REAL

for D being Division of A st x in rng D holds

( D . 1 <= x & x <= D . (len D) )

for A being non empty closed_interval Subset of REAL

for D being Division of A st x in rng D holds

( D . 1 <= x & x <= D . (len D) )

proof end;

theorem Th17: :: INTEGRA3:17

for p being FinSequence of REAL

for i, j, k being Element of NAT st p is increasing & i in dom p & j in dom p & k in dom p & p . i <= p . k & p . k <= p . j holds

p . k in rng (mid (p,i,j))

for i, j, k being Element of NAT st p is increasing & i in dom p & j in dom p & k in dom p & p . i <= p . k & p . k <= p . j holds

p . k in rng (mid (p,i,j))

proof end;

theorem Th18: :: INTEGRA3:18

for i being Element of NAT

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f being Function of A,REAL st f | A is bounded & i in dom D holds

lower_bound (rng (f | (divset (D,i)))) <= upper_bound (rng f)

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f being Function of A,REAL st f | A is bounded & i in dom D holds

lower_bound (rng (f | (divset (D,i)))) <= upper_bound (rng f)

proof end;

theorem Th19: :: INTEGRA3:19

for i being Element of NAT

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f being Function of A,REAL st f | A is bounded & i in dom D holds

upper_bound (rng (f | (divset (D,i)))) >= lower_bound (rng f)

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f being Function of A,REAL st f | A is bounded & i in dom D holds

upper_bound (rng (f | (divset (D,i)))) >= lower_bound (rng f)

proof end;

begin

:: Darboux's Theorem

theorem :: INTEGRA3:20

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for T being DivSequence of A st f | A is bounded & delta T is 0 -convergent & delta T is non-zero & vol A <> 0 holds

( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f )

for f being Function of A,REAL

for T being DivSequence of A st f | A is bounded & delta T is 0 -convergent & delta T is non-zero & vol A <> 0 holds

( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f )

proof end;

theorem :: INTEGRA3:21

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for T being DivSequence of A st f | A is bounded & delta T is 0 -convergent & delta T is non-zero & vol A <> 0 holds

( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )

for f being Function of A,REAL

for T being DivSequence of A st f | A is bounded & delta T is 0 -convergent & delta T is non-zero & vol A <> 0 holds

( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )

proof end;