:: Functional Sequence in Norm Space
:: by Hiroshi Yamazaki
::
:: Received October 25, 2020
:: Copyright (c) 2020-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, SUBSET_1, NUMBERS, REAL_1, FUNCT_1, NAT_1, PARTFUN1,
RELAT_1, TARSKI, VALUED_1, ARYTM_1, COMPLEX1, ARYTM_3, CARD_1, PBOOLE,
XXREAL_0, SEQ_2, ORDINAL2, FCONT_1, SEQFUNC, FUNCT_7, NORMSP_1, PRE_TOPC,
STRUCT_0, CFCONT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1,
NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, COMPLEX1, VALUED_1, SEQ_2,
SEQFUNC, STRUCT_0, PRE_TOPC, RLVECT_1, VFUNCT_1, NORMSP_0, NORMSP_1,
NFCONT_1;
constructors COMPLEX1, SEQ_2, FCONT_1, VALUED_1, RELSET_1, COMSEQ_2, SEQFUNC,
POWER, VFUNCT_1, NFCONT_1;
registrations XBOOLE_0, RELSET_1, XREAL_0, MEMBERED, PARTFUN1, NAT_1,
ORDINAL1, STRUCT_0, NORMSP_1;
requirements SUBSET, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, XBOOLE_0, SEQFUNC;
equalities RLVECT_1;
expansions TARSKI, SEQFUNC;
theorems FUNCT_1, PARTFUN1, TARSKI, ZFMISC_1, FUNCT_2, RELAT_1, XREAL_0,
XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, RELSET_1, SEQFUNC,
RLVECT_1, VFUNCT_1, LOPBAN_1, NORMSP_1, NFCONT_1, NORMSP_0, SUBSET_1,
RLVECT_4;
schemes SEQ_1, SEQFUNC, FUNCT_2;
begin :: 1. Preliminaries
reserve D for non empty set,
D1, D2, x, y, Z for set,
n, k for Nat,
p, x1, r for Real,
f for Function,
Y for RealNormSpace,
G, H, H1, H2, J for Functional_Sequence of D,the carrier of Y;
theorem
f is Functional_Sequence of D1, D2
iff (dom f = NAT & for x st x in NAT holds f.x is PartFunc of D1, D2)
proof
thus f is Functional_Sequence of D1, D2
implies (dom f = NAT & for x st x in NAT holds f.x is PartFunc of D1, D2)
proof
assume
A1: f is Functional_Sequence of D1, D2;
hence dom f = NAT by FUNCT_2:def 1;
let x;
assume x in NAT;
then x in dom f by A1,FUNCT_2:def 1; then
A2: f.x in rng f by FUNCT_1:def 3;
rng f c= PFuncs(D1, D2) by A1,RELAT_1:def 19;
hence thesis by A2, PARTFUN1:46;
end;
assume that
A3: dom f = NAT and
A4: for x st x in NAT holds f.x is PartFunc of D1, D2;
now
let y be object;
assume y in rng f;
then consider x being object such that
A5: x in dom f and
A6: y = f.x by FUNCT_1:def 3;
f.x is PartFunc of D1, D2 by A3, A4, A5;
hence y in PFuncs(D1, D2) by A6, PARTFUN1:45;
end;
then rng f c=PFuncs(D1, D2);
hence thesis by A3,FUNCT_2:def 1,RELSET_1:4;
end;
definition
let D;
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:
for n being Nat holds it.n = r(#)(H.n);
existence
proof
deffunc U(Nat) = r(#)(H.$1);
thus ex f being Functional_Sequence of D, the carrier of Y
st for n being Nat holds f.n = U(n) from SEQFUNC:sch 1;
end;
uniqueness
proof
let H1, H2 be Functional_Sequence of D, the carrier of Y such that
A1: for n being Nat holds H1.n=r(#)(H.n) and
A2: for n being Nat holds H2.n=r(#)(H.n);
now
let n be Element of NAT;
H1.n = r(#)(H.n) by A1;
hence H1.n = H2.n by A2;
end;
hence H1 = H2 by FUNCT_2:63;
end;
end;
definition
let D;
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:
for n being Nat holds it.n = -H.n;
existence
proof
take (-1)(#)H;
let n be Nat;
for n being Nat holds ((-1)(#)H).n = -H.n
proof
let n be Nat;
thus ((-1)(#)H).n =(-1)(#)(H.n) by Def1
.= -H.n by VFUNCT_1:23;
end;
hence thesis;
end;
uniqueness
proof
let H1, H2 be Functional_Sequence of D,the carrier of Y such that
A3: for n being Nat holds H1.n = -H.n and
A4: for n being Nat holds H2.n = -H.n;
now
let n be Element of NAT;
H1.n = -H.n by A3;
hence H1.n = H2.n by A4;
end;
hence H1 = H2 by FUNCT_2:63;
end;
involutiveness
proof
let G, H be Functional_Sequence of D,the carrier of Y such that
A5: for n being Nat holds G.n = -(H.n);
let n be Nat;
thus H.n = --(H.n) by VFUNCT_1:24
.= -(G.n) by A5;
end;
end;
definition
let D;
let Y be non empty NORMSTR;
let H be Functional_Sequence of D,the carrier of Y;
func ||.H.|| -> Functional_Sequence of D,REAL means
:Def4:
for n being Nat holds it.n = ||.(H.n) .||;
existence
proof
deffunc U(Nat) = ||. H.$1 .||;
thus ex f being Functional_Sequence of D, REAL st for n being Nat
holds f.n = U(n) from SEQFUNC:sch 1;
end;
uniqueness
proof
let H1, H2 be Functional_Sequence of D,REAL such that
A6: for n being Nat holds H1.n=||. H.n .|| and
A7: for n being Nat holds H2.n=||. H.n .||;
now
let n be Element of NAT;
H2.n = ||. H.n .|| by A7;
hence H1.n = H2.n by A6;
end;
hence H1 = H2 by FUNCT_2:63;
end;
end;
definition
let D;
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:
for n being Nat holds it.n = G.n + H.n;
existence
proof
deffunc U(Nat) = G.$1 + H.$1;
thus ex f being Functional_Sequence of D, the carrier of Y
st for n being Nat holds f.n = U(n) from SEQFUNC:sch 1;
end;
uniqueness
proof
let H1, H2 be Functional_Sequence of D,the carrier of Y such that
A1: for n being Nat holds H1.n=G.n+H.n and
A2: for n being Nat holds H2.n=G.n+H.n;
now
let n be Element of NAT;
H1.n = G.n+H.n by A1;
hence H1.n = H2.n by A2;
end;
hence H1 = H2 by FUNCT_2:63;
end;
end;
definition
let D;
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 G + -H;
correctness;
end;
theorem Th3:
H1 = G - H iff for n holds H1.n = G.n - H.n
proof
thus H1 = G - H implies for n holds H1.n = G.n - H.n
proof
assume
A1: H1 = G - H;
let n;
thus H1.n = G.n + (-H).n by A1, Def5
.= G.n + - H.n by Def3
.= G.n -H.n by VFUNCT_1:25;
end;
assume
A2: for n holds H1.n = G.n - H.n;
now
let n be Element of NAT;
thus H1.n = G.n - H.n by A2
.= G.n + (-H.n) by VFUNCT_1:25
.= G.n + (-H).n by Def3
.= (G - H).n by Def5;
end;
hence thesis by FUNCT_2:63;
end;
theorem
G + H = H + G & (G + H) + J = G + (H + J)
proof
now
let n be Element of NAT;
thus (G + H).n = H.n + G.n by Def5
.= (H + G).n by Def5;
end;
hence G + H = H + G by FUNCT_2:63;
now
let n be Element of NAT;
thus ((G + H) + J).n = (G + H).n + J.n by Def5
.= G.n + H.n + J.n by Def5
.= G.n + (H.n + J.n) by VFUNCT_1:5
.= G.n + (H + J).n by Def5
.= (G + (H + J)).n by Def5;
end;
hence thesis by FUNCT_2:63;
end;
theorem
-H = (-1)(#)H
proof
now
let n be Element of NAT;
thus (-H).n = -H.n by Def3
.= (-1)(#)(H.n) by VFUNCT_1:23
.=((-1)(#)H).n by Def1;
end;
hence thesis by FUNCT_2:63;
end;
theorem
r(#)(G + H) = r(#)G + r(#)H & r(#)(G - H) = r(#)G - r(#)H
proof
now
let n be Element of NAT;
thus (r(#)(G + H)).n = r(#)(G + H).n by Def1
.= r(#)(G.n + H.n) by Def5
.= r(#)(G.n) + r(#)(H.n) by VFUNCT_1:13
.=(r(#)G).n + r(#)(H.n) by Def1
.=(r(#)G).n + (r(#)H).n by Def1
.=(r(#)G + r(#)H).n by Def5;
end;
hence r(#)(G + H) = r(#)G + r(#)H by FUNCT_2:63;
now
let n be Element of NAT;
thus (r(#)(G - H)).n = r(#)(G - H).n by Def1
.= r(#)(G.n - H.n) by Th3
.= r(#)G.n - r(#)H.n by VFUNCT_1:15
.= (r(#)G).n - r(#)H.n by Def1
.= (r(#)G).n - (r(#)H).n by Def1
.= (r(#)G - r(#)H).n by Th3;
end;
hence thesis by FUNCT_2:63;
end;
theorem
(r*p)(#)H = r(#)(p(#)H)
proof
now
let n be Element of NAT;
thus ((r*p)(#)H).n=(r*p)(#)H.n by Def1
.=r(#)(p(#)H.n) by VFUNCT_1:14
.=r(#)(p(#)H).n by Def1
.=(r(#)(p(#)H)).n by Def1;
end;
hence thesis by FUNCT_2:63;
end;
theorem
1 (#) H = H
proof
now
let n be Element of NAT;
thus (1 (#) H).n = 1 (#) H.n by Def1
.= H.n by VFUNCT_1:18;
end;
hence thesis by FUNCT_2:63;
end;
theorem
||.r(#)H.|| = |.r.| (#) ||.H.||
proof
now
let n be Element of NAT;
thus ||.r(#)H .||.n=||. ((r(#)H).n) .|| by Def4
.=||. r(#)(H.n).|| by Def1
.=|.r.|(#)||. H.n .|| by VFUNCT_1:22
.=|.r.|(#)(||.H.||).n by Def4
.=(|.r.|(#)||.H.||).n by SEQFUNC:def 1;
end;
hence thesis by FUNCT_2:63;
end;
begin :: 2. Pointwise convergence
reserve
x for Element of D,
X for set,
S1, S2 for sequence of Y,
f for PartFunc of D,the carrier of Y;
definition
let D;
let Y be non empty NORMSTR;
let H be Functional_Sequence of D,the carrier of Y;
let x;
func H#x -> sequence of the carrier of Y means
:Def10:
for n holds it.n = (H.n)/.x;
existence
proof
deffunc U(Nat) = (H.$1)/.x;
consider f being sequence of the carrier of Y
such that
A1: for n being Element of NAT holds f.n = U(n) from FUNCT_2:sch 4;
reconsider f as sequence of the carrier of Y;
take f;
for n holds f.n = (H.n)/.x
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 12;
hence f.n = (H.n)/.x by A1;
end;
hence thesis;
end;
uniqueness
proof
let S1, S2 be sequence of the carrier of Y such that
A2: for n holds S1.n = (H.n)/.x and
A3: for n holds S2.n = (H.n)/.x;
now
let n be Element of NAT;
S1.n = (H.n)/.x by A2;
hence S1.n = S2.n by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let D, Y, H, X;
pred H is_point_conv_on X means
X common_on_dom H & ex f st X = dom f & for x st x in X
holds for p st p>0 ex k st for n st n>=k holds ||.(H.n)/.x - f/.x.|| < p;
end;
theorem Th18:
H is_point_conv_on X iff X common_on_dom H & ex f st X = dom f &
for x st x in X holds (H#x) is convergent & lim(H#x) = f.x
proof
thus H is_point_conv_on X implies X common_on_dom H & ex f st X = dom f &
for x st x in X holds (H#x) is convergent & lim(H#x) = f.x
proof
assume
A1: H is_point_conv_on X;
hence X common_on_dom H;
consider f such that
A2: X = dom f and
A3: for x st x in X holds for p st p>0 ex k st for n st n>=k holds
||.( H.n)/.x - f/.x.|| < p by A1;
take f;
thus X = dom f by A2;
let x;
assume
A4: x in X;
then
X4: f/.x = f.x by A2, PARTFUN1:def 6;
A5:
now
let p be Real;
assume
A6: p>0;
consider k such that
A7: for n st n >= k holds ||.(H.n)/.x - f/.x.|| < p by A3, A4, A6;
take k;
let n be Nat;
assume n >= k;
then ||.(H.n)/.x - f/.x.|| < p by A7;
hence ||.(H#x).n - f/.x.|| < p by Def10;
end;
hence (H#x) is convergent by NORMSP_1:def 6;
hence thesis by X4, A5, NORMSP_1:def 7;
end;
assume
A8: X common_on_dom H;
given f such that
A9: X = dom f and
A10: for x st x in X holds (H#x) is convergent & lim(H#x) = f.x;
ex f st X = dom f
& for x st x in X holds for p st p>0 ex k st for n st n >= k
holds ||.(H.n)/.x - f/.x.|| < p
proof
take f;
thus X = dom f by A9;
let x;
assume X10: x in X;
then
A11: (H#x) is convergent & lim(H#x) = f.x by A10;
X11: f/.x =f.x by PARTFUN1:def 6, X10, A9;
let p;
assume p>0;
then consider k being Nat such that
A12: for n being Nat st n >= k holds ||.(H#x).n - f/.x.|| < p
by A11, NORMSP_1:def 7, X11;
take k;
let n;
assume n >= k;
then ||.(H#x).n - f/.x.|| < p by A12;
hence thesis by Def10;
end;
hence thesis by A8;
end;
theorem Th19:
H is_point_conv_on X iff X common_on_dom H & for x st x in X
holds (H#x) is convergent
proof
defpred X[set] means $1 in X;
deffunc U(Element of D) = In(lim(H#$1),the carrier of Y);
consider f such that
A1: for x holds x in dom f iff X[x] and
A2: for x st x in dom f holds f.x = U(x) from SEQ_1:sch 3;
thus H is_point_conv_on X implies X common_on_dom H & for x st x in X
holds (H#x) is convergent
proof
assume
A3: H is_point_conv_on X;
hence X common_on_dom H;
let x;
assume
A4: x in X;
ex f st X = dom f & for x st x in X holds (H#x) is convergent
& lim(H#x) = f.x by A3, Th18;
hence thesis by A4;
end;
assume that
A5: X common_on_dom H and
A6: for x st x in X holds (H#x) is convergent;
now
take f;
thus
A7: X = dom f
proof
thus X c= dom f
proof
let x be object such that
A8: x in X;
X c= dom (H.0) by A5;
then X c= D by XBOOLE_1:1;
then reconsider x9 = x as Element of D by A8;
x9 in dom f by A1, A8;
hence thesis;
end;
let x be object;
assume x in dom f;
hence thesis by A1;
end;
let x;
assume
A9: x in X;
hence (H#x) is convergent by A6;
In(lim(H#x),the carrier of Y) = lim(H#x) by SUBSET_1:def 8;
hence f.x = lim(H#x) by A2, A7, A9;
end;
hence thesis by A5, Th18;
end;
begin :: 3. Uniform convergence and limit of functional sequence
definition
let D, Y, H, X;
pred H is_unif_conv_on X means
X common_on_dom H & ex f st X = dom f
& for p st p>0 ex k st for n,x st n>=k & x in X
holds ||.(H.n)/.x - f/.x.|| < p;
end;
definition
let D, Y, H, X;
assume
A1: H is_point_conv_on X;
func lim(H, X) -> PartFunc of D,the carrier of Y means
:Def13:
dom it = X & for x st x in dom it holds it.x = lim(H#x);
existence
proof
consider f such that
A2: X = dom f and
A3: for x st x in X holds (H#x) is convergent & lim(H#x) = f.x by A1, Th18;
take f;
thus dom f = X by A2;
let x;
assume x in dom f;
hence thesis by A2, A3;
end;
uniqueness
proof
deffunc U(Element of D) = lim(H#$1);
thus for f1,f2 be PartFunc of D,the carrier of Y st dom f1 = X
& (for x st x in dom f1 holds f1.x = U(x)) & dom f2 = X
& for x st x in dom f2 holds f2.x = U(x) holds f1 = f2 from SEQ_1:sch 4;
end;
end;
theorem Th20:
H is_point_conv_on X implies (f = lim(H, X) iff dom f = X & for x
st x in X holds for p st p>0 ex k st for n st n>=k
holds ||.(H.n)/.x - f/.x.|| < p)
proof
assume
A1: H is_point_conv_on X;
thus f = lim(H, X) implies dom f = X & for x st x in X
holds for p st p>0 ex k st for n st n>=k holds ||.(H.n)/.x - f/.x.|| < p
proof
assume
A2: f = lim(H, X);
hence
A3: dom f = X by A1, Def13;
let x;
assume
A4: x in X;
then
A5: H#x is convergent by A1, Th19;
X6: f/.x = f.x by PARTFUN1:def 6, A4, A3;
let p;
assume
A6: p>0;
f.x = lim(H#x) by A1, A2, A3, A4, Def13;
then consider k being Nat such that
A7: for n being Nat st n>=k holds ||.(H#x).n - f/.x.|| < p
by X6, A5, A6, NORMSP_1:def 7;
take k;
let n;
assume n>=k;
then ||.(H#x).n - f/.x.|| < p by A7;
hence thesis by Def10;
end;
assume that
A8: dom f = X and
A9: for x st x in X holds for p st p>0 ex k st for n st n>=k holds ||.
(H.n)/.x - f/.x.|| < p;
now
let x such that
A10: x in dom f;
X10: f/.x =f.x by A10, PARTFUN1:def 6;
A11:
now
let p be Real;
assume
p > 0; then
consider k such that
A13: for n st n >= k holds ||.(H.n)/.x - f/.x.|| < p by A8, A9, A10;
take k;
let n be Nat;
assume n >= k;
then ||.(H.n)/.x - f/.x.|| < p by A13;
hence ||.(H#x).n - f/.x.|| < p by Def10;
end;
then H#x is convergent by NORMSP_1:def 6;
hence f.x = lim(H#x) by X10, A11, NORMSP_1:def 7;
end;
hence thesis by A1, A8, Def13;
end;
theorem Th21:
H is_unif_conv_on X implies H is_point_conv_on X
proof
assume
A1: H is_unif_conv_on X;
now
consider f such that
A3: X = dom f and
A4: for p st p>0 ex k st for n,x st n>=k & x in X
holds ||.(H.n)/.x - f/. x.|| < p by A1;
take f;
thus X = dom f by A3;
let x;
assume
A5: x in X;
let p;
assume p>0;
then consider k such that
A6: for n,x st n>=k & x in X holds ||.(H.n)/.x - f/.x.|| < p by A4;
take k;
let n;
assume n >= k;
hence ||.(H.n)/.x - f/.x.|| < p by A5, A6;
end;
hence thesis by A1;
end;
theorem Th22:
Z c= X & Z<>{} & X common_on_dom H implies Z common_on_dom H
proof
assume that
A1: Z c= X and
A2: Z<>{} and
A3: X common_on_dom H;
now
let n;
X c= dom (H.n) by A3;
hence Z c= dom (H.n) by A1;
end;
hence thesis by A2;
end;
theorem
Z c= X & Z<>{} & H is_point_conv_on X implies H is_point_conv_on Z &
lim(H, X)|Z = lim(H,Z)
proof
assume that
A1: Z c= X and
A2: Z<>{} and
A3: H is_point_conv_on X;
consider f such that
A4: X = dom f and
A5: for x st x in X holds for p st p>0 ex k st for n st n>=k
holds ||.(H.n)/.x - f/.x.|| < p by A3;
now
take g = f|Z;
thus
A7: Z = dom g by A1, A4, RELAT_1:62;
let x;
assume
A8: x in Z;
then
X8: f/.x =f.x by A1, A4, PARTFUN1:def 6;
g/.x =g.x by A7, A8, PARTFUN1:def 6;
then
X10: g/.x = f/.x by A7, A8, FUNCT_1:47, X8;
let p;
assume p>0;
then consider k such that
A9: for n st n>=k holds ||.(H.n)/.x - f/.x.|| < p by A1, A5, A8;
take k;
let n;
assume n>=k;
hence ||.(H.n)/.x -g/.x.|| < p by A9, X10;
end;
hence
A10: H is_point_conv_on Z by A1, A2, A3, Th22;
A11:
now
let x;
assume
A12: x in dom (lim(H, X)|Z);
then
A13: x in (dom lim(H, X)) /\ Z by RELAT_1:61;
then
A14: x in dom lim(H, X) by XBOOLE_0:def 4;
x in Z by A13, XBOOLE_0:def 4;
then
A15: x in dom lim(H,Z) by A10, Def13;
thus (lim(H, X)|Z).x = (lim(H, X)).x by A12, FUNCT_1:47
.= lim (H#x) by A3, A14, Def13
.= (lim(H,Z)).x by A10, A15, Def13;
end;
dom lim(H, X) = X by A3, Def13;
then dom lim(H, X) /\ Z = Z by A1, XBOOLE_1:28;
then dom (lim(H, X)|Z) = Z by RELAT_1:61;
then dom (lim(H, X)|Z) = dom lim(H,Z) by A10, Def13;
hence thesis by A11, PARTFUN1:5;
end;
theorem
Z c= X & Z <> {} & H is_unif_conv_on X implies H is_unif_conv_on Z
proof
assume that
A1: Z c= X and
A2: Z <> {} and
A3: H is_unif_conv_on X;
consider f such that
A4: dom f = X and
A5: for p st p>0 ex k st for n,x st n>=k & x in X
holds ||.(H.n)/.x - f/.x.|| < p by A3;
now
take g = f|Z;
thus
A7: dom g = dom f /\ Z by RELAT_1:61
.= Z by A1, A4, XBOOLE_1:28;
let p;
assume p>0;
then consider k such that
A8: for n,x st n>=k & x in X holds ||.(H.n)/.x - f/.x.|| < p by A5;
take k;
let n, x;
assume that
A9: n >= k and
A10: x in Z;
x in Z & x in dom f by A7, A10, RELAT_1:57;
then f/.x = f.x by PARTFUN1:def 6
.= g.x by A7, A10, FUNCT_1:47
.= g/.x by A10, A7, PARTFUN1:def 6;
hence ||.(H.n)/.x -g/.x.|| < p by A1, A8, A9, A10;
end;
hence thesis by A1, A2, A3, Th22;
end;
theorem Th25:
X common_on_dom H implies for x be set st x in X holds {x} common_on_dom H
proof
assume
A1: X common_on_dom H;
let x be set;
assume
A2: x in X;
thus {x} <> {};
now
let n;
X c= dom(H.n) by A1;
hence {x} c= dom(H.n) by A2,ZFMISC_1:31;
end;
hence thesis;
end;
theorem :: LM01:
H is_point_conv_on X implies for x be set st x in X
holds {x} common_on_dom H by Th25;
theorem Th27:
{x} common_on_dom H1 & {x} common_on_dom H2
implies H1#x + H2#x = (H1+H2)#x & H1#x - H2#x = (H1-H2)#x
proof
assume that
A1: {x} common_on_dom H1 and
A2: {x} common_on_dom H2;
now
let n be Element of NAT;
A3: {x} c= dom (H2.n) by A2;
x in {x} & {x} c= dom(H1.n) by A1, TARSKI:def 1;
then x in (dom(H1.n) /\ dom(H2.n)) by A3, XBOOLE_0:def 4;
then
A4: x in dom(H1.n + H2.n) by VFUNCT_1:def 1;
X4: dom(H1.n + H2.n) = dom ((H1+H2).n) by Def5;
thus (H1#x + H2#x).n = (H1#x).n + (H2#x).n by NORMSP_1:def 2
.= (H1.n)/.x + (H2#x).n by Def10
.= (H1.n)/.x + (H2.n)/.x by Def10
.= ((H1.n) + (H2.n))/.x by A4, VFUNCT_1:def 1
.= ((H1.n) + (H2.n)).x by A4, PARTFUN1:def 6
.= ((H1+H2).n).x by Def5
.= ((H1+H2).n)/.x by A4, X4, PARTFUN1:def 6
.= ((H1+H2)#x).n by Def10;
end;
hence H1#x + H2#x = (H1+H2)#x by FUNCT_2:63;
now
let n be Element of NAT;
A5: {x} c= dom (H2.n) by A2;
x in {x} & {x} c= dom(H1.n) by A1, TARSKI:def 1;
then x in (dom(H1.n) /\ dom(H2.n)) by A5, XBOOLE_0:def 4;
then
A6: x in dom(H1.n - H2.n) by VFUNCT_1:def 2;
X6: dom (H1.n - H2.n) = dom ((H1-H2).n) by Th3;
thus (H1#x - H2#x).n = (H1#x).n - (H2#x).n by NORMSP_1:def 3
.= (H1.n)/.x - (H2#x).n by Def10
.= (H1.n)/.x - (H2.n)/.x by Def10
.= ((H1.n) - (H2.n))/.x by A6, VFUNCT_1:def 2
.= ((H1.n) - (H2.n)).x by A6, PARTFUN1:def 6
.= ((H1-H2).n).x by Th3
.= ((H1-H2).n)/.x by X6, A6, PARTFUN1:def 6
.= ((H1-H2)#x).n by Def10;
end;
hence H1#x - H2#x = (H1-H2)#x by FUNCT_2:63;
end;
reserve x for Element of D;
theorem Th28:
{x} common_on_dom H implies (||.H.||)#x = ||.H#x .|| & (-H)#x = (-1)*(H#x)
proof
assume
AS1: {x} common_on_dom H;
now
let n be Element of NAT;
x in {x} & {x} c= dom(H.n) by AS1, TARSKI:def 1;
then x in dom (H.n);
then
A2: x in dom ||.(H.n).|| by NORMSP_0:def 2;
thus ((||.H.||)#x).n = (||.H.||.n).x by SEQFUNC:def 10
.= ||.(H.n).||.x by Def4
.= ||.(H.n)/.x.|| by A2, NORMSP_0:def 2
.= ||.(H#x).n.|| by Def10
.= ||.(H#x).|| .n by NORMSP_0:def 4;
end;
hence (||.H.||)#x = ||. H#x .|| by FUNCT_2:63;
now
let n be Element of NAT;
x in {x} & {x} c= dom(H.n) by AS1, TARSKI:def 1;
then x in dom (H.n);
then
A2: x in dom (-(H.n)) by VFUNCT_1:def 5;
thus ((-H)#x).n = ((-H).n)/.x by Def10
.= (-H.n)/.x by Def3
.= -((H.n)/.x) by A2, VFUNCT_1:def 5
.= -((H#x).n) by Def10
.=(-1)*((H#x).n) by RLVECT_1:16
.= ((-1)*(H#x)).n by NORMSP_1:def 5;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th29:
{x} common_on_dom H implies (r(#)H)#x = r*(H#x)
proof
assume
A1: {x} common_on_dom H;
now
let n be Element of NAT;
x in {x} & {x} c= dom(H.n) by A1, TARSKI:def 1;
then x in dom (H.n);
then
A2: x in dom (r(#)(H.n)) by VFUNCT_1:def 4;
X2: (r(#)H).n = r(#)(H.n) by Def1;
thus ((r(#)H)#x).n = ((r(#)H).n)/.x by Def10
.= r*((H.n)/.x) by X2, A2, VFUNCT_1:def 4
.= r*((H#x).n) by Def10
.= (r*(H#x)).n by NORMSP_1:def 5;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th30:
X common_on_dom H1 & X common_on_dom H2 implies for x st x in X
holds H1#x + H2#x = (H1+H2)#x & H1#x - H2#x = (H1-H2)#x
proof
assume
A1: X common_on_dom H1 & X common_on_dom H2;
let x;
assume x in X;
then {x} common_on_dom H1 & {x} common_on_dom H2 by A1, Th25;
hence thesis by Th27;
end;
theorem :: Th31:
{x} common_on_dom H implies ||.H.||#x = ||.(H#x).|| & (-H)#x = (-1)*(H#x)
by Th28;
theorem Th32:
X common_on_dom H implies for x st x in X holds (r(#)H)#x = r*(H#x)
proof
assume
A1: X common_on_dom H;
let x;
assume x in X;
then {x} common_on_dom H by A1, Th25;
hence thesis by Th29;
end;
theorem :: Th33:
H1 is_point_conv_on X & H2 is_point_conv_on X
implies for x st x in X holds H1#x + H2#x = (H1+H2)#x
& H1#x - H2#x = (H1-H2)#x by Th30;
theorem
{x} common_on_dom H implies ||.H.||#x = ||.(H#x).|| & (-H)#x = (-1)*(H#x)
by Th28;
theorem
H is_point_conv_on X implies for x st x in X holds (r(#)H)#x = r*(H# x)
by Th32;
theorem Th36:
X common_on_dom H1 & X common_on_dom H2
implies X common_on_dom H1 + H2 & X common_on_dom H1-H2
proof
assume that
A1: X common_on_dom H1 and
A2: X common_on_dom H2;
now
let n;
X c= dom (H1.n) & X c= dom (H2.n) by A1, A2;
then X c= dom (H1.n) /\ dom (H2.n) by XBOOLE_1:19;
then X c= dom (H1.n + H2.n) by VFUNCT_1:def 1;
hence X c= dom ((H1+H2).n) by Def5;
end;
hence X common_on_dom H1+H2 by A1;
now
let n;
X c= dom (H1.n) & X c= dom (H2.n) by A1, A2;
then X c= dom (H1.n) /\ dom (H2.n) by XBOOLE_1:19;
then X c= dom (H1.n - H2.n) by VFUNCT_1:def 2;
hence X c= dom ((H1-H2).n) by Th3;
end;
hence X common_on_dom H1-H2 by A1;
end;
theorem Th37:
X common_on_dom H implies X common_on_dom ||.H.|| & X common_on_dom (-H)
proof
assume
A1: X common_on_dom H;
now
let n;
dom (H.n) = dom ||.H.n.|| by NORMSP_0:def 3
.= dom (||.H.||.n) by Def4;
hence X c= dom (||.H.||.n) by A1;
end;
hence X common_on_dom ||.H.|| by A1;
now
let n;
dom (H.n) = dom (-(H.n)) by VFUNCT_1:def 5
.= dom ((-H).n) by Def3;
hence X c= dom ((-H).n) by A1;
end;
hence thesis by A1;
end;
theorem Th38:
X common_on_dom H implies X common_on_dom r(#)H
proof
assume
A1: X common_on_dom H;
now
let n;
dom (H.n) = dom(r(#)(H.n)) by VFUNCT_1:def 4
.= dom ((r(#)H).n) by Def1;
hence X c= dom ((r(#)H).n) by A1;
end;
hence thesis by A1;
end;
theorem
H1 is_point_conv_on X & H2 is_point_conv_on X implies 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
assume that
A1: H1 is_point_conv_on X and
A2: H2 is_point_conv_on X;
A3:
now
let x;
assume
A4: x in X;
then H1#x is convergent & H2#x is convergent by A1, A2, Th19;
then (H1#x)+(H2#x) is convergent by NORMSP_1:19;
hence (H1+H2)#x is convergent by A1, A2, A4, Th30;
end;
A5:
now
let x;
assume
A6: x in X;
then H1#x is convergent & H2#x is convergent by A1, A2, Th19;
then (H1#x)-(H2#x) is convergent by NORMSP_1:20;
hence (H1-H2)#x is convergent by A1, A2, A6, Th30;
end;
thus
A8: H1+H2 is_point_conv_on X by A1, A2, A3, Th36, Th19;
A9:
now
let x;
assume
A10: x in dom (lim(H1, X)+lim(H2, X));
then
A11: x in (dom lim(H1, X))/\(dom lim(H2, X)) by VFUNCT_1:def 1;
then
A12: x in (dom lim(H2, X)) by XBOOLE_0:def 4;
A13: x in (dom lim(H1, X)) by A11, XBOOLE_0:def 4;
then
A14: x in X by A1, Def13; then
A15: H1#x is convergent & H2#x is convergent by A1, A2, Th19;
X15: (lim(H1, X)).x =(lim(H1, X))/.x by A13, PARTFUN1:def 6;
X16: (lim(H2, X)).x =(lim(H2, X))/.x by A12, PARTFUN1:def 6;
thus (lim(H1, X) + lim(H2, X)).x = (lim(H1, X) + lim(H2, X))/.x
by A10, PARTFUN1:def 6
.= (lim(H1, X))/.x + (lim(H2, X))/.x by A10, VFUNCT_1:def 1
.= lim(H1#x) + (lim(H2, X))/.x by X15, A1, A13, Def13
.= lim(H1#x) + lim(H2#x) by X16, A2, A12, Def13
.= lim((H1#x) + (H2#x)) by A15, NORMSP_1:25
.= lim((H1+H2)#x) by A1, A2, A14, Th30;
end;
A24:
now
let x;
assume
A25: x in dom (lim(H1, X) - lim(H2, X));
then
A26: x in (dom lim(H1, X))/\(dom lim(H2, X)) by VFUNCT_1:def 2;
then
A27: x in (dom lim(H2, X)) by XBOOLE_0:def 4;
A28: x in (dom lim(H1, X)) by A26, XBOOLE_0:def 4;
then
A29: x in X by A1, Def13;
then
A30: H1#x is convergent & H2#x is convergent by A1, A2, Th19;
X15: (lim(H1, X)).x =(lim(H1, X))/.x by A28, PARTFUN1:def 6;
X16: (lim(H2, X)).x =(lim(H2, X))/.x by A27, PARTFUN1:def 6;
thus (lim(H1, X) - lim(H2, X)).x
= (lim(H1, X) - lim(H2, X))/.x by A25, PARTFUN1:def 6
.= (lim(H1, X))/.x - (lim(H2, X))/.x by A25, VFUNCT_1:def 2
.= lim(H1#x) - (lim(H2, X))/.x by X15, A1, A28, Def13
.= lim(H1#x) - lim(H2#x) by X16, A2, A27, Def13
.= lim((H1#x) - (H2#x)) by A30, NORMSP_1:26
.= lim((H1-H2)#x) by A1, A2, A29, Th30;
end;
dom (lim(H1, X)+lim(H2, X))=(dom lim(H1, X)) /\ (dom lim(H2, X))
by VFUNCT_1:def 1
.= X /\ (dom lim(H2, X)) by A1, Def13
.= X /\ X by A2, Def13
.= X;
hence lim(H1+H2, X) = lim(H1, X) + lim(H2, X) by A8, A9, Def13;
X common_on_dom H1-H2 by A1, A2, Th36;
hence
A31: H1 - H2 is_point_conv_on X by A5, Th19;
dom (lim(H1, X)-lim(H2, X))=(dom lim(H1, X)) /\ (dom lim(H2, X))
by VFUNCT_1:def 2
.= X /\ (dom lim(H2, X)) by A1, Def13
.= X /\ X by A2, Def13
.= X;
hence lim(H1-H2, X) = lim(H1, X) - lim(H2, X) by A31, A24, Def13;
end;
theorem
H is_point_conv_on X
implies ||.H.|| is_point_conv_on X & lim (||.H.||, X) = ||. lim (H, X) .||
& -H is_point_conv_on X & lim (-H, X) = - lim(H, X)
proof
assume
A1: H is_point_conv_on X;
A2:
now
let x;
assume
X0: x in X; then
X1: {x} common_on_dom H by A1, Th25;
||. H#x .|| is convergent by X0, A1, Th19, NORMSP_1:23;
hence ||.H.||#x is convergent by Th28, X1;
end;
A3:
now
let x;
assume A30:x in dom (-lim(H, X));
then
A4: x in dom lim(H, X) by VFUNCT_1:def 5;
then
A5: x in X by A1, Def13;
X5: lim(H, X) /.x =lim(H, X) .x by A4, PARTFUN1:def 6;
X1: {x} common_on_dom H by A5, A1, Th25;
thus (-lim(H, X)).x = (-lim(H, X))/.x by A30, PARTFUN1:def 6
.= -(lim(H, X)/.x) by A30, VFUNCT_1:def 5
.= -(lim(H#x)) by X5, A1, A4, Def13
.=(-1)* (lim(H#x)) by RLVECT_1:16
.= lim((-1)*(H#x)) by A1, A5, Th19, NORMSP_1:28
.= lim((-H)#x) by Th28, X1;
end;
thus
A7: ||.H.|| is_point_conv_on X by A1, Th37, A2, SEQFUNC:20;
A8:
now
let x;
assume A91: x in dom ||.lim(H, X).||;
then
A9: x in dom lim(H, X) by NORMSP_0:def 3;
then
A90: x in X by A1, Def13;
then
A10: H#x is convergent by A1, Th19;
X1: {x} common_on_dom H by A90, A1, Th25;
X10: lim(H, X)/.x = lim(H, X).x by A9, PARTFUN1:def 6;
thus ||.lim(H, X).||.x = ||.lim(H, X)/.x.|| by A91, NORMSP_0:def 3
.= ||.lim(H#x).|| by A1, A9, X10, Def13
.= lim ||.(H#x).|| by A10, LOPBAN_1:20
.= lim(||.H.||#x) by Th28, X1;
end;
A11:
now
let x;
assume
A90: x in X;
then X10: (-1)*(H#x) is convergent by A1, Th19, NORMSP_1:22;
{x} common_on_dom H by A90, A1, Th25;
hence (-H)#x is convergent by Th28, X10;
end;
dom ||.lim(H, X).|| = dom lim(H, X) by NORMSP_0:def 3
.= X by A1, Def13;
hence lim (||.H.||, X) = ||. lim (H, X) .|| by A7, A8, SEQFUNC:def 13;
thus
A12: -H is_point_conv_on X by A1, Th37, A11, Th19;
dom (-lim(H, X)) = dom lim(H, X) by VFUNCT_1:def 5
.= X by A1, Def13;
hence thesis by A12, A3, Def13;
end;
theorem
H is_point_conv_on X
implies r(#)H is_point_conv_on X & lim (r(#)H, X) = r(#)(lim(H, X))
proof
assume
A1: H is_point_conv_on X;
A3:
now
let x;
assume
A4: x in dom(r(#)(lim(H, X)));
then
A5: x in dom lim(H, X) by VFUNCT_1:def 4;
then
A6: x in X by A1, Def13;
X1: lim(H, X)/.x = lim(H, X).x by PARTFUN1:def 6, A5;
X2: (r(#)lim(H, X)).x = (r(#)lim(H, X))/.x by PARTFUN1:def 6, A4;
thus (r(#)lim(H, X)).x = r*(lim(H, X)/.x) by X2, A4, VFUNCT_1:def 4
.= r*(lim(H#x)) by A1, A5, X1, Def13
.= lim(r*(H#x)) by A6, A1, Th19, NORMSP_1:28
.= lim((r(#)H)#x) by A1, A6, Th32;
end;
A8:
now
let x;
assume
A9: x in X;
then r*(H#x) is convergent by A1, Th19, NORMSP_1:22;
hence (r(#)H)#x is convergent by A1, A9, Th32;
end;
A10: r(#)H is_point_conv_on X by A1, Th38, A8, Th19;
dom(r(#)(lim(H, X))) = dom lim(H, X) by VFUNCT_1:def 4
.= X by A1, Def13;
hence thesis by A10, A3, Def13;
end;
theorem Th42:
H is_unif_conv_on X
iff X common_on_dom H & H is_point_conv_on X
& for r st 0<r ex k st for n, x st n >= k & x in X
holds ||.(H.n)/.x-(lim(H, X))/.x.|| < r
proof
thus H is_unif_conv_on X implies
X common_on_dom H & H is_point_conv_on X
& for r st 0<r ex k st for n,x st n>=k & x in X
holds ||.(H.n)/.x-(lim(H, X))/.x.||<r
proof
assume
A1: H is_unif_conv_on X;
then consider f such that
A2: X = dom f and
A3: for p st p>0 ex k st for n,x st n>= k & x in X
holds ||.(H.n)/.x-f/.x .|| < p;
thus X common_on_dom H by A1;
A4:
now
let x such that
A5: x in X;
let p;
assume p>0;
then consider k such that
A6: for n, x st n >= k & x in X holds ||.(H.n)/.x-f/.x.|| < p by A3;
take k;
let n;
assume n >= k;
hence ||.(H.n)/.x-f/.x.||<p by A5, A6;
end;
thus H is_point_conv_on X by A1, Th21;
then
A7: f = (lim(H, X)) by A2, A4, Th20;
let r;
assume r > 0;
then consider k such that
A8: for n,x st n>=k & x in X holds ||.(H.n)/.x-f/.x.||<r by A3;
take k;
let n,x;
assume n >= k & x in X;
hence thesis by A7, A8;
end;
assume that
A9: X common_on_dom H and
A10: H is_point_conv_on X and
A11: for r st 0 < r ex k st for n, x st n >= k & x in X
holds ||.(H.n)/.x-(lim(H, X))/.x.|| < r;
dom lim(H, X) = X by A10, Def13;
hence thesis by A9, A11;
end;
reserve
V, W for RealNormSpace,
H for Functional_Sequence of the carrier of V,the carrier of W;
theorem
H is_unif_conv_on X & (for n holds (H.n)|X is_continuous_on X)
implies lim(H, X) is_continuous_on X
proof
set l = lim(H, X);
assume that
A1: H is_unif_conv_on X and
A2: for n holds (H.n)|X is_continuous_on X;
A3: H is_point_conv_on X by A1, Th21;
then
A4: dom l = X by Def13;
A5: X common_on_dom H by A1;
for x0 be Point of V st x0 in X holds l|X is_continuous_in x0
proof
let x0 be Point of V;
assume
A6: x0 in X; then
A60: x0 in dom(l|X) by RELAT_1:62, A4;
for r be Real st 0 < r ex s be Real st 0 < s
& for x1 be Point of V st x1 in dom (l|X)
& ||.x1-x0.|| < s holds ||.(l|X)/.x1-(l|X)/.x0.|| < r
proof
let r be Real;
assume
A7: 0 < r;
reconsider r as Element of REAL by XREAL_0:def 1;
consider k such that
A8: for n for x1 being Element of V st n>=k & x1 in X
holds ||.(H.n)/.x1-l/.x1.||<r/3 by A1, A7, XREAL_1:222, Th42;
0 < r/3 by A7, XREAL_1:222;
then
consider k1 be Nat such that
A9: for n st n>=k1 holds ||.(H.n)/.x0 - l/.x0.|| < r/3 by A3, A6, Th20;
reconsider m = max(k,k1) as Nat by TARSKI:1;
set h = H.m;
A11: dom(h|X) = dom h /\ X by RELAT_1:61
.= X by A5, XBOOLE_1:28;
h|X is_continuous_on X by A2;
then h is_continuous_on X by NFCONT_1:21;
then h|X is_continuous_in x0 by A6, NFCONT_1:def 7;
then consider s be Real such that
A12: 0<s and
A13: for x1 be Point of V st x1 in dom (h|X) & ||. x1- x0 .||<s holds
||.( h|X)/.x1-(h|X)/.x0.|| < r/3 by A7, XREAL_1:222, NFCONT_1:7;
take s;
thus 0<s by A12;
let x1 be Point of V;
assume that
A14: x1 in dom (l|X) and
A15: ||. x1-x0 .||<s;
A16: dom (l|X) = dom l /\ X by RELAT_1:61
.= X by A4;
then ||.(h|X)/.x1-(h|X)/.x0.||<r/3 by A11, A13, A14, A15;
then ||.h/.x1-(h|X)/.x0.||<r/3 by A16, A11, A14, PARTFUN1:80;
then
A17: ||.h/.x1-h/.x0.||<r/3 by A11, A6, PARTFUN1:80;
||.h/.x0 - l/.x0.|| < r/3 by A9, XXREAL_0:25;
then ||.(h/.x1-h/.x0)+(h/.x0-l/.x0).||
<= ||.h/.x1-h/.x0.||+||.h/.x0-l/.x0.||
& ||.h/.x1-h/.x0.|| +||.h/.x0-l/.x0.|| < r/3 + r/3
by A17, NORMSP_1:def 1, XREAL_1:8;
then
A18: ||.(h/.x1-h/.x0)+(h/.x0-l/.x0).||<r/3+r/3 by XXREAL_0:2;
||.l/.x1 - l/.x0.|| = ||.l/.x1 -h/.x1 +h/.x1 - l/.x0.|| by RLVECT_4:1
.= ||.l/.x1 -h/.x1 +(h/.x1 - l/.x0) .|| by RLVECT_1:28
.= ||.l/.x1 -h/.x1 +(h/.x1 -h/.x0 + h/.x0 - l/.x0) .|| by RLVECT_4:1
.= ||.l/.x1 -h/.x1 +((h/.x1 -h/.x0) + (h/.x0 - l/.x0)) .||
by RLVECT_1:28; then
A19: ||.l/.x1 - l/.x0.||
<= ||.l/.x1-h/.x1.|| + ||.(h/.x1-h/.x0)+(h/.x0-l/.x0 ) .||
by NORMSP_1:def 1;
||.h/.x1-l/.x1.||<r/3 by A8, A16, A14, XXREAL_0:25;
then ||.-(l/.x1-h/.x1).||<r/3 by RLVECT_1:33;
then ||.l/.x1-h/.x1.||<r/3 by NORMSP_1:2;
then ||.l/.x1-h/.x1.|| + ||.(h/.x1-h/.x0)+(h/.x0-l/.x0).||
< r/3 +(r/3+r/3) by A18, XREAL_1:8;
then ||.l/.x1 - l/.x0.|| < r/3 +r/3+r/3 by A19, XXREAL_0:2;
then ||.(l|X)/.x1 - l/.x0.|| < r by A14, PARTFUN1:80;
hence thesis by A4,RELAT_1:68;
end;
hence thesis by NFCONT_1:7, A60;
end;
hence thesis by NFCONT_1:def 7, A4;
end;