:: F. Riesz Theorem
:: by Keiko Narita , Kazuhisa Nakasho and Yasunari Shidama
::
:: Copyright (c) 2017-2021 Association of Mizar Users

theorem LM91: :: DUALSP05:1
for d being Real holds |.(sgn d).| <= 1
proof end;

theorem LM86: :: DUALSP05:2
for x being Real holds |.x.| = (sgn x) * x
proof end;

definition
let A be non empty closed_interval Subset of REAL;
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 b1 being non empty strict compact TopSpace ex a, b being Real st
( a <= b & [.a,b.] = A & b1 = Closed-Interval-TSpace (a,b) )
proof end;
uniqueness
for b1, b2 being non empty strict compact TopSpace st ex a, b being Real st
( a <= b & [.a,b.] = A & b1 = Closed-Interval-TSpace (a,b) ) & ex a, b being Real st
( a <= b & [.a,b.] = A & b2 = Closed-Interval-TSpace (a,b) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7ClstoCmp defines ClstoCmp DUALSP05:def 1 :
for A being non empty closed_interval Subset of REAL
for b2 being non empty strict compact TopSpace holds
( b2 = ClstoCmp A iff ex a, b being Real st
( a <= b & [.a,b.] = A & b2 = Closed-Interval-TSpace (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 )
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 )
proof end;

theorem Lm1: :: DUALSP05:5
for A being non empty closed_interval Subset of REAL holds the carrier of () = A
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 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 holds v in BoundedFunctions the carrier of ()
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,() 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,();
let i be Nat;
assume A1: i in Seg ((len D) + 1) ;
func Dp1 (m,D,i) -> Point of () equals :defDp1: :: DUALSP05:def 2
m . () if i = 1
otherwise m . (D . (i - 1));
coherence
( ( i = 1 implies m . () is Point of () ) & ( not i = 1 implies m . (D . (i - 1)) is Point of () ) )
proof end;
correctness
consistency
for b1 being Point of () holds verum
;
;
end;

:: 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,()
for i being Nat st i in Seg ((len D) + 1) holds
( ( i = 1 implies Dp1 (m,D,i) = m . () ) & ( 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;
::: assume i in Seg(len D + 1);
func Dp2 (rho,D,i) -> Real equals :defDp2: :: DUALSP05:def 3
rho . () if i = 1
otherwise rho . (D . (i - 1));
correctness
coherence
( ( i = 1 implies rho . () is Real ) & ( not i = 1 implies rho . (D . (i - 1)) is Real ) )
;
consistency
for b1 being Real holds verum
;
;
end;

:: 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 . () ) & ( 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,()
for rho being Function of A,REAL ex s being FinSequence of () 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)
proof end;

theorem LM88: :: DUALSP05:11
for A being non empty set
for x being Element of 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 ()
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)) ) ) )
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
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 st rho is bounded_variation & ( for u being continuous PartFunc of REAL,REAL st dom u = A holds
f . u = integral (u,rho) ) holds
<= total_vd rho
proof end;

theorem :: DUALSP05:16
for A being non empty closed_interval Subset of REAL
for x being Point of 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) ) & = total_vd rho )
proof end;