Information Technology Reference
In-Depth Information
Our next step is to relate the outcomes extracted from extreme derivatives to
those extracted from the corresponding resolutions. By Lemma 4.3, we know that
the function
[0, 1]
ʩ
) defined in (4.1) for a deterministic
pLTS is continuous. Then its least fixed point
[0, 1]
ʩ
)
C
:(
R
ₒ
ₒ
(
R
ₒ
[0, 1]
ʩ
is also continuous
and can be captured by a chain of approximants. The functions
V
:
R
ₒ
n
,
n
V
≥
0, are
defined by induction on
n
:
0
(
r
)(
ˉ
)
V
=
0
n
+
1
n
)
V
=
C
(
V
V =
n
≥
0
n
.
This is used in the following result.
Then
V
Lemma 6.8
Let ʔ be a subdistribution in an ˉ-respecting deterministic pLTS. If
ʔ
then
(
ʔ
)
.
ʔ
⃒
V
(
ʔ
)
= V
˄
−ₒ
ˉ
Proof
Since the pLTS is
ˉ
-respecting, we know that
s
ʔ
implies
s
−ₒ
for
˄
−ₒ
any
ˉ
. Therefore, from the definition of the function
C
we have that
s
ʔ
implies
n
+
1
(
s
)
n
(
ʔ
), whence by lifting and linearity we get,
V
= V
˄
−ₒ
ʔ
then
n
+
1
(
ʔ
)
n
(
ʔ
) for all
n
If
ʔ
V
= V
≥
0.
(6.13)
ʔ
. Referring to Definition
6.4
and carrying out a
straightforward induction based on (
6.13
), we have
Now, suppose
ʔ
⃒
k
=
0
V
n
n
−
k
+
1
(
ʔ
k
)
n
+
1
(
ʔ
)
0
(
ʔ
n
+
1
)
V
= V
+
(6.14)
for all
n
≥
0. This can be simplified further by noting
V
0
(
ʔ
)(
ˉ
)
(i)
=
0, for every
ʔ
V
m
+
1
(
ʔ
)
= V
≥
0, provided
ʔ
is stable.
Applying these remarks to (
6.14
) above, since all
ʔ
k
(ii)
(
ʔ
) for every
m
are stable, we obtain
n
k
=
0
V
n
+
1
(
ʔ
)
(
ʔ
k
)
V
=
(6.15)
We conclude by reasoning as follows
n
≥
0
V
n
+
1
(
ʔ
)
V
(
ʔ
)
=
n
k
=
0
V
(
ʔ
k
)
=
from (
6.15
) above
n
≥
0
n
n
≥
0
V
ʔ
k
=
V
by linearity of
k
=
0
Search WWH ::
Custom Search