:: 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 :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, INTEGRA1, SUBSET_1, FUNCT_1, FINSEQ_1, NAT_1, RELAT_1, MEASURE7, XBOOLE_0, XXREAL_2, XXREAL_0, SEQ_4, CARD_1, REAL_1, ARYTM_3, ARYTM_1, CARD_3, FINSEQ_2, INTEGRA2, SEQ_1, SEQ_2, ORDINAL2, COMPLEX1, XXREAL_1, FUNCT_3, PARTFUN1, TARSKI, FINSET_1, INTEGR15, MEASURE5, FUNCT_7, INTEGR22, VALUED_0, ZFMISC_1, FCONT_2, ORDINAL4, FUNCOP_1; notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, VALUED_0, COMPLEX1, XXREAL_2, FINSEQ_1, FINSEQ_2, SEQ_1, SEQ_2, RVSUM_1, SEQ_4, RCOMP_1, FCONT_1, FCONT_2, MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3, INTEGR22; constructors REAL_1, FINSEQOP, MONOID_0, SEQ_4, NAT_D, FCONT_1, FCONT_2, RELSET_1, SEQ_2, INTEGRA3, COMSEQ_2, INTEGR22; registrations NUMBERS, XREAL_0, INTEGRA1, NAT_1, MEMBERED, ORDINAL1, FCONT_1, VALUED_0, RELSET_1, CARD_1, MEASURE5, FINSEQ_1, RVSUM_1, FINSET_1, SEQ_4, FINSEQ_2, RELAT_1, SEQM_3, INT_1, XXREAL_2; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: 1. Preliminaries theorem :: INTEGR23:1 for E be Real, q be FinSequence of REAL, S be FinSequence of REAL st len S = len q & for i be Nat st i in dom S holds ex r be Real st r = q.i & S.i= r * E holds Sum S = (Sum q) * E; theorem :: INTEGR23:2 for xseq, yseq be FinSequence of REAL st len xseq = len yseq & (for i be Element of NAT st i in dom xseq holds ex v be Real st v = xseq.i & yseq.i = |.v.|) holds |.Sum xseq.| <= Sum yseq; theorem :: INTEGR23:3 for p,q be FinSequence of REAL st len p = len q & (for j be Nat st j in dom p holds |. p.j .| <= q.j) holds |. Sum(p) .| <= Sum(q); theorem :: INTEGR23:4 for n be Nat, a be object holds len (n |-> a) = n; theorem :: INTEGR23:5 for p be FinSequence, a be object holds p = (len p) |-> a iff (for k be object st k in dom p holds p.k = a); theorem :: INTEGR23:6 for p be FinSequence of REAL, i be Nat, r be Real st i in dom p & p.i = r & for k be Nat st k in dom p & k <> i holds p.k = 0 holds Sum p = r; theorem :: INTEGR23:7 for p,q be FinSequence of REAL st len p <= len q & for i be 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; theorem :: INTEGR23:8 for a,b,c,d be Real st b <= c holds [.a,b.] /\ [.c,d.] c= [.b,b.]; theorem :: INTEGR23:9 for a be Real, A be Subset of REAL, rho be real-valued Function st A c= [.a,a.] holds vol(A,rho) = 0; theorem :: INTEGR23:10 for s be non empty increasing FinSequence of REAL, m be Nat st m in dom s holds s|m is non empty increasing FinSequence of REAL; theorem :: INTEGR23:11 for s,t be non empty increasing FinSequence of REAL st s.(len s) < t.1 holds s^t is non empty increasing FinSequence of REAL; theorem :: INTEGR23:12 for s be non empty increasing FinSequence of REAL, a be Real st s.(len s) < a holds s^<*a*> is non empty increasing FinSequence of REAL; theorem :: INTEGR23:13 for T be FinSequence of REAL, n,m be Nat st n+1 < m <= len T holds ex TM1 be FinSequence of REAL st len TM1 = m-(n+1) & rng TM1 c= rng T & for i be Nat st i in dom TM1 holds TM1.i = T.(i+n); theorem :: INTEGR23:14 for T be non empty increasing FinSequence of REAL, n,m be Nat st n+1 < m <= len T holds ex TM1 be non empty increasing FinSequence of REAL st len TM1 = m-(n+1) & rng TM1 c= rng T & for i be Nat st i in dom TM1 holds TM1.i = T.(i+n); theorem :: INTEGR23:15 for p be FinSequence of REAL, n,m be Nat st n+1 < m <= len p holds ex pM1 be FinSequence of REAL st len pM1 = m-(n+1)-1 & rng pM1 c= rng p & for i be Nat st i in dom pM1 holds pM1.i = p.(i+n+1); begin :: 2. Existence of Riemann-Stieltjes Integral for Continuous Functions theorem :: INTEGR23:16 for A be non empty closed_interval Subset of REAL, T be Division of A, rho be real-valued Function, B be non empty closed_interval Subset of REAL, S0 be non empty increasing FinSequence of REAL, ST be FinSequence of REAL st B c= A & lower_bound B = lower_bound A & ex S be Division of B st S = S0 & len ST = len S & for j be Nat st j in dom S holds ex p be FinSequence of REAL st ST.j = Sum p & len p = len T & for i be Nat st i in dom T holds p.i = |. vol(divset(T,i) /\ divset(S,j), rho) .| holds ex H be Division of B, F be var_volume of rho,H st Sum ST = Sum(F); theorem :: INTEGR23:17 for A be non empty closed_interval Subset of REAL, rho be Function of A,REAL, T,S be Division of A st rho is bounded_variation holds ex ST be FinSequence of REAL st len ST = len S & Sum ST <= total_vd(rho) & for j be Nat st j in dom S holds ex p be FinSequence of REAL st ST.j = Sum p & len p = len T & for i be Nat st i in dom T holds p.i = |. vol(divset(T,i) /\ divset(S,j),rho) .|; theorem :: INTEGR23:18 for A be non empty closed_interval Subset of REAL, rho be Function of A,REAL, u be PartFunc of REAL,REAL st rho is bounded_variation & dom u = A & u|A is uniformly_continuous holds for T being DivSequence of A, S be middle_volume_Sequence of rho,u,T st delta T is convergent & lim delta T = 0 holds middle_sum(S) is convergent; theorem :: INTEGR23:19 for A be non empty closed_interval Subset of REAL, rho be Function of A,REAL, u be PartFunc of REAL,REAL, T0,T,T1 be DivSequence of A, S0 be middle_volume_Sequence of rho,u,T0, S be middle_volume_Sequence of rho,u,T st for i be Nat holds T1.(2*i) = T0.i & T1.(2*i+1) = T.i ex S1 be middle_volume_Sequence of rho,u,T1 st for i be Nat holds S1.(2*i) = S0.i & S1.(2*i+1) = S.i; theorem :: INTEGR23:20 for Sq0,Sq,Sq1 be Real_Sequence st Sq1 is convergent & for i be 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; theorem :: INTEGR23:21 for A be non empty closed_interval Subset of REAL, rho be Function of A,REAL, u be continuous PartFunc of REAL,REAL st rho is bounded_variation & dom u = A holds u is_RiemannStieltjes_integrable_with rho;