let V be non empty MetrSpace; ( V is convex implies for x, y being Element of V
for p being Real st p > 0 holds
ex f being FinSequence of the carrier of V st
( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds
dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist ((f /. i),(f /. (i + 1))) ) holds
dist (x,y) = Sum F ) ) )
assume A1:
V is convex
; for x, y being Element of V
for p being Real st p > 0 holds
ex f being FinSequence of the carrier of V st
( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds
dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist ((f /. i),(f /. (i + 1))) ) holds
dist (x,y) = Sum F ) )
set A = the carrier of V;
let x, y be Element of V; for p being Real st p > 0 holds
ex f being FinSequence of the carrier of V st
( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds
dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist ((f /. i),(f /. (i + 1))) ) holds
dist (x,y) = Sum F ) )
defpred S1[ set , set , set ] means for a1, a2 being Element of the carrier of V st $1 = [a1,a2] holds
ex b being Element of the carrier of V st
( $2 = [a1,b] & $3 = [b,a2] & dist (a1,a2) = 2 * (dist (a1,b)) & dist (a1,a2) = 2 * (dist (b,a2)) );
A2:
for a being Element of [: the carrier of V, the carrier of V:] ex c, d being Element of [: the carrier of V, the carrier of V:] st S1[a,c,d]
proof
let a be
Element of
[: the carrier of V, the carrier of V:];
ex c, d being Element of [: the carrier of V, the carrier of V:] st S1[a,c,d]
consider a19,
a29 being
object such that A3:
(
a19 in the
carrier of
V &
a29 in the
carrier of
V )
and A4:
a = [a19,a29]
by ZFMISC_1:def 2;
reconsider a19 =
a19,
a29 =
a29 as
Element of the
carrier of
V by A3;
consider z being
Element of the
carrier of
V such that A5:
dist (
a19,
z)
= (1 / 2) * (dist (a19,a29))
and A6:
dist (
z,
a29)
= (1 - (1 / 2)) * (dist (a19,a29))
by A1;
take c =
[a19,z];
ex d being Element of [: the carrier of V, the carrier of V:] st S1[a,c,d]
take d =
[z,a29];
S1[a,c,d]
let a1,
a2 be
Element of the
carrier of
V;
( a = [a1,a2] implies ex b being Element of the carrier of V st
( c = [a1,b] & d = [b,a2] & dist (a1,a2) = 2 * (dist (a1,b)) & dist (a1,a2) = 2 * (dist (b,a2)) ) )
assume A7:
a = [a1,a2]
;
ex b being Element of the carrier of V st
( c = [a1,b] & d = [b,a2] & dist (a1,a2) = 2 * (dist (a1,b)) & dist (a1,a2) = 2 * (dist (b,a2)) )
take
z
;
( c = [a1,z] & d = [z,a2] & dist (a1,a2) = 2 * (dist (a1,z)) & dist (a1,a2) = 2 * (dist (z,a2)) )
thus
c = [a1,z]
by A4, A7, XTUPLE_0:1;
( d = [z,a2] & dist (a1,a2) = 2 * (dist (a1,z)) & dist (a1,a2) = 2 * (dist (z,a2)) )
thus
d = [z,a2]
by A4, A7, XTUPLE_0:1;
( dist (a1,a2) = 2 * (dist (a1,z)) & dist (a1,a2) = 2 * (dist (z,a2)) )
a1 = a19
by A4, A7, XTUPLE_0:1;
hence
dist (
a1,
a2)
= 2
* (dist (a1,z))
by A4, A5, A7, XTUPLE_0:1;
dist (a1,a2) = 2 * (dist (z,a2))
a2 = a29
by A4, A7, XTUPLE_0:1;
hence
dist (
a1,
a2)
= 2
* (dist (z,a2))
by A4, A6, A7, XTUPLE_0:1;
verum
end;
consider D being binary DecoratedTree of [: the carrier of V, the carrier of V:] such that
A8:
dom D = {0,1} *
and
A9:
D . {} = [x,y]
and
A10:
for z being Node of D holds S1[D . z,D . (z ^ <*0*>),D . (z ^ <*1*>)]
from BINTREE2:sch 1(A2);
reconsider dD = dom D as full Tree by A8, BINTREE2:def 2;
let p be Real; ( p > 0 implies ex f being FinSequence of the carrier of V st
( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds
dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist ((f /. i),(f /. (i + 1))) ) holds
dist (x,y) = Sum F ) ) )
assume A11:
p > 0
; ex f being FinSequence of the carrier of V st
( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds
dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist ((f /. i),(f /. (i + 1))) ) holds
dist (x,y) = Sum F ) )
per cases
( dist (x,y) >= p or dist (x,y) < p )
;
suppose
dist (
x,
y)
>= p
;
ex f being FinSequence of the carrier of V st
( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds
dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist ((f /. i),(f /. (i + 1))) ) holds
dist (x,y) = Sum F ) )then
(dist (x,y)) / p >= 1
by A11, XREAL_1:181;
then
log (2,
((dist (x,y)) / p))
>= log (2,1)
by PRE_FF:10;
then
log (2,
((dist (x,y)) / p))
>= 0
by POWER:51;
then reconsider n1 =
[\(log (2,((dist (x,y)) / p)))/] as
Element of
NAT by INT_1:53;
defpred S2[
Nat]
means for
t being
Tuple of $1,
BOOLEAN st
t = 0* $1 holds
(D . ('not' t)) `2 = y;
defpred S3[
Nat]
means (D . (0* $1)) `1 = x;
reconsider n =
n1 + 1 as non
zero Element of
NAT ;
reconsider N = 2
to_power n as non
zero Element of
NAT by POWER:34;
set r =
(dist (x,y)) / N;
reconsider FSL =
FinSeqLevel (
n,
dD) as
FinSequence of
dom D by FINSEQ_2:24;
deffunc H1(
Nat)
-> Element of
[: the carrier of V, the carrier of V:] =
D . (FSL /. $1);
consider g being
FinSequence of
[: the carrier of V, the carrier of V:] such that A12:
len g = N
and A13:
for
k being
Nat st
k in dom g holds
g . k = H1(
k)
from FINSEQ_2:sch 1();
A14:
dom g = Seg N
by A12, FINSEQ_1:def 3;
A15:
for
j being
Nat st
S3[
j] holds
S3[
j + 1]
proof
let j be
Nat;
( S3[j] implies S3[j + 1] )
assume A16:
(D . (0* j)) `1 = x
;
S3[j + 1]
reconsider zj =
0* j as
Node of
D by A8, BINARI_3:4;
consider a,
b being
object such that A17:
(
a in the
carrier of
V &
b in the
carrier of
V )
and A18:
D . zj = [a,b]
by ZFMISC_1:def 2;
reconsider a1 =
a,
b1 =
b as
Element of the
carrier of
V by A17;
A19:
ex
z1 being
Element of the
carrier of
V st
(
D . (zj ^ <*0*>) = [a1,z1] &
D . (zj ^ <*1*>) = [z1,b1] &
dist (
a1,
b1)
= 2
* (dist (a1,z1)) &
dist (
a1,
b1)
= 2
* (dist (z1,b1)) )
by A10, A18;
thus (D . (0* (j + 1))) `1 =
(D . (zj ^ <*0*>)) `1
by FINSEQ_2:60
.=
a1
by A19
.=
x
by A18, A16
;
verum
end; A20:
S3[
0 ]
by A9;
A21:
for
j being
Nat holds
S3[
j]
from NAT_1:sch 2(A20, A15);
2
to_power n > 0
by POWER:34;
then
0 + 1
<= 2
to_power n
by NAT_1:13;
then A22:
1
<= len (FinSeqLevel (n,dD))
by BINTREE2:19;
A23:
for
j being non
zero Nat st
S2[
j] holds
S2[
j + 1]
proof
let j be non
zero Nat;
( S2[j] implies S2[j + 1] )
assume A24:
for
t being
Tuple of
j,
BOOLEAN st
t = 0* j holds
(D . ('not' t)) `2 = y
;
S2[j + 1]
let t be
Tuple of
j + 1,
BOOLEAN ;
( t = 0* (j + 1) implies (D . ('not' t)) `2 = y )
consider t1 being
Element of
j -tuples_on BOOLEAN,
dd being
Element of
BOOLEAN such that A25:
t = t1 ^ <*dd*>
by FINSEQ_2:117;
assume A26:
t = 0* (j + 1)
;
(D . ('not' t)) `2 = y
then
t = (0* j) ^ <*0*>
by FINSEQ_2:60;
then
t1 = 0* j
by A25, FINSEQ_2:17;
then A27:
(D . ('not' t1)) `2 = y
by A24;
dd =
t . ((len t1) + 1)
by A25, FINSEQ_1:42
.=
((j + 1) |-> 0) . (j + 1)
by A26
.=
FALSE
;
then
'not' dd = 1
;
then A28:
'not' t = ('not' t1) ^ <*1*>
by A25, BINARI_2:9;
reconsider nt1 =
'not' t1 as
Node of
D by A8, FINSEQ_1:def 11;
consider a,
b being
object such that A29:
(
a in the
carrier of
V &
b in the
carrier of
V )
and A30:
D . nt1 = [a,b]
by ZFMISC_1:def 2;
reconsider a1 =
a,
b1 =
b as
Element of the
carrier of
V by A29;
ex
b being
Element of the
carrier of
V st
(
D . (nt1 ^ <*0*>) = [a1,b] &
D . (nt1 ^ <*1*>) = [b,b1] &
dist (
a1,
b1)
= 2
* (dist (a1,b)) &
dist (
a1,
b1)
= 2
* (dist (b,b1)) )
by A10, A30;
hence (D . ('not' t)) `2 =
b1
by A28
.=
y
by A30, A27
;
verum
end; A31:
S2[1]
proof
reconsider pusty =
<*> {0,1} as
Node of
D by A8, FINSEQ_1:def 11;
let t be
Tuple of 1,
BOOLEAN ;
( t = 0* 1 implies (D . ('not' t)) `2 = y )
A32:
ex
b being
Element of the
carrier of
V st
(
D . (pusty ^ <*0*>) = [x,b] &
D . (pusty ^ <*1*>) = [b,y] &
dist (
x,
y)
= 2
* (dist (x,b)) &
dist (
x,
y)
= 2
* (dist (b,y)) )
by A9, A10;
assume
t = 0* 1
;
(D . ('not' t)) `2 = y
then
t = <*FALSE*>
by FINSEQ_2:59;
hence (D . ('not' t)) `2 =
(D . (pusty ^ <*1*>)) `2
by BINARI_3:14, FINSEQ_1:34
.=
y
by A32
;
verum
end; A33:
for
j being non
zero Nat holds
S2[
j]
from NAT_1:sch 10(A31, A23);
deffunc H2(
Nat)
-> Element of the
carrier of
V =
(g /. $1) `1 ;
consider h being
FinSequence of the
carrier of
V such that A34:
len h = N
and A35:
for
k being
Nat st
k in dom h holds
h . k = H2(
k)
from FINSEQ_2:sch 1();
A36:
dom h = Seg N
by A34, FINSEQ_1:def 3;
A37:
1
<= N
by NAT_1:14;
then A38:
1
in Seg N
by FINSEQ_1:1;
then A39:
1
in dom h
by A34, FINSEQ_1:def 3;
take f =
h ^ <*y*>;
( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds
dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist ((f /. i),(f /. (i + 1))) ) holds
dist (x,y) = Sum F ) )A40:
len f =
(len h) + (len <*y*>)
by FINSEQ_1:22
.=
(len h) + 1
by FINSEQ_1:39
;
1
<= N + 1
by NAT_1:11;
hence f /. 1 =
f . 1
by A34, A40, FINSEQ_4:15
.=
h . 1
by A39, FINSEQ_1:def 7
.=
(g /. 1) `1
by A35, A36, A38
.=
(g . 1) `1
by A12, A37, FINSEQ_4:15
.=
(D . (FSL /. 1)) `1
by A13, A14, A38
.=
(D . ((FinSeqLevel (n,dD)) . 1)) `1
by A22, FINSEQ_4:15
.=
(D . (0* n)) `1
by BINTREE2:15
.=
x
by A21
;
( f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds
dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist ((f /. i),(f /. (i + 1))) ) holds
dist (x,y) = Sum F ) )
len f in Seg (len f)
by A40, FINSEQ_1:4;
then
len f in dom f
by FINSEQ_1:def 3;
hence A41:
f /. (len f) =
(h ^ <*y*>) . ((len h) + 1)
by A40, PARTFUN1:def 6
.=
y
by FINSEQ_1:42
;
( ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds
dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist ((f /. i),(f /. (i + 1))) ) holds
dist (x,y) = Sum F ) )A42:
for
i being
Element of
NAT st 1
<= i &
i <= (len f) - 1 holds
dist (
(f /. i),
(f /. (i + 1)))
= (dist (x,y)) / N
proof
0* n in BOOLEAN *
by BINARI_3:4;
then reconsider ze =
0* n as
Tuple of
n,
BOOLEAN by FINSEQ_1:def 11;
reconsider ze =
ze as
Element of
n -tuples_on BOOLEAN by FINSEQ_2:131;
defpred S4[ non
zero Nat]
means for
j being non
zero Element of
NAT st
j <= 2
to_power $1 holds
for
DF1,
DF2 being
Element of
V st
DF1 = (D . ((FinSeqLevel ($1,dD)) . j)) `1 &
DF2 = (D . ((FinSeqLevel ($1,dD)) . j)) `2 holds
dist (
DF1,
DF2)
= (dist (x,y)) / (2 to_power $1);
let i be
Element of
NAT ;
( 1 <= i & i <= (len f) - 1 implies dist ((f /. i),(f /. (i + 1))) = (dist (x,y)) / N )
assume that A43:
1
<= i
and A44:
i <= (len f) - 1
;
dist ((f /. i),(f /. (i + 1))) = (dist (x,y)) / N
A45:
len FSL = N
by BINTREE2:19;
A46:
now f /. (i + 1) = (D . ((FinSeqLevel (n,dD)) . i)) `2 per cases
( i < (len f) - 1 or i = (len f) - 1 )
by A44, XXREAL_0:1;
suppose
i < (len f) - 1
;
f /. (i + 1) = (D . ((FinSeqLevel (n,dD)) . i)) `2 then
i < (len f) -' 1
by A40, NAT_1:11, XREAL_1:233;
then
i + 1
<= (len f) -' 1
by NAT_1:13;
then A47:
i + 1
<= (len f) - 1
by A40, NAT_1:11, XREAL_1:233;
then A48:
(i + 1) - 1
<= (2 to_power n) - 1
by A34, A40, XREAL_1:9;
defpred S5[ non
zero Nat]
means for
i being
Nat st 1
<= i &
i <= (2 to_power $1) - 1 holds
(D . ((FinSeqLevel ($1,dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ($1,dD)) . i)) `2 ;
A49:
for
n being non
zero Nat st
S5[
n] holds
S5[
n + 1]
proof
let n be non
zero Nat;
( S5[n] implies S5[n + 1] )
reconsider nn =
n as non
zero Element of
NAT by ORDINAL1:def 12;
reconsider zb =
dD -level n as non
empty set by A8, BINTREE2:10;
assume A50:
for
i being
Nat st 1
<= i &
i <= (2 to_power n) - 1 holds
(D . ((FinSeqLevel (n,dD)) . (i + 1))) `1 = (D . ((FinSeqLevel (n,dD)) . i)) `2
;
S5[n + 1]
let i be
Nat;
( 1 <= i & i <= (2 to_power (n + 1)) - 1 implies (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . i)) `2 )
assume that A51:
1
<= i
and A52:
i <= (2 to_power (n + 1)) - 1
;
(D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . i)) `2
reconsider ii =
i as
Element of
NAT by ORDINAL1:def 12;
A53:
1
+ 1
<= i + 1
by A51, XREAL_1:6;
then A54:
(i + 1) div 2
>= 1
by NAT_2:13;
2
to_power (n + 1) > 0
by POWER:34;
then A55:
2
to_power (n + 1) >= 0 + 1
by NAT_1:13;
then
i <= (2 to_power (n + 1)) -' 1
by A52, XREAL_1:233;
then
i < ((2 to_power (n + 1)) -' 1) + 1
by NAT_1:13;
then A56:
i < ((2 to_power (n + 1)) - 1) + 1
by A55, XREAL_1:233;
then A57:
i + 1
<= 2
to_power (n + 1)
by NAT_1:13;
then
i + 1
<= (2 to_power n) * (2 to_power 1)
by POWER:27;
then
i + 1
<= (2 to_power n) * 2
by POWER:25;
then A58:
((i + 1) + 1) div 2
<= 2
to_power n
by NAT_2:25;
i + 1
<= (i + 1) + 1
by NAT_1:11;
then
2
<= (i + 1) + 1
by A53, XXREAL_0:2;
then
((i + 1) + 1) div 2
>= 1
by NAT_2:13;
then
((i + 1) + 1) div 2
in Seg (2 to_power n)
by A58, FINSEQ_1:1;
then
((i + 1) + 1) div 2
in dom (FinSeqLevel (nn,dD))
by BINTREE2:20;
then
(FinSeqLevel (n,dD)) . (((i + 1) + 1) div 2) in zb
by FINSEQ_2:11;
then reconsider FF =
(FinSeqLevel (nn,dD)) . (((i + 1) + 1) div 2) as
Tuple of
n,
BOOLEAN by BINTREE2:5;
reconsider FF =
FF as
Element of
n -tuples_on BOOLEAN by FINSEQ_2:131;
reconsider FF1 =
FF as
Node of
D by A8, FINSEQ_1:def 11;
consider a9,
b9 being
object such that A59:
(
a9 in the
carrier of
V &
b9 in the
carrier of
V )
and A60:
D . FF1 = [a9,b9]
by ZFMISC_1:def 2;
i <= (2 to_power n) * (2 to_power 1)
by A56, POWER:27;
then
i <= (2 to_power n) * 2
by POWER:25;
then
(i + 1) div 2
<= 2
to_power n
by NAT_2:25;
then
(i + 1) div 2
in Seg (2 to_power n)
by A54, FINSEQ_1:1;
then
(i + 1) div 2
in dom (FinSeqLevel (nn,dD))
by BINTREE2:20;
then
(FinSeqLevel (n,dD)) . ((i + 1) div 2) in zb
by FINSEQ_2:11;
then reconsider F =
(FinSeqLevel (nn,dD)) . ((i + 1) div 2) as
Tuple of
n,
BOOLEAN by BINTREE2:5;
reconsider F =
F as
Element of
n -tuples_on BOOLEAN by FINSEQ_2:131;
reconsider F1 =
F as
Node of
D by A8, FINSEQ_1:def 11;
consider a,
b being
object such that A61:
(
a in the
carrier of
V &
b in the
carrier of
V )
and A62:
D . F1 = [a,b]
by ZFMISC_1:def 2;
reconsider a1 =
a,
b1 =
b,
a19 =
a9,
b19 =
b9 as
Element of the
carrier of
V by A61, A59;
consider d being
Element of the
carrier of
V such that A63:
D . (F1 ^ <*0*>) = [a1,d]
and A64:
D . (F1 ^ <*1*>) = [d,b1]
and
dist (
a1,
b1)
= 2
* (dist (a1,d))
and
dist (
a1,
b1)
= 2
* (dist (d,b1))
by A10, A62;
consider d9 being
Element of the
carrier of
V such that A65:
D . (FF1 ^ <*0*>) = [a19,d9]
and A66:
D . (FF1 ^ <*1*>) = [d9,b19]
and
dist (
a19,
b19)
= 2
* (dist (a19,d9))
and
dist (
a19,
b19)
= 2
* (dist (d9,b19))
by A10, A60;
A67:
i =
(i + 1) - 1
.=
(i + 1) -' 1
by NAT_1:11, XREAL_1:233
;
now (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . ii)) `2 per cases
( i is odd or i is even )
;
suppose
i is
odd
;
(D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . ii)) `2 then A68:
i mod 2
= 1
by NAT_2:22;
then
(i + 1) mod 2
= 0
by A67, NAT_2:18;
then
i + 1 is
even
by NAT_2:21;
then
(i + 1) div 2
= ((i + 1) + 1) div 2
by NAT_2:26;
then A69:
d = d9
by A63, A65, XTUPLE_0:1;
thus (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 =
(D . (FF ^ <*(((2 * 1) + i) mod 2)*>)) `1
by A57, BINTREE2:24
.=
(D . (FF ^ <*1*>)) `1
by A68, NAT_D:21
.=
d
by A66, A69
.=
(D . (F ^ <*0*>)) `2
by A63
.=
(D . (F ^ <*((ii + 1) mod 2)*>)) `2
by A67, A68, NAT_2:18
.=
(D . ((FinSeqLevel ((n + 1),dD)) . ii)) `2
by A51, A56, BINTREE2:24
;
verum end; suppose
i is
even
;
(D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . ii)) `2 then A70:
i mod 2
= 0
by NAT_2:21;
then A71: 1 =
(i -' 1) mod 2
by A51, NAT_2:18
.=
((i -' 1) + (2 * 1)) mod 2
by NAT_D:21
.=
(((i -' 1) + 1) + 1) mod 2
.=
(i + 1) mod 2
by A51, XREAL_1:235
;
A72:
1
+ (1 + i) >= 1
by NAT_1:11;
(1 + 1) + (i -' 1) =
(1 + 1) + (i - 1)
by A51, XREAL_1:233
.=
((1 + 1) + i) - 1
;
then
1
= (((1 + 1) + i) -' 1) mod 2
by A71, A72, XREAL_1:233;
then
((1 + 1) + i) mod 2
= 0
by NAT_2:18;
then
(i + 1) + 1
= (2 * (((i + 1) + 1) div 2)) + 0
by NAT_D:2;
then A73:
2
divides (i + 1) + 1
by NAT_D:3;
1
<= (i + 1) + 1
by NAT_1:11;
then
(((i + 1) + 1) -' 1) div 2
= (((i + 1) + 1) div 2) - 1
by A73, NAT_2:15;
then
(i + 1) div 2
= (((i + 1) + 1) div 2) - 1
by NAT_D:34;
then A74:
((i + 1) div 2) + 1
= ((i + 1) + 1) div 2
;
then A75:
(i + 1) div 2
<= (2 to_power n) - 1
by A58, XREAL_1:19;
A76:
a9 =
(D . ((FinSeqLevel (n,dD)) . (((i + 1) + 1) div 2))) `1
by A60
.=
(D . ((FinSeqLevel (n,dD)) . ((i + 1) div 2))) `2
by A50, A54, A74, A75
.=
b
by A62
;
thus (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 =
(D . (FF ^ <*(((2 * 1) + i) mod 2)*>)) `1
by A57, BINTREE2:24
.=
(D . (FF ^ <*0*>)) `1
by A70, NAT_D:21
.=
a19
by A65
.=
(D . (F ^ <*1*>)) `2
by A64, A76
.=
(D . ((FinSeqLevel ((n + 1),dD)) . ii)) `2
by A51, A56, A71, BINTREE2:24
;
verum end; end; end;
hence
(D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . i)) `2
;
verum
end; A77:
S5[1]
proof
reconsider pusty =
<*> {0,1} as
Node of
D by A8, FINSEQ_1:def 11;
let i be
Nat;
( 1 <= i & i <= (2 to_power 1) - 1 implies (D . ((FinSeqLevel (1,dD)) . (i + 1))) `1 = (D . ((FinSeqLevel (1,dD)) . i)) `2 )
A78:
(2 to_power 1) - 1 =
(1 + 1) - 1
by POWER:25
.=
1
;
consider b being
Element of the
carrier of
V such that A79:
D . (pusty ^ <*0*>) = [x,b]
and A80:
D . (pusty ^ <*1*>) = [b,y]
and
dist (
x,
y)
= 2
* (dist (x,b))
and
dist (
x,
y)
= 2
* (dist (b,y))
by A9, A10;
assume
( 1
<= i &
i <= (2 to_power 1) - 1 )
;
(D . ((FinSeqLevel (1,dD)) . (i + 1))) `1 = (D . ((FinSeqLevel (1,dD)) . i)) `2
then A81:
i = 1
by A78, XXREAL_0:1;
hence (D . ((FinSeqLevel (1,dD)) . (i + 1))) `1 =
(D . <*1*>) `1
by BINTREE2:23
.=
(D . (pusty ^ <*1*>)) `1
by FINSEQ_1:34
.=
b
by A80
.=
(D . (pusty ^ <*0*>)) `2
by A79
.=
(D . <*0*>) `2
by FINSEQ_1:34
.=
(D . ((FinSeqLevel (1,dD)) . i)) `2
by A81, BINTREE2:22
;
verum
end; A82:
for
n being non
zero Nat holds
S5[
n]
from NAT_1:sch 10(A77, A49);
A83:
1
<= 1
+ i
by NAT_1:11;
then A84:
i + 1
in Seg (len h)
by A40, A47, FINSEQ_1:1;
then
i + 1
in dom h
by FINSEQ_1:def 3;
hence f /. (i + 1) =
h /. (i + 1)
by FINSEQ_4:68
.=
h . (i + 1)
by A40, A47, A83, FINSEQ_4:15
.=
(g /. (i + 1)) `1
by A34, A35, A36, A84
.=
(g . (i + 1)) `1
by A12, A34, A40, A47, A83, FINSEQ_4:15
.=
(D . (FSL /. (i + 1))) `1
by A13, A14, A34, A84
.=
(D . ((FinSeqLevel (n,dD)) . (i + 1))) `1
by A34, A40, A45, A47, A83, FINSEQ_4:15
.=
(D . ((FinSeqLevel (n,dD)) . i)) `2
by A43, A48, A82
;
verum end; end; end;
A86:
for
l being non
zero Nat st
S4[
l] holds
S4[
l + 1]
proof
let l be non
zero Nat;
( S4[l] implies S4[l + 1] )
reconsider dDll =
dD -level l as non
empty set by A8, BINTREE2:10;
reconsider ll =
l as non
zero Element of
NAT by ORDINAL1:def 12;
reconsider dDll1 =
dD -level (l + 1) as non
empty set by A8, BINTREE2:10;
assume A87:
for
j being non
zero Element of
NAT st
j <= 2
to_power l holds
for
DF1,
DF2 being
Element of
V st
DF1 = (D . ((FinSeqLevel (l,dD)) . j)) `1 &
DF2 = (D . ((FinSeqLevel (l,dD)) . j)) `2 holds
dist (
DF1,
DF2)
= (dist (x,y)) / (2 to_power l)
;
S4[l + 1]
let j be non
zero Element of
NAT ;
( j <= 2 to_power (l + 1) implies for DF1, DF2 being Element of V st DF1 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `2 holds
dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1)) )
(j + 1) div 2
<> 0
then reconsider j1 =
(j + 1) div 2 as non
zero Element of
NAT ;
assume A88:
j <= 2
to_power (l + 1)
;
for DF1, DF2 being Element of V st DF1 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `2 holds
dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1))
then
j <= (2 to_power l) * (2 to_power 1)
by POWER:27;
then A89:
j <= (2 to_power l) * 2
by POWER:25;
then
(
j1 >= 1 &
j1 <= 2
to_power l )
by NAT_1:14, NAT_2:25;
then
j1 in Seg (2 to_power l)
by FINSEQ_1:1;
then
(j + 1) div 2
in dom (FinSeqLevel (ll,dD))
by BINTREE2:20;
then
(FinSeqLevel (l,dD)) . ((j + 1) div 2) in dDll
by FINSEQ_2:11;
then reconsider FSLlprim =
(FinSeqLevel (ll,dD)) . ((j + 1) div 2) as
Tuple of
l,
BOOLEAN by BINTREE2:5;
reconsider FSLlprim =
FSLlprim as
Element of
l -tuples_on BOOLEAN by FINSEQ_2:131;
A90:
FinSeqLevel (
(l + 1),
dD) is
FinSequence of
dom D
by FINSEQ_2:24;
j >= 1
by NAT_1:14;
then
j in Seg (2 to_power (l + 1))
by A88, FINSEQ_1:1;
then A91:
j in dom (FinSeqLevel ((l + 1),dD))
by BINTREE2:20;
then reconsider Fj =
(FinSeqLevel ((l + 1),dD)) . j as
Element of
dom D by A90, FINSEQ_2:11;
(FinSeqLevel ((l + 1),dD)) . j in dDll1
by A91, FINSEQ_2:11;
then reconsider FSLl1 =
(FinSeqLevel ((l + 1),dD)) . j as
Tuple of
l + 1,
BOOLEAN by BINTREE2:5;
consider FSLl being
Element of
l -tuples_on BOOLEAN,
d being
Element of
BOOLEAN such that A92:
FSLl1 = FSLl ^ <*d*>
by FINSEQ_2:117;
let DF1,
DF2 be
Element of
V;
( DF1 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `2 implies dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1)) )
assume
(
DF1 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `1 &
DF2 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `2 )
;
dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1))
then A93:
D . Fj = [DF1,DF2]
by MCART_1:21;
reconsider NFSLl =
FSLl as
Node of
D by A8, FINSEQ_1:def 11;
consider x1,
y1 being
object such that A94:
(
x1 in the
carrier of
V &
y1 in the
carrier of
V )
and A95:
D . NFSLl = [x1,y1]
by ZFMISC_1:def 2;
reconsider x1 =
x1,
y1 =
y1 as
Element of the
carrier of
V by A94;
consider b being
Element of the
carrier of
V such that A96:
D . (NFSLl ^ <*0*>) = [x1,b]
and A97:
D . (NFSLl ^ <*1*>) = [b,y1]
and A98:
dist (
x1,
y1)
= 2
* (dist (x1,b))
and A99:
dist (
x1,
y1)
= 2
* (dist (b,y1))
by A10, A95;
A100:
(FinSeqLevel ((ll + 1),dD)) . j = FSLlprim ^ <*((j + 1) mod 2)*>
by A88, BINTREE2:24;
then
FSLl = FSLlprim
by A92, FINSEQ_2:17;
then A101:
(
x1 = (D . ((FinSeqLevel (l,dD)) . j1)) `1 &
y1 = (D . ((FinSeqLevel (l,dD)) . j1)) `2 )
by A95;
A102:
d = (j + 1) mod 2
by A92, A100, FINSEQ_2:17;
now dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1))per cases
( d = 0 or d = 1 )
by A102, NAT_D:12;
suppose
d = 0
;
dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1))then
(
DF1 = x1 &
DF2 = b )
by A93, A92, A96, XTUPLE_0:1;
then
2
* (dist (DF1,DF2)) = (((dist (x,y)) / (2 to_power l)) / 2) * 2
by A87, A89, A98, A101, NAT_2:25;
hence dist (
DF1,
DF2) =
(dist (x,y)) / ((2 to_power l) * 2)
by XCMPLX_1:78
.=
(dist (x,y)) / ((2 to_power l) * (2 to_power 1))
by POWER:25
.=
(dist (x,y)) / (2 to_power (l + 1))
by POWER:27
;
verum end; suppose
d = 1
;
dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1))then
(
DF1 = b &
DF2 = y1 )
by A93, A92, A97, XTUPLE_0:1;
then
2
* (dist (DF1,DF2)) = (((dist (x,y)) / (2 to_power l)) / 2) * 2
by A87, A89, A99, A101, NAT_2:25;
hence dist (
DF1,
DF2) =
(dist (x,y)) / ((2 to_power l) * 2)
by XCMPLX_1:78
.=
(dist (x,y)) / ((2 to_power l) * (2 to_power 1))
by POWER:25
.=
(dist (x,y)) / (2 to_power (l + 1))
by POWER:27
;
verum end; end; end;
hence
dist (
DF1,
DF2)
= (dist (x,y)) / (2 to_power (l + 1))
;
verum
end;
A103:
S4[1]
proof
reconsider pusty =
<*> {0,1} as
Node of
D by A8, FINSEQ_1:def 11;
let j be non
zero Element of
NAT ;
( j <= 2 to_power 1 implies for DF1, DF2 being Element of V st DF1 = (D . ((FinSeqLevel (1,dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel (1,dD)) . j)) `2 holds
dist (DF1,DF2) = (dist (x,y)) / (2 to_power 1) )
assume A104:
j <= 2
to_power 1
;
for DF1, DF2 being Element of V st DF1 = (D . ((FinSeqLevel (1,dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel (1,dD)) . j)) `2 holds
dist (DF1,DF2) = (dist (x,y)) / (2 to_power 1)
A105:
FinSeqLevel (1,
dD) is
FinSequence of
dom D
by FINSEQ_2:24;
j >= 1
by NAT_1:14;
then
j in Seg (2 to_power 1)
by A104, FINSEQ_1:1;
then
j in dom (FinSeqLevel (1,dD))
by BINTREE2:20;
then reconsider FSL1j =
(FinSeqLevel (1,dD)) . j as
Element of
dom D by A105, FINSEQ_2:11;
let DF1,
DF2 be
Element of
V;
( DF1 = (D . ((FinSeqLevel (1,dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel (1,dD)) . j)) `2 implies dist (DF1,DF2) = (dist (x,y)) / (2 to_power 1) )
assume A106:
(
DF1 = (D . ((FinSeqLevel (1,dD)) . j)) `1 &
DF2 = (D . ((FinSeqLevel (1,dD)) . j)) `2 )
;
dist (DF1,DF2) = (dist (x,y)) / (2 to_power 1)
( 2
to_power 1
= 2 &
j >= 1 )
by NAT_1:14, POWER:25;
then A107:
j in Seg 2
by A104, FINSEQ_1:1;
now dist (DF1,DF2) = (dist (x,y)) / 2per cases
( j = 1 or j = 2 )
by A107, FINSEQ_1:2, TARSKI:def 2;
suppose A108:
j = 1
;
dist (DF1,DF2) = (dist (x,y)) / 2A109:
ex
b being
Element of the
carrier of
V st
(
D . (pusty ^ <*0*>) = [x,b] &
D . (pusty ^ <*1*>) = [b,y] &
dist (
x,
y)
= 2
* (dist (x,b)) &
dist (
x,
y)
= 2
* (dist (b,y)) )
by A9, A10;
A110:
D . (pusty ^ <*0*>) =
D . <*0*>
by FINSEQ_1:34
.=
D . FSL1j
by A108, BINTREE2:22
.=
[DF1,DF2]
by A106, MCART_1:21
;
then
DF1 = x
by A109, XTUPLE_0:1;
hence
dist (
DF1,
DF2)
= (dist (x,y)) / 2
by A110, A109, XTUPLE_0:1;
verum end; suppose A111:
j = 2
;
dist (DF1,DF2) = (dist (x,y)) / 2consider b being
Element of the
carrier of
V such that
D . (pusty ^ <*0*>) = [x,b]
and A112:
D . (pusty ^ <*1*>) = [b,y]
and
dist (
x,
y)
= 2
* (dist (x,b))
and A113:
dist (
x,
y)
= 2
* (dist (b,y))
by A9, A10;
A114:
D . (pusty ^ <*1*>) =
D . <*1*>
by FINSEQ_1:34
.=
D . FSL1j
by A111, BINTREE2:23
.=
[DF1,DF2]
by A106, MCART_1:21
;
then
DF1 = b
by A112, XTUPLE_0:1;
hence
dist (
DF1,
DF2)
= (dist (x,y)) / 2
by A114, A112, A113, XTUPLE_0:1;
verum end; end; end;
hence
dist (
DF1,
DF2)
= (dist (x,y)) / (2 to_power 1)
by POWER:25;
verum
end;
A115:
for
l being non
zero Nat holds
S4[
l]
from NAT_1:sch 10(A103, A86);
A116:
i in Seg (len h)
by A40, A43, A44, FINSEQ_1:1;
then
i in dom h
by FINSEQ_1:def 3;
then f /. i =
h /. i
by FINSEQ_4:68
.=
h . i
by A40, A43, A44, FINSEQ_4:15
.=
(g /. i) `1
by A34, A35, A36, A116
.=
(g . i) `1
by A12, A34, A40, A43, A44, FINSEQ_4:15
.=
(D . (FSL /. i)) `1
by A13, A14, A34, A116
.=
(D . ((FinSeqLevel (n,dD)) . i)) `1
by A34, A40, A43, A44, A45, FINSEQ_4:15
;
hence
dist (
(f /. i),
(f /. (i + 1)))
= (dist (x,y)) / N
by A34, A40, A43, A44, A46, A115;
verum
end;
log (2,
((dist (x,y)) / p))
< n * 1
by INT_1:29;
then
log (2,
((dist (x,y)) / p))
< n * (log (2,2))
by POWER:52;
then
log (2,
((dist (x,y)) / p))
< log (2,
(2 to_power n))
by POWER:55;
then
(dist (x,y)) / p < N
by PRE_FF:10;
then
((dist (x,y)) / p) * p < N * p
by A11, XREAL_1:68;
then
dist (
x,
y)
< N * p
by A11, XCMPLX_1:87;
then
(dist (x,y)) / N < (N * p) / N
by XREAL_1:74;
then
(dist (x,y)) / N < (p / N) * N
by XCMPLX_1:74;
then
(dist (x,y)) / N < p
by XCMPLX_1:87;
hence
for
i being
Element of
NAT st 1
<= i &
i <= (len f) - 1 holds
dist (
(f /. i),
(f /. (i + 1)))
< p
by A42;
for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist ((f /. i),(f /. (i + 1))) ) holds
dist (x,y) = Sum Flet F be
FinSequence of
REAL ;
( len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist ((f /. i),(f /. (i + 1))) ) implies dist (x,y) = Sum F )assume that A117:
len F = (len f) - 1
and A118:
for
i being
Element of
NAT st 1
<= i &
i <= len F holds
F /. i = dist (
(f /. i),
(f /. (i + 1)))
;
dist (x,y) = Sum FA119:
rng F = {((dist (x,y)) / N)}
proof
thus
rng F c= {((dist (x,y)) / N)}
XBOOLE_0:def 10 {((dist (x,y)) / N)} c= rng Fproof
let a be
object ;
TARSKI:def 3 ( not a in rng F or a in {((dist (x,y)) / N)} )
assume
a in rng F
;
a in {((dist (x,y)) / N)}
then consider c being
object such that A120:
c in dom F
and A121:
F . c = a
by FUNCT_1:def 3;
c in Seg (len F)
by A120, FINSEQ_1:def 3;
then
c in { t where t is Nat : ( 1 <= t & t <= len F ) }
by FINSEQ_1:def 1;
then consider c1 being
Nat such that A122:
c1 = c
and A123:
( 1
<= c1 &
c1 <= len F )
;
reconsider c1 =
c1 as
Element of
NAT by ORDINAL1:def 12;
a =
F /. c1
by A121, A122, A123, FINSEQ_4:15
.=
dist (
(f /. c1),
(f /. (c1 + 1)))
by A118, A123
.=
(dist (x,y)) / N
by A42, A117, A123
;
hence
a in {((dist (x,y)) / N)}
by TARSKI:def 1;
verum
end;
let a be
object ;
TARSKI:def 3 ( not a in {((dist (x,y)) / N)} or a in rng F )
assume
a in {((dist (x,y)) / N)}
;
a in rng F
then
a = (dist (x,y)) / N
by TARSKI:def 1;
then A124:
a =
dist (
(f /. 1),
(f /. (1 + 1)))
by A34, A40, A37, A42
.=
F /. 1
by A34, A40, A37, A117, A118
.=
F . 1
by A34, A40, A37, A117, FINSEQ_4:15
;
1
in Seg (len F)
by A34, A40, A37, A117, FINSEQ_1:1;
then
1
in dom F
by FINSEQ_1:def 3;
hence
a in rng F
by A124, FUNCT_1:def 3;
verum
end;
dom F = Seg (len F)
by FINSEQ_1:def 3;
then
F = (len F) |-> ((dist (x,y)) / N)
by A119, FUNCOP_1:9;
hence Sum F =
((N + 1) - 1) * ((dist (x,y)) / N)
by A34, A40, A117, RVSUM_1:80
.=
dist (
x,
y)
by XCMPLX_1:87
;
verum end; suppose A125:
dist (
x,
y)
< p
;
ex f being FinSequence of the carrier of V st
( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds
dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist ((f /. i),(f /. (i + 1))) ) holds
dist (x,y) = Sum F ) )take f =
<*x,y*>;
( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds
dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist ((f /. i),(f /. (i + 1))) ) holds
dist (x,y) = Sum F ) )thus A126:
f /. 1
= x
by FINSEQ_4:17;
( f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds
dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist ((f /. i),(f /. (i + 1))) ) holds
dist (x,y) = Sum F ) )
len f = 2
by FINSEQ_1:44;
hence
f /. (len f) = y
by FINSEQ_4:17;
( ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds
dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist ((f /. i),(f /. (i + 1))) ) holds
dist (x,y) = Sum F ) )A127:
(len f) - 1 =
(1 + 1) - 1
by FINSEQ_1:44
.=
1
;
thus
for
i being
Element of
NAT st 1
<= i &
i <= (len f) - 1 holds
dist (
(f /. i),
(f /. (i + 1)))
< p
for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist ((f /. i),(f /. (i + 1))) ) holds
dist (x,y) = Sum Flet F be
FinSequence of
REAL ;
( len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist ((f /. i),(f /. (i + 1))) ) implies dist (x,y) = Sum F )assume that A128:
len F = (len f) - 1
and A129:
for
i being
Element of
NAT st 1
<= i &
i <= len F holds
F /. i = dist (
(f /. i),
(f /. (i + 1)))
;
dist (x,y) = Sum Freconsider dxy =
dist (
x,
y) as
Element of
REAL by XREAL_0:def 1;
1
<= len F
by A127, A128;
then
1
in dom F
by FINSEQ_3:25;
then
F /. 1
= F . 1
by PARTFUN1:def 6;
then F . 1 =
dist (
(f /. 1),
(f /. (1 + 1)))
by A127, A128, A129
.=
dist (
x,
y)
by A126, FINSEQ_4:17
;
then
F = <*dxy*>
by A127, A128, FINSEQ_5:14;
then
Sum F = dxy
by FINSOP_1:11;
hence
dist (
x,
y)
= Sum F
;
verum end; end;