defpred S1[ Nat, object , object ] means ex K being Lipschitzian LinearOperator of (diff_SP (($1 + 1),E,F)),(diff_SP (($1 + 1),E,G)) ex M being Lipschitzian LinearOperator of (diff_SP ($1,E,F)),(diff_SP ($1,E,G)) st
( $3 = K & In ($2,(R_NormSpace_of_BoundedLinearOperators ((diff_SP ($1,E,F)),(diff_SP ($1,E,G))))) = M & ( for V being Lipschitzian LinearOperator of E,(diff_SP ($1,E,F)) holds K . V = M * V ) );
A1:
for i being Nat
for x being set ex y being set st S1[i,x,y]
proof
let i be
Nat;
for x being set ex y being set st S1[i,x,y]let x be
set ;
ex y being set st S1[i,x,y]
set N =
In (
x,
(R_NormSpace_of_BoundedLinearOperators ((diff_SP (i,E,F)),(diff_SP (i,E,G)))));
reconsider M =
In (
x,
(R_NormSpace_of_BoundedLinearOperators ((diff_SP (i,E,F)),(diff_SP (i,E,G))))) as
Lipschitzian LinearOperator of
(diff_SP (i,E,F)),
(diff_SP (i,E,G)) by LOPBAN_1:def 9;
defpred S2[
object ,
object ]
means ex
V being
Lipschitzian LinearOperator of
E,
(diff_SP (i,E,F)) st
( $1
= V & $2
= M * V );
A2:
for
x being
object st
x in the
carrier of
(diff_SP ((i + 1),E,F)) holds
ex
y being
object st
(
y in the
carrier of
(diff_SP ((i + 1),E,G)) &
S2[
x,
y] )
proof
let x be
object ;
( x in the carrier of (diff_SP ((i + 1),E,F)) implies ex y being object st
( y in the carrier of (diff_SP ((i + 1),E,G)) & S2[x,y] ) )
assume
x in the
carrier of
(diff_SP ((i + 1),E,F))
;
ex y being object st
( y in the carrier of (diff_SP ((i + 1),E,G)) & S2[x,y] )
then
x in the
carrier of
(R_NormSpace_of_BoundedLinearOperators (E,(diff_SP (i,E,F))))
by NDIFF_6:10;
then reconsider V =
x as
Lipschitzian LinearOperator of
E,
(diff_SP (i,E,F)) by LOPBAN_1:def 9;
take y =
M * V;
( y in the carrier of (diff_SP ((i + 1),E,G)) & S2[x,y] )
M * V is
Lipschitzian LinearOperator of
E,
(diff_SP (i,E,G))
by LOPBAN_2:2;
then
M * V in the
carrier of
(R_NormSpace_of_BoundedLinearOperators (E,(diff_SP (i,E,G))))
by LOPBAN_1:def 9;
hence
(
y in the
carrier of
(diff_SP ((i + 1),E,G)) &
S2[
x,
y] )
by NDIFF_6:10;
verum
end;
consider K being
Function of the
carrier of
(diff_SP ((i + 1),E,F)), the
carrier of
(diff_SP ((i + 1),E,G)) such that A3:
for
x being
object st
x in the
carrier of
(diff_SP ((i + 1),E,F)) holds
S2[
x,
K . x]
from FUNCT_2:sch 1(A2);
A4:
diff_SP (
(i + 1),
E,
F)
= R_NormSpace_of_BoundedLinearOperators (
E,
(diff_SP (i,E,F)))
by NDIFF_6:10;
A5:
diff_SP (
(i + 1),
E,
G)
= R_NormSpace_of_BoundedLinearOperators (
E,
(diff_SP (i,E,G)))
by NDIFF_6:10;
reconsider MP =
M as
Point of
(R_NormSpace_of_BoundedLinearOperators ((diff_SP (i,E,F)),(diff_SP (i,E,G)))) ;
for
x,
y being
Element of
(diff_SP ((i + 1),E,F)) holds
K . (x + y) = (K . x) + (K . y)
proof
let x,
y be
Element of
(diff_SP ((i + 1),E,F));
K . (x + y) = (K . x) + (K . y)
consider V1 being
Lipschitzian LinearOperator of
E,
(diff_SP (i,E,F)) such that A6:
(
x = V1 &
K . x = M * V1 )
by A3;
consider V2 being
Lipschitzian LinearOperator of
E,
(diff_SP (i,E,F)) such that A7:
(
y = V2 &
K . y = M * V2 )
by A3;
consider V3 being
Lipschitzian LinearOperator of
E,
(diff_SP (i,E,F)) such that A8:
(
x + y = V3 &
K . (x + y) = M * V3 )
by A3;
reconsider V1P =
V1 as
Point of
(R_NormSpace_of_BoundedLinearOperators (E,(diff_SP (i,E,F)))) by LOPBAN_1:def 9;
reconsider V2P =
V2 as
Point of
(R_NormSpace_of_BoundedLinearOperators (E,(diff_SP (i,E,F)))) by LOPBAN_1:def 9;
A9:
x + y =
V1P + V2P
by A6, A7, NDIFF_6:10
.=
V1 + V2
by Th11
;
A10:
M * V1 is
Lipschitzian LinearOperator of
E,
(diff_SP (i,E,G))
by A5, A6, LOPBAN_1:def 9;
A11:
M * V2 is
Lipschitzian LinearOperator of
E,
(diff_SP (i,E,G))
by A5, A7, LOPBAN_1:def 9;
thus K . (x + y) =
(M * V1) + (M * V2)
by A8, A9, Th14
.=
(K . x) + (K . y)
by A5, A6, A7, A10, A11, Th11
;
verum
end;
then A12:
K is
additive
;
for
x being
VECTOR of
(diff_SP ((i + 1),E,F)) for
a being
Real holds
K . (a * x) = a * (K . x)
proof
let x be
VECTOR of
(diff_SP ((i + 1),E,F));
for a being Real holds K . (a * x) = a * (K . x)let a be
Real;
K . (a * x) = a * (K . x)
consider V1 being
Lipschitzian LinearOperator of
E,
(diff_SP (i,E,F)) such that A13:
(
x = V1 &
K . x = M * V1 )
by A3;
consider V2 being
Lipschitzian LinearOperator of
E,
(diff_SP (i,E,F)) such that A14:
(
a * x = V2 &
K . (a * x) = M * V2 )
by A3;
reconsider V1P =
V1 as
Point of
(R_NormSpace_of_BoundedLinearOperators (E,(diff_SP (i,E,F)))) by LOPBAN_1:def 9;
A15:
a * x =
a * V1P
by A13, NDIFF_6:10
.=
a (#) V1
by LOPBAN13:30
;
A16:
M * V1 is
Lipschitzian LinearOperator of
E,
(diff_SP (i,E,G))
by A5, A13, LOPBAN_1:def 9;
thus K . (a * x) =
a (#) (M * V1)
by A14, A15, Th14
.=
a * (K . x)
by A5, A13, A16, LOPBAN13:30
;
verum
end;
then reconsider K =
K as
LinearOperator of
(diff_SP ((i + 1),E,F)),
(diff_SP ((i + 1),E,G)) by A12, LOPBAN_1:def 5;
for
x being
VECTOR of
(diff_SP ((i + 1),E,F)) holds
||.(K . x).|| <= ||.MP.|| * ||.x.||
proof
let x be
VECTOR of
(diff_SP ((i + 1),E,F));
||.(K . x).|| <= ||.MP.|| * ||.x.||
consider V1 being
Lipschitzian LinearOperator of
E,
(diff_SP (i,E,F)) such that A17:
(
x = V1 &
K . x = M * V1 )
by A3;
reconsider V1P =
V1 as
Point of
(R_NormSpace_of_BoundedLinearOperators (E,(diff_SP (i,E,F)))) by LOPBAN_1:def 9;
(BoundedLinearOperatorsNorm (E,(diff_SP (i,E,F)))) . V1 =
||.V1P.||
.=
||.x.||
by A17, NDIFF_6:10
;
hence
||.(K . x).|| <= ||.MP.|| * ||.x.||
by A5, A17, LOPBAN_2:2;
verum
end;
then reconsider K =
K as
Lipschitzian LinearOperator of
(diff_SP ((i + 1),E,F)),
(diff_SP ((i + 1),E,G)) by NORMSP_1:4, LOPBAN_1:def 8;
A18:
for
V being
Lipschitzian LinearOperator of
E,
(diff_SP (i,E,F)) holds
K . V = M * V
take
K
;
S1[i,x,K]
thus
S1[
i,
x,
K]
by A18;
verum
end;
consider f being Function such that
A20:
( dom f = NAT & f . 0 = L & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) )
from RECDEF_1:sch 1(A1);
take
f
; ( dom f = NAT & f . 0 = L & ( for i being Nat ex K being Lipschitzian LinearOperator of (diff_SP ((i + 1),E,F)),(diff_SP ((i + 1),E,G)) ex M being Lipschitzian LinearOperator of (diff_SP (i,E,F)),(diff_SP (i,E,G)) st
( f . (i + 1) = K & In ((f . i),(R_NormSpace_of_BoundedLinearOperators ((diff_SP (i,E,F)),(diff_SP (i,E,G))))) = M & ( for V being Lipschitzian LinearOperator of E,(diff_SP (i,E,F)) holds K . V = M * V ) ) ) )
thus
( dom f = NAT & f . 0 = L & ( for i being Nat ex K being Lipschitzian LinearOperator of (diff_SP ((i + 1),E,F)),(diff_SP ((i + 1),E,G)) ex M being Lipschitzian LinearOperator of (diff_SP (i,E,F)),(diff_SP (i,E,G)) st
( f . (i + 1) = K & In ((f . i),(R_NormSpace_of_BoundedLinearOperators ((diff_SP (i,E,F)),(diff_SP (i,E,G))))) = M & ( for V being Lipschitzian LinearOperator of E,(diff_SP (i,E,F)) holds K . V = M * V ) ) ) )
by A20; verum