:: by Keiko Narita , Kazuhisa Nakasho and Yasunari Shidama

::

:: Received August 30, 2017

:: Copyright (c) 2017-2019 Association of Mizar Users

definition

let A be non empty closed_interval Subset of REAL;

ex b_{1} being non empty strict compact TopSpace ex a, b being Real st

( a <= b & [.a,b.] = A & b_{1} = Closed-Interval-TSpace (a,b) )

for b_{1}, b_{2} being non empty strict compact TopSpace st ex a, b being Real st

( a <= b & [.a,b.] = A & b_{1} = Closed-Interval-TSpace (a,b) ) & ex a, b being Real st

( a <= b & [.a,b.] = A & b_{2} = Closed-Interval-TSpace (a,b) ) holds

b_{1} = b_{2}

end;
func ClstoCmp A -> non empty strict compact TopSpace means :Def7ClstoCmp: :: DUALSP05:def 1

ex a, b being Real st

( a <= b & [.a,b.] = A & it = Closed-Interval-TSpace (a,b) );

existence ex a, b being Real st

( a <= b & [.a,b.] = A & it = Closed-Interval-TSpace (a,b) );

ex b

( a <= b & [.a,b.] = A & b

proof end;

uniqueness for b

( a <= b & [.a,b.] = A & b

( a <= b & [.a,b.] = A & b

b

proof end;

:: deftheorem Def7ClstoCmp defines ClstoCmp DUALSP05:def 1 :

for A being non empty closed_interval Subset of REAL

for b_{2} being non empty strict compact TopSpace holds

( b_{2} = ClstoCmp A iff ex a, b being Real st

( a <= b & [.a,b.] = A & b_{2} = Closed-Interval-TSpace (a,b) ) );

for A being non empty closed_interval Subset of REAL

for b

( b

( a <= b & [.a,b.] = A & b

theorem Th80a: :: DUALSP05:3

for X being non empty strict SubSpace of R^1

for f being RealMap of X

for g being PartFunc of REAL,REAL

for x being Point of X

for x0 being Real st g = f & x = x0 holds

( ( for V being Subset of REAL st f . x in V & V is open holds

ex W being Subset of X st

( x in W & W is open & f .: W c= V ) ) iff g is_continuous_in x0 )

for f being RealMap of X

for g being PartFunc of REAL,REAL

for x being Point of X

for x0 being Real st g = f & x = x0 holds

( ( for V being Subset of REAL st f . x in V & V is open holds

ex W being Subset of X st

( x in W & W is open & f .: W c= V ) ) iff g is_continuous_in x0 )

proof end;

theorem Th80b: :: DUALSP05:4

for X being non empty strict SubSpace of R^1

for f being RealMap of X

for g being PartFunc of REAL,REAL st g = f holds

( f is continuous iff g is continuous )

for f being RealMap of X

for g being PartFunc of REAL,REAL st g = f holds

( f is continuous iff g is continuous )

proof end;

theorem Th80: :: DUALSP05:6

for A being non empty closed_interval Subset of REAL

for u being Function holds

( u is Point of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) iff ( dom u = A & u is continuous PartFunc of REAL,REAL ) )

for u being Function holds

( u is Point of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) iff ( dom u = A & u is continuous PartFunc of REAL,REAL ) )

proof end;

theorem Lm2: :: DUALSP05:7

for A being non empty closed_interval Subset of REAL

for v being Point of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) holds v in BoundedFunctions the carrier of (ClstoCmp A)

for v being Point of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) holds v in BoundedFunctions the carrier of (ClstoCmp A)

proof end;

theorem LM83: :: DUALSP05:8

for A being non empty closed_interval Subset of REAL

for a, b being Real st A = [.a,b.] holds

ex x being Function of A,(BoundedFunctions A) st

for s being Real st s in [.a,b.] holds

( ( s = a implies x . s = [.a,b.] --> 0 ) & ( s <> a implies x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) )

for a, b being Real st A = [.a,b.] holds

ex x being Function of A,(BoundedFunctions A) st

for s being Real st s in [.a,b.] holds

( ( s = a implies x . s = [.a,b.] --> 0 ) & ( s <> a implies x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) )

proof end;

definition

let A be non empty closed_interval Subset of REAL;

let D be Division of A;

let m be Function of A,(BoundedFunctions A);

let i be Nat;

assume A1: i in Seg ((len D) + 1) ;

( ( i = 1 implies m . (lower_bound A) is Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) ) & ( not i = 1 implies m . (D . (i - 1)) is Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) ) )

