:: by Keiko Narita , Noboru Endou and Yasunari Shidama

::

:: Received October 7, 2013

:: Copyright (c) 2013-2016 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

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

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

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 )

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

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

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 )

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

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

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

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

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']

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']

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

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

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 )

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 )

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 )

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 )

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)

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)

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

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

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

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

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 )

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 )

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

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

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

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;