:: The Basic Existence Theorem of Riemann-Stieltjes Integral
:: by Kazuhisa Nakasho , Keiko Narita and Yasunari Shidama
::
:: Received October 18, 2016
:: Copyright (c) 2016-2021 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

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

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

proof end;

theorem Th4: :: INTEGR23:4

for n being Nat
for a being object holds len (n |-> a) = n

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 )

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

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

proof end;

theorem Th10: :: INTEGR23:8

for a, b, c, d being Real st b <= c holds
[.a,b.] /\ [.c,d.] c= [.b,b.]

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

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

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

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

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) ) )

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) ) )

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) ) )

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

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)).| ) ) ) )

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

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 )

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 )

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

proof end;