consistency

for b_{1} being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) holds verum;

;

end;
let D be Division of A;

let m be Function of A,(BoundedFunctions A);

let i be Nat;

assume A1: i in Seg ((len D) + 1) ;

func Dp1 (m,D,i) -> Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) equals :defDp1: :: DUALSP05:def 2

m . (lower_bound A) if i = 1

otherwise m . (D . (i - 1));

coherence m . (lower_bound A) if i = 1

otherwise m . (D . (i - 1));

( ( i = 1 implies m . (lower_bound A) is Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) ) & ( not i = 1 implies m . (D . (i - 1)) is Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) ) )

proof end;

correctness consistency

for b

;

:: deftheorem defDp1 defines Dp1 DUALSP05:def 2 :

for A being non empty closed_interval Subset of REAL

for D being Division of A

for m being Function of A,(BoundedFunctions A)

for i being Nat st i in Seg ((len D) + 1) holds

( ( i = 1 implies Dp1 (m,D,i) = m . (lower_bound A) ) & ( not i = 1 implies Dp1 (m,D,i) = m . (D . (i - 1)) ) );

for A being non empty closed_interval Subset of REAL

for D being Division of A

for m being Function of A,(BoundedFunctions A)

for i being Nat st i in Seg ((len D) + 1) holds

( ( i = 1 implies Dp1 (m,D,i) = m . (lower_bound A) ) & ( not i = 1 implies Dp1 (m,D,i) = m . (D . (i - 1)) ) );

definition

let A be non empty closed_interval Subset of REAL;

let D be Division of A;

let rho be Function of A,REAL;

let i be Nat;

coherence

( ( i = 1 implies rho . (lower_bound A) is Real ) & ( not i = 1 implies rho . (D . (i - 1)) is Real ) );

consistency

for b_{1} being Real holds verum;

;

end;
let D be Division of A;

let rho be Function of A,REAL;

let i be Nat;

::: assume i in Seg(len D + 1);

func Dp2 (rho,D,i) -> Real equals :defDp2: :: DUALSP05:def 3

rho . (lower_bound A) if i = 1

otherwise rho . (D . (i - 1));

correctness rho . (lower_bound A) if i = 1

otherwise rho . (D . (i - 1));

coherence

( ( i = 1 implies rho . (lower_bound A) is Real ) & ( not i = 1 implies rho . (D . (i - 1)) is Real ) );

consistency

for b

;

:: deftheorem defDp2 defines Dp2 DUALSP05:def 3 :

for A being non empty closed_interval Subset of REAL

for D being Division of A

for rho being Function of A,REAL

for i being Nat holds

( ( i = 1 implies Dp2 (rho,D,i) = rho . (lower_bound A) ) & ( not i = 1 implies Dp2 (rho,D,i) = rho . (D . (i - 1)) ) );

for A being non empty closed_interval Subset of REAL

for D being Division of A

for rho being Function of A,REAL

for i being Nat holds

( ( i = 1 implies Dp2 (rho,D,i) = rho . (lower_bound A) ) & ( not i = 1 implies Dp2 (rho,D,i) = rho . (D . (i - 1)) ) );

theorem LM84: :: DUALSP05:9

for A being non empty closed_interval Subset of REAL

for D being Division of A

for m being Function of A,(BoundedFunctions A)

for rho being Function of A,REAL ex s being FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st

( len s = len D & ( for i being Nat st i in dom s holds

s . i = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i))) ) )

for D being Division of A

for m being Function of A,(BoundedFunctions A)

for rho being Function of A,REAL ex s being FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st

( len s = len D & ( for i being Nat st i in dom s holds

s . i = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i))) ) )

proof end;

theorem LM87: :: DUALSP05:10

for V being RealLinearSpace

for f being Functional of V

for s being FinSequence of V st f is additive holds

f . (Sum s) = Sum (f * s)

for f being Functional of V

for s being FinSequence of V st f is additive holds

f . (Sum s) = Sum (f * s)

