:: F. Riesz Theorem
:: by Keiko Narita , Kazuhisa Nakasho and Yasunari Shidama
::
:: Received August 30, 2017
:: 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 b₁ being non empty strict compact TopSpace ex a, b being Real st
( a <= b & [.a,b.] = A & b₁ = Closed-Interval-TSpace (a,b) )

proof end;

uniqueness
for b₁, b₂ being non empty strict compact TopSpace st ex a, b being Real st
( a <= b & [.a,b.] = A & b₁ = Closed-Interval-TSpace (a,b) ) & ex a, b being Real st
( a <= b & [.a,b.] = A & b₂ = Closed-Interval-TSpace (a,b) ) holds
b₁ = b₂

proof end;

end;

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

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

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

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
( ( 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₁ being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) 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,(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;

::: 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
coherence
( ( i = 1 implies rho . (lower_bound A) is Real ) & ( not i = 1 implies rho . (D . (i - 1)) is Real ) );
consistency
for b₁ 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 . (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))) ) )

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

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

proof end;