let X be RealNormSpace; for f being sequence of (DualSp X)
for x being sequence of X st ||.f.|| is bounded holds
ex M being sequence of (DualSp X) st
( M is subsequence of f & ( for k being Nat holds M # (x . k) is convergent ) )
let f be sequence of (DualSp X); for x being sequence of X st ||.f.|| is bounded holds
ex M being sequence of (DualSp X) st
( M is subsequence of f & ( for k being Nat holds M # (x . k) is convergent ) )
let x be sequence of X; ( ||.f.|| is bounded implies ex M being sequence of (DualSp X) st
( M is subsequence of f & ( for k being Nat holds M # (x . k) is convergent ) ) )
assume
||.f.|| is bounded
; ex M being sequence of (DualSp X) st
( M is subsequence of f & ( for k being Nat holds M # (x . k) is convergent ) )
then consider F being sequence of (Funcs (NAT, the carrier of (DualSp X))), N being sequence of (Funcs (NAT,NAT)) such that
A0:
( F . 0 is subsequence of f & (F . 0) # (x . 0) is convergent & N . 0 is V132() sequence of NAT & F . 0 = f * (N . 0) & ( for k being Nat holds F . (k + 1) is subsequence of F . k ) & ( for k being Nat holds (F . (k + 1)) # (x . (k + 1)) is convergent ) & ( for k being Nat holds (F . (k + 1)) # (x . (k + 1)) is subsequence of (F . k) # (x . (k + 1)) ) & ( for k being Nat holds N . (k + 1) is V132() sequence of NAT ) & ( for k being Nat holds F . (k + 1) = (F . k) * (N . (k + 1)) ) )
by Lm814C;
deffunc H1( Element of NAT ) -> Element of the carrier of (DualSp X) = (F . $1) . $1;
consider M being Function of NAT,(DualSp X) such that
A1:
for k being Element of NAT holds M . k = H1(k)
from FUNCT_2:sch 4();
reconsider M = M as sequence of (DualSp X) ;
A2:
for k being Nat holds M . k = (F . k) . k
set D = Funcs (NAT,NAT);
reconsider A = N . 0 as Element of Funcs (NAT,NAT) by FUNCT_2:8;
defpred S1[ Nat, sequence of NAT, sequence of NAT] means $3 = $2 * (N . ($1 + 1));
P1:
for n being Nat
for x being Element of Funcs (NAT,NAT) ex y being Element of Funcs (NAT,NAT) st S1[n,x,y]
proof
let n be
Nat;
for x being Element of Funcs (NAT,NAT) ex y being Element of Funcs (NAT,NAT) st S1[n,x,y]let x be
Element of
Funcs (
NAT,
NAT);
ex y being Element of Funcs (NAT,NAT) st S1[n,x,y]
reconsider y =
x * (N . (n + 1)) as
Element of
Funcs (
NAT,
NAT)
by FUNCT_2:8;
take
y
;
S1[n,x,y]
thus
y = x * (N . (n + 1))
;
verum
end;
consider J being sequence of (Funcs (NAT,NAT)) such that
P2:
( J . 0 = A & ( for n being Nat holds S1[n,J . n,J . (n + 1)] ) )
from RECDEF_1:sch 2(P1);
defpred S2[ Nat] means J . $1 is V132() sequence of NAT;
Q0:
S2[ 0 ]
by P2, A0;
Q1:
for n being Nat st S2[n] holds
S2[n + 1]
Q2:
for n being Nat holds S2[n]
from NAT_1:sch 2(Q0, Q1);
defpred S3[ Nat] means F . $1 = f * (J . $1);
Q0:
S3[ 0 ]
by P2, A0;
Q1:
for n being Nat st S3[n] holds
S3[n + 1]
proof
let n be
Nat;
( S3[n] implies S3[n + 1] )
assume X2:
S3[
n]
;
S3[n + 1]
F . (n + 1) =
(F . n) * (N . (n + 1))
by A0
.=
f * ((J . n) * (N . (n + 1)))
by X2, RELAT_1:36
;
hence
F . (n + 1) = f * (J . (n + 1))
by P2;
verum
end;
A41:
for n being Nat holds S3[n]
from NAT_1:sch 2(Q0, Q1);
deffunc H2( Element of NAT ) -> Element of NAT = (J . $1) . $1;
consider L being Function of NAT,NAT such that
A5:
for k being Element of NAT holds L . k = H2(k)
from FUNCT_2:sch 4();
reconsider L = L as sequence of NAT ;
A6:
for k being Nat holds L . k = (J . k) . k
reconsider L0 = L as Real_Sequence by FUNCT_2:7, NUMBERS:19;
for k being Nat holds L0 . k < L0 . (k + 1)
then
L0 is V132()
;
then reconsider L = L as V132() sequence of NAT ;
for k being Nat holds M . k = (f * L) . k
then A71:
M = f * L
;
for k being Nat holds M # (x . k) is convergent
proof
let k be
Nat;
M # (x . k) is convergent
Q1:
(F . k) # (x . k) is
convergent
A0X:
for
k being
Nat holds
N . k is
V132()
sequence of
NAT
defpred S4[
Nat,
sequence of
NAT]
means for
i being
Nat holds $2
. i = ((N . (k + $1)) . (k + i)) - k;
P11:
for
n being
Element of
NAT ex
y being
Element of
Funcs (
NAT,
NAT) st
S4[
n,
y]
consider Nk being
Function of
NAT,
(Funcs (NAT,NAT)) such that P12:
for
n being
Element of
NAT holds
S4[
n,
Nk . n]
from FUNCT_2:sch 3(P11);
P13:
for
n being
Element of
NAT holds
Nk . n is
V132()
sequence of
NAT
A0k:
for
n being
Nat holds
(F . (k + (n + 1))) ^\ k = ((F . (k + n)) ^\ k) * (Nk . (n + 1))
proof
let n be
Nat;
(F . (k + (n + 1))) ^\ k = ((F . (k + n)) ^\ k) * (Nk . (n + 1))
XX1:
F . ((k + 1) + n) = (F . (k + n)) * (N . ((k + n) + 1))
by A0;
for
i being
Nat holds
(((F . (k + n)) ^\ k) * (Nk . (n + 1))) . i = (((F . (k + n)) * (N . ((k + n) + 1))) ^\ k) . i
hence
(F . (k + (n + 1))) ^\ k = ((F . (k + n)) ^\ k) * (Nk . (n + 1))
by XX1;
verum
end;
reconsider Ak =
id NAT as
Element of
Funcs (
NAT,
NAT)
by FUNCT_2:8;
defpred S5[
Nat,
sequence of
NAT,
sequence of
NAT]
means $3
= $2
* (Nk . ($1 + 1));
P14:
for
n being
Nat for
x being
Element of
Funcs (
NAT,
NAT) ex
y being
Element of
Funcs (
NAT,
NAT) st
S5[
n,
x,
y]
proof
let n be
Nat;
for x being Element of Funcs (NAT,NAT) ex y being Element of Funcs (NAT,NAT) st S5[n,x,y]let x be
Element of
Funcs (
NAT,
NAT);
ex y being Element of Funcs (NAT,NAT) st S5[n,x,y]
reconsider y =
x * (Nk . (n + 1)) as
Element of
Funcs (
NAT,
NAT)
by FUNCT_2:8;
take
y
;
S5[n,x,y]
thus
y = x * (Nk . (n + 1))
;
verum
end;
consider Jk being
sequence of
(Funcs (NAT,NAT)) such that P15:
(
Jk . 0 = Ak & ( for
n being
Nat holds
S5[
n,
Jk . n,
Jk . (n + 1)] ) )
from RECDEF_1:sch 2(P14);
defpred S6[
Nat]
means Jk . $1 is
V132()
sequence of
NAT;
QJ0:
S6[
0 ]
by P15;
QJ1:
for
n being
Nat st
S6[
n] holds
S6[
n + 1]
AJ32:
for
n being
Nat holds
S6[
n]
from NAT_1:sch 2(QJ0, QJ1);
defpred S7[
Nat]
means (F . (k + $1)) ^\ k = ((F . k) ^\ k) * (Jk . $1);
QJ0:
S7[
0 ]
by P15, FUNCT_2:17;
QJ1:
for
n being
Nat st
S7[
n] holds
S7[
n + 1]
proof
let n be
Nat;
( S7[n] implies S7[n + 1] )
assume X2:
S7[
n]
;
S7[n + 1]
thus (F . (k + (n + 1))) ^\ k =
((F . (k + n)) ^\ k) * (Nk . (n + 1))
by A0k
.=
((F . k) ^\ k) * ((Jk . n) * (Nk . (n + 1)))
by X2, RELAT_1:36
.=
((F . k) ^\ k) * (Jk . (n + 1))
by P15
;
verum
end;
BJ4:
for
n being
Nat holds
S7[
n]
from NAT_1:sch 2(QJ0, QJ1);
deffunc H3(
Element of
NAT )
-> Element of
NAT =
(Jk . $1) . $1;
consider Lk being
Function of
NAT,
NAT such that AJ5:
for
n being
Element of
NAT holds
Lk . n = H3(
n)
from FUNCT_2:sch 4();
reconsider Lk =
Lk as
sequence of
NAT ;
AJ6:
for
k being
Nat holds
Lk . k = (Jk . k) . k
reconsider L0k =
Lk as
Real_Sequence by FUNCT_2:7, NUMBERS:19;
for
k being
Nat holds
L0k . k < L0k . (k + 1)
then
L0k is
V132()
;
then reconsider Lk =
Lk as
V132()
sequence of
NAT ;
for
n being
Nat holds
(M ^\ k) . n = (((F . k) ^\ k) * Lk) . n
then P11:
M ^\ k = ((F . k) ^\ k) * Lk
;
Q12:
for
n being
Nat holds
((M ^\ k) # (x . k)) . n = ((M # (x . k)) ^\ k) . n
for
n being
Nat holds
((((F . k) ^\ k) * Lk) # (x . k)) . n = ((((F . k) ^\ k) # (x . k)) * Lk) . n
then
(((F . k) ^\ k) * Lk) # (x . k) = (((F . k) ^\ k) # (x . k)) * Lk
;
then Q2:
(M # (x . k)) ^\ k = (((F . k) ^\ k) # (x . k)) * Lk
by P11, Q12;
for
n being
Nat holds
(((F . k) # (x . k)) ^\ k) . n = (((F . k) ^\ k) # (x . k)) . n
then
((F . k) # (x . k)) ^\ k = ((F . k) ^\ k) # (x . k)
;
then
(M # (x . k)) ^\ k is
convergent
by Q1, Q2, SEQ_4:16;
hence
M # (x . k) is
convergent
by SEQ_4:21;
verum
end;
hence
ex M being sequence of (DualSp X) st
( M is subsequence of f & ( for k being Nat holds M # (x . k) is convergent ) )
by A71; verum