:: INTEGRA3 semantic presentation

Lm1: for a being Real
for p being FinSequence of REAL st a in dom p holds
( 1 <= a & a <= len p )

proof end;

Lm2: for a being Real holds a - 1 <= a
by XREAL_1:148;

Lm3: for j being Nat holds (j -' j) + 1 = 1

proof end;

Lm4: for n being Nat st 1 <= n & n <= 2 & not n = 1 holds
n = 2

proof end;

theorem Th1: :: INTEGRA3:1

for A being closed-interval Subset of REAL
for D being Element of divs A st vol A <> 0 holds
ex i being Nat st
( i in dom D & vol (divset D,i) > 0 )

proof end;

theorem Th2: :: INTEGRA3:2

for x being Real
for A being closed-interval Subset of REAL
for D being Element of divs A st x in A holds
ex j being Nat st
( j in dom D & x in divset D,j )

proof end;

theorem Th3: :: INTEGRA3:3

for A being closed-interval Subset of REAL
for D1, D2 being Element of divs A ex D being Element of divs A st
( D1 <= D & D2 <= D & rng D = (rng D1) \/ (rng D2) )

proof end;

theorem Th4: :: INTEGRA3:4

for A being closed-interval Subset of REAL
for D, D1 being Element of divs A st delta D1 < min (rng (upper_volume (chi A,A),D)) holds
for x, y being Real
for i being 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 Th5: :: INTEGRA3:5

for p, q being FinSequence of REAL st rng p = rng q & p is increasing & q is increasing holds
p = q

proof end;

theorem Th6: :: INTEGRA3:6

for i, j being Nat
for A being closed-interval Subset of REAL
for D, D1 being Element of divs 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 Th7: :: INTEGRA3:7

for i, j being Nat
for A being closed-interval Subset of REAL
for D, D1 being Element of divs 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;

theorem Th8: :: INTEGRA3:8

for A being closed-interval Subset of REAL
for D being Element of divs A holds delta D >= 0

proof end;

Lm5: for A being closed-interval Subset of REAL
for g being Function of A, REAL st g is_bounded_on A holds
sup (rng g) >= inf (rng g)

proof end;

Lm6: for A, B being closed-interval Subset of REAL
for f being Function of A, REAL st f is_bounded_on A & B c= A holds
( inf (rng (f | B)) >= inf (rng f) & inf (rng f) <= sup (rng (f | B)) & sup (rng (f | B)) <= sup (rng f) & inf (rng (f | B)) <= sup (rng f) )

proof end;

Lm7: for j being Nat
for A being closed-interval Subset of REAL
for D1 being Element of divs A st j in dom D1 holds
vol (divset D1,j) <= delta D1

proof end;

Lm8: for x being Real
for A being closed-interval Subset of REAL
for j1 being Nat
for D1, D2 being Element of divs A 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 Th9: :: INTEGRA3:9

for x being Real
for A being closed-interval Subset of REAL
for g being Function of A, REAL
for D1, D2 being Element of divs A st x in divset D1,(len D1) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & g is_bounded_on A holds
(Sum (lower_volume g,D2)) - (Sum (lower_volume g,D1)) <= ((sup (rng g)) - (inf (rng g))) * (delta D1)

proof end;

theorem Th10: :: INTEGRA3:10

for x being Real
for A being closed-interval Subset of REAL
for g being Function of A, REAL
for D1, D2 being Element of divs A st x in divset D1,(len D1) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & g is_bounded_on A holds
(Sum (upper_volume g,D1)) - (Sum (upper_volume g,D2)) <= ((sup (rng g)) - (inf (rng g))) * (delta D1)

proof end;

Lm9: for y being Real
for A being closed-interval Subset of REAL
for f being PartFunc of A, REAL st vol A <> 0 & y in rng (lower_sum_set f) holds
ex D being Element of divs A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > inf A )

proof end;

theorem Th11: :: INTEGRA3:11

