:: 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-2021 Association of Mizar Users

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;