let X be RealNormSpace-Sequence; :: thesis: for Y being RealNormSpace

for f being MultilinearOperator of X,Y

for K being Real st 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) holds

for v0, v1 being Point of (product X)

for Cv0, Cv1 being FinSequence

for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds

Cv1 . j = Cv0 . j ) holds

||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||

let Y be RealNormSpace; :: thesis: for f being MultilinearOperator of X,Y

for K being Real st 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) holds

for v0, v1 being Point of (product X)

for Cv0, Cv1 being FinSequence

for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds

Cv1 . j = Cv0 . j ) holds

||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||

let f be MultilinearOperator of X,Y; :: thesis: for K being Real st 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) holds

for v0, v1 being Point of (product X)

for Cv0, Cv1 being FinSequence

for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds

Cv1 . j = Cv0 . j ) holds

||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||

let K be Real; :: thesis: ( 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) implies for v0, v1 being Point of (product X)

for Cv0, Cv1 being FinSequence

for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds

Cv1 . j = Cv0 . j ) holds

||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).|| )

assume A1: ( 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) ) ; :: thesis: for v0, v1 being Point of (product X)

for Cv0, Cv1 being FinSequence

for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds

Cv1 . j = Cv0 . j ) holds

||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||

let v0, v1 be Point of (product X); :: thesis: for Cv0, Cv1 being FinSequence

for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds

Cv1 . j = Cv0 . j ) holds

||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||

let Cv0, Cv1 be FinSequence; :: thesis: for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds

Cv1 . j = Cv0 . j ) holds

||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||

let i be Element of dom X; :: thesis: ( Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds

Cv1 . j = Cv0 . j ) implies ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).|| )

assume A2: ( Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds

Cv1 . j = Cv0 . j ) ) ; :: thesis: ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||

( f is Function of (product X),Y & f is Multilinear ) ;

then A3: f * (reproj (i,v0)) is LinearOperator of (X . i),Y ;

A4: product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;

then A5: ex g being Function st

( Cv1 = g & dom g = dom (carr X) & ( for i being object st i in dom (carr X) holds

g . i in (carr X) . i ) ) by A2, CARD_3:def 5;

A6: ex g being Function st

( (reproj (i,v0)) . (v1 . i) = g & dom g = dom (carr X) & ( for i being object st i in dom (carr X) holds

g . i in (carr X) . i ) ) by A4, CARD_3:def 5;

for x being object st x in dom v1 holds

v1 . x = ((reproj (i,v0)) . (v1 . i)) . x

reconsider v3 = (reproj (i,v0)) . ((v1 . i) - (v0 . i)) as Point of (product X) ;

(f /. v1) - (f /. v0) = (f . ((reproj (i,v0)) . (v1 . i))) - (f . ((reproj (i,v0)) . (v0 . i))) by A10, LOPBAN10:17

.= ((f * (reproj (i,v0))) . (v1 . i)) - (f . ((reproj (i,v0)) . (v0 . i))) by FUNCT_2:15

.= ((f * (reproj (i,v0))) . (v1 . i)) - ((f * (reproj (i,v0))) . (v0 . i)) by FUNCT_2:15

.= ((f * (reproj (i,v0))) . (v1 . i)) + ((- 1) * ((f * (reproj (i,v0))) . (v0 . i))) by RLVECT_1:16

.= ((f * (reproj (i,v0))) . (v1 . i)) + ((f * (reproj (i,v0))) . ((- 1) * (v0 . i))) by A3, LOPBAN_1:def 5

.= (f * (reproj (i,v0))) . ((v1 . i) + ((- 1) * (v0 . i))) by A3, VECTSP_1:def 20

.= (f * (reproj (i,v0))) . ((v1 . i) - (v0 . i)) by RLVECT_1:16

.= f . v3 by FUNCT_2:15 ;

then A12: ||.((f /. v1) - (f /. v0)).|| <= K * (NrProduct v3) by A1;

1 is Element of REAL by XREAL_0:def 1;

then reconsider R1 = (len X) |-> 1 as FinSequence of REAL by FINSEQ_2:63;

A13: dom R1 = Seg (len X) by FUNCT_2:def 1;

i in dom X ;

then A14: i in dom R1 by A13, FINSEQ_1:def 3;

reconsider Nv1v0 = ||.((v1 - v0) . i).|| as Element of REAL ;

reconsider R2 = R1 +* (i,Nv1v0) as FinSequence of REAL ;

