let D, K be Real; ( 0 <= D & 0 <= K implies for n being Nat
for k being FinSequence of NAT
for N being non empty FinSequence st N is_LayerFunc_Seq D,K,k,n holds
OutPutFunc (N,k,n) is_LayerFunc D |^ n,K )
assume A1:
( 0 <= D & 0 <= K )
; for n being Nat
for k being FinSequence of NAT
for N being non empty FinSequence st N is_LayerFunc_Seq D,K,k,n holds
OutPutFunc (N,k,n) is_LayerFunc D |^ n,K
defpred S1[ Nat] means for k being FinSequence of NAT
for N being 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:
S1[ 0 ]
;
A3:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A4:
S1[
n]
;
S1[n + 1]
let k be
FinSequence of
NAT ;
for N being non empty FinSequence st len N = n + 1 & N is_LayerFunc_Seq D,K,k,n + 1 holds
OutPutFunc (N,k,(n + 1)) is_LayerFunc D |^ (n + 1),Klet N be non
empty FinSequence;
( len N = n + 1 & N is_LayerFunc_Seq D,K,k,n + 1 implies OutPutFunc (N,k,(n + 1)) is_LayerFunc D |^ (n + 1),K )
assume A5:
(
len N = n + 1 &
N is_LayerFunc_Seq D,
K,
k,
n + 1 )
;
OutPutFunc (N,k,(n + 1)) is_LayerFunc D |^ (n + 1),K
then A6:
(
len N = n + 1 &
N is_Multilayer_perceptron_with k,
n + 1 & ( for
i being
Nat st 1
<= i &
i < len k holds
ex
Ni being
Function of
(REAL-NS (k . i)),
(REAL-NS (k . (i + 1))) st
(
N . i = Ni &
Ni is_LayerFunc D,
K ) ) )
;
per cases
( n = 0 or n <> 0 )
;
suppose A7:
n = 0
;
OutPutFunc (N,k,(n + 1)) is_LayerFunc D |^ (n + 1),Kconsider p being
FinSequence such that A8:
(
len p = len N &
p . 1
= N . 1 & ( for
i being
Nat st 1
<= i &
i < len N holds
ex
NN being
Function of
(REAL-NS (k . (i + 1))),
(REAL-NS (k . (i + 2))) ex
pp being
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 being
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;
verum end; suppose
n <> 0
;
OutPutFunc (N,k,(n + 1)) is_LayerFunc D |^ (n + 1),Kthen consider k1 being
FinSequence of
NAT ,
N1 being non
empty FinSequence,
NN being
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 being
Nat st 1
<= i &
i < len k1 holds
ex
Ni being
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;
( 1 <= i & i < len k1 implies ex Ni being Function of (REAL-NS (k1 . i)),(REAL-NS (k1 . (i + 1))) st
( N1 . i = Ni & Ni is_LayerFunc D,K ) )
assume A11:
( 1
<= i &
i < len k1 )
;
ex Ni being Function of (REAL-NS (k1 . i)),(REAL-NS (k1 . (i + 1))) st
( N1 . i = Ni & Ni is_LayerFunc D,K )
len k1 <= len k
by A6, A10, NAT_1:11;
then
i < len k
by A11, XXREAL_0:2;
then consider Ni being
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
ex
Ni being
Function of
(REAL-NS (k1 . i)),
(REAL-NS (k1 . (i + 1))) st
(
N1 . i = Ni &
Ni is_LayerFunc D,
K )
by A10, A13, A14, A16, FUNCT_1:49;
verum
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 being
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 being
Point of
(REAL-NS (k . 1)) holds
||.(((OutPutFunc (N,k,(n + 1))) . x) - ((OutPutFunc (N,k,(n + 1))) . y)).|| <= (D |^ (n + 1)) * ||.(x - y).||
proof
let x,
y be
Point of
(REAL-NS (k . 1));
||.(((OutPutFunc (N,k,(n + 1))) . x) - ((OutPutFunc (N,k,(n + 1))) . y)).|| <= (D |^ (n + 1)) * ||.(x - y).||
A22:
(OutPutFunc (N,k,(n + 1))) . x = NN . ((OutPutFunc (N1,k1,n)) . x)
by FUNCT_2:15, A10, A18;
A23:
(OutPutFunc (N,k,(n + 1))) . 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:
||.(((OutPutFunc (N,k,(n + 1))) . x) - ((OutPutFunc (N,k,(n + 1))) . 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
||.(((OutPutFunc (N,k,(n + 1))) . x) - ((OutPutFunc (N,k,(n + 1))) . y)).|| <= (D |^ (n + 1)) * ||.(x - y).||
by A18, A24, XXREAL_0:2;
verum
end;
for
x being
Point of
(REAL-NS (k . 1)) holds
||.((OutPutFunc (N,k,(n + 1))) . x).|| <= K
proof
let x be
Point of
(REAL-NS (k . 1));
||.((OutPutFunc (N,k,(n + 1))) . x).|| <= K
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
||.((OutPutFunc (N,k,(n + 1))) . x).|| <= K
by FUNCT_2:15, A10, A18;
verum
end; hence
OutPutFunc (
N,
k,
(n + 1))
is_LayerFunc D |^ (n + 1),
K
by A21;
verum end;
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A2, A3);
hence
for n being Nat
for k being FinSequence of NAT
for N being non empty FinSequence st N is_LayerFunc_Seq D,K,k,n holds
OutPutFunc (N,k,n) is_LayerFunc D |^ n,K
; verum