proof end;

theorem LM88: :: DUALSP05:11

for A being non empty set

for x being Element of (R_Normed_Algebra_of_BoundedFunctions A) holds x is Function of A,REAL

for x being Element of (R_Normed_Algebra_of_BoundedFunctions A) holds x is Function of A,REAL

proof end;

theorem LM89: :: DUALSP05:12

for A being non empty closed_interval Subset of REAL

for s being FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))

for z being FinSequence of REAL

for g being Function of A,REAL

for t being Element of A st len s = len z & g = Sum s & ( for k being Nat st k in dom z holds

ex sk being Function of A,REAL st

( sk = s . k & z . k = sk . t ) ) holds

g . t = Sum z

for s being FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))

for z being FinSequence of REAL

for g being Function of A,REAL

for t being Element of A st len s = len z & g = Sum s & ( for k being Nat st k in dom z holds

ex sk being Function of A,REAL st

( sk = s . k & z . k = sk . t ) ) holds

g . t = Sum z

proof end;

theorem LM94: :: DUALSP05:13

for A being non empty closed_interval Subset of REAL

for D being Division of A

for t being Element of A st lower_bound A < D . 1 holds

ex i being Element of NAT st

( i in dom D & t in divset (D,i) & ( i = 1 or ( lower_bound (divset (D,i)) < t & t <= upper_bound (divset (D,i)) ) ) )

for D being Division of A

for t being Element of A st lower_bound A < D . 1 holds

ex i being Element of NAT st

( i in dom D & t in divset (D,i) & ( i = 1 or ( lower_bound (divset (D,i)) < t & t <= upper_bound (divset (D,i)) ) ) )

proof end;

LM95A: for A being non empty closed_interval Subset of REAL

for D being Division of A st 0 < vol A & D . 1 = lower_bound A holds

D /^ 1 is Division of A

proof end;

LM95B: for A being non empty closed_interval Subset of REAL

for D being Division of A st 0 < vol A & D . 1 = lower_bound A holds

lower_bound A < (D /^ 1) . 1

proof end;

LM95C: for A being non empty closed_interval Subset of REAL

for D, E being Division of A

for rho being Function of A,REAL

for K being var_volume of rho,D

for L being var_volume of rho,E st 0 < vol A & D . 1 = lower_bound A & E = D /^ 1 holds

Sum K = Sum L

proof end;

theorem LM95: :: DUALSP05:14

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

for B being Real st 0 < vol A & ( for D being Division of A

for K being var_volume of rho,D st lower_bound A < D . 1 holds

Sum K <= B ) holds

for D being Division of A

for K being var_volume of rho,D holds Sum K <= B

for rho being Function of A,REAL

for B being Real st 0 < vol A & ( for D being Division of A

for K being var_volume of rho,D st lower_bound A < D . 1 holds

Sum K <= B ) holds

for D being Division of A

for K being var_volume of rho,D holds Sum K <= B

proof end;

theorem Lm83: :: DUALSP05:15

for A being non empty closed_interval Subset of REAL

for rho being Function of A,REAL

for f being Point of (DualSp (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A))) st rho is bounded_variation & ( for u being continuous PartFunc of REAL,REAL st dom u = A holds

f . u = integral (u,rho) ) holds

||.f.|| <= total_vd rho

for rho being Function of A,REAL

for f being Point of (DualSp (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A))) st rho is bounded_variation & ( for u being continuous PartFunc of REAL,REAL st dom u = A holds

f . u = integral (u,rho) ) holds

||.f.|| <= total_vd rho

proof end;

theorem :: DUALSP05:16

for A being non empty closed_interval Subset of REAL

for x being Point of (DualSp (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A))) st 0 < vol A holds

ex rho being Function of A,REAL st

( rho is bounded_variation & ( for u being continuous PartFunc of REAL,REAL st dom u = A holds

x . u = integral (u,rho) ) & ||.x.|| = total_vd rho )

for x being Point of (DualSp (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A))) st 0 < vol A holds

ex rho being Function of A,REAL st

( rho is bounded_variation & ( for u being continuous PartFunc of REAL,REAL st dom u = A holds

x . u = integral (u,rho) ) & ||.x.|| = total_vd rho )

proof end;