defpred S1[ Nat] means for S, E, F, G being RealNormSpace
for Z being Subset of S
for B being Lipschitzian BilinearOperator of E,F,G
for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for W being PartFunc of S,G st W = B * w & w = <:u,v:> & u is_differentiable_on $1,Z & diff (u,$1,Z) is_continuous_on Z & v is_differentiable_on $1,Z & diff (v,$1,Z) is_continuous_on Z holds
( W is_differentiable_on $1,Z & diff (W,$1,Z) is_continuous_on Z );
A1:
S1[ 0 ]
proof
let S,
E,
F,
G be
RealNormSpace;
for Z being Subset of S
for B being Lipschitzian BilinearOperator of E,F,G
for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for W being PartFunc of S,G st W = B * w & w = <:u,v:> & u is_differentiable_on 0 ,Z & diff (u,0,Z) is_continuous_on Z & v is_differentiable_on 0 ,Z & diff (v,0,Z) is_continuous_on Z holds
( W is_differentiable_on 0 ,Z & diff (W,0,Z) is_continuous_on Z )let Z be
Subset of
S;
for B being Lipschitzian BilinearOperator of E,F,G
for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for W being PartFunc of S,G st W = B * w & w = <:u,v:> & u is_differentiable_on 0 ,Z & diff (u,0,Z) is_continuous_on Z & v is_differentiable_on 0 ,Z & diff (v,0,Z) is_continuous_on Z holds
( W is_differentiable_on 0 ,Z & diff (W,0,Z) is_continuous_on Z )let B be
Lipschitzian BilinearOperator of
E,
F,
G;
for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for W being PartFunc of S,G st W = B * w & w = <:u,v:> & u is_differentiable_on 0 ,Z & diff (u,0,Z) is_continuous_on Z & v is_differentiable_on 0 ,Z & diff (v,0,Z) is_continuous_on Z holds
( W is_differentiable_on 0 ,Z & diff (W,0,Z) is_continuous_on Z )let u be
PartFunc of
S,
E;
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for W being PartFunc of S,G st W = B * w & w = <:u,v:> & u is_differentiable_on 0 ,Z & diff (u,0,Z) is_continuous_on Z & v is_differentiable_on 0 ,Z & diff (v,0,Z) is_continuous_on Z holds
( W is_differentiable_on 0 ,Z & diff (W,0,Z) is_continuous_on Z )let v be
PartFunc of
S,
F;
for w being PartFunc of S,[:E,F:]
for W being PartFunc of S,G st W = B * w & w = <:u,v:> & u is_differentiable_on 0 ,Z & diff (u,0,Z) is_continuous_on Z & v is_differentiable_on 0 ,Z & diff (v,0,Z) is_continuous_on Z holds
( W is_differentiable_on 0 ,Z & diff (W,0,Z) is_continuous_on Z )let w be
PartFunc of
S,
[:E,F:];
for W being PartFunc of S,G st W = B * w & w = <:u,v:> & u is_differentiable_on 0 ,Z & diff (u,0,Z) is_continuous_on Z & v is_differentiable_on 0 ,Z & diff (v,0,Z) is_continuous_on Z holds
( W is_differentiable_on 0 ,Z & diff (W,0,Z) is_continuous_on Z )let W be
PartFunc of
S,
G;
( W = B * w & w = <:u,v:> & u is_differentiable_on 0 ,Z & diff (u,0,Z) is_continuous_on Z & v is_differentiable_on 0 ,Z & diff (v,0,Z) is_continuous_on Z implies ( W is_differentiable_on 0 ,Z & diff (W,0,Z) is_continuous_on Z ) )
assume A2:
(
W = B * w &
w = <:u,v:> &
u is_differentiable_on 0 ,
Z &
diff (
u,
0,
Z)
is_continuous_on Z &
v is_differentiable_on 0 ,
Z &
diff (
v,
0,
Z)
is_continuous_on Z )
;
( W is_differentiable_on 0 ,Z & diff (W,0,Z) is_continuous_on Z )
dom B = [#] [:E,F:]
by FUNCT_2:def 1;
then
rng w c= dom B
;
then A3:
dom W = dom w
by A2, RELAT_1:27;
dom w = (dom u) /\ (dom v)
by A2, FUNCT_3:def 7;
hence
W is_differentiable_on 0 ,
Z
by A2, A3, XBOOLE_1:19;
diff (W,0,Z) is_continuous_on Z
A4:
diff_SP (
0,
S,
E)
= E
by NDIFF_6:7;
A5:
diff_SP (
0,
S,
F)
= F
by NDIFF_6:7;
A6:
diff_SP (
0,
S,
G)
= G
by NDIFF_6:7;
A7:
diff (
u,
0,
Z)
= u | Z
by NDIFF_6:11;
A8:
diff (
v,
0,
Z)
= v | Z
by NDIFF_6:11;
A9:
diff (
W,
0,
Z)
= W | Z
by NDIFF_6:11;
A10:
u is_continuous_on Z
by A2, A4, A7, NFCONT_1:21;
A11:
v is_continuous_on Z
by A2, A5, A8, NFCONT_1:21;
A12:
w is_continuous_on Z
by A2, A10, A11, Th41;
A13:
w .: Z c= [#] [:E,F:]
;
B is_continuous_on [#] [:E,F:]
by NDIFF_1:45, NDIFF12:14;
then
W is_continuous_on Z
by A2, A13, A12, Th16;
hence
diff (
W,
0,
Z)
is_continuous_on Z
by A6, A9, NFCONT_1:21;
verum
end;
A14:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A15:
S1[
i]
;
S1[i + 1]
let S,
E,
F,
G be
RealNormSpace;
for Z being Subset of S
for B being Lipschitzian BilinearOperator of E,F,G
for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for W being PartFunc of S,G st W = B * w & w = <:u,v:> & u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z & v is_differentiable_on i + 1,Z & diff (v,(i + 1),Z) is_continuous_on Z holds
( W is_differentiable_on i + 1,Z & diff (W,(i + 1),Z) is_continuous_on Z )let Z be
Subset of
S;
for B being Lipschitzian BilinearOperator of E,F,G
for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for W being PartFunc of S,G st W = B * w & w = <:u,v:> & u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z & v is_differentiable_on i + 1,Z & diff (v,(i + 1),Z) is_continuous_on Z holds
( W is_differentiable_on i + 1,Z & diff (W,(i + 1),Z) is_continuous_on Z )let B be
Lipschitzian BilinearOperator of
E,
F,
G;
for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for W being PartFunc of S,G st W = B * w & w = <:u,v:> & u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z & v is_differentiable_on i + 1,Z & diff (v,(i + 1),Z) is_continuous_on Z holds
( W is_differentiable_on i + 1,Z & diff (W,(i + 1),Z) is_continuous_on Z )let u be
PartFunc of
S,
E;
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for W being PartFunc of S,G st W = B * w & w = <:u,v:> & u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z & v is_differentiable_on i + 1,Z & diff (v,(i + 1),Z) is_continuous_on Z holds
( W is_differentiable_on i + 1,Z & diff (W,(i + 1),Z) is_continuous_on Z )let v be
PartFunc of
S,
F;
for w being PartFunc of S,[:E,F:]
for W being PartFunc of S,G st W = B * w & w = <:u,v:> & u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z & v is_differentiable_on i + 1,Z & diff (v,(i + 1),Z) is_continuous_on Z holds
( W is_differentiable_on i + 1,Z & diff (W,(i + 1),Z) is_continuous_on Z )let w be
PartFunc of
S,
[:E,F:];
for W being PartFunc of S,G st W = B * w & w = <:u,v:> & u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z & v is_differentiable_on i + 1,Z & diff (v,(i + 1),Z) is_continuous_on Z holds
( W is_differentiable_on i + 1,Z & diff (W,(i + 1),Z) is_continuous_on Z )let W be
PartFunc of
S,
G;
( W = B * w & w = <:u,v:> & u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z & v is_differentiable_on i + 1,Z & diff (v,(i + 1),Z) is_continuous_on Z implies ( W is_differentiable_on i + 1,Z & diff (W,(i + 1),Z) is_continuous_on Z ) )
assume A16:
(
W = B * w &
w = <:u,v:> &
u is_differentiable_on i + 1,
Z &
diff (
u,
(i + 1),
Z)
is_continuous_on Z &
v is_differentiable_on i + 1,
Z &
diff (
v,
(i + 1),
Z)
is_continuous_on Z )
;
( W is_differentiable_on i + 1,Z & diff (W,(i + 1),Z) is_continuous_on Z )
0 <= i
by NAT_1:2;
then
(
u is_differentiable_on 0 + 1,
Z &
v is_differentiable_on 0 + 1,
Z )
by A16, NDIFF_6:17, XREAL_1:7;
then A17:
(
u | Z is_differentiable_on Z &
v | Z is_differentiable_on Z )
by NDIFF_6:15;
A18:
u is_differentiable_on Z
by A16, A17;
A19:
v is_differentiable_on Z
by A16, A17;
A20:
(
W is_differentiable_on Z & ( for
x being
Point of
S st
x in Z holds
for
ds being
Point of
S holds
((W `| Z) /. x) . ds = (B . ((((u `| Z) /. x) . ds),(v /. x))) + (B . ((u /. x),(((v `| Z) /. x) . ds))) ) )
by A16, A18, A19, Th35;
A21:
u `| Z is_differentiable_on i,
Z
by A16, Th36;
A22:
v `| Z is_differentiable_on i,
Z
by A16, Th36;
set V10 = the
Point of
E;
set V20 = the
Point of
F;
reconsider BP =
B as
Point of
(R_NormSpace_of_BoundedBilinearOperators (E,F,G)) by LOPBAN_9:def 4;
defpred S2[
object ,
object ]
means ex
V2 being
Point of
F st
(
V2 = $1 & $2
= B * (reproj1 [ the Point of E,V2]) );
A23:
for
x being
object st
x in the
carrier of
F holds
ex
y being
object st
(
y in the
carrier of
(R_NormSpace_of_BoundedLinearOperators (E,G)) &
S2[
x,
y] )
proof
let x be
object ;
( x in the carrier of F implies ex y being object st
( y in the carrier of (R_NormSpace_of_BoundedLinearOperators (E,G)) & S2[x,y] ) )
assume
x in the
carrier of
F
;
ex y being object st
( y in the carrier of (R_NormSpace_of_BoundedLinearOperators (E,G)) & S2[x,y] )
then reconsider V2 =
x as
Point of
F ;
take y =
B * (reproj1 [ the Point of E,V2]);
( y in the carrier of (R_NormSpace_of_BoundedLinearOperators (E,G)) & S2[x,y] )
B * (reproj1 [ the Point of E,V2]) is
Lipschitzian LinearOperator of
E,
G
by NDIFF12:2;
hence
(
y in the
carrier of
(R_NormSpace_of_BoundedLinearOperators (E,G)) &
S2[
x,
y] )
by LOPBAN_1:def 9;
verum
end;
consider B2 being
Function of the
carrier of
F, the
carrier of
(R_NormSpace_of_BoundedLinearOperators (E,G)) such that A24:
for
x being
object st
x in the
carrier of
F holds
S2[
x,
B2 . x]
from FUNCT_2:sch 1(A23);
A25:
for
V2 being
Point of
F holds
B2 . V2 = B * (reproj1 [ the Point of E,V2])
defpred S3[
object ,
object ]
means ex
V1 being
Point of
E st
(
V1 = $1 & $2
= B * (reproj2 [V1, the Point of F]) );
A26:
for
x being
object st
x in the
carrier of
E holds
ex
y being
object st
(
y in the
carrier of
(R_NormSpace_of_BoundedLinearOperators (F,G)) &
S3[
x,
y] )
proof
let x be
object ;
( x in the carrier of E implies ex y being object st
( y in the carrier of (R_NormSpace_of_BoundedLinearOperators (F,G)) & S3[x,y] ) )
assume
x in the
carrier of
E
;
ex y being object st
( y in the carrier of (R_NormSpace_of_BoundedLinearOperators (F,G)) & S3[x,y] )
then reconsider V1 =
x as
Point of
E ;
take y =
B * (reproj2 [V1, the Point of F]);
( y in the carrier of (R_NormSpace_of_BoundedLinearOperators (F,G)) & S3[x,y] )
B * (reproj2 [V1, the Point of F]) is
Lipschitzian LinearOperator of
F,
G
by NDIFF12:2;
hence
(
y in the
carrier of
(R_NormSpace_of_BoundedLinearOperators (F,G)) &
S3[
x,
y] )
by LOPBAN_1:def 9;
verum
end;
consider B1 being
Function of the
carrier of
E, the
carrier of
(R_NormSpace_of_BoundedLinearOperators (F,G)) such that A27:
for
x being
object st
x in the
carrier of
E holds
S3[
x,
B1 . x]
from FUNCT_2:sch 1(A26);
A28:
for
V1 being
Point of
E holds
B1 . V1 = B * (reproj2 [V1, the Point of F])
for
x,
y being
Element of
F holds
B2 . (x + y) = (B2 . x) + (B2 . y)
proof
let x,
y be
Element of
F;
B2 . (x + y) = (B2 . x) + (B2 . y)
A29:
B2 . y = B * (reproj1 [ the Point of E,y])
by A25;
set f =
B * (reproj1 [ the Point of E,x]);
set g =
B * (reproj1 [ the Point of E,y]);
set h =
B * (reproj1 [ the Point of E,(x + y)]);
for
s being
VECTOR of
E holds
(B2 . (x + y)) . s = ((B2 . x) . s) + ((B2 . y) . s)
proof
let s be
VECTOR of
E;
(B2 . (x + y)) . s = ((B2 . x) . s) + ((B2 . y) . s)
thus (B2 . (x + y)) . s =
(B * (reproj1 [ the Point of E,(x + y)])) . s
by A25
.=
B . ((reproj1 [ the Point of E,(x + y)]) . s)
by FUNCT_2:15
.=
B . [s,([ the Point of E,(x + y)] `2)]
by NDIFF_7:def 1
.=
B . (
s,
(x + y))
by BINOP_1:def 1
.=
(B . (s,x)) + (B . (s,y))
by LOPBAN_8:12
.=
(B . [s,x]) + (B . (s,y))
by BINOP_1:def 1
.=
(B . [s,([ the Point of E,x] `2)]) + (B . [s,y])
by BINOP_1:def 1
.=
(B . ((reproj1 [ the Point of E,x]) . s)) + (B . [s,([ the Point of E,y] `2)])
by NDIFF_7:def 1
.=
(B . ((reproj1 [ the Point of E,x]) . s)) + (B . ((reproj1 [ the Point of E,y]) . s))
by NDIFF_7:def 1
.=
((B * (reproj1 [ the Point of E,x])) . s) + (B . ((reproj1 [ the Point of E,y]) . s))
by FUNCT_2:15
.=
((B * (reproj1 [ the Point of E,x])) . s) + ((B * (reproj1 [ the Point of E,y])) . s)
by FUNCT_2:15
.=
((B2 . x) . s) + ((B2 . y) . s)
by A25, A29
;
verum
end;
hence
B2 . (x + y) = (B2 . x) + (B2 . y)
by LOPBAN_1:35;
verum
end;
then A30:
B2 is
additive
;
for
x being
VECTOR of
F for
a being
Real holds
B2 . (a * x) = a * (B2 . x)
proof
let x be
VECTOR of
F;
for a being Real holds B2 . (a * x) = a * (B2 . x)let a be
Real;
B2 . (a * x) = a * (B2 . x)
set f =
B * (reproj1 [ the Point of E,x]);
set g =
B * (reproj1 [ the Point of E,(a * x)]);
for
s being
VECTOR of
E holds
(B2 . (a * x)) . s = a * ((B2 . x) . s)
proof
let s be
VECTOR of
E;
(B2 . (a * x)) . s = a * ((B2 . x) . s)
thus (B2 . (a * x)) . s =
(B * (reproj1 [ the Point of E,(a * x)])) . s
by A25
.=
B . ((reproj1 [ the Point of E,(a * x)]) . s)
by FUNCT_2:15
.=
B . [s,([ the Point of E,(a * x)] `2)]
by NDIFF_7:def 1
.=
B . (
s,
(a * x))
by BINOP_1:def 1
.=
a * (B . (s,x))
by LOPBAN_8:12
.=
a * (B . [s,([ the Point of E,x] `2)])
by BINOP_1:def 1
.=
a * (B . ((reproj1 [ the Point of E,x]) . s))
by NDIFF_7:def 1
.=
a * ((B * (reproj1 [ the Point of E,x])) . s)
by FUNCT_2:15
.=
a * ((B2 . x) . s)
by A25
;
verum
end;
hence
B2 . (a * x) = a * (B2 . x)
by LOPBAN_1:36;
verum
end;
then reconsider B2 =
B2 as
LinearOperator of
F,
(R_NormSpace_of_BoundedLinearOperators (E,G)) by A30, LOPBAN_1:def 5;
for
x,
y being
Element of
E holds
B1 . (x + y) = (B1 . x) + (B1 . y)
proof
let x,
y be
Element of
E;
B1 . (x + y) = (B1 . x) + (B1 . y)
A31:
B1 . y = B * (reproj2 [y, the Point of F])
by A28;
set f =
B * (reproj2 [x, the Point of F]);
set g =
B * (reproj2 [y, the Point of F]);
set h =
B * (reproj2 [(x + y), the Point of F]);
for
s being
VECTOR of
F holds
(B1 . (x + y)) . s = ((B1 . x) . s) + ((B1 . y) . s)
proof
let s be
VECTOR of
F;
(B1 . (x + y)) . s = ((B1 . x) . s) + ((B1 . y) . s)
thus (B1 . (x + y)) . s =
(B * (reproj2 [(x + y), the Point of F])) . s
by A28
.=
B . ((reproj2 [(x + y), the Point of F]) . s)
by FUNCT_2:15
.=
B . [([(x + y), the Point of F] `1),s]
by NDIFF_7:def 2
.=
B . (
(x + y),
s)
by BINOP_1:def 1
.=
(B . (x,s)) + (B . (y,s))
by LOPBAN_8:12
.=
(B . [x,s]) + (B . (y,s))
by BINOP_1:def 1
.=
(B . [([x, the Point of F] `1),s]) + (B . [y,s])
by BINOP_1:def 1
.=
(B . ((reproj2 [x, the Point of F]) . s)) + (B . [([y, the Point of F] `1),s])
by NDIFF_7:def 2
.=
(B . ((reproj2 [x, the Point of F]) . s)) + (B . ((reproj2 [y, the Point of F]) . s))
by NDIFF_7:def 2
.=
((B * (reproj2 [x, the Point of F])) . s) + (B . ((reproj2 [y, the Point of F]) . s))
by FUNCT_2:15
.=
((B * (reproj2 [x, the Point of F])) . s) + ((B * (reproj2 [y, the Point of F])) . s)
by FUNCT_2:15
.=
((B1 . x) . s) + ((B1 . y) . s)
by A28, A31
;
verum
end;
hence
B1 . (x + y) = (B1 . x) + (B1 . y)
by LOPBAN_1:35;
verum
end;
then A32:
B1 is
additive
;
for
x being
VECTOR of
E for
a being
Real holds
B1 . (a * x) = a * (B1 . x)
proof
let x be
VECTOR of
E;
for a being Real holds B1 . (a * x) = a * (B1 . x)let a be
Real;
B1 . (a * x) = a * (B1 . x)
set f =
B * (reproj2 [x, the Point of F]);
set g =
B * (reproj2 [(a * x), the Point of F]);
for
s being
VECTOR of
F holds
(B1 . (a * x)) . s = a * ((B1 . x) . s)
proof
let s be
VECTOR of
F;
(B1 . (a * x)) . s = a * ((B1 . x) . s)
thus (B1 . (a * x)) . s =
(B * (reproj2 [(a * x), the Point of F])) . s
by A28
.=
B . ((reproj2 [(a * x), the Point of F]) . s)
by FUNCT_2:15
.=
B . [([(a * x), the Point of F] `1),s]
by NDIFF_7:def 2
.=
B . (
(a * x),
s)
by BINOP_1:def 1
.=
a * (B . (x,s))
by LOPBAN_8:12
.=
a * (B . [([x, the Point of F] `1),s])
by BINOP_1:def 1
.=
a * (B . ((reproj2 [x, the Point of F]) . s))
by NDIFF_7:def 2
.=
a * ((B * (reproj2 [x, the Point of F])) . s)
by FUNCT_2:15
.=
a * ((B1 . x) . s)
by A28
;
verum
end;
hence
B1 . (a * x) = a * (B1 . x)
by LOPBAN_1:36;
verum
end;
then reconsider B1 =
B1 as
LinearOperator of
E,
(R_NormSpace_of_BoundedLinearOperators (F,G)) by A32, LOPBAN_1:def 5;
now for V2 being Point of F holds ||.(B2 . V2).|| <= ||.BP.|| * ||.V2.||let V2 be
Point of
F;
||.(B2 . V2).|| <= ||.BP.|| * ||.V2.||A33:
B2 . V2 = B * (reproj1 [ the Point of E,V2])
by A25;
set L1 =
B * (reproj1 [ the Point of E,V2]);
set z =
[ the Point of E,V2];
consider BP0 being
Point of
(R_NormSpace_of_BoundedBilinearOperators (E,F,G)) such that A34:
(
B = BP0 & ( for
x being
VECTOR of
E holds
||.((B * (reproj1 [ the Point of E,V2])) . x).|| <= (||.BP0.|| * ||.([ the Point of E,V2] `2).||) * ||.x.|| ) & ( for
y being
VECTOR of
F holds
||.((B * (reproj2 [ the Point of E,V2])) . y).|| <= (||.BP0.|| * ||.([ the Point of E,V2] `1).||) * ||.y.|| ) )
by NDIFF12:2;
A35:
0 <= ||.BP0.||
by NORMSP_1:4;
reconsider LL1 =
B * (reproj1 [ the Point of E,V2]) as
Lipschitzian LinearOperator of
E,
G by A33, LOPBAN_1:def 9;
A36:
now for t being VECTOR of E st ||.t.|| <= 1 holds
||.(LL1 . t).|| <= ||.BP0.|| * ||.([ the Point of E,V2] `2).||let t be
VECTOR of
E;
( ||.t.|| <= 1 implies ||.(LL1 . t).|| <= ||.BP0.|| * ||.([ the Point of E,V2] `2).|| )assume A37:
||.t.|| <= 1
;
||.(LL1 . t).|| <= ||.BP0.|| * ||.([ the Point of E,V2] `2).||A38:
||.(LL1 . t).|| <= (||.BP0.|| * ||.([ the Point of E,V2] `2).||) * ||.t.||
by A34;
0 <= ||.([ the Point of E,V2] `2).||
by NORMSP_1:4;
then
0 <= ||.BP0.|| * ||.([ the Point of E,V2] `2).||
by A35, XREAL_1:127;
then
(||.BP0.|| * ||.([ the Point of E,V2] `2).||) * ||.t.|| <= (||.BP0.|| * ||.([ the Point of E,V2] `2).||) * 1
by A37, XREAL_1:64;
hence
||.(LL1 . t).|| <= ||.BP0.|| * ||.([ the Point of E,V2] `2).||
by A38, XXREAL_0:2;
verum end; then
upper_bound (PreNorms LL1) <= ||.BP0.|| * ||.([ the Point of E,V2] `2).||
by SEQ_4:45;
hence
||.(B2 . V2).|| <= ||.BP.|| * ||.V2.||
by A33, A34, LOPBAN_1:30;
verum end;
then reconsider B2 =
B2 as
Lipschitzian LinearOperator of
F,
(R_NormSpace_of_BoundedLinearOperators (E,G)) by LOPBAN_1:def 8, NORMSP_1:4;
now for V1 being Point of E holds ||.(B1 . V1).|| <= ||.BP.|| * ||.V1.||let V1 be
Point of
E;
||.(B1 . V1).|| <= ||.BP.|| * ||.V1.||A39:
B1 . V1 = B * (reproj2 [V1, the Point of F])
by A28;
set L1 =
B * (reproj2 [V1, the Point of F]);
set z =
[V1, the Point of F];
consider BP0 being
Point of
(R_NormSpace_of_BoundedBilinearOperators (E,F,G)) such that A40:
(
B = BP0 & ( for
x being
VECTOR of
E holds
||.((B * (reproj1 [V1, the Point of F])) . x).|| <= (||.BP0.|| * ||.([V1, the Point of F] `2).||) * ||.x.|| ) & ( for
y being
VECTOR of
F holds
||.((B * (reproj2 [V1, the Point of F])) . y).|| <= (||.BP0.|| * ||.([V1, the Point of F] `1).||) * ||.y.|| ) )
by NDIFF12:2;
A41:
0 <= ||.BP0.||
by NORMSP_1:4;
reconsider LL1 =
B * (reproj2 [V1, the Point of F]) as
Lipschitzian LinearOperator of
F,
G by A39, LOPBAN_1:def 9;
A42:
now for t being VECTOR of F st ||.t.|| <= 1 holds
||.(LL1 . t).|| <= ||.BP0.|| * ||.([V1, the Point of F] `1).||let t be
VECTOR of
F;
( ||.t.|| <= 1 implies ||.(LL1 . t).|| <= ||.BP0.|| * ||.([V1, the Point of F] `1).|| )assume A43:
||.t.|| <= 1
;
||.(LL1 . t).|| <= ||.BP0.|| * ||.([V1, the Point of F] `1).||A44:
||.(LL1 . t).|| <= (||.BP0.|| * ||.([V1, the Point of F] `1).||) * ||.t.||
by A40;
0 <= ||.([V1, the Point of F] `1).||
by NORMSP_1:4;
then
0 <= ||.BP0.|| * ||.([V1, the Point of F] `1).||
by A41, XREAL_1:127;
then
(||.BP0.|| * ||.([V1, the Point of F] `1).||) * ||.t.|| <= (||.BP0.|| * ||.([V1, the Point of F] `1).||) * 1
by A43, XREAL_1:64;
hence
||.(LL1 . t).|| <= ||.BP0.|| * ||.([V1, the Point of F] `1).||
by A44, XXREAL_0:2;
verum end; then
upper_bound (PreNorms LL1) <= ||.BP0.|| * ||.([V1, the Point of F] `1).||
by SEQ_4:45;
hence
||.(B1 . V1).|| <= ||.BP.|| * ||.V1.||
by A39, A40, LOPBAN_1:30;
verum end;
then reconsider B1 =
B1 as
Lipschitzian LinearOperator of
E,
(R_NormSpace_of_BoundedLinearOperators (F,G)) by LOPBAN_1:def 8, NORMSP_1:4;
A45:
for
x being
Point of
S st
x in Z holds
for
V being
Point of
E holds
((B2 * v) /. x) . V = B . (
V,
(v /. x))
proof
let x be
Point of
S;
( x in Z implies for V being Point of E holds ((B2 * v) /. x) . V = B . (V,(v /. x)) )
assume A46:
x in Z
;
for V being Point of E holds ((B2 * v) /. x) . V = B . (V,(v /. x))
v /. x in the
carrier of
F
;
then
v /. x in dom B2
by FUNCT_2:def 1;
then A47:
(B2 * v) /. x =
B2 /. (v /. x)
by A16, A46, PARTFUN2:4
.=
B * (reproj1 [ the Point of E,(v /. x)])
by A25
;
let V be
Point of
E;
((B2 * v) /. x) . V = B . (V,(v /. x))
A48:
[ the Point of E,(v /. x)] `2 = v /. x
;
thus ((B2 * v) /. x) . V =
B . ((reproj1 [ the Point of E,(v /. x)]) . V)
by A47, FUNCT_2:15
.=
B . [V,(v /. x)]
by A48, NDIFF_7:def 1
.=
B . (
V,
(v /. x))
by BINOP_1:def 1
;
verum
end;
A49:
for
x being
Point of
S st
x in Z holds
for
ds being
Point of
S holds
B . (
(((u `| Z) /. x) . ds),
(v /. x))
= (((B2 * v) /. x) * ((u `| Z) /. x)) . ds
proof
let x be
Point of
S;
( x in Z implies for ds being Point of S holds B . ((((u `| Z) /. x) . ds),(v /. x)) = (((B2 * v) /. x) * ((u `| Z) /. x)) . ds )
assume A50:
x in Z
;
for ds being Point of S holds B . ((((u `| Z) /. x) . ds),(v /. x)) = (((B2 * v) /. x) * ((u `| Z) /. x)) . ds
let ds be
Point of
S;
B . ((((u `| Z) /. x) . ds),(v /. x)) = (((B2 * v) /. x) * ((u `| Z) /. x)) . ds
reconsider F1 =
(B2 * v) /. x as
Lipschitzian LinearOperator of
E,
G by LOPBAN_1:def 9;
reconsider F2 =
(u `| Z) /. x as
Lipschitzian LinearOperator of
S,
E by LOPBAN_1:def 9;
A51:
modetrans (
F1,
E,
G)
= F1
by LOPBAN_1:def 11;
A52:
dom F2 = the
carrier of
S
by FUNCT_2:def 1;
thus (((B2 * v) /. x) * ((u `| Z) /. x)) . ds =
(F1 * F2) . ds
by A51, LOPBAN_1:def 11
.=
((B2 * v) /. x) . (((u `| Z) /. x) . ds)
by A52, FUNCT_1:13
.=
B . (
(((u `| Z) /. x) . ds),
(v /. x))
by A45, A50
;
verum
end;
A53:
for
x being
Point of
S st
x in Z holds
for
V being
Point of
F holds
((B1 * u) /. x) . V = B . (
(u /. x),
V)
proof
let x be
Point of
S;
( x in Z implies for V being Point of F holds ((B1 * u) /. x) . V = B . ((u /. x),V) )
assume A54:
x in Z
;
for V being Point of F holds ((B1 * u) /. x) . V = B . ((u /. x),V)
u /. x in the
carrier of
E
;
then
u /. x in dom B1
by FUNCT_2:def 1;
then A55:
(B1 * u) /. x =
B1 /. (u /. x)
by A16, A54, PARTFUN2:4
.=
B * (reproj2 [(u /. x), the Point of F])
by A28
;
let V be
Point of
F;
((B1 * u) /. x) . V = B . ((u /. x),V)
A56:
[(u /. x), the Point of F] `1 = u /. x
;
thus ((B1 * u) /. x) . V =
B . ((reproj2 [(u /. x), the Point of F]) . V)
by A55, FUNCT_2:15
.=
B . [(u /. x),V]
by A56, NDIFF_7:def 2
.=
B . (
(u /. x),
V)
by BINOP_1:def 1
;
verum
end;
A57:
for
x being
Point of
S st
x in Z holds
for
ds being
Point of
S holds
B . (
(u /. x),
(((v `| Z) /. x) . ds))
= (((B1 * u) /. x) * ((v `| Z) /. x)) . ds
proof
let x be
Point of
S;
( x in Z implies for ds being Point of S holds B . ((u /. x),(((v `| Z) /. x) . ds)) = (((B1 * u) /. x) * ((v `| Z) /. x)) . ds )
assume A58:
x in Z
;
for ds being Point of S holds B . ((u /. x),(((v `| Z) /. x) . ds)) = (((B1 * u) /. x) * ((v `| Z) /. x)) . ds
let ds be
Point of
S;
B . ((u /. x),(((v `| Z) /. x) . ds)) = (((B1 * u) /. x) * ((v `| Z) /. x)) . ds
reconsider F1 =
(B1 * u) /. x as
Lipschitzian LinearOperator of
F,
G by LOPBAN_1:def 9;
reconsider F2 =
(v `| Z) /. x as
Lipschitzian LinearOperator of
S,
F by LOPBAN_1:def 9;
A59:
modetrans (
F1,
F,
G)
= F1
by LOPBAN_1:def 11;
A60:
dom F2 = the
carrier of
S
by FUNCT_2:def 1;
thus (((B1 * u) /. x) * ((v `| Z) /. x)) . ds =
(F1 * F2) . ds
by A59, LOPBAN_1:def 11
.=
((B1 * u) /. x) . (((v `| Z) /. x) . ds)
by A60, FUNCT_1:13
.=
B . (
(u /. x),
(((v `| Z) /. x) . ds))
by A53, A58
;
verum
end;
A61:
for
x being
Point of
S st
x in Z holds
for
ds being
Point of
S holds
((W `| Z) /. x) . ds = ((((B2 * v) /. x) * ((u `| Z) /. x)) . ds) + ((((B1 * u) /. x) * ((v `| Z) /. x)) . ds)
proof
let x be
Point of
S;
( x in Z implies for ds being Point of S holds ((W `| Z) /. x) . ds = ((((B2 * v) /. x) * ((u `| Z) /. x)) . ds) + ((((B1 * u) /. x) * ((v `| Z) /. x)) . ds) )
assume A62:
x in Z
;
for ds being Point of S holds ((W `| Z) /. x) . ds = ((((B2 * v) /. x) * ((u `| Z) /. x)) . ds) + ((((B1 * u) /. x) * ((v `| Z) /. x)) . ds)
let ds be
Point of
S;
((W `| Z) /. x) . ds = ((((B2 * v) /. x) * ((u `| Z) /. x)) . ds) + ((((B1 * u) /. x) * ((v `| Z) /. x)) . ds)
A63:
B . (
(((u `| Z) /. x) . ds),
(v /. x))
= (((B2 * v) /. x) * ((u `| Z) /. x)) . ds
by A49, A62;
thus ((W `| Z) /. x) . ds =
(B . ((((u `| Z) /. x) . ds),(v /. x))) + (B . ((u /. x),(((v `| Z) /. x) . ds)))
by A16, A18, A19, A62, Th35
.=
((((B2 * v) /. x) * ((u `| Z) /. x)) . ds) + ((((B1 * u) /. x) * ((v `| Z) /. x)) . ds)
by A57, A62, A63
;
verum
end;
A64:
for
x being
Point of
S st
x in Z holds
(W `| Z) /. x = (((B2 * v) /. x) * ((u `| Z) /. x)) + (((B1 * u) /. x) * ((v `| Z) /. x))
0 + i <= i + 1
by XREAL_1:7;
then
(
u is_differentiable_on i,
Z &
v is_differentiable_on i,
Z )
by A16, NDIFF_6:17;
then A65:
(
B1 * u is_differentiable_on i,
Z &
B2 * v is_differentiable_on i,
Z )
by Th25;
A66:
(
B1 * u is_differentiable_on i + 1,
Z &
B2 * v is_differentiable_on i + 1,
Z )
by A16, Th25;
consider BX1 being
Lipschitzian BilinearOperator of
(R_NormSpace_of_BoundedLinearOperators (S,E)),
(R_NormSpace_of_BoundedLinearOperators (E,G)),
(R_NormSpace_of_BoundedLinearOperators (S,G)) such that A67:
for
u being
Point of
(R_NormSpace_of_BoundedLinearOperators (S,E)) for
v being
Point of
(R_NormSpace_of_BoundedLinearOperators (E,G)) holds
BX1 . (
u,
v)
= v * u
by Th38;
set w1 =
<:(u `| Z),(B2 * v):>;
A68:
dom <:(u `| Z),(B2 * v):> =
(dom (u `| Z)) /\ (dom (B2 * v))
by FUNCT_3:def 7
.=
Z /\ (dom (B2 * v))
by A18, NDIFF_1:def 9
.=
Z
by A65, XBOOLE_1:28
;
A69:
rng <:(u `| Z),(B2 * v):> c= [:(rng (u `| Z)),(rng (B2 * v)):]
by FUNCT_3:51;
[:(rng (u `| Z)),(rng (B2 * v)):] c= [: the carrier of (R_NormSpace_of_BoundedLinearOperators (S,E)), the carrier of (R_NormSpace_of_BoundedLinearOperators (E,G)):]
by ZFMISC_1:96;
then
rng <:(u `| Z),(B2 * v):> c= the
carrier of
[:(R_NormSpace_of_BoundedLinearOperators (S,E)),(R_NormSpace_of_BoundedLinearOperators (E,G)):]
by A69, XBOOLE_1:1;
then reconsider w1 =
<:(u `| Z),(B2 * v):> as
PartFunc of
S,
[:(R_NormSpace_of_BoundedLinearOperators (S,E)),(R_NormSpace_of_BoundedLinearOperators (E,G)):] by A68, RELSET_1:4;
A70:
diff (
(u `| Z),
i,
Z)
is_continuous_on Z
by A16, Th37;
A71:
diff (
(B2 * v),
i,
Z)
is_continuous_on Z
by A66, NDIFF_1:45, NDIFF_6:14;
set W1 =
BX1 * w1;
A72:
(
BX1 * w1 is_differentiable_on i,
Z &
diff (
(BX1 * w1),
i,
Z)
is_continuous_on Z )
by A15, A21, A65, A70, A71;
dom BX1 = the
carrier of
[:(R_NormSpace_of_BoundedLinearOperators (S,E)),(R_NormSpace_of_BoundedLinearOperators (E,G)):]
by FUNCT_2:def 1;
then
rng w1 c= dom BX1
;
then A73:
dom (BX1 * w1) = Z
by A68, RELAT_1:27;
consider BX2 being
Lipschitzian BilinearOperator of
(R_NormSpace_of_BoundedLinearOperators (S,F)),
(R_NormSpace_of_BoundedLinearOperators (F,G)),
(R_NormSpace_of_BoundedLinearOperators (S,G)) such that A74:
for
u being
Point of
(R_NormSpace_of_BoundedLinearOperators (S,F)) for
v being
Point of
(R_NormSpace_of_BoundedLinearOperators (F,G)) holds
BX2 . (
u,
v)
= v * u
by Th38;
set w2 =
<:(v `| Z),(B1 * u):>;
A75:
dom <:(v `| Z),(B1 * u):> =
(dom (v `| Z)) /\ (dom (B1 * u))
by FUNCT_3:def 7
.=
Z /\ (dom (B1 * u))
by A19, NDIFF_1:def 9
.=
Z
by A65, XBOOLE_1:28
;
A76:
rng <:(v `| Z),(B1 * u):> c= [:(rng (v `| Z)),(rng (B1 * u)):]
by FUNCT_3:51;
[:(rng (v `| Z)),(rng (B1 * u)):] c= [: the carrier of (R_NormSpace_of_BoundedLinearOperators (S,F)), the carrier of (R_NormSpace_of_BoundedLinearOperators (F,G)):]
by ZFMISC_1:96;
then
rng <:(v `| Z),(B1 * u):> c= the
carrier of
[:(R_NormSpace_of_BoundedLinearOperators (S,F)),(R_NormSpace_of_BoundedLinearOperators (F,G)):]
by A76, XBOOLE_1:1;
then reconsider w2 =
<:(v `| Z),(B1 * u):> as
PartFunc of
S,
[:(R_NormSpace_of_BoundedLinearOperators (S,F)),(R_NormSpace_of_BoundedLinearOperators (F,G)):] by RELSET_1:4, A75;
A77:
diff (
(v `| Z),
i,
Z)
is_continuous_on Z
by A16, Th37;
A78:
diff (
(B1 * u),
i,
Z)
is_continuous_on Z
by A66, NDIFF_1:45, NDIFF_6:14;
set W2 =
BX2 * w2;
A79:
(
BX2 * w2 is_differentiable_on i,
Z &
diff (
(BX2 * w2),
i,
Z)
is_continuous_on Z )
by A15, A22, A65, A77, A78;
dom BX2 = the
carrier of
[:(R_NormSpace_of_BoundedLinearOperators (S,F)),(R_NormSpace_of_BoundedLinearOperators (F,G)):]
by FUNCT_2:def 1;
then
rng w2 c= dom BX2
;
then A80:
dom (BX2 * w2) = Z
by A75, RELAT_1:27;
A81:
dom (W `| Z) = Z
by A20, NDIFF_1:def 9;
A82:
(dom (BX1 * w1)) /\ (dom (BX2 * w2)) = Z
by A73, A80;
A83:
for
c being
Element of
S st
c in dom (W `| Z) holds
(W `| Z) /. c = ((BX1 * w1) /. c) + ((BX2 * w2) /. c)
proof
let x be
Element of
S;
( x in dom (W `| Z) implies (W `| Z) /. x = ((BX1 * w1) /. x) + ((BX2 * w2) /. x) )
assume
x in dom (W `| Z)
;
(W `| Z) /. x = ((BX1 * w1) /. x) + ((BX2 * w2) /. x)
then A84:
x in Z
by A20, NDIFF_1:def 9;
A85:
dom (u `| Z) = Z
by A18, NDIFF_1:def 9;
A86:
(BX1 * w1) /. x =
(BX1 * w1) . x
by A73, A84, PARTFUN1:def 6
.=
BX1 . (w1 . x)
by A68, A84, FUNCT_1:13
.=
BX1 . [((u `| Z) . x),((B2 * v) . x)]
by A68, A84, FUNCT_3:def 7
.=
BX1 . [((u `| Z) /. x),((B2 * v) . x)]
by A84, A85, PARTFUN1:def 6
.=
BX1 . [((u `| Z) /. x),((B2 * v) /. x)]
by A65, A84, PARTFUN1:def 6
.=
BX1 . (
((u `| Z) /. x),
((B2 * v) /. x))
by BINOP_1:def 1
.=
((B2 * v) /. x) * ((u `| Z) /. x)
by A67
;
A87:
dom (v `| Z) = Z
by A19, NDIFF_1:def 9;
(BX2 * w2) /. x =
(BX2 * w2) . x
by A80, A84, PARTFUN1:def 6
.=
BX2 . (w2 . x)
by A75, A84, FUNCT_1:13
.=
BX2 . [((v `| Z) . x),((B1 * u) . x)]
by A75, A84, FUNCT_3:def 7
.=
BX2 . [((v `| Z) /. x),((B1 * u) . x)]
by A84, A87, PARTFUN1:def 6
.=
BX2 . [((v `| Z) /. x),((B1 * u) /. x)]
by A65, A84, PARTFUN1:def 6
.=
BX2 . (
((v `| Z) /. x),
((B1 * u) /. x))
by BINOP_1:def 1
.=
((B1 * u) /. x) * ((v `| Z) /. x)
by A74
;
hence
(W `| Z) /. x = ((BX1 * w1) /. x) + ((BX2 * w2) /. x)
by A64, A84, A86;
verum
end;
then A88:
W `| Z = (BX1 * w1) + (BX2 * w2)
by A81, A82, VFUNCT_1:def 1;
A89:
BX1 * w1 is_continuous_on Z
proof
per cases
( i = 0 or i <> 0 )
;
suppose A90:
i = 0
;
BX1 * w1 is_continuous_on Zthen A91:
diff_SP (
i,
S,
(R_NormSpace_of_BoundedLinearOperators (S,G)))
= R_NormSpace_of_BoundedLinearOperators (
S,
G)
by NDIFF_6:7;
diff (
(BX1 * w1),
i,
Z) =
(BX1 * w1) | Z
by A90, NDIFF_6:11
.=
BX1 * w1
by A73
;
hence
BX1 * w1 is_continuous_on Z
by A15, A21, A65, A70, A71, A91;
verum end;
end;
A92:
BX2 * w2 is_continuous_on Z
proof
per cases
( i = 0 or i <> 0 )
;
suppose A93:
i = 0
;
BX2 * w2 is_continuous_on Zthen A94:
diff_SP (
i,
S,
(R_NormSpace_of_BoundedLinearOperators (S,G)))
= R_NormSpace_of_BoundedLinearOperators (
S,
G)
by NDIFF_6:7;
diff (
(BX2 * w2),
i,
Z) =
(BX2 * w2) | Z
by A93, NDIFF_6:11
.=
BX2 * w2
by A80
;
hence
BX2 * w2 is_continuous_on Z
by A15, A22, A65, A77, A78, A94;
verum end;
end;
A95:
diff (
(W `| Z),
i,
Z)
is_continuous_on Z
proof
per cases
( i = 0 or i <> 0 )
;
suppose A96:
i = 0
;
diff ((W `| Z),i,Z) is_continuous_on Zthen A97:
diff_SP (
i,
S,
(R_NormSpace_of_BoundedLinearOperators (S,G)))
= R_NormSpace_of_BoundedLinearOperators (
S,
G)
by NDIFF_6:7;
diff (
(W `| Z),
i,
Z) =
(W `| Z) | Z
by A96, NDIFF_6:11
.=
(BX1 * w1) + (BX2 * w2)
by A81, A82, A83, VFUNCT_1:def 1
;
hence
diff (
(W `| Z),
i,
Z)
is_continuous_on Z
by A89, A92, A97, NFCONT_1:25;
verum end; suppose
i <> 0
;
diff ((W `| Z),i,Z) is_continuous_on Zthen A98:
1
<= i
by NAT_1:14;
diff (
(W `| Z),
i,
Z) =
diff (
((BX1 * w1) + (BX2 * w2)),
i,
Z)
by A81, A82, A83, VFUNCT_1:def 1
.=
(diff ((BX1 * w1),i,Z)) + (diff ((BX2 * w2),i,Z))
by A72, A79, A98, NDIFF_6:20
;
hence
diff (
(W `| Z),
i,
Z)
is_continuous_on Z
by A72, A79, NFCONT_1:25;
verum end;
end;
W `| Z is_differentiable_on i,
Z
hence
(
W is_differentiable_on i + 1,
Z &
diff (
W,
(i + 1),
Z)
is_continuous_on Z )
by A20, A95, Th33;
verum
end;
for i being Nat holds S1[i]
from NAT_1:sch 2(A1, A14);
hence
for i being Nat
for S, E, F, G being RealNormSpace
for Z being Subset of S
for B being Lipschitzian BilinearOperator of E,F,G
for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for W being PartFunc of S,G st W = B * w & w = <:u,v:> & u is_differentiable_on i,Z & diff (u,i,Z) is_continuous_on Z & v is_differentiable_on i,Z & diff (v,i,Z) is_continuous_on Z holds
( W is_differentiable_on i,Z & diff (W,i,Z) is_continuous_on Z )
; verum