:: Functional Sequence in Norm Space
:: by Hiroshi Yamazaki
::
:: Copyright (c) 2020-2021 Association of Mizar Users

theorem :: SEQFUNC2:1
for D1, D2 being set
for f being Function holds
( f is Functional_Sequence of D1,D2 iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is PartFunc of D1,D2 ) ) )
proof end;

definition
let D be non empty set ;
let Y be non empty NORMSTR ;
let H be Functional_Sequence of D, the carrier of Y;
let r be Real;
func r (#) H -> Functional_Sequence of D, the carrier of Y means :Def1: :: SEQFUNC2:def 1
for n being Nat holds it . n = r (#) (H . n);
existence
ex b1 being Functional_Sequence of D, the carrier of Y st
for n being Nat holds b1 . n = r (#) (H . n)
proof end;
uniqueness
for b1, b2 being Functional_Sequence of D, the carrier of Y st ( for n being Nat holds b1 . n = r (#) (H . n) ) & ( for n being Nat holds b2 . n = r (#) (H . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines (#) SEQFUNC2:def 1 :
for D being non empty set
for Y being non empty NORMSTR
for H being Functional_Sequence of D, the carrier of Y
for r being Real
for b5 being Functional_Sequence of D, the carrier of Y holds
( b5 = r (#) H iff for n being Nat holds b5 . n = r (#) (H . n) );

definition
let D be non empty set ;
let Y be RealNormSpace;
let H be Functional_Sequence of D, the carrier of Y;
func - H -> Functional_Sequence of D, the carrier of Y means :Def3: :: SEQFUNC2:def 2
for n being Nat holds it . n = - (H . n);
existence
ex b1 being Functional_Sequence of D, the carrier of Y st
for n being Nat holds b1 . n = - (H . n)
proof end;
uniqueness
for b1, b2 being Functional_Sequence of D, the carrier of Y st ( for n being Nat holds b1 . n = - (H . n) ) & ( for n being Nat holds b2 . n = - (H . n) ) holds
b1 = b2
proof end;
involutiveness
for b1, b2 being Functional_Sequence of D, the carrier of Y st ( for n being Nat holds b1 . n = - (b2 . n) ) holds
for n being Nat holds b2 . n = - (b1 . n)
proof end;
end;

:: deftheorem Def3 defines - SEQFUNC2:def 2 :
for D being non empty set
for Y being RealNormSpace
for H, b4 being Functional_Sequence of D, the carrier of Y holds
( b4 = - H iff for n being Nat holds b4 . n = - (H . n) );

definition
let D be non empty set ;
let Y be non empty NORMSTR ;
let H be Functional_Sequence of D, the carrier of Y;
func -> Functional_Sequence of D,REAL means :Def4: :: SEQFUNC2:def 3
for n being Nat holds it . n = ||.(H . n).||;
existence
ex b1 being Functional_Sequence of D,REAL st
for n being Nat holds b1 . n = ||.(H . n).||
proof end;
uniqueness
for b1, b2 being Functional_Sequence of D,REAL st ( for n being Nat holds b1 . n = ||.(H . n).|| ) & ( for n being Nat holds b2 . n = ||.(H . n).|| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines ||. SEQFUNC2:def 3 :
for D being non empty set
for Y being non empty NORMSTR
for H being Functional_Sequence of D, the carrier of Y
for b4 being Functional_Sequence of D,REAL holds
( b4 = iff for n being Nat holds b4 . n = ||.(H . n).|| );

definition
let D be non empty set ;
let Y be non empty NORMSTR ;
let G, H be Functional_Sequence of D, the carrier of Y;
func G + H -> Functional_Sequence of D, the carrier of Y means :Def5: :: SEQFUNC2:def 4
for n being Nat holds it . n = (G . n) + (H . n);
existence
ex b1 being Functional_Sequence of D, the carrier of Y st
for n being Nat holds b1 . n = (G . n) + (H . n)
proof end;
uniqueness
for b1, b2 being Functional_Sequence of D, the carrier of Y st ( for n being Nat holds b1 . n = (G . n) + (H . n) ) & ( for n being Nat holds b2 . n = (G . n) + (H . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines + SEQFUNC2:def 4 :
for D being non empty set
for Y being non empty NORMSTR
for G, H, b5 being Functional_Sequence of D, the carrier of Y holds
( b5 = G + H iff for n being Nat holds b5 . n = (G . n) + (H . n) );

definition
let D be non empty set ;
let Y be RealNormSpace;
let G, H be Functional_Sequence of D, the carrier of Y;
func G - H -> Functional_Sequence of D, the carrier of Y equals :: SEQFUNC2:def 5
G + (- H);
correctness
coherence
G + (- H) is Functional_Sequence of D, the carrier of Y
;
;
end;

:: deftheorem defines - SEQFUNC2:def 5 :
for D being non empty set
for Y being RealNormSpace
for G, H being Functional_Sequence of D, the carrier of Y holds G - H = G + (- H);

theorem Th3: :: SEQFUNC2:2
for D being non empty set
for Y being RealNormSpace
for G, H, H1 being Functional_Sequence of D, the carrier of Y holds
( H1 = G - H iff for n being Nat holds H1 . n = (G . n) - (H . n) )
proof end;

theorem :: SEQFUNC2:3
for D being non empty set
for Y being RealNormSpace
for G, H, J being Functional_Sequence of D, the carrier of Y holds
( G + H = H + G & (G + H) + J = G + (H + J) )
proof end;

theorem :: SEQFUNC2:4
for D being non empty set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y holds - H = (- 1) (#) H
proof end;

theorem :: SEQFUNC2:5
for D being non empty set
for r being Real
for Y being RealNormSpace
for G, H being Functional_Sequence of D, the carrier of Y holds
( r (#) (G + H) = (r (#) G) + (r (#) H) & r (#) (G - H) = (r (#) G) - (r (#) H) )
proof end;

theorem :: SEQFUNC2:6
for D being non empty set
for p, r being Real
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y holds (r * p) (#) H = r (#) (p (#) H)
proof end;

theorem :: SEQFUNC2:7
for D being non empty set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y holds 1 (#) H = H
proof end;

theorem :: SEQFUNC2:8
for D being non empty set
for r being Real
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y holds ||.(r (#) H).|| = |.r.| (#)
proof end;

definition
let D be non empty set ;
let Y be non empty NORMSTR ;
let H be Functional_Sequence of D, the carrier of Y;
let x be Element of D;
func H # x -> sequence of the carrier of Y means :Def10: :: SEQFUNC2:def 6
for n being Nat holds it . n = (H . n) /. x;
existence
ex b1 being sequence of the carrier of Y st
for n being Nat holds b1 . n = (H . n) /. x
proof end;
uniqueness
for b1, b2 being sequence of the carrier of Y st ( for n being Nat holds b1 . n = (H . n) /. x ) & ( for n being Nat holds b2 . n = (H . n) /. x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines # SEQFUNC2:def 6 :
for D being non empty set
for Y being non empty NORMSTR
for H being Functional_Sequence of D, the carrier of Y
for x being Element of D
for b5 being sequence of the carrier of Y holds
( b5 = H # x iff for n being Nat holds b5 . n = (H . n) /. x );

definition
let D be non empty set ;
let Y be RealNormSpace;
let H be Functional_Sequence of D, the carrier of Y;
let X be set ;
pred H is_point_conv_on X means :: SEQFUNC2:def 7
( X common_on_dom H & ex f being PartFunc of D, the carrier of Y st
( X = dom f & ( for x being Element of D st x in X holds
for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (f /. x)).|| < p ) ) );
end;

:: deftheorem defines is_point_conv_on SEQFUNC2:def 7 :
for D being non empty set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set holds
( H is_point_conv_on X iff ( X common_on_dom H & ex f being PartFunc of D, the carrier of Y st
( X = dom f & ( for x being Element of D st x in X holds
for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (f /. x)).|| < p ) ) ) );

theorem Th18: :: SEQFUNC2:9
for D being non empty set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set holds
( H is_point_conv_on X iff ( X common_on_dom H & ex f being PartFunc of D, the carrier of Y st
( X = dom f & ( for x being Element of D st x in X holds
( H # x is convergent & lim (H # x) = f . x ) ) ) ) )
proof end;

theorem Th19: :: SEQFUNC2:10
for D being non empty set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set holds
( H is_point_conv_on X iff ( X common_on_dom H & ( for x being Element of D st x in X holds
H # x is convergent ) ) )
proof end;

definition
let D be non empty set ;
let Y be RealNormSpace;
let H be Functional_Sequence of D, the carrier of Y;
let X be set ;
pred H is_unif_conv_on X means :: SEQFUNC2:def 8
( X common_on_dom H & ex f being PartFunc of D, the carrier of Y st
( X = dom f & ( for p being Real st p > 0 holds
ex k being Nat st
for n being Nat
for x being Element of D st n >= k & x in X holds
||.(((H . n) /. x) - (f /. x)).|| < p ) ) );
end;

:: deftheorem defines is_unif_conv_on SEQFUNC2:def 8 :
for D being non empty set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set holds
( H is_unif_conv_on X iff ( X common_on_dom H & ex f being PartFunc of D, the carrier of Y st
( X = dom f & ( for p being Real st p > 0 holds
ex k being Nat st
for n being Nat
for x being Element of D st n >= k & x in X holds
||.(((H . n) /. x) - (f /. x)).|| < p ) ) ) );

definition
let D be non empty set ;
let Y be RealNormSpace;
let H be Functional_Sequence of D, the carrier of Y;
let X be set ;
assume A1: H is_point_conv_on X ;
func lim (H,X) -> PartFunc of D, the carrier of Y means :Def13: :: SEQFUNC2:def 9
( dom it = X & ( for x being Element of D st x in dom it holds
it . x = lim (H # x) ) );
existence
ex b1 being PartFunc of D, the carrier of Y st
( dom b1 = X & ( for x being Element of D st x in dom b1 holds
b1 . x = lim (H # x) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of D, the carrier of Y st dom b1 = X & ( for x being Element of D st x in dom b1 holds
b1 . x = lim (H # x) ) & dom b2 = X & ( for x being Element of D st x in dom b2 holds
b2 . x = lim (H # x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines lim SEQFUNC2:def 9 :
for D being non empty set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st H is_point_conv_on X holds
for b5 being PartFunc of D, the carrier of Y holds
( b5 = lim (H,X) iff ( dom b5 = X & ( for x being Element of D st x in dom b5 holds
b5 . x = lim (H # x) ) ) );

theorem Th20: :: SEQFUNC2:11
for D being non empty set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set
for f being PartFunc of D, the carrier of Y st H is_point_conv_on X holds
( f = lim (H,X) iff ( dom f = X & ( for x being Element of D st x in X holds
for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (f /. x)).|| < p ) ) )
proof end;

theorem Th21: :: SEQFUNC2:12
for D being non empty set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st H is_unif_conv_on X holds
H is_point_conv_on X
proof end;

theorem Th22: :: SEQFUNC2:13
for D being non empty set
for Z being set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st Z c= X & Z <> {} & X common_on_dom H holds
Z common_on_dom H
proof end;

theorem :: SEQFUNC2:14
for D being non empty set
for Z being set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st Z c= X & Z <> {} & H is_point_conv_on X holds
( H is_point_conv_on Z & (lim (H,X)) | Z = lim (H,Z) )
proof end;

theorem :: SEQFUNC2:15
for D being non empty set
for Z being set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st Z c= X & Z <> {} & H is_unif_conv_on X holds
H is_unif_conv_on Z
proof end;

theorem Th25: :: SEQFUNC2:16
for D being non empty set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st X common_on_dom H holds
for x being set st x in X holds
{x} common_on_dom H
proof end;

theorem :: SEQFUNC2:17
for D being non empty set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st H is_point_conv_on X holds
for x being set st x in X holds
{x} common_on_dom H by Th25;

theorem Th27: :: SEQFUNC2:18
for D being non empty set
for Y being RealNormSpace
for H1, H2 being Functional_Sequence of D, the carrier of Y
for x being Element of D st {x} common_on_dom H1 & {x} common_on_dom H2 holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x )
proof end;

theorem Th28: :: SEQFUNC2:19
for D being non empty set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for x being Element of D st {x} common_on_dom H holds
( # x = ||.(H # x).|| & (- H) # x = (- 1) * (H # x) )
proof end;

theorem Th29: :: SEQFUNC2:20
for D being non empty set
for r being Real
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for x being Element of D st {x} common_on_dom H holds
(r (#) H) # x = r * (H # x)
proof end;

theorem Th30: :: SEQFUNC2:21
for D being non empty set
for Y being RealNormSpace
for H1, H2 being Functional_Sequence of D, the carrier of Y
for X being set st X common_on_dom H1 & X common_on_dom H2 holds
for x being Element of D st x in X holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x )
proof end;

theorem :: SEQFUNC2:22
for D being non empty set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for x being Element of D st {x} common_on_dom H holds
( # x = ||.(H # x).|| & (- H) # x = (- 1) * (H # x) ) by Th28;

theorem Th32: :: SEQFUNC2:23
for D being non empty set
for r being Real
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st X common_on_dom H holds
for x being Element of D st x in X holds
(r (#) H) # x = r * (H # x)
proof end;

theorem :: SEQFUNC2:24
for D being non empty set
for Y being RealNormSpace
for H1, H2 being Functional_Sequence of D, the carrier of Y
for X being set st H1 is_point_conv_on X & H2 is_point_conv_on X holds
for x being Element of D st x in X holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x ) by Th30;

theorem :: SEQFUNC2:25
for D being non empty set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for x being Element of D st {x} common_on_dom H holds
( # x = ||.(H # x).|| & (- H) # x = (- 1) * (H # x) ) by Th28;

theorem :: SEQFUNC2:26
for D being non empty set
for r being Real
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st H is_point_conv_on X holds
for x being Element of D st x in X holds
(r (#) H) # x = r * (H # x) by Th32;

theorem Th36: :: SEQFUNC2:27
for D being non empty set
for Y being RealNormSpace
for H1, H2 being Functional_Sequence of D, the carrier of Y
for X being set st X common_on_dom H1 & X common_on_dom H2 holds
( X common_on_dom H1 + H2 & X common_on_dom H1 - H2 )
proof end;

theorem Th37: :: SEQFUNC2:28
for D being non empty set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st X common_on_dom H holds
( X common_on_dom & X common_on_dom - H )
proof end;

theorem Th38: :: SEQFUNC2:29
for D being non empty set
for r being Real
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st X common_on_dom H holds
X common_on_dom r (#) H
proof end;

theorem :: SEQFUNC2:30
for D being non empty set
for Y being RealNormSpace
for H1, H2 being Functional_Sequence of D, the carrier of Y
for X being set st H1 is_point_conv_on X & H2 is_point_conv_on X holds
( H1 + H2 is_point_conv_on X & lim ((H1 + H2),X) = (lim (H1,X)) + (lim (H2,X)) & H1 - H2 is_point_conv_on X & lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X)) )
proof end;

theorem :: SEQFUNC2:31
for D being non empty set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st H is_point_conv_on X holds
( is_point_conv_on X & lim (,X) = ||.(lim (H,X)).|| & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) )
proof end;

theorem :: SEQFUNC2:32
for D being non empty set
for r being Real
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st H is_point_conv_on X holds
( r (#) H is_point_conv_on X & lim ((r (#) H),X) = r (#) (lim (H,X)) )
proof end;

theorem Th42: :: SEQFUNC2:33
for D being non empty set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set holds
( H is_unif_conv_on X iff ( X common_on_dom H & H is_point_conv_on X & ( for r being Real st 0 < r holds
ex k being Nat st
for n being Nat
for x being Element of D st n >= k & x in X holds
||.(((H . n) /. x) - ((lim (H,X)) /. x)).|| < r ) ) )
proof end;

theorem :: SEQFUNC2:34
for X being set
for V, W being RealNormSpace
for H being Functional_Sequence of the carrier of V, the carrier of W st H is_unif_conv_on X & ( for n being Nat holds (H . n) | X is_continuous_on X ) holds
lim (H,X) is_continuous_on X
proof end;