for A being closed-interval Subset of REAL
for D being Element of divs A
for r being Real
for i, j being Nat st i in dom D & j in dom D & i <= j & r < (mid D,i,j) . 1 holds
ex B being closed-interval Subset of REAL st
( r = inf B & sup B = (mid D,i,j) . (len (mid D,i,j)) & len (mid D,i,j) = (j - i) + 1 & mid D,i,j is DivisionPoint of B )

proof end;

Lm10: for A being closed-interval Subset of REAL
for D1 being Element of divs A st vol A <> 0 & len D1 = 1 holds
<*(inf A)*> ^ D1 is non empty increasing FinSequence of REAL

proof end;

Lm11: for A being closed-interval Subset of REAL
for D2 being Element of divs A st inf A < D2 . 1 holds
<*(inf A)*> ^ D2 is non empty increasing FinSequence of REAL

proof end;

Lm12: for A being closed-interval Subset of REAL
for f being PartFunc of A, REAL
for D1, MD1 being Element of divs A st MD1 = <*(inf A)*> ^ D1 holds
( ( for i being 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;

Lm13: for A being closed-interval Subset of REAL
for D2, MD2 being Element of divs A st MD2 = <*(inf A)*> ^ D2 holds
vol (divset MD2,1) = 0

proof end;

Lm14: for A being closed-interval Subset of REAL
for f being Function of A, REAL
for D1, MD1 being Element of divs A st MD1 = <*(inf A)*> ^ D1 holds
delta MD1 = delta D1

proof end;

theorem Th12: :: INTEGRA3:12

for x being Real
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for D1, D2 being Element of divs A st x in divset D1,(len D1) & vol A <> 0 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & f is_bounded_on A & x > inf A holds
(Sum (lower_volume f,D2)) - (Sum (lower_volume f,D1)) <= ((sup (rng f)) - (inf (rng f))) * (delta D1)

proof end;

theorem Th13: :: INTEGRA3:13

for x being Real
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for D1, D2 being Element of divs A st x in divset D1,(len D1) & vol A <> 0 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & f is_bounded_on A & x > inf A holds
(Sum (upper_volume f,D1)) - (Sum (upper_volume f,D2)) <= ((sup (rng f)) - (inf (rng f))) * (delta D1)

proof end;

theorem Th14: :: INTEGRA3:14

for A being closed-interval Subset of REAL
for D1, D2 being Element of divs A
for r being Real
for i, j being Nat 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 closed-interval Subset of REAL ex MD1, MD2 being Element of divs B st
( r = inf B & sup B = MD2 . (len MD2) & sup 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 Th15: :: INTEGRA3:15

for x being Real
for A being closed-interval Subset of REAL
for D being Element of divs A st x in rng D holds
( D . 1 <= x & x <= D . (len D) )

proof end;

theorem Th16: :: INTEGRA3:16

for p being FinSequence of REAL
for i, j, k being 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 Th17: :: INTEGRA3:17

for i being Nat
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for D being Element of divs A st f is_bounded_on A & i in dom D holds
inf (rng (f | (divset D,i))) <= sup (rng f)

proof end;

theorem Th18: :: INTEGRA3:18

for i being Nat
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for D being Element of divs A st f is_bounded_on A & i in dom D holds
sup (rng (f | (divset D,i))) >= inf (rng f)

proof end;

theorem :: INTEGRA3:19

for A being closed-interval Subset of REAL
for f being Function of A, REAL
for T being DivSequence of A st f is_bounded_on A & delta T is convergent_to_0 & vol A <> 0 holds
( lower_sum f,T is convergent & lim (lower_sum f,T) = lower_integral f )

proof end;

theorem :: INTEGRA3:20

for A being closed-interval Subset of REAL
for f being Function of A, REAL
for T being DivSequence of A st f is_bounded_on A & delta T is convergent_to_0 & vol A <> 0 holds
( upper_sum f,T is convergent & lim (upper_sum f,T) = upper_integral f )

proof end;