INTEGR21: The Linearity of Riemann Integral on Functions from $\mathbbbR$ into Real {B}anach Space

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

environ

vocabularies HIDDEN, 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 HIDDEN, 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;
definitions INTEGR19, TARSKI;
theorems TARSKI, ABSVALUE, RLVECT_1, NORMSP_0, SEQ_2, PARTFUN1, PARTFUN2, FUNCT_1, NAT_1, FUNCT_2, NORMSP_1, XREAL_1, LOPBAN_1, XXREAL_0, XREAL_0, ORDINAL1, RELAT_1, NFCONT_3, VFUNCT_1, XBOOLE_0, FINSEQ_1, COMSEQ_2, SEQM_3, INTEGR15, INTEGRA2, XXREAL_1, COMPLEX1, XBOOLE_1, INTEGR19, INTEGRA4, INTEGRA5, INTEGRA3, INTEGRA1, INTEGR18, INTEGRA6, FINSEQ_3, FINSEQ_5, RFINSEQ, XXREAL_2, INTEGR20, SUBSET_1;
schemes FUNCT_2, FINSEQ_1;
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;
constructors HIDDEN, 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;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities ALGSTR_0, FINSEQ_1, INTEGRA5, INTEGRA1, INTEGRA3, INTEGR15, INTEGR18, XCMPLX_0;
expansions INTEGRA5, INTEGRA4, INTEGR18, NORMSP_1, INTEGR19, TARSKI;

Lm2: for a, b, c, d being Real st a <= b & c in ['a,b'] & d in ['a,b'] holds
['(min (c,d)),(max (c,d))'] c= ['a,b']

proof end;

Lm3: for X, Y, Z being non empty set
for f being PartFunc of X,Y st Z c= dom f holds
f | Z is Function of Z,Y

proof end;

theorem Th1915: :: INTEGR21:1

for Z being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of Z st f is bounded & A c= dom f holds
f | A is bounded

proof end;

theorem Th1915a: :: INTEGR21:2

for Z being RealNormSpace
for A, B being non empty closed_interval Subset of REAL
for f being 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

proof end;

theorem Th1915b: :: INTEGR21:3

for Z being RealNormSpace
for a, b, c, d being Real
for f being 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

proof end;

theorem Th1935: :: INTEGR21:4

for Z being RealNormSpace
for X, Y being set
for f1, f2 being 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 )

proof end;

theorem Th1935a: :: INTEGR21:5

for Z being RealNormSpace
for r being Real
for X being set
for f being PartFunc of REAL, the carrier of Z st f | X is bounded holds
(r (#) f) | X is bounded

proof end;

theorem Th1935b: :: INTEGR21:6

for Z being RealNormSpace
for X being set
for f being PartFunc of REAL, the carrier of Z st f | X is bounded holds
(- f) | X is bounded

proof end;

theorem Th1914: :: INTEGR21:7

for Z being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of Z holds
( f is bounded iff ||.f.|| is bounded )

proof end;

theorem Th1918: :: INTEGR21:8

for Z being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of Z st A c= dom f holds
||.(f | A).|| = ||.f.|| | A

proof end;

theorem Th1919: :: INTEGR21:9

for Z being RealNormSpace
for A being non empty closed_interval Subset of REAL
for g being PartFunc of REAL, the carrier of Z st A c= dom g & g | A is bounded holds
||.g.|| | A is bounded

proof end;

theorem Th3: :: INTEGR21:10

for a, b being Real
for Y being RealNormSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f holds
||.f.|| | ['a,b'] is bounded

proof end;

theorem Th1: :: INTEGR21:11

for a, b being Real
for Y being RealNormSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f holds
f | ['a,b'] is bounded

proof end;

theorem Th4: :: INTEGR21:12

for a, b being Real
for Y being RealNormSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f holds
||.f.|| is_integrable_on ['a,b']

proof end;

theorem Th1909: :: INTEGR21:13

for a, b, c, d being Real
for Y being RealBanachSpace
for f being 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']

proof end;

theorem Th1947: :: INTEGR21:14

for a, b being Real
for Y being RealBanachSpace
for f being PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f holds
integral (f,b,a) = - (integral (f,a,b))

proof end;

Lm62: for a, b, c being Real
for X being RealBanachSpace
for f being continuous PartFunc of REAL, the carrier of X st a <= b & ['a,b'] c= dom f & c in ['a,b'] & b <> c holds
integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b))