||.v0.|| + 1 is Element of REAL by XREAL_0:def 1;

then reconsider R3 = (len X) |-> (||.v0.|| + 1) as FinSequence of REAL by FINSEQ_2:63;

set R4 = mlt (R2,R3);

dom R2 = dom R1 by FUNCT_7:30;

then ( dom R2 = Seg (len X) & dom R3 = Seg (len X) ) by FUNCT_2:def 1;

then A15: ( len R2 = len X & len R3 = len X ) by FINSEQ_1:def 3;

then ( R2 is Element of (len X) -tuples_on REAL & R3 is Element of (len X) -tuples_on REAL ) by FINSEQ_2:92;

then A16: Product (mlt (R2,R3)) = (Product R2) * (Product R3) by RVSUM_1:107;

A17: Product R2 = ||.((v1 - v0) . i).|| by A14, LM03;

A18: Product R3 = (||.v0.|| + 1) to_power (len X) by NAT_4:55

.= (||.v0.|| + 1) |^ (len X) ;

consider Nx being FinSequence of REAL such that

A19: ( dom Nx = dom X & ( for i being Element of dom X holds Nx . i = ||.(v3 . i).|| ) & NrProduct v3 = Product Nx ) by LOPBAN10:def 9;

dom Nx = Seg (len X) by A19, FINSEQ_1:def 3;

then A20: len Nx = len X by FINSEQ_1:def 3;

dom (mlt (R2,R3)) = (dom R2) /\ (dom R3) by VALUED_1:def 4

.= (Seg (len R2)) /\ (dom R3) by FINSEQ_1:def 3

.= (Seg (len R2)) /\ (Seg (len R3)) by FINSEQ_1:def 3

.= Seg (len X) by A15 ;

then A21: len (mlt (R2,R3)) = len X by FINSEQ_1:def 3;

for k being Element of NAT st k in dom Nx holds

( Nx . k <= (mlt (R2,R3)) . k & 0 <= Nx . k )

then K * (NrProduct v3) <= K * (((||.v0.|| + 1) |^ (len X)) * ||.((v1 - v0) . i).||) by A1, XREAL_1:66;

hence ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).|| by A12, XXREAL_0:2; :: thesis: verum

for f being MultilinearOperator of X,Y

for K being Real st 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) holds

for v0, v1 being Point of (product X)

for Cv0, Cv1 being FinSequence

for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds

Cv1 . j = Cv0 . j ) holds

||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||

let Y be RealNormSpace; :: thesis: for f being MultilinearOperator of X,Y

for K being Real st 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) holds

for v0, v1 being Point of (product X)

for Cv0, Cv1 being FinSequence

for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds

Cv1 . j = Cv0 . j ) holds

||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||

let f be MultilinearOperator of X,Y; :: thesis: for K being Real st 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) holds

for v0, v1 being Point of (product X)

for Cv0, Cv1 being FinSequence

for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds

Cv1 . j = Cv0 . j ) holds

||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||

let K be Real; :: thesis: ( 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) implies for v0, v1 being Point of (product X)

for Cv0, Cv1 being FinSequence

for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds

Cv1 . j = Cv0 . j ) holds

||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).|| )

assume A1: ( 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) ) ; :: thesis: for v0, v1 being Point of (product X)

for Cv0, Cv1 being FinSequence

for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds

Cv1 . j = Cv0 . j ) holds

||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||

let v0, v1 be Point of (product X); :: thesis: for Cv0, Cv1 being FinSequence

for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds

Cv1 . j = Cv0 . j ) holds

||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||

let Cv0, Cv1 be FinSequence; :: thesis: for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds

Cv1 . j = Cv0 . j ) holds

||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||

let i be Element of dom X; :: thesis: ( Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds

Cv1 . j = Cv0 . j ) implies ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).|| )

assume A2: ( Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds

Cv1 . j = Cv0 . j ) ) ; :: thesis: ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||

( f is Function of (product X),Y & f is Multilinear ) ;

then A3: f * (reproj (i,v0)) is LinearOperator of (X . i),Y ;

A4: product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;

then A5: ex g being Function st

( Cv1 = g & dom g = dom (carr X) & ( for i being object st i in dom (carr X) holds

g . i in (carr X) . i ) ) by A2, CARD_3:def 5;

A6: ex g being Function st

( (reproj (i,v0)) . (v1 . i) = g & dom g = dom (carr X) & ( for i being object st i in dom (carr X) holds

g . i in (carr X) . i ) ) by A4, CARD_3:def 5;

