:: The Linearity of Riemann Integral on Functions from $\mathbbbR$ into Real
:: {B}anach Space
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received October 7, 2013
:: Copyright (c) 2013-2016 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 PRE_TOPC, NORMSP_1, FUNCT_1, ARYTM_1, NAT_1, SUBSET_1, NUMBERS,
CARD_1, XXREAL_0, REAL_1, ARYTM_3, RELAT_1, ORDINAL2, SEQ_2, LOPBAN_1,
STRUCT_0, COMPLEX1, VALUED_1, SUPINF_2, XBOOLE_0, INTEGRA1, INTEGRA2,
FINSEQ_1, TARSKI, INTEGRA5, INTEGR15, INTEGRA4, MEASURE7, CARD_3,
XXREAL_1, PARTFUN1, SEQ_4, XXREAL_2, MEASURE5, FUNCT_3, ORDINAL4,
RFINSEQ;
notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, VALUED_0, COMPLEX1,
XXREAL_2, FINSEQ_1, FINSEQ_2, SEQ_2, RFUNCT_1, RVSUM_1, RFINSEQ, SEQ_4,
RCOMP_1, MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3, INTEGRA4, INTEGRA5,
STRUCT_0, PRE_TOPC, RLVECT_1, VFUNCT_1, NORMSP_0, NORMSP_1, LOPBAN_1,
INTEGR15, INTEGR18, NFCONT_3, INTEGR19;
constructors ABIAN, SEQ_2, RELSET_1, SEQ_4, VFUNCT_1, PDIFF_1, RLSUB_1,
FCONT_1, NFCONT_1, INTEGRA3, INTEGRA4, NDIFF_3, INTEGR18, RVSUM_1,
INTEGR19, INTEGR15, COMSEQ_2, VALUED_2, BINOM, FDIFF_1, NFCONT_2, C0SP2,
ORDEQ_01, RFINSEQ, RFUNCT_1, RFINSEQ2, SQUARE_1, PDIFF_7, NDIFF_5,
INTEGR20, NEWTON;
registrations STRUCT_0, NAT_1, XXREAL_0, NUMBERS, XBOOLE_0, FUNCT_2, XREAL_0,
MEMBERED, NORMSP_1, RELAT_1, RELSET_1, INTEGRA1, ORDINAL1, NFCONT_3,
XXREAL_2, RLVECT_1, VALUED_0, FINSEQ_1, FINSET_1, MEASURE5, SEQM_3,
INT_1, CARD_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
begin :: Some Properties of Bounded Functions
reserve Z for RealNormSpace;
reserve a,b,c,d,e,r for Real;
reserve A,B for non empty closed_interval Subset of REAL;
theorem :: INTEGR21:1
for f be PartFunc of REAL,the carrier of Z st
f is bounded & A c= dom f holds f|A is bounded;
theorem :: INTEGR21:2
for f be PartFunc of REAL,the carrier of Z
st f|A is bounded & B c= A & B c= dom (f|A)
holds f|B is bounded;
theorem :: INTEGR21:3
for f be PartFunc of REAL,the carrier of Z
st a <= c & c <= d & d <= b & f| ['a,b'] is bounded & ['a,b'] c= dom f
holds f| ['c,d'] is bounded;
theorem :: INTEGR21:4
for X,Y be set, f1,f2 be PartFunc of REAL,the carrier of Z
st f1|X is bounded & f2|Y is bounded
holds (f1+f2) | (X /\ Y) is bounded & (f1-f2) | (X /\ Y) is bounded;
theorem :: INTEGR21:5
for X be set, f be PartFunc of REAL,the carrier of Z
st f|X is bounded holds (r(#)f)|X is bounded;
theorem :: INTEGR21:6
for X be set, f be PartFunc of REAL,the carrier of Z
st f|X is bounded holds (-f)|X is bounded;
theorem :: INTEGR21:7
for f be Function of A,the carrier of Z holds
f is bounded iff ||.f.|| is bounded;
theorem :: INTEGR21:8
for f be PartFunc of REAL,the carrier of Z st
A c= dom f holds ||.f|A.|| = (||.f.||) |A;
theorem :: INTEGR21:9
for g be PartFunc of REAL,the carrier of Z
st A c= dom g & g|A is bounded
holds (||.g.||) |A is bounded;
begin :: Some Properties of Integral of Continuous Functions
reserve X,Y for RealBanachSpace;
reserve E for Point of Y;
theorem :: INTEGR21:10
for Y be RealNormSpace,
f be continuous PartFunc of REAL,the carrier of Y
st a <= b & ['a,b'] c= dom f holds ||.f.|| | ['a,b'] is bounded;
theorem :: INTEGR21:11
for Y be RealNormSpace, f be continuous PartFunc of REAL,the carrier of Y
st a <= b & ['a,b'] c= dom f holds f|['a,b'] is bounded;
theorem :: INTEGR21:12
for Y be RealNormSpace,
f be continuous PartFunc of REAL,the carrier of Y
st a <= b & ['a,b'] c= dom f
holds ||.f.|| is_integrable_on ['a,b'];
theorem :: INTEGR21:13
for f be continuous PartFunc of REAL,the carrier of Y
st a <= c & c <= d & d <= b & ['a,b'] c= dom f
holds f is_integrable_on ['c,d'];
theorem :: INTEGR21:14
for f be PartFunc of REAL,the carrier of Y st a <= b & ['a,b'] c= dom f
holds integral(f,b,a) = - integral(f,a,b);
theorem :: INTEGR21:15
for f be continuous PartFunc of REAL,the carrier of Y
st a <= b & ['a,b'] c= dom f & c in ['a,b'] holds
f is_integrable_on ['a,c'] & f is_integrable_on ['c,b']
& integral(f,a,b) = integral(f,a,c) + integral(f,c,b);
theorem :: INTEGR21:16
for f,g be continuous PartFunc of REAL,the carrier of Y
st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g
holds f+g is_integrable_on ['c,d'] & (f+g) | ['c,d'] is bounded;
theorem :: INTEGR21:17
for f be continuous PartFunc of REAL,the carrier of Y
st a <= c & c <= d & d <= b & ['a,b'] c= dom f
holds r(#)f is_integrable_on ['c,d'] & (r(#)f) | ['c,d'] is bounded;
theorem :: INTEGR21:18
for f be continuous PartFunc of REAL,the carrier of Y
st a <= c & c <= d & d <= b & f is_integrable_on ['a,b']
& f| ['a,b'] is bounded & ['a,b'] c= dom f
holds -f is_integrable_on ['c,d'] & (-f) | ['c,d'] is bounded;
theorem :: INTEGR21:19
for f,g be continuous PartFunc of REAL,the carrier of Y
st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g
holds f-g is_integrable_on ['c,d'] & (f-g) | ['c,d'] is bounded;
theorem :: INTEGR21:20
for f be PartFunc of REAL,the carrier of Y
st A c= dom f & f|A is bounded & f is_integrable_on A
& ||.f.|| is_integrable_on A
holds ||.integral(f,A).|| <= integral(||.f.||,A);
theorem :: INTEGR21:21
for f be PartFunc of REAL,the carrier of Y
st a<=b & ['a,b'] c= dom f & f is_integrable_on ['a,b']
& ||.f.|| is_integrable_on ['a,b'] & f| ['a ,b'] is bounded
holds ||.integral(f,a,b).|| <= integral(||.f.||,a,b);
theorem :: INTEGR21:22
for f be continuous PartFunc of REAL,the carrier of Y
st a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b']
holds ||.f.|| is_integrable_on ['min(c,d),max(c,d)']
& ||.f.|| | ['min(c,d),max(c,d)'] is bounded
& ||. integral(f,c,d) .|| <= integral(||.f.||,min(c,d),max(c,d));
theorem :: INTEGR21:23
for f be continuous PartFunc of REAL,the carrier of Y
st a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b']
holds integral(r(#)f,c,d) = r*integral(f,c,d);
theorem :: INTEGR21:24
for f be continuous PartFunc of REAL,the carrier of Y
st a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b']
holds integral(-f,c,d) = -integral(f,c,d);
theorem :: INTEGR21:25
for f be continuous PartFunc of REAL,the carrier of Y
st ( a<=b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b']
& for x be Real st x in ['min(c,d),max(c,d)']
holds ||. f/.x .|| <= e )
holds ||.integral(f,c,d).|| <= e * |.d-c.|;
theorem :: INTEGR21:26
for Y be RealNormSpace,
A be non empty closed_interval Subset of REAL,
f be Function of A,the carrier of Y,
E be Point of Y
st rng f = {E} holds f is integrable & integral f = (vol A) * E;
theorem :: INTEGR21:27
for f be PartFunc of REAL,the carrier of Y, E be Point of Y
st ( a <= b & ['a,b'] c= dom f
& for x be Real st x in ['a,b'] holds f/.x = E ) holds
f is_integrable_on ['a,b'] & integral(f,a,b) = (b-a)*E;
theorem :: INTEGR21:28
for f be PartFunc of REAL,the carrier of Y
st a <= b & c in ['a,b'] & d in ['a,b'] & ['a,b'] c= dom f
& for x be Real st x in ['a,b'] holds f/.x = E
holds integral(f,c,d) = (d-c)*E;
theorem :: INTEGR21:29
for f be continuous PartFunc of REAL,the carrier of Y
st a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral(f,a,d) = integral(f,a,c) + integral(f,c,d);
theorem :: INTEGR21:30
for f,g be continuous PartFunc of REAL,the carrier of Y
st a <= b & ['a,b'] c= dom f & ['a,b'] c= dom g
& c in ['a,b'] & d in ['a,b']
holds integral(f-g,c,d) = integral(f,c,d) - integral(g,c,d);