:: by Kazuhisa Nakasho , Keiko Narita and Yasunari Shidama

::

:: Received October 18, 2016

:: Copyright (c) 2016-2017 Association of Mizar Users

theorem Th1: :: INTEGR23:1

for E being Real

for q, S being FinSequence of REAL st len S = len q & ( for i being Nat st i in dom S holds

ex r being Real st

( r = q . i & S . i = r * E ) ) holds

Sum S = (Sum q) * E

for q, S being FinSequence of REAL st len S = len q & ( for i being Nat st i in dom S holds

ex r being Real st

( r = q . i & S . i = r * E ) ) holds

Sum S = (Sum q) * E

proof end;

Lm1: for xseq, yseq being FinSequence of REAL st len xseq = (len yseq) + 1 & xseq | (len yseq) = yseq holds

ex v being Real st

( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )

proof end;

theorem Th2: :: INTEGR23:2

for xseq, yseq being FinSequence of REAL st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds

ex v being Real st

( v = xseq . i & yseq . i = |.v.| ) ) holds

|.(Sum xseq).| <= Sum yseq

ex v being Real st

( v = xseq . i & yseq . i = |.v.| ) ) holds

|.(Sum xseq).| <= Sum yseq

proof end;

theorem Th3: :: INTEGR23:3

for p, q being FinSequence of REAL st len p = len q & ( for j being Nat st j in dom p holds

|.(p . j).| <= q . j ) holds

|.(Sum p).| <= Sum q

|.(p . j).| <= q . j ) holds

|.(Sum p).| <= Sum q

proof end;

theorem Th5: :: INTEGR23:5

for p being FinSequence

for a being object holds

( p = (len p) |-> a iff for k being object st k in dom p holds

p . k = a )

for a being object holds

( p = (len p) |-> a iff for k being object st k in dom p holds

p . k = a )

proof end;

theorem Th8: :: INTEGR23:6

for p being FinSequence of REAL

for i being Nat

for r being Real st i in dom p & p . i = r & ( for k being Nat st k in dom p & k <> i holds

p . k = 0 ) holds

Sum p = r

for i being Nat

for r being Real st i in dom p & p . i = r & ( for k being Nat st k in dom p & k <> i holds

p . k = 0 ) holds

Sum p = r

proof end;

theorem Th9: :: INTEGR23:7

for p, q being FinSequence of REAL st len p <= len q & ( for i being Nat st i in dom q holds

( ( i <= len p implies q . i = p . i ) & ( len p < i implies q . i = 0 ) ) ) holds

Sum q = Sum p

( ( i <= len p implies q . i = p . i ) & ( len p < i implies q . i = 0 ) ) ) holds

Sum q = Sum p

proof end;

theorem Th11: :: INTEGR23:9

for a being Real

for A being Subset of REAL

for rho being real-valued Function st A c= [.a,a.] holds

vol (A,rho) = 0

for A being Subset of REAL

for rho being real-valued Function st A c= [.a,a.] holds

vol (A,rho) = 0

proof end;

theorem Th12: :: INTEGR23:10

for s being non empty increasing FinSequence of REAL

for m being Nat st m in dom s holds

s | m is non empty increasing FinSequence of REAL

for m being Nat st m in dom s holds

s | m is non empty increasing FinSequence of REAL

proof end;

theorem Th13: :: INTEGR23:11

for s, t being non empty increasing FinSequence of REAL st s . (len s) < t . 1 holds

s ^ t is non empty increasing FinSequence of REAL

s ^ t is non empty increasing FinSequence of REAL

proof end;

theorem Th14: :: INTEGR23:12

for s being non empty increasing FinSequence of REAL

for a being Real st s . (len s) < a holds

s ^ <*a*> is non empty increasing FinSequence of REAL

for a being Real st s . (len s) < a holds

s ^ <*a*> is non empty increasing FinSequence of REAL

proof end;

theorem Th15: :: INTEGR23:13

for T being FinSequence of REAL

for n, m being Nat st n + 1 < m & m <= len T holds

ex TM1 being FinSequence of REAL st

( len TM1 = m - (n + 1) & rng TM1 c= rng T & ( for i being Nat st i in dom TM1 holds

TM1 . i = T . (i + n) ) )

for n, m being Nat st n + 1 < m & m <= len T holds

ex TM1 being FinSequence of REAL st

( len TM1 = m - (n + 1) & rng TM1 c= rng T & ( for i being Nat st i in dom TM1 holds

TM1 . i = T . (i + n) ) )

proof end;

theorem Th16: :: INTEGR23:14

for T being non empty increasing FinSequence of REAL

for n, m being Nat st n + 1 < m & m <= len T holds

ex TM1 being non empty increasing FinSequence of REAL st

( len TM1 = m - (n + 1) & rng TM1 c= rng T & ( for i being Nat st i in dom TM1 holds

TM1 . i = T . (i + n) ) )

for n, m being Nat st n + 1 < m & m <= len T holds

ex TM1 being non empty increasing FinSequence of REAL st

( len TM1 = m - (n + 1) & rng TM1 c= rng T & ( for i being Nat st i in dom TM1 holds

TM1 . i = T . (i + n) ) )

proof end;

theorem Th17: :: INTEGR23:15

for p being FinSequence of REAL

for n, m being Nat st n + 1 < m & m <= len p holds

ex pM1 being FinSequence of REAL st

( len pM1 = (m - (n + 1)) - 1 & rng pM1 c= rng p & ( for i being Nat st i in dom pM1 holds

pM1 . i = p . ((i + n) + 1) ) )

for n, m being Nat st n + 1 < m & m <= len p holds