for x being object st x in dom v1 holds

v1 . x = ((reproj (i,v0)) . (v1 . i)) . x

proof

then A10:
v1 = (reproj (i,v0)) . (v1 . i)
by A2, A5, A6, FUNCT_1:2;
let x be object ; :: thesis: ( x in dom v1 implies v1 . x = ((reproj (i,v0)) . (v1 . i)) . x )

assume x in dom v1 ; :: thesis: v1 . x = ((reproj (i,v0)) . (v1 . i)) . x

then reconsider j = x as Element of dom X by A2, A5, DCARXX;

end;assume x in dom v1 ; :: thesis: v1 . x = ((reproj (i,v0)) . (v1 . i)) . x

then reconsider j = x as Element of dom X by A2, A5, DCARXX;

reconsider v3 = (reproj (i,v0)) . ((v1 . i) - (v0 . i)) as Point of (product X) ;

(f /. v1) - (f /. v0) = (f . ((reproj (i,v0)) . (v1 . i))) - (f . ((reproj (i,v0)) . (v0 . i))) by A10, LOPBAN10:17

.= ((f * (reproj (i,v0))) . (v1 . i)) - (f . ((reproj (i,v0)) . (v0 . i))) by FUNCT_2:15

.= ((f * (reproj (i,v0))) . (v1 . i)) - ((f * (reproj (i,v0))) . (v0 . i)) by FUNCT_2:15

.= ((f * (reproj (i,v0))) . (v1 . i)) + ((- 1) * ((f * (reproj (i,v0))) . (v0 . i))) by RLVECT_1:16

.= ((f * (reproj (i,v0))) . (v1 . i)) + ((f * (reproj (i,v0))) . ((- 1) * (v0 . i))) by A3, LOPBAN_1:def 5

.= (f * (reproj (i,v0))) . ((v1 . i) + ((- 1) * (v0 . i))) by A3, VECTSP_1:def 20

.= (f * (reproj (i,v0))) . ((v1 . i) - (v0 . i)) by RLVECT_1:16

.= f . v3 by FUNCT_2:15 ;

then A12: ||.((f /. v1) - (f /. v0)).|| <= K * (NrProduct v3) by A1;

1 is Element of REAL by XREAL_0:def 1;

then reconsider R1 = (len X) |-> 1 as FinSequence of REAL by FINSEQ_2:63;

A13: dom R1 = Seg (len X) by FUNCT_2:def 1;

i in dom X ;

then A14: i in dom R1 by A13, FINSEQ_1:def 3;

reconsider Nv1v0 = ||.((v1 - v0) . i).|| as Element of REAL ;

reconsider R2 = R1 +* (i,Nv1v0) as FinSequence of REAL ;

||.v0.|| + 1 is Element of REAL by XREAL_0:def 1;

then reconsider R3 = (len X) |-> (||.v0.|| + 1) as FinSequence of REAL by FINSEQ_2:63;

set R4 = mlt (R2,R3);

dom R2 = dom R1 by FUNCT_7:30;

then ( dom R2 = Seg (len X) & dom R3 = Seg (len X) ) by FUNCT_2:def 1;

then A15: ( len R2 = len X & len R3 = len X ) by FINSEQ_1:def 3;

then ( R2 is Element of (len X) -tuples_on REAL & R3 is Element of (len X) -tuples_on REAL ) by FINSEQ_2:92;

then A16: Product (mlt (R2,R3)) = (Product R2) * (Product R3) by RVSUM_1:107;

A17: Product R2 = ||.((v1 - v0) . i).|| by A14, LM03;

A18: Product R3 = (||.v0.|| + 1) to_power (len X) by NAT_4:55

.= (||.v0.|| + 1) |^ (len X) ;

consider Nx being FinSequence of REAL such that

A19: ( dom Nx = dom X & ( for i being Element of dom X holds Nx . i = ||.(v3 . i).|| ) & NrProduct v3 = Product Nx ) by LOPBAN10:def 9;

dom Nx = Seg (len X) by A19, FINSEQ_1:def 3;

then A20: len Nx = len X by FINSEQ_1:def 3;

dom (mlt (R2,R3)) = (dom R2) /\ (dom R3) by VALUED_1:def 4

.= (Seg (len R2)) /\ (dom R3) by FINSEQ_1:def 3

.= (Seg (len R2)) /\ (Seg (len R3)) by FINSEQ_1:def 3

.= Seg (len X) by A15 ;

