:: Compactness of Neural Networks
:: by Keiichi Miyajima and Hiroshi Yamazaki
::
:: Received April 30, 2022
:: Copyright (c) 2022-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 NEURONS1, ASCOLI, STRUCT_0, NUMBERS, PRE_TOPC, ORDINAL2,
PCOMPS_1, NORMSP_0, RELAT_1, CARD_3, SUBSET_1, RCOMP_1, XBOOLE_0,
FUNCT_1, TARSKI, CARD_1, ARYTM_3, ARYTM_1, COMPLEX1, RLVECT_1, ALGSTR_0,
REAL_1, FUNCT_2, VALUED_1, SUPINF_2, REALSET1, ZFMISC_1, XXREAL_0,
NORMSP_1, NORMSP_2, REWRITE1, NAT_1, RLVECT_2, RLVECT_3, SEQ_2, ORDEQ_01,
PARTFUN1, C0SP2, METRIC_1, RELAT_2, RLSUB_1, RLTOPSP1, FINSET_1, TBSP_1,
TOPMETR4, C0SP3, FINSEQ_1, REAL_NS1, RLVECT_5, NEWTON;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, CARD_1, RELSET_1,
PARTFUN1, FUNCT_2, BINOP_1, REALSET1, FINSET_1, ORDINAL1, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, COMPLEX1, FINSEQ_1, NEWTON, STRUCT_0,
ALGSTR_0, RLSUB_1, RLVECT_1, RLVECT_2, RLVECT_3, RLVECT_5, PCOMPS_1,
TBSP_1, NORMSP_0, NORMSP_1, NFCONT_1, COMPTS_1, PRE_TOPC, METRIC_1,
RUSUB_4, TOPMETR, CONVEX1, RLTOPSP1, LOPBAN_1, NORMSP_3, NORMSP_2,
TOPMETR4, C0SP3, REAL_NS1, ASCOLI;
constructors REALSET1, RSSPACE, PCOMPS_1, TBSP_1, NFCONT_1, TOPMETR, NORMSP_2,
RUSUB_4, CONVEX1, RLVECT_5, ABIAN, RLVECT_3, NEWTON, NORMSP_3, TOPMETR4,
C0SP3, ASCOLI, REAL_NS1;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, XREAL_0, ALGSTR_0,
NUMBERS, ORDINAL1, MEMBERED, VALUED_0, COMPTS_1, FUNCT_1, NEWTON,
FUNCT_2, TOPMETR, RELSET_1, NORMSP_1, NORMSP_2, RLVECT_1, RLVECT_5,
PARTFUN1, NORMSP_3, C0SP3, TBSP_1, CARD_1, NAT_1, FINSEQ_1, REAL_NS1,
ASCOLI;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI, RLVECT_1, ALGSTR_0, XBOOLE_0;
equalities ALGSTR_0, RLVECT_1, STRUCT_0, NORMSP_0, NORMSP_2, CONVEX1, RUSUB_4,
PCOMPS_1, C0SP3, METRIC_1, FINSEQ_1;
expansions TARSKI, RLVECT_1, STRUCT_0, NORMSP_0, NORMSP_1, RLTOPSP1, NFCONT_1,
PRE_TOPC, ASCOLI;
theorems FUNCT_1, PARTFUN1, ALGSTR_0, ZFMISC_1, TARSKI, XBOOLE_1, XREAL_0,
XXREAL_0, NORMSP_0, NORMSP_1, NORMSP_2, RLTOPSP1, NEWTON, XREAL_1,
RLVECT_1, FUNCT_2, RLVECT_5, RLVECT_2, RLVECT_3, NAT_1, FINSEQ_3,
XBOOLE_0, PRE_TOPC, RLSUB_1, ORDINAL1, TOPMETR4, POWER, TOPMETR,
NORMSP_3, PCOMPS_1, C0SP3, METRIC_1, FINSEQ_1, ASCOLI, INT_1, REAL_NS2,
REAL_NS3, BINOP_1, XCMPLX_1;
schemes FUNCT_2, NAT_1, RECDEF_1;
begin :: Preliminaries
reserve RNS1,RNS2 for RealLinearSpace;
theorem
the RLSStruct of RNS1 = the RLSStruct of RNS2
implies the carrier of RNS1 = the carrier of RNS2;
theorem
the RLSStruct of RNS1 = the RLSStruct of RNS2
implies 0.(RNS1) = 0.(RNS2);
theorem
the RLSStruct of RNS1 = the RLSStruct of RNS2
implies
for p,q be Element of RNS1,
f,g be Element of RNS2
st p=f & q=g
holds p+q = f+g;
theorem
the RLSStruct of RNS1 = the RLSStruct of RNS2
implies
for r be Real,
q be Element of RNS1,
g be Element of RNS2
st q = g
holds r*q = r*g;
theorem Th5:
the RLSStruct of RNS1 = the RLSStruct of RNS2
implies
for q be Element of RNS1,
g be Element of RNS2
st q = g
holds -q = -g
proof
assume A1: the RLSStruct of RNS1 = the RLSStruct of RNS2;
let q be Element of RNS1,
g be Element of RNS2;
assume A2: q = g;
thus -q = (-1)*q by RLVECT_1:16
.= (-1)*g by A2,A1
.= -g by RLVECT_1:16;
end;
theorem
the RLSStruct of RNS1 = the RLSStruct of RNS2
implies
for p,q be Element of RNS1,
f,g be Element of RNS2
st p=f & q=g
holds p-q = f-g by Th5;
theorem Th7:
the RLSStruct of RNS1 = the RLSStruct of RNS2
implies
for X being set
for n being Nat holds
( X is Linear_Combination of RNS2
iff X is Linear_Combination of RNS1 )
proof
assume A1: the RLSStruct of RNS1 = the RLSStruct of RNS2;
let X be set;
let n be Nat;
hereby assume X is Linear_Combination of RNS2; then
reconsider Lr = X as Linear_Combination of RNS2;
consider T being finite Subset of RNS2 such that
A2: for v being Element of RNS2 st not v in T holds
Lr.v = 0 by RLVECT_2:def 3;
reconsider T0=T as finite Subset of RNS1 by A1;
thus X is Linear_Combination of RNS1 by A2,RLVECT_2:def 3,A1;
end;
assume X is Linear_Combination of RNS1; then
reconsider Lr = X as Linear_Combination of RNS1;
consider T being finite Subset of RNS1 such that
A3: for v being Element of RNS1 st not v in T holds
Lr.v = 0 by RLVECT_2:def 3;
thus X is Linear_Combination of RNS2 by A3,RLVECT_2:def 3,A1;
end;
theorem
the RLSStruct of RNS1 = the RLSStruct of RNS2
implies
for Lv be Linear_Combination of RNS1,
Lr be Linear_Combination of RNS2 st Lr = Lv
holds Carrier Lr = Carrier Lv;
theorem
the RLSStruct of RNS1 = the RLSStruct of RNS2
implies
for F be set
holds
F is Subset of RNS1
iff
F is Subset of RNS2;
theorem
the RLSStruct of RNS1 = the RLSStruct of RNS2
implies
for F be set
holds
F is FinSequence of RNS1
iff
F is FinSequence of RNS2;
theorem
the RLSStruct of RNS1 = the RLSStruct of RNS2
implies
for F be set
holds
F is Function of RNS1, REAL
iff
F is Function of RNS2, REAL;
theorem Th12:
the RLSStruct of RNS1 = the RLSStruct of RNS2
implies
for FFr be FinSequence of RNS1,
fr be Function of RNS1,REAL,
Fv be FinSequence of RNS2,
fv be Function of RNS2,REAL st fr = fv & FFr = Fv
holds fr(#)FFr = fv(#)Fv
proof
assume A1: the RLSStruct of RNS1 = the RLSStruct of RNS2;
let FFr be FinSequence of RNS1,
fr be Function of RNS1,REAL,
Fv be FinSequence of RNS2,
fv be Function of RNS2,REAL;
assume A2: fr = fv & FFr = Fv; then
A3: len(fv(#)Fv) = len FFr by RLVECT_2:def 7;
for i being Nat st i in dom (fv(#)Fv) holds
(fv(#)Fv).i = (fr.(FFr/.i)) * (FFr/.i)
proof
let i be Nat;
assume i in dom (fv(#)Fv);
hence (fv(#)Fv).i = (fv.(Fv/.i)) * (Fv/.i) by RLVECT_2:def 7
.= (fr.(FFr/.i)) * (FFr/.i) by A2,A1;
end;
hence thesis by A3,A1,RLVECT_2:def 7;
end;
theorem Th13:
the RLSStruct of RNS1 = the RLSStruct of RNS2
implies
for Ft be FinSequence of RNS1,
FFr be FinSequence of RNS2 st Ft = FFr
holds Sum Ft = Sum FFr
proof
assume A1: the RLSStruct of RNS1 = the RLSStruct of RNS2;
let F be FinSequence of RNS1,
Fv be FinSequence of RNS2;
assume A2: F = Fv;
set T = RNS1;
set V = RNS2;
consider f being sequence of the carrier of T such that
A3: Sum F = f.(len F) and
A4: f.0 = 0.T and
A5: for j being Nat
for v being Element of T st j < len F & v = F.(j+1) holds
f.(j+1) = (f.j)+v by RLVECT_1:def 12;
consider fv being sequence of the carrier of V such that
A6: Sum Fv = fv.(len Fv) and
A7: fv.0 = 0.V and
A8: for j being Nat
for v being Element of V st j < len Fv & v = Fv.(j+1) holds
fv.(j+1) = (fv.j)+v by RLVECT_1:def 12;
defpred S1[Nat] means $1 <= len F implies f.$1 = fv.$1;
A9: for i being Nat st S1[i] holds S1[i+1]
proof
let i be Nat;
assume A10: S1[i];
assume A11: i+1 <= len F; then
A12: i+1 in dom F by NAT_1:11, FINSEQ_3:25; then
F.(i+1) = F/.(i+1) by PARTFUN1:def 6; then
A13: f.(i+1) = (f.i) + F/.(i+1) by A5, A11, NAT_1:13;
A14: Fv/.(i+1) = Fv.(i+1) by A2, A12, PARTFUN1:def 6;
thus f.(i+1) = fv.i + Fv/.(i+1) by A10, A11, A13, NAT_1:13, A1, A2
.= fv.(i+1) by A2, A8, A11, NAT_1:13, A14;
end;
A15: S1[ 0 ] by A4, A7, A1;
for n being Nat holds S1[n] from NAT_1:sch 2(A15, A9);
hence Sum F = Sum Fv by A2, A3, A6;
end;
theorem Th14:
the RLSStruct of RNS1 = the RLSStruct of RNS2
implies
for Lr be Linear_Combination of RNS2,
Lt be Linear_Combination of RNS1 st Lr = Lt
holds Sum Lr = Sum Lt
proof
assume A1: the RLSStruct of RNS1 = the RLSStruct of RNS2;
let Lr be Linear_Combination of RNS2,
Lt be Linear_Combination of RNS1;
assume A2: Lr = Lt;
set R = RNS2;
set T = RNS1;
consider Ft being FinSequence of the carrier of RNS1 such that
A3: Ft is one-to-one & rng Ft = Carrier Lt and
A4: Sum Lt = Sum (Lt (#) Ft) by RLVECT_2:def 8;
reconsider FFr = Ft as FinSequence of the carrier of RNS2 by A1;
thus Sum Lt = Sum (Lr (#) FFr) by A2, Th12, A1, Th13, A4
.= Sum Lr by A3, A2, RLVECT_2:def 8;
end;
theorem
the RLSStruct of RNS1 = the RLSStruct of RNS2
implies
for Ar be Subset of RNS2,
At be Subset of RNS1 st Ar = At
holds
for X be object holds
X is Linear_Combination of Ar
iff
X is Linear_Combination of At
proof
assume A1: the RLSStruct of RNS1 = the RLSStruct of RNS2;
let Ar be Subset of RNS2,
At be Subset of RNS1;
assume A2: Ar = At;
let X be object;
hereby assume
X is Linear_Combination of Ar; then
reconsider L=X as Linear_Combination of Ar;
reconsider L1 = L as Linear_Combination of RNS1 by Th7,A1;
(Carrier L1 = Carrier L & Carrier L c= Ar) by RLVECT_2:def 6;
hence X is Linear_Combination of At by A2, RLVECT_2:def 6;
end;
assume X is Linear_Combination of At; then
reconsider L=X as Linear_Combination of At;
reconsider L1 = L as Linear_Combination of RNS2 by Th7, A1;
(Carrier L1 = Carrier L & Carrier L c= At) by RLVECT_2:def 6;
hence X is Linear_Combination of Ar by A2, RLVECT_2:def 6;
end;
theorem Th16:
the RLSStruct of RNS1 = the RLSStruct of RNS2
implies
for Ar be Subset of RNS2,
At be Subset of RNS1 st Ar = At
holds [#]Lin Ar = [#]Lin At
proof
assume A1: the RLSStruct of RNS1 = the RLSStruct of RNS2;
let Ar be Subset of RNS2,
At be Subset of RNS1;
assume A2: Ar = At;
hereby
let x be object;
assume x in [#] (Lin Ar); then
x in Lin Ar; then
consider L being Linear_Combination of Ar such that
A3: x = Sum L by RLVECT_3:14;
reconsider L1 = L as Linear_Combination of RNS1 by Th7,A1;
(Carrier L1 = Carrier L & Carrier L c= Ar) by RLVECT_2:def 6; then
A4: L1 is Linear_Combination of At by A2, RLVECT_2:def 6;
Sum L1 = Sum L by Th14, A1; then
x in Lin At by A3, A4, RLVECT_3:14;
hence x in [#] (Lin At);
end;
let x be object;
assume x in [#] (Lin At); then
x in Lin At; then
consider L being Linear_Combination of At such that
A5: x = Sum L by RLVECT_3:14;
reconsider L1 = L as Linear_Combination of RNS2 by Th7,A1;
(Carrier L1 = Carrier L & Carrier L c= At) by RLVECT_2:def 6; then
A6: L1 is Linear_Combination of Ar by A2, RLVECT_2:def 6;
Sum L1 = Sum L by Th14,A1; then
x in Lin Ar by A5, A6, RLVECT_3:14;
hence x in [#] (Lin Ar);
end;
theorem Th17:
the RLSStruct of RNS1 = the RLSStruct of RNS2
implies
for Ar be Subset of RNS2,
At be Subset of RNS1 st Ar = At
holds
Ar is linearly-independent
iff
At is linearly-independent
proof
assume A1: the RLSStruct of RNS1 = the RLSStruct of RNS2;
let Ar be Subset of RNS2,
At be Subset of RNS1;
assume A2: Ar = At;
hereby
assume A3: Ar is linearly-independent;
now
let L be Linear_Combination of At;
reconsider L1 = L as Linear_Combination of RNS2 by Th7,A1;
A4: Carrier L1 = Carrier L;
assume Sum L = 0.(RNS1); then
A5: 0.(RNS2) = Sum L1 by Th14,A1;
L1 is Linear_Combination of Ar by A2, A4, RLVECT_2:def 6;
hence Carrier L = {} by A3, A5, RLVECT_3:def 1;
end;
hence At is linearly-independent by RLVECT_3:def 1;
end;
assume A6: At is linearly-independent;
now
let L be Linear_Combination of Ar;
reconsider L1 = L as Linear_Combination of RNS1 by Th7, A1;
Carrier L1 = Carrier L; then
reconsider L1 = L as Linear_Combination of At by A2, RLVECT_2:def 6;
assume Sum L = 0.(RNS2); then
0.(RNS1) = Sum L1 by Th14, A1;
hence Carrier L = {} by A6, RLVECT_3:def 1;
end;
hence Ar is linearly-independent by RLVECT_3:def 1;
end;
theorem
the RLSStruct of RNS1 = the RLSStruct of RNS2
implies
for X being object
holds
(X is Subspace of RNS2
iff
X is Subspace of RNS1)
proof
assume A1: the RLSStruct of RNS1 = the RLSStruct of RNS2;
let X be object;
hereby
assume X is Subspace of RNS2; then
reconsider V = X as Subspace of RNS2;
A2: the carrier of V c= the carrier of RNS2
& 0.V = 0.(RNS2)
& the addF of V = (the addF of RNS2) || the carrier of V
& the Mult of V = (the Mult of RNS2) | [:REAL, the carrier of V:]
by RLSUB_1:def 2;
0.V = 0.(RNS1) by A2,A1;
hence X is Subspace of RNS1 by A1, A2, RLSUB_1:def 2;
end;
assume X is Subspace of RNS1; then
reconsider V = X as Subspace of RNS1;
A4: the carrier of V c= the carrier of RNS1
& 0.V = 0.(RNS1)
& the addF of V = (the addF of RNS1) || the carrier of V
& the Mult of V = (the Mult of RNS1) | [:REAL, the carrier of V:]
by RLSUB_1:def 2;
0.V = 0.(RNS2) by A4,A1;
hence X is Subspace of RNS2 by A1,A4,RLSUB_1:def 2;
end;
theorem
the RLSStruct of RNS1 = the RLSStruct of RNS2
implies
for L be Linear_Combination of RNS2,
S be Linear_Combination of RNS1
st L = S
holds
Sum L = Sum S
proof
assume A1:the RLSStruct of RNS1 = the RLSStruct of RNS2;
let L be Linear_Combination of RNS2,
S be Linear_Combination of RNS1;
assume A2: L = S;
consider F being FinSequence of RNS2 such that
A3: F is one-to-one & rng F = Carrier L
& Sum L = Sum (L (#) F) by RLVECT_2:def 8;
reconsider E = F as FinSequence of RNS1 by A1;
A4: Sum(L(#)F) = Sum(S(#)E) by A2,A1,Th12,Th13;
reconsider SS=Sum L as Element of RNS1 by A1;
thus thesis by RLVECT_2:def 8,A2,A3,A4;
end;
theorem Th20:
the RLSStruct of RNS1 = the RLSStruct of RNS2
implies
for X be set
holds
X is Basis of RNS1
iff
X is Basis of RNS2
proof
assume A1:the RLSStruct of RNS1 = the RLSStruct of RNS2;
let X be set;
set V = RNS1;
set W = RNS2;
hereby assume
X is Basis of V; then
reconsider A = X as Basis of V;
reconsider B = A as Subset of W by A1;
A is linearly-independent
& Lin A = RLSStruct(# the carrier of V, the ZeroF of V,
the addF of V, the Mult of V #) by RLVECT_3:def 3;
then
A3: B is linearly-independent by A1,Th17;
set W0 = (Omega).W;
A4: W0 = RLSStruct(# the carrier of W, the ZeroF of W,
the addF of W, the Mult of W #) by RLSUB_1:def 4;
A5: Lin B is strict Subspace of W0 by REAL_NS2:49;
A6: [#]Lin A = the carrier of W by A1,RLVECT_3:def 3;
the carrier of Lin B = [#](Lin B)
.= the carrier of W0 by Th16,A1,A6,A4; then
Lin B = W0 by A5,RLSUB_1:32
.= RLSStruct(# the carrier of W, the ZeroF of W,
the addF of W, the Mult of W #) by RLSUB_1:def 4;
hence X is Basis of W by A3, RLVECT_3:def 3;
end;
assume X is Basis of W; then
reconsider A = X as Basis of W;
reconsider B = A as Subset of V by A1;
A is linearly-independent
& Lin A = RLSStruct(# the carrier of W, the ZeroF of W,
the addF of W, the Mult of W #) by RLVECT_3:def 3; then
A8: B is linearly-independent by A1,Th17;
set V0 = (Omega).V;
A9: V0 = RLSStruct(# the carrier of V, the ZeroF of V,
the addF of V, the Mult of V #) by RLSUB_1:def 4;
A10: Lin B is strict Subspace of V0 by REAL_NS2:49;
A11: [#]Lin A = the carrier of V by A1,RLVECT_3:def 3;
the carrier of Lin B = [#](Lin B)
.= the carrier of V0 by A9,Th16,A11,A1; then
Lin B = V0 by A10,RLSUB_1:32
.= RLSStruct(# the carrier of V, the ZeroF of V,
the addF of V, the Mult of V #) by RLSUB_1:def 4;
hence X is Basis of V by A8,RLVECT_3:def 3;
end;
theorem Th21:
for RNS1,RNS2 be RealLinearSpace
st the RLSStruct of RNS1 = the RLSStruct of RNS2
& RNS1 is finite-dimensional
holds RNS2 is finite-dimensional & dim RNS2 = dim RNS1
proof
let RNS1,RNS2 be RealLinearSpace;
assume A1: the RLSStruct of RNS1 = the RLSStruct of RNS2
& RNS1 is finite-dimensional; then
consider A being finite Subset of RNS1 such that
A2: A is Basis of RNS1 by RLVECT_5:def 1;
A3: dim RNS1 = card A by RLVECT_5:def 2, A2, A1;
reconsider B = A as finite Subset of RNS2 by A1;
A4: B is Basis of RNS2 by Th20, A1, A2;
hence RNS2 is finite-dimensional by RLVECT_5:def 1;
hence dim RNS2 = dim RNS1 by RLVECT_5:def 2, A3, A4;
end;
theorem Th22:
for RNS be RealNormSpace
holds the NORMSTR of RNS is strict RealNormSpace
proof
let l0 be RealNormSpace;
set l = the NORMSTR of l0;
reconsider l as non empty NORMSTR;
A1: l is Abelian
proof
let v, w be VECTOR of l;
reconsider v1 = v, w1 = w as VECTOR of l0;
thus v+w = v1+w1
.= w1+v1
.= w+v;
end;
A2: l is right_zeroed
proof
let v be VECTOR of l;
reconsider v1 = v as VECTOR of l0;
thus v+(0.l) = v1+(0.l0)
.= v;
end;
A3: l is right_complementable
proof
let v be VECTOR of l;
reconsider v1 = v as VECTOR of l0;
consider w1 being VECTOR of l0 such that
A4: v1+w1 = 0.l0 by ALGSTR_0:def 11;
reconsider w = w1 as VECTOR of l;
take w;
thus v+w = 0.l by A4;
end;
A5: for v being VECTOR of l holds 1*v = v
proof
let v be VECTOR of l;
reconsider v1 = v as VECTOR of l0;
thus 1*v = 1*v1
.= v by RLVECT_1:def 8;
end;
A6: for a, b being Real
for v being VECTOR of l holds (a*b)*v = a*(b*v)
proof
let a, b be Real;
let v be VECTOR of l;
reconsider v1 = v as VECTOR of l0;
thus (a*b)*v = (a*b)*v1
.= a*(b*v1) by RLVECT_1:def 7
.= a*(b*v);
end;
A7: for a, b being Real
for v being VECTOR of l holds (a+b)*v = (a*v)+(b*v)
proof
let a, b be Real;
let v be VECTOR of l;
reconsider v1 = v as VECTOR of l0;
thus (a+b)*v = (a+b)*v1
.= (a*v1)+(b*v1) by RLVECT_1:def 6
.= (a*v)+(b*v);
end;
A8: for a being Real
for v, w being VECTOR of l holds a*(v+w) = (a*v)+(a*w)
proof
let a be Real;
let v, w be VECTOR of l;
reconsider v1 = v, w1 = w as VECTOR of l0;
thus a*(v+w) = a*(v1+w1)
.= (a*v1)+(a*w1) by RLVECT_1:def 5
.= (a*v)+(a*w);
end;
A9:l is add-associative
proof
let u, v, w be VECTOR of l;
reconsider u1 = u, v1 = v, w1 = w as VECTOR of l0;
thus (u+v)+w = (u1+v1)+w1
.= u1+(v1+w1) by RLVECT_1:def 3
.= u+(v+w);
end;
now
let x, y be Point of l;
let a be Real;
reconsider u = x, w = y as VECTOR of l0;
||.u.|| = 0 iff u =0.l0 by NORMSP_0:def 5,def 6;
hence ||.x.|| = 0 iff x = 0.l;
thus ||.(a * x).|| = ||.(a * u).||
.= |.a.| * ||.u.|| by NORMSP_1:def 1
.= |.a.| * ||.x.||;
||.(u + w).|| <= ||.u.|| + ||.w.|| by NORMSP_1:def 1;
hence ||.(x + y).|| <= ||.x.|| + ||.y.||;
end; then
l is discerning reflexive RealNormSpace-like;
hence thesis by A1, A2, A3, A5, A6, A7, A8, A9,
RLVECT_1:def 5, def 6, def 7, def 8;
end;
theorem Th23:
for RNS be RealNormSpace
holds ex T be NormedLinearTopSpace
st the NORMSTR of RNS = the NORMSTR of T
proof
let RNS0 be RealNormSpace;
reconsider RNS = the NORMSTR of RNS0 as strict RealNormSpace by Th22;
set LRNS = LinearTopSpaceNorm RNS;
A1: the carrier of LRNS = the carrier of RNS
& 0. LRNS = 0. RNS
& the addF of LRNS = the addF of RNS
& the Mult of LRNS = the Mult of RNS
& the topology of LRNS = the topology of TopSpaceNorm RNS
by NORMSP_2:def 4;
reconsider N = the normF of RNS as Function of the carrier of LRNS, REAL by A1;
set W = RLNormTopStruct
(# the carrier of LRNS,
the ZeroF of LRNS,
the addF of LRNS,
the Mult of LRNS,
the topology of LRNS,
N #);
now
let x, y be Point of W;
let a be Real;
reconsider u = x, w = y as VECTOR of RNS by NORMSP_2:def 4;
||.u.|| = 0 iff u =0.RNS by NORMSP_0:def 5,def 6;
hence ||.x.|| = 0 iff x = 0.W by A1;
thus ||.(a*x).|| = ||.(a*u).|| by NORMSP_2:def 4
.= |.a.| * ||.u.|| by NORMSP_1:def 1
.= |.a.| * ||.x.||;
||.(u+w).|| <= ||.u.|| + ||.w.|| by NORMSP_1:def 1;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by NORMSP_2:def 4;
end; then
A2: W is discerning reflexive RealNormSpace-like;
A3: W is TopSpace-like right_complementable
Abelian add-associative right_zeroed
vector-distributive scalar-distributive
scalar-associative scalar-unital
add-continuous Mult-continuous
proof
A4: for x1, x2 being Point of W
for V being Subset of W st V is open & x1+x2 in V holds
ex V1, V2 being Subset of W st
V1 is open & V2 is open & x1 in V1 & x2 in V2 & V1+V2 c= V
proof
let x1, x2 be Point of W;
let V be Subset of W;
assume A5: V is open & x1+x2 in V;
reconsider V0 = V as Subset of LRNS;
reconsider xx1=x1, xx2=x2 as Point of LRNS;
V0 is open & xx1+xx2 in V0 by A5; then
consider V10, V20 being Subset of LRNS such that
A6: V10 is open & V20 is open & xx1 in V10 & xx2 in V20 & V10+V20 c= V0
by RLTOPSP1:def 8;
reconsider V1=V10, V2=V20 as Subset of W;
A7: for z be object holds z in V10+V20 iff z in V1+V2
proof
let z be object;
hereby assume z in V10 + V20; then
consider u0, v0 be Element of LRNS such that
A8: z=u0+v0 & u0 in V10 & v0 in V20;
reconsider u=u0, v=v0 as Element of W;
u+v = u0+v0;
hence z in V1+V2 by A8;
end;
assume z in V1 + V2; then
consider u0, v0 be Element of W such that
A9: z = u0+v0 & u0 in V10 & v0 in V20;
reconsider u=u0, v=v0 as Element of LRNS;
u+v = u0+v0;
hence z in V10+V20 by A9;
end;
take V1,V2;
thus thesis by A6,A7;
end;
A10: now
let a, b be Real;
let v be VECTOR of W;
reconsider v1 = v as VECTOR of LRNS;
A11: (a*v1) + (b*v1) = (a*v) + (b*v);
(a+b) * v = (a+b) * v1;
hence (a+b) * v = (a*v) + (b*v) by A11, RLVECT_1:def 6;
end;
A12: for a being Real
for x being Point of W
for V being Subset of W st V is open & a * x in V holds
ex r being positive Real,
Z being Subset of W st Z is open & x in Z &
for s being Real st |.(s - a).| < r holds s * Z c= V
proof
let a be Real;
let x be Point of W,
V be Subset of W;
assume A13: V is open & a * x in V;
reconsider V0 = V as Subset of LRNS;
reconsider xx=x as Point of LRNS;
V0 is open & a*xx in V0 by A13; then
consider r being positive Real,
Z0 being Subset of LRNS such that
A14: Z0 is open & xx in Z0 &
for s being Real st |.(s - a).| < r holds
s * Z0 c= V0 by RLTOPSP1:def 9;
reconsider Z= Z0 as Subset of W;
take r,Z;
for s being Real st |.(s - a).| < r holds s * Z c= V
proof
let s be Real;
assume |.(s - a).| < r; then
A15: s * Z0 c= V0 by A14;
for z be object holds z in s * Z0 iff z in s * Z
proof
let z be object;
hereby assume z in s * Z0; then
consider u0 be Element of LRNS such that
A16: z=s*u0 & u0 in Z0;
reconsider u =u0 as Element of W;
s*u = s*u0;
hence z in s * Z by A16;
end;
assume z in s * Z; then
consider u0 be Element of W such that
A17: z=s*u0 & u0 in Z0;
reconsider u = u0 as Element of LRNS;
s*u = s*u0;
hence z in s * Z0 by A17;
end;
hence thesis by A15;
end;
hence thesis by A14;
end;
A18: W is Abelian
proof
let v, w be VECTOR of W;
reconsider v1 = v, w1 = w as VECTOR of LRNS;
thus v+w = v1+w1
.= w1+v1
.= w+v;
end;
A19: W is add-associative
proof
let v, w, x be VECTOR of W;
reconsider v1 = v, w1 = w, x1 = x as VECTOR of LRNS;
thus (v+w)+x = (v1+w1)+x1
.= v1+(w1+x1) by RLVECT_1:def 3
.= v+(w+x);
end;
A20: W is right_zeroed
proof
let v be VECTOR of W;
reconsider v1 = v as VECTOR of LRNS;
thus v+(0.W) = v1+(0.LRNS)
.= v;
end;
A21: W is right_complementable
proof
let v be VECTOR of W;
reconsider v1 = v as VECTOR of LRNS;
reconsider w = -v1 as VECTOR of W;
take w;
thus v+w = v1-v1
.= 0.LRNS by RLVECT_1:15
.= 0.W;
end;
A22: now
let a, b be Real;
let v be VECTOR of W;
reconsider v1 = v as VECTOR of LRNS;
a*(b*v1) = a*(b*v); then
(a*b)*v1 = a*(b*v) by RLVECT_1:def 7;
hence (a*b)*v = a*(b*v);
end;
A23: now
let a be Real;
let v, w be VECTOR of W;
reconsider v1 = v, w1 = w as VECTOR of LRNS;
A24: (a*v1)+(a*w1) = (a*v)+(a*w);
a*(v+w) = a*(v1+w1);
hence a*(v+w) = (a*v)+(a*w) by A24, RLVECT_1:def 5;
end;
now
let v be VECTOR of W;
reconsider v1 = v as VECTOR of LRNS;
thus 1*v = 1*v1
.= v by RLVECT_1:def 8;
end;
hence thesis by A4, A10, A12, A18, A19, A20, A21, A22, A23, PRE_TOPC:def 1;
end;
now
let p, q be Point of W;
reconsider p1 = p, q1 = q as Point of LRNS;
assume p <> q; then
consider W1, V1 being Subset of LRNS such that
A25: W1 is open and
A26: V1 is open and
A27: p1 in W1 & q1 in V1 & W1 misses V1 by PRE_TOPC:def 10;
reconsider WW = W1, V = V1 as Subset of W;
A28: V is open by A26;
WW is open by A25;
hence ex b1, b2 being Element of bool the carrier of W st
b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 by A27, A28;
end; then
W is T_2; then
reconsider W as NormedLinearTopSpace by A1, A2, A3, C0SP3:def 6;
take W;
thus the NORMSTR of RNS0 = the NORMSTR of W by A1;
end;
theorem
for RNS be RealNormSpace
st RNS is finite-dimensional
holds ex T be NormedLinearTopSpace
st the NORMSTR of RNS = the NORMSTR of T & T is finite-dimensional
proof
let RNS be RealNormSpace;
assume A1: RNS is finite-dimensional;
consider T be NormedLinearTopSpace such that
A2: the NORMSTR of RNS = the NORMSTR of T by Th23;
take T;
the RLSStruct of T = the RLSStruct of RNS by A2;
hence thesis by Th21, A1, A2;
end;
theorem Th25:
for T be NormedLinearTopSpace,
RNS be RealNormSpace
st T is finite-dimensional & RNS = the NORMSTR of T
holds
RNS is finite-dimensional & dim RNS = dim T
proof
let T be NormedLinearTopSpace,
RNS be RealNormSpace;
assume A1: T is finite-dimensional
& RNS = the NORMSTR of T; then
the RLSStruct of T = the RLSStruct of RNS;
hence thesis by Th21, A1;
end;
begin :: The Ascoli-Arzela theorem on the finite dimensional normed linear spaces
theorem Th26:
for M be non empty MetrSpace, S be non empty compact TopSpace,
T be NormedLinearTopSpace
st S = TopSpaceMetr(M) & T is complete & T is finite-dimensional
& dim (T) <> 0
holds
for G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T))
st G = H
holds
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T))
| H is totally_bounded
iff
G is equibounded & G is equicontinuous
proof
let M be non empty MetrSpace, S be non empty compact TopSpace,
T be NormedLinearTopSpace;
assume that
A1: S = TopSpaceMetr(M) and
A2: T is complete and
A3: T is finite-dimensional & dim T <> 0;
let G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T));
assume A4: G = H;
hence (MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T))
| H is totally_bounded
implies
G is equibounded & G is equicontinuous by A1, A2, ASCOLI:13;
assume A5: G is equibounded & G is equicontinuous;
for x be Point of S,
Hx be non empty Subset of MetricSpaceNorm T
st Hx = {f.x where f is Function of S,T :f in H}
holds ((MetricSpaceNorm T)) | Cl(Hx) is compact
proof
let x be Point of S,
Hx be non empty Subset of MetricSpaceNorm T;
assume A6: Hx = {f.x where f is Function of S,T :f in H };
reconsider Tx = Hx as non empty Subset of TopSpaceNorm T;
reconsider Fx = Hx as non empty Subset of T;
A7: Cl(Fx) = Cl(Hx) by ASCOLI:1;
consider RNS be RealNormSpace such that
A8: RNS = the NORMSTR of T &
the topology of T = the topology of TopSpaceNorm RNS by C0SP3:def 6;
A9: RNS is finite-dimensional & dim RNS <> 0 by A3, A8, Th25;
reconsider Fx0 = Fx as non empty Subset of RNS by A8;
A10: for a being Element of RNS
for b being Element of RNS
holds (distance_by_norm_of RNS).(a,b) = (distance_by_norm_of T).(a,b)
proof
let a be Element of RNS;
let b be Element of RNS;
reconsider a1=a, b1=b as Element of T by A8;
A11: a-b = a+(-1)*b by RLVECT_1:16
.= (the addF of T).(a1,(-1)*b1 ) by A8
.= a1-b1 by RLVECT_1:16;
thus (distance_by_norm_of RNS).(a,b) = ||.a-b.|| by NORMSP_2:def 1
.= ||.a1-b1.|| by A11,A8
.= (distance_by_norm_of T).(a,b) by NORMSP_2:def 1;
end;
A12: MetricSpaceNorm RNS
= MetricSpaceNorm T by A10,A8,BINOP_1:2; then
A13: Cl(Fx0) = Cl(Fx) by A7,ASCOLI:1;
reconsider ClHx = Cl(Hx) as non empty Subset of MetricSpaceNorm RNS by A8;
consider K be Real such that
A14: for f be Function of the carrier of M, the carrier of T
st f in G holds
for x be Element of M holds ||.f.x.|| <= K by A5;
reconsider x0=x as Element of M by A1;
A15: now let y be Point of RNS;
assume y in Fx0; then
consider f be Function of S,T such that
A16: y=f.x & f in H by A6;
reconsider g = f as Function of the carrier of M,the carrier of T by A1;
||.g.x0.|| = ||.y.|| by A16,A8;
hence ||.y.|| <= K by A4, A14, A16;
end;
set r = K+1;
for y be Point of RNS st y in Cl(Fx0)
holds ||.y.|| < r
proof
let y be Point of RNS;
assume y in Cl(Fx0); then
consider seq being sequence of RNS such that
A17: rng seq c= Fx0 & seq is convergent & lim seq = y by NORMSP_3:6;
A18: { y where y is Point of RNS : ||.(0.RNS - y).|| <= K }
is closed Subset of TopSpaceNorm RNS by NORMSP_2:9; then
reconsider B={ y where y is Point of RNS : ||.(0.RNS - y).|| <= K }
as Subset of RNS;
A19: B is closed by NORMSP_2:15,A18;
rng seq c= B
proof
let z be object;
assume A20: z in rng seq; then
reconsider z1=z as Point of RNS;
||.z1.|| <= K by A15, A17, A20; then
||.0.RNS-z1.|| <= K by NORMSP_1:2;
hence z in B;
end; then
y in B by A17,A19; then
ex z be Point of RNS st y=z & ||.(0.RNS - z).|| <= K; then
A21: ||.y.|| <= K by NORMSP_1:2;
K+0 < 1+K by XREAL_1:8;
hence thesis by A21,XXREAL_0:2;
end; then
Cl(Fx0) is compact by A9, REAL_NS3:38; then
ClHx is sequentially_compact by A7, A13, TOPMETR4:18;
hence ((MetricSpaceNorm T)) | Cl(Hx) is compact by A12, TOPMETR4:14;
end;
hence (MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T))
| H is totally_bounded by A1, A2, A4, A5, ASCOLI:16;
end;
theorem Th27:
for M be non empty MetrSpace, S be non empty compact TopSpace,
T be NormedLinearTopSpace
st S = TopSpaceMetr(M) & T is complete & T is finite-dimensional
& dim (T) <> 0
holds
for G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T))
st G = H
holds
Cl(H) is sequentially_compact
iff
G is equibounded & G is equicontinuous
proof
let M be non empty MetrSpace, S be non empty compact TopSpace,
T be NormedLinearTopSpace;
assume that
A1: S = TopSpaceMetr(M) and
A2: T is complete and
A3: T is finite-dimensional & dim (T) <> 0;
let G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T));
assume G = H; then
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T))
| H is totally_bounded
iff
G is equibounded & G is equicontinuous by Th26, A1, A2, A3;
hence thesis by ASCOLI:11, A2;
end;
theorem Th28:
for M be non empty MetrSpace, S be non empty compact TopSpace,
T be NormedLinearTopSpace
st S = TopSpaceMetr(M) & T is complete & T is finite-dimensional
& dim (T) <> 0
holds
for G be Subset of Funcs(the carrier of M, the carrier of T),
F be non empty Subset of R_NormSpace_of_ContinuousFunctions(S,T)
st G = F
holds
Cl(F) is compact
iff
G is equibounded & G is equicontinuous
proof
let M be non empty MetrSpace, S be non empty compact TopSpace,
T be NormedLinearTopSpace;
assume that
A1: S = TopSpaceMetr(M) and
A2: T is complete and
A3: T is finite-dimensional & dim (T) <> 0;
let G be Subset of Funcs(the carrier of M, the carrier of T),
F be non empty Subset of
(R_NormSpace_of_ContinuousFunctions(S,T));
assume A4: G = F;
reconsider H = F as non empty Subset of
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T));
A5: Cl(H) = Cl(F) by ASCOLI:1;
Cl(H) is sequentially_compact
iff
G is equibounded & G is equicontinuous by Th27, A1, A2, A3, A4;
hence thesis by TOPMETR4:18, A5;
end;
theorem Th29:
for RNS be non empty RealNormSpace,T be NormedLinearTopSpace,
X be non empty Subset of RNS,
S be non empty compact strict TopSpace,
G be non empty Subset of R_NormSpace_of_ContinuousFunctions(S,T)
st S is SubSpace of TopSpaceNorm RNS
& the carrier of S = X
& X is compact
& T is complete & T is finite-dimensional & dim T <> 0
&
ex K,D be Real st 0 < K & 0 < D
&
for F be Function of X,T
st F in G
holds
( (for x,y be Point of RNS
st x in X & y in X holds ||.F/.x-F/.y.|| <= D*||.x-y.|| )
&
(for x be Point of RNS st x in X holds ||.F/.x.|| <= K ) )
holds
Cl(G) is compact
proof
let RNS be non empty RealNormSpace, T be NormedLinearTopSpace,
X be non empty Subset of RNS,
S be non empty compact strict TopSpace,
G be non empty Subset of R_NormSpace_of_ContinuousFunctions(S,T);
assume that
A1: S is SubSpace of TopSpaceNorm RNS and
A2: the carrier of S = X and X is compact and
A3: T is complete & T is finite-dimensional & dim T <> 0 and
A4: ex K,D be Real st 0< K & 0 < D &
for F be Function of X,T st F in G
holds
( (for x,y be Point of RNS
st x in X & y in X holds ||.F/.x-F/.y.|| <= D*||.x-y.|| )
&
(for x be Point of RNS st x in X holds ||.F/.x.|| <= K ) );
reconsider Y = X as non empty Subset of MetricSpaceNorm RNS;
reconsider M = (MetricSpaceNorm RNS) | Y as non empty MetrSpace;
A5: [#] S c= [#] TopSpaceNorm RNS
& for P being Subset of S holds
( P in the topology of S
iff ex Q being Subset of TopSpaceNorm RNS
st
Q in the topology of TopSpaceNorm RNS
& P = Q /\ ([#] S) ) by A1, PRE_TOPC:def 4;
A6: the carrier of M = Y by TOPMETR:def 2;
A7: for z be object holds
z in the topology of S
iff
z in (Family_open_set M)
proof
let z be object;
hereby assume A8: z in the topology of S; then
reconsider P = z as Subset of S;
consider Q being Subset of TopSpaceNorm RNS such that
A9: Q in the topology of TopSpaceNorm RNS
& P = Q /\ ([#] S) by A1,PRE_TOPC:def 4, A8;
reconsider P1 = P as Subset of M by A2, TOPMETR:def 2;
for x being Element of M
st x in P1 holds
ex r being Real st r > 0 & Ball (x,r) c= P1
proof
let x be Element of M;
assume x in P1; then
A10: x in Q & x in [#]S by A9, XBOOLE_0:def 4;
reconsider x1=x as Point of MetricSpaceNorm RNS by TOPMETR:8;
consider r being Real such that
A11: r > 0 & Ball (x1,r) c= Q by A9, A10, PCOMPS_1:def 4;
take r;
thus r > 0 by A11;
Ball (x,r) = Ball (x1,r) /\ (the carrier of M) by TOPMETR:9
.= Ball (x1,r) /\ [#]S by A2,TOPMETR:def 2;
hence Ball (x,r) c= P1 by A9, A11, XBOOLE_1:27;
end;
hence z in Family_open_set M by PCOMPS_1:def 4;
end;
assume A13: z in Family_open_set M; then
reconsider P1 = z as Subset of M;
reconsider P = P1 as Subset of S by A2, TOPMETR:def 2;
defpred QQ[object, object] means
ex x be Point of M,
r be Real st $1 = x & $2=r & 0 < r &
Ball(x,r) c= P1;
A14: for z be object st z in P1
ex r be object st r in REAL & QQ[z,r]
proof
let z be object;
assume A15: z in P1; then
reconsider x=z as Point of M;
consider r being Real such that
A16: r > 0 & Ball (x,r) c= P1 by A13, A15, PCOMPS_1:def 4;
thus thesis by A16, XREAL_0:def 1;
end;
consider R being Function of P1, REAL such that
A17: for z being object st z in P1
holds QQ[z,R.z] from FUNCT_2:sch 1(A14);
A18: for z be Point of M st z in P1 holds
Ball(z,R.z) c= P1 & 0 < R.z
proof
let z be Point of M;
assume z in P1; then
QQ[z,R.z] by A17;
hence thesis;
end;
set B = {Ball(x1,R/.x1) where x1 is Point of MetricSpaceNorm RNS
: ex x be Point of M st x=x1 & x in P1};
set Q = union B;
A19: for z be object st z in Q
holds
ex x1 be Point of MetricSpaceNorm RNS
st z in Ball(x1,R/.x1)
& Ball(x1,R/.x1) c= Q & 0 < R/.x1
& ex x be Point of M st x=x1 & x in P1
& Ball(x,R/.x1) c= P1
proof
let z be object;
assume z in Q; then
consider X be set such that
A20: z in X & X in B by TARSKI:def 4;
consider x1 be Point of MetricSpaceNorm RNS such that
A21: X = Ball(x1,R/.x1) & ex x be Point of M st x=x1
& x in P1 by A20;
take x1;
consider x be Point of M such that
A22: x = x1 & x in P1 by A21;
A23: Ball(x,R.x) c= P1 & 0 < R.x by A18, A22;
dom R = P1 by FUNCT_2:def 1; then
R.x = R/.x1 by A22, PARTFUN1:def 6;
hence thesis by A20, A21, A22, A23, ZFMISC_1:74;
end;
for z be object st z in Q
holds z in the carrier of TopSpaceNorm RNS
proof
let z be object;
assume z in Q; then
consider x1 be Point of MetricSpaceNorm RNS such that
A24: z in Ball(x1,R/.x1)
& Ball(x1,R/.x1) c= Q & 0 < R/.x1
& ex x be Point of M st x=x1 & x in P1
& Ball(x,R/.x1) c= P1 by A19;
thus z in the carrier of TopSpaceNorm RNS by A24;
end; then
Q c= the carrier of TopSpaceNorm RNS; then
reconsider Q as Subset of TopSpaceNorm RNS;
for x being Element of MetricSpaceNorm RNS
st x in Q
holds
ex r being Real st r > 0 & Ball (x,r) c= Q
proof
let x be Element of MetricSpaceNorm RNS;
assume x in Q; then
consider x1 be Point of MetricSpaceNorm RNS such that
A25: x in Ball(x1,R/.x1)
& Ball(x1,R/.x1) c= Q & 0 < R/.x1
& ex x be Point of M st x=x1 & x in P1
& Ball(x,R/.x1) c= P1 by A19;
x in { y where y is Element of MetricSpaceNorm RNS
: dist (x1,y) < R/.x1 } by METRIC_1:def 14, A25; then
ex y be Element of MetricSpaceNorm RNS
st x=y & dist (x1,y) < R/.x1; then
A26: 0 < R/.x1 - dist (x1,x) by XREAL_1:50;
set r = (R/.x1 - dist (x1,x)) /2;
take r;
thus 0 < r by A26, XREAL_1:215;
A27: r < R/.x1 - dist (x1,x) by A26, XREAL_1:216;
for z be object st z in Ball(x,r)
holds z in Ball(x1,R/.x1)
proof
let z be object;
assume A28: z in Ball(x,r); then
reconsider w=z as Point of MetricSpaceNorm RNS;
w in { y where y is Element of MetricSpaceNorm RNS
: dist (x,y) < r } by METRIC_1:def 14, A28; then
A29: ex y be Element of MetricSpaceNorm RNS
st w=y & dist (x,y) < r;
A30: dist(x1,w) <= dist(x1,x) + dist(x,w) by METRIC_1:4;
A31: dist(x1,x) + dist(x,w) < dist(x1,x) + r by A29, XREAL_1:8;
dist(x1,x) + r < dist(x1,x) + (R/.x1 - dist (x1,x)) by A27, XREAL_1:8;
then
dist(x1,x) + dist(x,w) < R/.x1 by A31, XXREAL_0:2; then
dist(x1,w) < R/.x1 by A30, XXREAL_0:2; then
w in { y where y is Element of MetricSpaceNorm RNS
: dist (x1,y) < R/.x1 };
hence z in Ball(x1,R/.x1) by METRIC_1:def 14;
end;
hence Ball(x,r) c= Q by A25;
end; then
A32: Q in the topology of TopSpaceNorm RNS by PCOMPS_1:def 4;
for z be object holds
z in P iff z in Q /\ ([#] S)
proof
let z be object;
hereby assume A33: z in P; then
reconsider w = z as Point of M;
A34: Ball(w,R.w) c= P1 & 0 < R.w by A18, A33;
reconsider w1 = w as Point of MetricSpaceNorm RNS by TARSKI:def 3,A6;
A35: Ball(w,R.w) = Ball(w1,R.w) /\ (the carrier of M) by TOPMETR:9
.= Ball(w1,R.w) /\ [#]S by A2, TOPMETR:def 2;
dist(w,w) < R.w by A34,METRIC_1:1; then
w in { y where y is Element of M : dist (w,y) < R.w }; then
A36: w in Ball(w,R.w) by METRIC_1:def 14;
dom R = P1 by FUNCT_2:def 1; then
R.w = R/.w1 by A33, PARTFUN1:def 6; then
Ball(w1,R.w) in B by A33; then
Ball(w1,R.w) c= Q by ZFMISC_1:74; then
Ball(w1,R.w) /\ [#]S c= Q /\ [#]S by XBOOLE_1:27;
hence z in Q /\ ([#] S) by A36, A35;
end;
assume A37: z in Q /\ ([#] S); then
z in Q & z in ([#] S) by XBOOLE_0:def 4; then
consider x1 be Point of MetricSpaceNorm RNS such that
A38: z in Ball(x1,R/.x1)
& Ball(x1,R/.x1) c= Q & 0 < R/.x1
& ex x be Point of M st x=x1 & x in P1
& Ball(x,R/.x1) c= P1 by A19;
consider x be Point of M such that
A39: x=x1 & x in P1
& Ball(x,R/.x1) c= P1 by A38;
Ball(x,R/.x1) = Ball(x1,R/.x1) /\ (the carrier of M) by TOPMETR:9, A39
.= Ball(x1,R/.x1) /\ [#]S by A2, TOPMETR:def 2; then
z in Ball(x,R/.x1) by A37, A38, XBOOLE_0:def 4;
hence z in P by A39;
end;
hence z in the topology of S by A5, A32, TARSKI:2;
end;
for z be object
st z in ContinuousFunctions(S,T)
holds
z in Funcs(the carrier of M, the carrier of T)
proof
let z be object;
assume z in ContinuousFunctions(S,T); then
ex f be Function of the carrier of S,
the carrier of T st z=f & f is continuous;
hence z in Funcs(the carrier of M, the carrier of T) by FUNCT_2:8, A6, A2;
end; then
ContinuousFunctions(S,T) c= Funcs(the carrier of M, the carrier of T); then
reconsider H = G as Subset of Funcs(the carrier of M, the carrier of T)
by XBOOLE_1:1;
S = TopSpaceMetr(M) by A2, A7, A6, TARSKI:2; then
A40: Cl(G) is compact
iff
H is equibounded & H is equicontinuous by Th28, A3;
consider K, D be Real such that
A41: 0< K & 0 < D
& for F be Function of X,T
st F in G
holds
( ( for x,y be Point of RNS
st x in X & y in X holds ||.F/.x-F/.y.|| <= D*||.x-y.|| )
&
( for x be Point of RNS st x in X holds ||.F/.x.|| <= K ) ) by A4;
A42: for f be Function of the carrier of M, the carrier of T
st f in H
holds
for x be Element of M
holds ||.f.x.|| <= K
proof
let f be Function of the carrier of M, the carrier of T;
assume A43: f in H;
reconsider F = f as Function of X, the carrier of T by A6;
let x be Element of M;
reconsider x1 = x as Point of MetricSpaceNorm RNS by TARSKI:def 3, A6;
reconsider x2 = x1 as Point of RNS;
dom F = X by FUNCT_2:def 1; then
F/.x2 = f.x by A6, PARTFUN1:def 6;
hence ||.f.x.|| <= K by A41, A43, A6;
end;
for e be Real st 0 < e
ex d be Real st 0 < d
&
for f be Function of the carrier of M, the carrier of T
st f in H
holds
for x1,x2 be Point of M
st dist(x1,x2) < d holds ||.f.x1-f.x2.|| < e
proof
let e be Real;
assume A45: 0 < e;
set d = e/D;
take d;
thus 0 < d by A41, A45, XREAL_1:139;
let f be Function of the carrier of M, the carrier of T;
assume A46: f in H;
reconsider F = f as Function of X, the carrier of T by A6;
let x, y be Element of M;
assume A47: dist(x,y) < d;
reconsider x1 = x, y1 = y as Point of MetricSpaceNorm RNS
by TARSKI:def 3, A6;
reconsider x2 = x1, y2 = y1 as Point of RNS;
A48: dom F = X by FUNCT_2:def 1; then
A49: F/.x2 = f.x by A6, PARTFUN1:def 6;
F/.y2 = f.y by A6, A48, PARTFUN1:def 6; then
A50: ||.f.x-f.y.|| <= D*||.x2-y2.|| by A6, A41, A46, A49;
dist(x1,y1) < d by A47, TOPMETR:def 1; then
||.x2-y2.|| < d by NORMSP_2:def 1; then
D*||.x2-y2.|| < D * d by XREAL_1:68, A41; then
D*||.x2-y2.|| < e by A41, XCMPLX_1:87;
hence ||.f.x-f.y.|| < e by A50, XXREAL_0:2;
end;
hence thesis by A40, A42;
end;
begin :: High order & Multilayer Perceptron
Lm1:
ex N be FinSequence
st
ex k be FinSequence of NAT
st
len N + 1 = len k
&
for i be Nat st 1<=i & i < len k
holds N.i is Function of REAL-NS (k.i), REAL-NS (k.(i+1))
proof
set k = <*1,1*>;
rng k c= NAT by ORDINAL1:def 12; then
reconsider k as FinSequence of NAT by FINSEQ_1:def 4;
set N=<* id the carrier of REAL-NS 1 *>;
take N,k;
thus len N+1 = 1+1 by FINSEQ_1:39
.= len k by FINSEQ_1:44;
let i be Nat;
assume A1:1<=i & i < len k; then
i < 1 + 1 by FINSEQ_1:44; then
i <=1 by NAT_1:13; then
A2: i=1 by A1, XXREAL_0:1;
thus N.i is Function of REAL-NS (k.i), REAL-NS (k.(i+1))
by A2;
end;
definition
let n be Nat,
k be FinSequence of NAT,
N be FinSequence;
pred N is_Multilayer_perceptron_with k, n means
len N = n & len N + 1 = len k
&
for i be Nat st 1 <= i & i < len k
holds N.i is Function of REAL-NS (k.i), REAL-NS (k.(i+1));
end;
definition
let N be FinSequence;
attr N is Multilayer_perceptron_like means :Def2:
ex k be FinSequence of NAT
st
len N+1 = len k
&
for i be Nat st 1 <= i & i < len k
holds N.i is Function of REAL-NS (k.i), REAL-NS (k.(i+1));
end;
registration
cluster Multilayer_perceptron_like for FinSequence;
existence
proof
consider N be FinSequence such that
A1: ex k be FinSequence of NAT
st
len N + 1 = len k
&
for i be Nat st 1<=i & i < len k
holds N.i is Function of REAL-NS (k.i), REAL-NS (k.(i+1)) by Lm1;
take N;
thus thesis by A1;
end;
end;
definition
mode Multilayer_perceptron is Multilayer_perceptron_like FinSequence;
end;
theorem
for N be Multilayer_perceptron
holds
ex k be FinSequence of NAT
st
len N + 1 = len k
&
for i be Nat st 1<=i & i < len k
holds N.i is Function of REAL-NS (k.i), REAL-NS (k.(i+1)) by Def2;
definition
let n be Nat,
k be FinSequence of NAT,
N be FinSequence;
assume A1: N is_Multilayer_perceptron_with k,n;
assume A2: len N <> 0;
func OutPutFunc(N,k,n) -> Function of REAL-NS (k.1), REAL-NS (k.(n+1))
means :Def3:
ex p be FinSequence
st
len p = len N
&
p.1 = N.1
& ( for i be Nat st 1 <= i & i < len N
holds
ex NN be Function of REAL-NS (k.(i+1)), REAL-NS (k.(i+2)),
pp be Function of REAL-NS (k.1), REAL-NS (k.(i+1))
st NN=N.(i+1) & pp =p.i
&
p.(i+1) = NN*pp )
& it = p.(len N);
existence
proof
set X0 = { the carrier of REAL-NS (k.i)
where i is Nat : 1<=i & i <=len N+1 };
1<=1 & 1 <=len N +1 by NAT_1:11; then
the carrier of REAL-NS (k.1) in X0; then
reconsider X = union X0 as non empty set by TARSKI:def 4;
defpred P1[ Nat, object, object ] means
ex pp be PartFunc of X, X,
NN be Function of REAL-NS (k.($1+1)), REAL-NS (k.($1+2))
st pp=$2 & NN= N.($1+1)
& $3=NN*pp;
A3: for i being Nat st 1 <= i & i < len N holds
for x being Element of PFuncs(X,X)
ex y being Element of PFuncs(X,X)
st P1[i,x,y]
proof
let i be Nat;
assume A4: 1 <= i & i < len N;
let x be Element of PFuncs(X,X);
i+1 <= len N by A4,NAT_1:13; then
A5: 1 <= i+1 & i+1 < len k by A1, NAT_1:13, NAT_1:11; then
N.(i+1) is Function of REAL-NS (k.(i+1)), REAL-NS (k.((i+1)+1)) by A1;
then
reconsider NN=N.(i+1) as Function of REAL-NS (k.(i+1)), REAL-NS (k.(i+2));
the carrier of REAL-NS (k.(i+1)) in X0 by A1, A5; then
A6: the carrier of REAL-NS (k.(i+1)) c= X by ZFMISC_1:74;
i+1 <=i+1+1 by NAT_1:11; then
A7: 1 <= i+2 by NAT_1:11;
i+1 + 1 <= len k by NAT_1:13, A5; then
the carrier of REAL-NS (k.(i+2)) in X0 by A1, A7; then
the carrier of REAL-NS (k.(i+2)) c= X by ZFMISC_1:74; then
dom NN c= X & rng NN c= X by A6; then
NN in PFuncs(X,X) by PARTFUN1:def 3; then
reconsider NN as PartFunc of X, X by PARTFUN1:46;
reconsider pp=x as PartFunc of X, X by PARTFUN1:46;
set y = NN*pp;
reconsider y as Element of PFuncs(X,X) by PARTFUN1:45;
take y;
thus P1[i,x,y];
end;
A9: 1<=len N by NAT_1:14, A2;
A10: 1<= 1 & 1 < len k by A1, A2, NAT_1:13, NAT_1:14; then
reconsider N1=N.1 as Function of REAL-NS (k.1),REAL-NS (k.(1+1)) by A1;
the carrier of REAL-NS (k.1) in X0 by A10, A1; then
A11:the carrier of REAL-NS (k.1) c= X by ZFMISC_1:74;
1+1 <= len k by A10, NAT_1:13; then
the carrier of REAL-NS (k.2) in X0 by A1; then
the carrier of REAL-NS (k.2) c= X by ZFMISC_1:74; then
dom N1 c= X & rng N1 c= X by A11; then
reconsider N1 as Element of PFuncs(X,X) by PARTFUN1:def 3;
consider p being FinSequence of PFuncs(X,X) such that
A14: len p = len N and
A15: p.1 = N1 or len N = 0 and
A16: for i being Nat st 1 <= i & i < len N holds
P1[i,p . i,p . (i + 1)] from RECDEF_1:sch 4(A3);
defpred PP[Nat] means
1 <= $1 & $1 <len N
implies
ex NN be Function of REAL-NS (k.($1+1)), REAL-NS (k.($1+2)),
pp be Function of REAL-NS (k.1), REAL-NS (k.($1+1))
st NN=N.($1+1) & pp =p.$1 & p.($1+1) = NN*pp;
A17:PP[0];
A18:for i be Nat st PP[i] holds PP[i+1]
proof
let i be Nat;
assume A19: PP[i];
assume A20: 1 <= i+1 & i+1 < len N; then
consider pp be PartFunc of X,X,
NN be Function of REAL-NS (k.((i+1)+1)), REAL-NS (k.((i+1)+2))
such that
A21: pp=p.(i+1) & NN=N.((i+1)+1) & p.((i+1)+1)=NN*pp by A16;
per cases;
suppose i=0;
hence thesis by A21,A2,A15;
end;
suppose i <> 0; then
consider NN1 be Function of REAL-NS (k.(i+1)),REAL-NS (k.(i+2)),
pp1 be Function of REAL-NS (k.1),REAL-NS (k.(i+1))
such that
A24: NN1=N.(i+1) & pp1 =p.i &
p.(i+1) = NN1*pp1 by A19, A20, NAT_1:14, NAT_1:13;
thus thesis by A21, A24;
end;
end;
A25:for i be Nat holds PP[i] from NAT_1:sch 2(A17,A18);
p.(len N) is Function of REAL-NS (k.1), REAL-NS (k.(n+1))
proof
per cases;
suppose 1=len N;
hence p.(len N) is Function of REAL-NS (k.1), REAL-NS (k.(n+1))
by A1, A15;
end;
suppose 1 <> len N; then
1 < len N by A9, XXREAL_0:1; then
A27: 1+1 <=len N by NAT_1:13;
reconsider i = len N-1 as Nat by A9, INT_1:5, ORDINAL1:def 12;
A28: 1+1 -1 <= len N -1 by A27, XREAL_1:9;
len N -1 < len N - 0 by XREAL_1:15; then
consider NN be Function of REAL-NS (k.(i+1)),REAL-NS (k.(i+2)),
pp be Function of REAL-NS (k.1),REAL-NS (k.(i+1))
such that
A29: NN=N.(i+1) & pp =p.i & p.(i+1) = NN*pp by A25, A28;
thus p.(len N) is Function of REAL-NS (k.1), REAL-NS (k.(n+1))
by A1, A29;
end;
end; then
reconsider F = p.(len N) as Function of REAL-NS (k.1), REAL-NS (k.(n+1));
take F;
thus thesis by A2, A14, A15, A25;
end;
uniqueness
proof
let F1, F2 be Function of REAL-NS (k.1), REAL-NS (k.(n+1));
given p1 be FinSequence such that
A32: len p1 = len N &
p1.1 = N.1 &
( for i be Nat st 1 <= i & i < len N holds
ex NN be Function of REAL-NS (k.(i+1)),REAL-NS (k.(i+2)),
pp be Function of REAL-NS (k.1),REAL-NS (k.(i+1))
st NN=N.(i+1) & pp=p1.i & p1.(i+1)=NN*pp ) &
F1 = p1.(len N);
given p2 be FinSequence such that
A33: len p2 = len N &
p2.1 = N.1 &
( for i be Nat st 1 <= i & i < len N holds
ex NN be Function of REAL-NS (k.(i+1)),REAL-NS (k.(i+2)),
pp be Function of REAL-NS (k.1),REAL-NS (k.(i+1))
st NN=N.(i+1) & pp=p2.i & p2.(i+1)=NN*pp ) &
F2 = p2.(len N);
defpred P1[Nat,object,object] means
ex NN be Function of REAL-NS (k.($1+1)),REAL-NS (k.($1+2)),
pp be Function of REAL-NS (k.1),REAL-NS (k.($1+1))
st NN=N.($1+1) & pp=$2 & $3 = NN*pp;
A34: len p1 = len N &
(p1.1 = N.1 or len N = 0) &
for i be Nat st 1 <= i & i < len N holds
P1[i,p1.i,p1.(i+1)] by A32;
A35: len p2 = len N &
(p2.1 = N.1 or len N = 0) &
for i be Nat st 1 <= i & i < len N holds
P1[i,p2.i,p2.(i+1)] by A33;
A36: for i being Nat st 1 <= i & i <len N holds
for x, y1, y2 being set st P1[i,x,y1] & P1[i,x,y2] holds
y1 = y2;
p1=p2 from RECDEF_1:sch 7(A36,A34,A35);
hence F1=F2 by A32, A33;
end;
end;
theorem Th31:
for n be Nat,
k be FinSequence of NAT,
N be non empty FinSequence
st n <> 0 & N is_Multilayer_perceptron_with k,(n+1)
holds
ex k1 be FinSequence of NAT,
N1 be non empty FinSequence,
NN be Function of REAL-NS (k.(n+1)), REAL-NS (k.(n+2))
st N1=N|n & k1 = k| (n+1) & NN=N.(n+1) &
N1 is_Multilayer_perceptron_with k1,n &
OutPutFunc(N,k,n+1) = NN* OutPutFunc(N1,k1,n)
proof
let n be Nat;
let k be FinSequence of NAT;
let N be non empty FinSequence;
assume A1: n <>0;
assume A2: N is_Multilayer_perceptron_with k,(n+1); then
A3: len (N|n) = n by FINSEQ_1:59,NAT_1:11;
reconsider N1= N|n as non empty FinSequence by A1;
reconsider k1= k|(n+1) as FinSequence of NAT;
for i be Nat st 1<=i & i < len k1
holds N1.i is Function of REAL-NS (k1.i),REAL-NS (k1.(i+1))
proof
let i be Nat;
assume A4: 1<=i & i < len k1;
A5: len k1 = n+1 by A2, FINSEQ_1:59, NAT_1:11; then
len k1 <= len k by NAT_1:11, A2; then
i < len k by A4, XXREAL_0:2; then
A7: N.i is Function of REAL-NS (k.i), REAL-NS (k.(i+1)) by A2, A4;
i in Seg (n+1) by A4,A5; then
A8: k1.i = k.i by FUNCT_1:49;
A9: i+1 <=len k1 by NAT_1:13, A4;
1 <= i+1 by NAT_1:11; then
i+1 in Seg (n+1) by A5,A9; then
A10: k1.(i+1) = k.(i+1) by FUNCT_1:49;
i <= n by A4, A5, NAT_1:13; then
i in Seg n by A4;
hence thesis by A7,A8,A10,FUNCT_1:49;
end; then
A11: N1 is_Multilayer_perceptron_with k1,n by A2, FINSEQ_1:59, NAT_1:11, A3;
consider p be FinSequence such that
A12: len p = len N &
p.1 = N.1 &
( for i be Nat st 1 <= i & i <len N
holds
ex NN be Function of REAL-NS (k.(i+1)), REAL-NS (k.(i+2)),
pp be Function of REAL-NS (k.1), REAL-NS (k.(i+1))
st NN=N.(i+1) & pp =p.i & p.(i+1) = NN*pp ) &
OutPutFunc(N,k,n+1) = p.(len N) by Def3, A2;
set p1=p|n;
A13: 1 <= n by A1, NAT_1:14; then
A14: 1 in Seg n; then
A15: p1.1 = p.1 by FUNCT_1:49
.= N1.1 by FUNCT_1:49, A14, A12;
A16: len p1 = n by A2, A12, FINSEQ_1:59, NAT_1:11
.= len N1 by A2, FINSEQ_1:59, NAT_1:11;
A17:now let i be Nat;
assume A18: 1 <= i & i < len N1;
A19: len N1 = n by A2, FINSEQ_1:59, NAT_1:11; then
A20: len N1 <= len N by A2, NAT_1:11; then
i < len N by A18, XXREAL_0:2; then
consider NN be Function of REAL-NS (k.(i+1)), REAL-NS (k.(i+2)),
pp be Function of REAL-NS (k.1), REAL-NS (k.(i+1)) such that
A21: NN=N.(i+1) & pp=p.i & p.(i+1) = NN*pp by A18, A12;
i in Seg n by A18, A19; then
A22: p1.i = p.i by FUNCT_1:49;
A23: i+1 <= len N1 by NAT_1:13, A18;
A24: 1 <= i+1 by NAT_1:11; then
A25: i+1 in Seg n by A19, A23; then
A26: N1.(i+1) = N.(i+1) by FUNCT_1:49;
A27: p1.(i+1) = p.(i+1) by FUNCT_1:49, A25;
i+1 <= n+1 by A2, A20, A23, XXREAL_0:2; then
i+1 in Seg (n+1) by A24; then
A28: k1.(i+1) = k.(i+1) by FUNCT_1:49;
1 <= 1 & 1 <=n+1 by NAT_1:11; then
1 in Seg (n+1); then
A29: k1.1 = k.1 by FUNCT_1:49;
A30: (i+1)+1 <= len N1 +1 by A23, XREAL_1:7;
1<=(i+1) +1 by NAT_1:11; then
(i+1) +1 in Seg (n+1) by A19, A30; then
k1.(i+2) = k.(i+2) by FUNCT_1:49;
hence ex NN be Function of REAL-NS (k1.(i+1)), REAL-NS (k1.(i+2)),
pp be Function of REAL-NS (k1.1), REAL-NS (k1.(i+1))
st NN=N1.(i+1) & pp = p1.i &
p1.(i+1) = NN*pp by A21, A22, A26, A27, A28, A29;
end;
A32: n in Seg n by A13;
n+0 < n+1 by XREAL_1:8; then
consider NN be Function of REAL-NS (k.(n+1)), REAL-NS (k.(n+2)),
pp be Function of REAL-NS (k.1), REAL-NS (k.(n+1)) such that
A33: NN=N.(n+1) & pp =p.n & p.(n+1) = NN*pp by A1, A2, A12, NAT_1:14;
A34: pp=p1.(len N1) by A3, A32, A33, FUNCT_1:49;
1 <= 1 & 1 <=n+1 by NAT_1:11; then
1 in Seg (n+1); then
A35: k1.1 = k.1 by FUNCT_1:49;
A36: k1.(n+1) = k.(n+1) by FUNCT_1:49, FINSEQ_1:4;
take k1,N1,NN;
thus N1=N|n & k1=k|(n+1) & NN=N.(n+1) by A33;
thus N1 is_Multilayer_perceptron_with k1,n by A11;
thus OutPutFunc(N,k,n+1) = NN*OutPutFunc(N1,k1,n)
by A11, A15, A16, A17, A33, A34, A35, A36, Def3,A2,A12;
end;
definition
let n be Nat,
k be FinSequence of NAT;
func NEURONS(n,k) -> Subset of
Funcs(the carrier of REAL-NS (k.1),the carrier of REAL-NS (k.(n+1)))
equals
{ F where F is Function of REAL-NS (k.1),REAL-NS (k.(n+1))
: ex N be FinSequence st N is_Multilayer_perceptron_with k,n
& F = OutPutFunc(N,k,n) };
correctness
proof
set X = { F where F is Function of REAL-NS (k.1),REAL-NS (k.(n+1))
: ex N be FinSequence st N is_Multilayer_perceptron_with k,n
& F = OutPutFunc(N,k,n) };
set Y = Funcs(the carrier of REAL-NS (k.1),the carrier of REAL-NS (k.(n+1)));
now let z be object;
assume z in X; then
ex F be Function of REAL-NS (k.1),REAL-NS (k.(n+1))
st z=F & ex N be FinSequence st N is_Multilayer_perceptron_with k,n
& F = OutPutFunc(N,k,n);
hence z in Y by FUNCT_2:8;
end;
hence thesis by TARSKI:def 3;
end;
end;
theorem
for n be Nat,
k be FinSequence of NAT,
S be non empty compact strict TopSpace,
M be non empty SubSpace of MetricSpaceNorm REAL-NS (k.1),
X be non empty Subset of REAL-NS (k.1),
T be NormedLinearTopSpace
st
S = TopSpaceMetr(M)
& the carrier of M = X
& X is compact
& T is complete & T is finite-dimensional
& dim (T) <> 0
& REAL-NS (k.(n+1)) = the NORMSTR of T
holds
for G be Subset of Funcs(the carrier of M, the carrier of T),
F be non empty Subset of R_NormSpace_of_ContinuousFunctions(S,T)
st G = F & G c= { f|X where f is Function of REAL-NS (k.1),
REAL-NS (k.(n+1)): f in NEURONS(n,k) }
holds
Cl(F) is compact
iff
G is equibounded & G is equicontinuous by Th28;
theorem
for n be Nat,
k be FinSequence of NAT,
S be non empty compact strict TopSpace,
X be non empty Subset of REAL-NS (k.1),
T be NormedLinearTopSpace
st
S is SubSpace of TopSpaceNorm REAL-NS (k.1)
& the carrier of S = X
& X is compact
& T is complete & T is finite-dimensional
& dim (T) <> 0
& REAL-NS (k.(n+1)) = the NORMSTR of T
holds
for G be non empty Subset of R_NormSpace_of_ContinuousFunctions(S,T)
st G c= { f|X where f is Function of REAL-NS (k.1),
REAL-NS (k.(n+1)): f in NEURONS(n,k) }
& ex K,D be Real st 0 < K & 0 < D
& for F be Function of X,T st F in G
holds
( ( for x,y be Point of REAL-NS (k.1)
st x in X & y in X holds ||.F/.x-F/.y.|| <= D*||.x-y.|| )
&
( for x be Point of REAL-NS (k.1) st x in X holds ||.F/.x.|| <= K ) )
holds
Cl(G) is compact by Th29;
definition
let X,Y be RealNormSpace;
let F be Function of X,Y;
let D,K be Real;
pred F is_LayerFunc D,K means
( for x,y be Point of X holds ||.F.x-F.y.|| <= D*||.x-y.|| )
&
( for x be Point of X holds ||.F.x.|| <= K );
end;
definition
let n be Nat;
let k be FinSequence of NAT;
let D,K be Real;
let N be FinSequence;
pred N is_LayerFunc_Seq D,K,k,n means
len N = n
& N is_Multilayer_perceptron_with k,n
& for i be Nat st 1<=i & i < len k
holds
ex Ni be Function of REAL-NS (k.i),REAL-NS (k.(i+1))
st N.i = Ni & Ni is_LayerFunc D,K;
end;
theorem Th34:
for D,K be Real st 0<= D & 0<= K
holds
for n be Nat,
k be FinSequence of NAT,
N be non empty FinSequence
st N is_LayerFunc_Seq D,K,k,n
holds OutPutFunc(N,k,n) is_LayerFunc D|^n,K
proof
let D,K be Real;
assume A1: 0<= D & 0<= K;
defpred P[Nat] means
for k be FinSequence of NAT,
N be non empty FinSequence
st len N = $1 & N is_LayerFunc_Seq D,K,k,$1
holds OutPutFunc(N,k,$1) is_LayerFunc D|^$1,K;
A2:P[0];
A3:for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A4: P[n];
let k be FinSequence of NAT,
N be non empty FinSequence;
assume A5: len N = n+1 & N is_LayerFunc_Seq D,K,k,n+1; then
A6:len N = n+1
& N is_Multilayer_perceptron_with k,(n+1)
& for i be Nat st 1<=i & i < len k
holds
ex Ni be Function of REAL-NS (k.i),REAL-NS (k.(i+1))
st N.i = Ni & Ni is_LayerFunc D,K;
per cases;
suppose A7: n=0;
consider p be FinSequence such that
A8: len p = len N
& p.1 = N.1
& ( for i be Nat st 1 <= i & i <len N
holds
ex NN be Function of REAL-NS (k.(i+1)),REAL-NS (k.(i+2)),
pp be Function of REAL-NS (k.1),REAL-NS (k.(i+1))
st NN=N.(i+1) & pp =p.i & p.(i+1) = NN*pp )
& OutPutFunc(N,k,(n+1)) = p.(len N) by Def3,A5;
consider Ni be Function of REAL-NS (k.1),REAL-NS (k.(1+1)) such that
A9: N.1 = Ni & Ni is_LayerFunc D,K by A6,A7;
thus OutPutFunc(N,k,(n+1)) is_LayerFunc D|^(n+1),K by A5,A7,A8,A9;
end;
suppose n<>0; then
consider k1 be FinSequence of NAT,
N1 be non empty FinSequence,
NN be Function of REAL-NS (k.(n+1)),REAL-NS (k.(n+2))
such that
A10: N1=N|n & k1 = k| (n+1) & NN=N.(n+1) &
N1 is_Multilayer_perceptron_with k1,n &
OutPutFunc(N,k,n+1) = NN* OutPutFunc(N1,k1,n) by A5,Th31;
for i be Nat st 1<=i & i < len k1 holds
ex Ni be Function of REAL-NS (k1.i),REAL-NS (k1.(i+1))
st N1.i = Ni & Ni is_LayerFunc D,K
proof
let i be Nat;
assume A11: 1<=i & i < len k1;
len k1 <= len k by A6,A10,NAT_1:11; then
i < len k by A11,XXREAL_0:2; then
consider Ni be Function of REAL-NS (k.i),REAL-NS (k.(i+1)) such that
A13: N.i = Ni & Ni is_LayerFunc D,K by A5,A11;
i in Seg (n+1) by A11,A10; then
A14: k1.i = k.i by A10,FUNCT_1:49;
A15: i+1 <=len k1 by NAT_1:13,A11;
1 <= i+1 by NAT_1:11; then
i+1 in Seg (n+1) by A10,A15; then
A16: k1.(i+1) = k.(i+1) by A10,FUNCT_1:49;
i <= n by A11,A10,NAT_1:13; then
i in Seg n by A11;
hence thesis by A10,A13,A14,A16,FUNCT_1:49;
end; then
N1 is_LayerFunc_Seq D,K,k1,n by A10; then
A17: OutPutFunc(N1,k1,n) is_LayerFunc D|^n,K by A4;
1 <= 1 & 1 <=n+1 by NAT_1:11; then
1 in Seg (n+1); then
A18: k1.1 = k.1 by A10,FUNCT_1:49;
A19: k1.(n+1) = k.(n+1) by A10,FUNCT_1:49,FINSEQ_1:4;
(n+1) + 0 < (n+1) + 1 by XREAL_1:8; then
A20: ex Ni be Function of REAL-NS (k.(n+1)),REAL-NS (k.((n+1)+1))
st N.(n+1) = Ni & Ni is_LayerFunc D,K by A6, NAT_1:11;
set F = OutPutFunc(N,k,n+1);
A21: for x,y be Point of REAL-NS (k.1)
holds ||.F.x-F.y.|| <= D|^(n+1)*||.x-y.||
proof
let x,y be Point of REAL-NS (k.1);
A22: F.x = NN.(OutPutFunc(N1,k1,n).x) by FUNCT_2:15,A10,A18;
A23: F.y = NN.(OutPutFunc(N1,k1,n).y) by FUNCT_2:15,A10,A18;
reconsider x2=x,y2=y as Point of REAL-NS (k1.1) by A18;
reconsider x1=OutPutFunc(N1,k1,n).x, y1=OutPutFunc(N1,k1,n).y
as Point of REAL-NS (k.(n+1)) by A18,A19,FUNCT_2:5;
A24: ||.F.x-F.y.|| <= D*||.x1-y1.|| by A10,A20,A22,A23;
D*||.x1-y1.|| <= D*((D|^n)* ||.x2-y2.||) by A1,A17,A19,XREAL_1:64;
then
D*||.x1-y1.|| <= (D*(D|^n))* ||.x2-y2.||; then
D*||.x1-y1.|| <= (D|^(n+1))* ||.x2-y2.|| by NEWTON:6;
hence thesis by A18,A24,XXREAL_0:2;
end;
for x be Point of REAL-NS (k.1) holds ||.F.x.|| <= K
proof
let x be Point of REAL-NS (k.1);
reconsider x1=OutPutFunc(N1,k1,n).x
as Point of REAL-NS (k.(n+1)) by A18,A19,FUNCT_2:5;
||.NN.x1.|| <= K by A10,A20;
hence ||.F.x.|| <= K by FUNCT_2:15,A10,A18;
end;
hence OutPutFunc(N,k,n+1) is_LayerFunc D|^(n+1),K by A21;
end;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem
for n be Nat,
k be FinSequence of NAT,
S be non empty compact strict TopSpace,
X be non empty Subset of REAL-NS (k.1),
T be NormedLinearTopSpace
st
S is SubSpace of TopSpaceNorm REAL-NS (k.1)
& the carrier of S = X
& X is compact
& T is complete & T is finite-dimensional
& dim (T) <> 0
& REAL-NS (k.(n+1)) = the NORMSTR of T
holds
for G be non empty Subset of R_NormSpace_of_ContinuousFunctions(S,T),
D,K be Real
st 0 < D & 0 < K
& G c= { F|X where F is Function of REAL-NS (k.1),REAL-NS (k.(n+1))
: ex N be non empty FinSequence
st N is_LayerFunc_Seq D,K,k,n
& F = OutPutFunc(N,k,n) }
holds
Cl(G) is compact
proof
let n be Nat,
k be FinSequence of NAT,
S be non empty compact strict TopSpace,
X be non empty Subset of REAL-NS (k.1),
T be NormedLinearTopSpace;
assume A1:
S is SubSpace of TopSpaceNorm REAL-NS (k.1)
& the carrier of S = X
& X is compact
& T is complete & T is finite-dimensional
& dim (T) <> 0
& REAL-NS (k.(n+1)) = the NORMSTR of T;
let G be non empty Subset of R_NormSpace_of_ContinuousFunctions(S,T),
D,K be Real;
assume A2: 0 < D & 0 < K
& G c= { F|X where F is Function of REAL-NS (k.1),REAL-NS (k.(n+1))
: ex N be non empty FinSequence
st N is_LayerFunc_Seq D,K,k,n
& F = OutPutFunc(N,k,n) };
set K1= K+1;
set D1 = D|^n +1;
A3:0 <= D|^n by A2,POWER:3;
for F be Function of X,T st F in G
holds
( ( for x,y be Point of REAL-NS (k.1)
st x in X & y in X holds ||.F/.x-F/.y.|| <= D1*||.x-y.|| )
&
( for x be Point of REAL-NS (k.1) st x in X holds ||.F/.x.|| <= K1 ) )
proof
let F be Function of X,T;
assume F in G; then
F in { F|X where F is Function of REAL-NS (k.1),REAL-NS (k.(n+1))
: ex N be non empty FinSequence
st N is_LayerFunc_Seq D,K,k,n
& F = OutPutFunc(N,k,n) } by A2; then
consider F0 be Function of REAL-NS (k.1),REAL-NS (k.(n+1)) such that
A4: F =F0 | X
& ex N be non empty FinSequence
st N is_LayerFunc_Seq D,K,k,n
& F0 = OutPutFunc(N,k,n);
consider N be non empty FinSequence such that
A5: N is_LayerFunc_Seq D,K,k,n
& F0 = OutPutFunc(N,k,n) by A4;
A6: F0 is_LayerFunc D|^n,K by Th34,A5,A2;
A7: dom F = X by FUNCT_2:def 1;
thus for x,y be Point of REAL-NS (k.1)
st x in X & y in X holds ||.F/.x-F/.y.|| <= D1*||.x-y.||
proof
let x,y be Point of REAL-NS (k.1);
assume A8: x in X & y in X; then
A9: F/.x = F.x by A7,PARTFUN1:def 6
.= F0.x by A4,A8,FUNCT_1:49;
A10: F/.y = F.y by A7,A8,PARTFUN1:def 6
.= F0.y by A4,A8,FUNCT_1:49;
the RLSStruct of REAL-NS (k.(n+1)) = the RLSStruct of T by A1;
then ||.F0.x-F0.y.|| = ||.F/.x-F/.y.|| by A1,A9,A10,Th5; then
A12: ||.F/.x-F/.y.|| <= (D|^n)*||.x-y.|| by A6;
(D|^n) + 0 < (D|^n) +1 by XREAL_1:8; then
(D|^n)*||.x-y.|| <= D1*||.x-y.|| by XREAL_1:64;
hence ||.F/.x-F/.y.|| <= D1*||.x-y.|| by A12,XXREAL_0:2;
end;
let x be Point of REAL-NS (k.1);
assume A13: x in X; then
F/.x = F.x by A7,PARTFUN1:def 6
.= F0.x by A4,A13,FUNCT_1:49; then
||.F0.x.|| = ||.F/.x.|| by A1; then
A15: ||.F/.x.|| <= K by A6;
K + 0 < K +1 by XREAL_1:8;
hence ||.F/.x.|| <= K1 by A15,XXREAL_0:2;
end;
hence Cl(G) is compact by Th29,A1,A3,A2;
end;