proof end;

theorem Th1908: :: INTEGR21:15

for a, b, c being Real
for Y being RealBanachSpace
for f being 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)) )

proof end;

theorem :: INTEGR21:16

for a, b, c, d being Real
for Y being RealBanachSpace
for f, g being 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 )

proof end;

theorem Th1911: :: INTEGR21:17

for a, b, c, d, r being Real
for Y being RealBanachSpace
for f being 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 )

proof end;

theorem :: INTEGR21:18

for a, b, c, d being Real
for Y being RealBanachSpace
for f being 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 )

proof end;

theorem :: INTEGR21:19

for a, b, c, d being Real
for Y being RealBanachSpace
for f, g being 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 )

proof end;

Lm8: for A being non empty closed_interval Subset of REAL
for Y being RealBanachSpace
for h being Function of A, the carrier of Y
for f being Function of A,REAL st h is bounded & h is integrable & f = ||.h.|| & f is integrable holds
||.(integral h).|| <= integral f

proof end;

theorem Th1920: :: INTEGR21:20

for A being non empty closed_interval Subset of REAL
for Y being RealBanachSpace
for f being 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)

proof end;

theorem Th1921: :: INTEGR21:21

for a, b being Real
for Y being RealBanachSpace
for f being 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)

proof end;

Lm10: for a, b, c, d being Real
for Y being RealBanachSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= b & c <= d & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
( f is_integrable_on ['c,d'] & ||.f.|| is_integrable_on ['c,d'] & ||.f.|| | ['c,d'] is bounded & ||.(integral (f,c,d)).|| <= integral (||.f.||,c,d) )

proof end;

theorem Th1922: :: INTEGR21:22

for a, b, c, d being Real
for Y being RealBanachSpace
for f being 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))) )

proof end;

Th1925a: for a, b, c, d, r being Real
for Y being RealBanachSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= b & c <= d & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral ((r (#) f),c,d) = r * (integral (f,c,d))

proof end;

theorem Th1925: :: INTEGR21:23

for a, b, c, d, r being Real
for Y being RealBanachSpace
for f being 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))

proof end;

theorem :: INTEGR21:24

for a, b, c, d being Real
for Y being RealBanachSpace
for f being 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))

proof end;

theorem :: INTEGR21:25

for a, b, c, d, e being Real
for Y being RealBanachSpace
for f being 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 being Real st x in ['(min (c,d)),(max (c,d))'] holds
||.(f /. x).|| <= e ) holds
||.(integral (f,c,d)).|| <= e * |.(d - c).|

proof end;

Th1928: for a, b, c, d being Real
for Y being RealBanachSpace
for f, g being continuous PartFunc of REAL, the carrier of Y st a <= b & c <= d & ['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))

proof end;

theorem Th404: :: INTEGR21:26

for Y being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of Y
for E being Point of Y st rng f = {E} holds
( f is integrable & integral f = (vol A) * E )

proof end;

theorem Th1929: :: INTEGR21:27

for a, b being Real
for Y being RealBanachSpace
for f being PartFunc of REAL, the carrier of Y
for E being Point of Y st a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds
f /. x = E ) holds
( f is_integrable_on ['a,b'] & integral (f,a,b) = (b - a) * E )

proof end;

theorem :: INTEGR21:28

for a, b, c, d being Real
for Y being RealBanachSpace
for E being Point of Y
for f being 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 being Real st x in ['a,b'] holds
f /. x = E ) holds
integral (f,c,d) = (d - c) * E

proof end;

Th1931: for a, b, c, d being Real
for Y being RealBanachSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= b & c <= d & ['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))

proof end;

theorem :: INTEGR21:29

for a, b, c, d being Real
for Y being RealBanachSpace
for f being 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))

proof end;

theorem :: INTEGR21:30

for a, b, c, d being Real
for Y being RealBanachSpace
for f, g being 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))

proof end;