then A21: len (mlt (R2,R3)) = len X by FINSEQ_1:def 3;

for k being Element of NAT st k in dom Nx holds

( Nx . k <= (mlt (R2,R3)) . k & 0 <= Nx . k )

proof

then
NrProduct v3 <= ||.((v1 - v0) . i).|| * ((||.v0.|| + 1) |^ (len X))
by A16, A17, A18, A19, A20, A21, FINSEQ_9:34;
let k be Element of NAT ; :: thesis: ( k in dom Nx implies ( Nx . k <= (mlt (R2,R3)) . k & 0 <= Nx . k ) )

assume k in dom Nx ; :: thesis: ( Nx . k <= (mlt (R2,R3)) . k & 0 <= Nx . k )

then A22: k in Seg (len Nx) by FINSEQ_1:def 3;

then reconsider j = k as Element of dom X by A20, FINSEQ_1:def 3;

A24: Nx . k = ||.(v3 . j).|| by A19;

A26: (mlt (R2,R3)) . k = (R2 . k) * (R3 . j) by RVSUM_1:60

.= (R2 . k) * (||.v0.|| + 1) by A20, A22, FUNCOP_1:7 ;

end;assume k in dom Nx ; :: thesis: ( Nx . k <= (mlt (R2,R3)) . k & 0 <= Nx . k )

then A22: k in Seg (len Nx) by FINSEQ_1:def 3;

then reconsider j = k as Element of dom X by A20, FINSEQ_1:def 3;

A24: Nx . k = ||.(v3 . j).|| by A19;

A26: (mlt (R2,R3)) . k = (R2 . k) * (R3 . j) by RVSUM_1:60

.= (R2 . k) * (||.v0.|| + 1) by A20, A22, FUNCOP_1:7 ;

now :: thesis: Nx . k <= (mlt (R2,R3)) . kend;

hence
( Nx . k <= (mlt (R2,R3)) . k & 0 <= Nx . k )
by A24; :: thesis: verumper cases
( j = i or j <> i )
;

end;

suppose A27:
j = i
; :: thesis: Nx . k <= (mlt (R2,R3)) . k

v3 . j =
(v1 . i) - (v0 . i)
by A27, LOPBAN10:15

.= (v1 - v0) . i by LOPBAN10:26 ;

then A29: Nx . k = ||.((v1 - v0) . i).|| by A19, A27;

1 + 0 <= ||.v0.|| + 1 by XREAL_1:7;

then ||.((v1 - v0) . i).|| * 1 <= ||.((v1 - v0) . i).|| * (||.v0.|| + 1) by XREAL_1:66;

hence Nx . k <= (mlt (R2,R3)) . k by A13, A20, A22, A26, A27, A29, FUNCT_7:31; :: thesis: verum

end;.= (v1 - v0) . i by LOPBAN10:26 ;

then A29: Nx . k = ||.((v1 - v0) . i).|| by A19, A27;

1 + 0 <= ||.v0.|| + 1 by XREAL_1:7;

then ||.((v1 - v0) . i).|| * 1 <= ||.((v1 - v0) . i).|| * (||.v0.|| + 1) by XREAL_1:66;

hence Nx . k <= (mlt (R2,R3)) . k by A13, A20, A22, A26, A27, A29, FUNCT_7:31; :: thesis: verum

suppose A30:
j <> i
; :: thesis: Nx . k <= (mlt (R2,R3)) . k

then A31: R2 . k =
R1 . j
by FUNCT_7:32

.= 1 by A20, A22, FUNCOP_1:7 ;

||.(v0 . j).|| <= ||.v0.|| by A4, PRVECT_2:10;

then ||.(v0 . j).|| + 0 <= ||.v0.|| + 1 by XREAL_1:7;

hence Nx . k <= (mlt (R2,R3)) . k by A24, A26, A30, A31, LOPBAN10:16; :: thesis: verum

end;.= 1 by A20, A22, FUNCOP_1:7 ;

||.(v0 . j).|| <= ||.v0.|| by A4, PRVECT_2:10;

then ||.(v0 . j).|| + 0 <= ||.v0.|| + 1 by XREAL_1:7;

hence Nx . k <= (mlt (R2,R3)) . k by A24, A26, A30, A31, LOPBAN10:16; :: thesis: verum

then K * (NrProduct v3) <= K * (((||.v0.|| + 1) |^ (len X)) * ||.((v1 - v0) . i).||) by A1, XREAL_1:66;

hence ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).|| by A12, XXREAL_0:2; :: thesis: verum