ex pM1 being FinSequence of REAL st

( len pM1 = (m - (n + 1)) - 1 & rng pM1 c= rng p & ( for i being Nat st i in dom pM1 holds

pM1 . i = p . ((i + n) + 1) ) )

proof end;

theorem Th18: :: INTEGR23:16

for A being non empty closed_interval Subset of REAL

for T being Division of A

for rho being real-valued Function

for B being non empty closed_interval Subset of REAL

for S0 being non empty increasing FinSequence of REAL

for ST being FinSequence of REAL st B c= A & lower_bound B = lower_bound A & ex S being Division of B st

( S = S0 & len ST = len S & ( for j being Nat st j in dom S holds

ex p being FinSequence of REAL st

( ST . j = Sum p & len p = len T & ( for i being Nat st i in dom T holds

p . i = |.(vol (((divset (T,i)) /\ (divset (S,j))),rho)).| ) ) ) ) holds

ex H being Division of B ex F being var_volume of rho,H st Sum ST = Sum F

for T being Division of A

for rho being real-valued Function

for B being non empty closed_interval Subset of REAL

for S0 being non empty increasing FinSequence of REAL

for ST being FinSequence of REAL st B c= A & lower_bound B = lower_bound A & ex S being Division of B st

( S = S0 & len ST = len S & ( for j being Nat st j in dom S holds

ex p being FinSequence of REAL st

( ST . j = Sum p & len p = len T & ( for i being Nat st i in dom T holds

p . i = |.(vol (((divset (T,i)) /\ (divset (S,j))),rho)).| ) ) ) ) holds

ex H being Division of B ex F being var_volume of rho,H st Sum ST = Sum F

proof end;

Lm2: for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

for T, S being Division of A

for ST being FinSequence of REAL st rho is bounded_variation & len ST = len S & ( for j being Nat st j in dom S holds

ex p being FinSequence of REAL st

( ST . j = Sum p & len p = len T & ( for i being Nat st i in dom T holds

p . i = |.(vol (((divset (T,i)) /\ (divset (S,j))),rho)).| ) ) ) holds

ex H being Division of A ex F being var_volume of rho,H st Sum ST = Sum F

proof end;

theorem Th19: :: INTEGR23:17

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

for T, S being Division of A st rho is bounded_variation holds

ex ST being FinSequence of REAL st

( len ST = len S & Sum ST <= total_vd rho & ( for j being Nat st j in dom S holds

ex p being FinSequence of REAL st

( ST . j = Sum p & len p = len T & ( for i being Nat st i in dom T holds

p . i = |.(vol (((divset (T,i)) /\ (divset (S,j))),rho)).| ) ) ) )

for rho being Function of A,REAL

for T, S being Division of A st rho is bounded_variation holds

ex ST being FinSequence of REAL st

( len ST = len S & Sum ST <= total_vd rho & ( for j being Nat st j in dom S holds

ex p being FinSequence of REAL st

( ST . j = Sum p & len p = len T & ( for i being Nat st i in dom T holds

p . i = |.(vol (((divset (T,i)) /\ (divset (S,j))),rho)).| ) ) ) )

proof end;

theorem Th20: :: INTEGR23:18

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

for u being PartFunc of REAL,REAL st rho is bounded_variation & dom u = A & u | A is uniformly_continuous holds

for T being DivSequence of A

for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds

middle_sum S is convergent

for rho being Function of A,REAL

for u being PartFunc of REAL,REAL st rho is bounded_variation & dom u = A & u | A is uniformly_continuous holds

for T being DivSequence of A

for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds

middle_sum S is convergent

proof end;

theorem Th21: :: INTEGR23:19

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

for u being PartFunc of REAL,REAL

for T0, T, T1 being DivSequence of A

for S0 being middle_volume_Sequence of rho,u,T0

for S being middle_volume_Sequence of rho,u,T st ( for i being Nat holds

( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i ) ) holds

ex S1 being middle_volume_Sequence of rho,u,T1 st

for i being Nat holds

( S1 . (2 * i) = S0 . i & S1 . ((2 * i) + 1) = S . i )

for rho being Function of A,REAL

for u being PartFunc of REAL,REAL

for T0, T, T1 being DivSequence of A

for S0 being middle_volume_Sequence of rho,u,T0

for S being middle_volume_Sequence of rho,u,T st ( for i being Nat holds

( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i ) ) holds

ex S1 being middle_volume_Sequence of rho,u,T1 st

for i being Nat holds

( S1 . (2 * i) = S0 . i & S1 . ((2 * i) + 1) = S . i )

proof end;

theorem Th22: :: INTEGR23:20

for Sq0, Sq, Sq1 being Real_Sequence st Sq1 is convergent & ( for i being Nat holds

( Sq1 . (2 * i) = Sq0 . i & Sq1 . ((2 * i) + 1) = Sq . i ) ) holds

( Sq0 is convergent & lim Sq0 = lim Sq1 & Sq is convergent & lim Sq = lim Sq1 )

( Sq1 . (2 * i) = Sq0 . i & Sq1 . ((2 * i) + 1) = Sq . i ) ) holds

( Sq0 is convergent & lim Sq0 = lim Sq1 & Sq is convergent & lim Sq = lim Sq1 )

proof end;

theorem :: INTEGR23:21

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

for u being continuous PartFunc of REAL,REAL st rho is bounded_variation & dom u = A holds

u is_RiemannStieltjes_integrable_with rho

for rho being Function of A,REAL

for u being continuous PartFunc of REAL,REAL st rho is bounded_variation & dom u = A holds

u is_RiemannStieltjes_integrable_with rho

proof end;