Probabilistic Testing Semantics - Semantics of Probabilistic Processes: An Operational Approach - page 75

4.3 Bounded Continuity

In this section we introduce a notion of bounded continuity for real-valued functions.
We will exploit it to show the continuity of the function defined in ( 4.1 ), and then

use it again in Chap. 6. We begin with a handy lemma below.

C

Lemma 4.2 (Exchange of Suprema) Let function g : N × N ₒ R be such that it

is

(i) monotone in both of its arguments, so that i 1 ≤ i 2 implies g ( i 1 , j ) ≤ g ( i 2 , j ) ,

and j 1 ≤ j 2 implies g ( i , j 1 ) ≤ g ( i , j 2 ) , for all i , i 1 , i 2 , j , j 1 , j 2 ∈ N , and

(ii) bounded above, so that there is a c ∈ R ≥ 0 with g ( i , j ) ≤ c for all i , j ∈ N .

Then

=

lim
i ₒ∞

lim
j ₒ∞

g ( i , j ) lim

j ₒ∞

lim
i ₒ∞

g ( i , j ) .

Proof Conditions (i) and (ii) guarantee the existence of all the limits. Moreover, for
a nondecreasing sequence, its limit and supremum agree, and both sides equal the
supremum of all g ( i , j ) for i , j

∈ N . In fact, ( R , ≤ ) is a complete partially ordered

set (CPO) and it is a basic result of CPOs [ 7 ] that

⊛
⊝
j ∈N

⊞

g ( i , j ) .

⊠ =

g ( i , j )

i ∈N j ∈N i ∈N

The following proposition states that some real functions satisfy the property of
bounded continuity , which allows the exchange of limit and sum operations.

Proposition 4.2 (Bounded Continuity—Nonnegative Function) Suppose a func-
tion f :

N × N ₒ R ≥ 0 satisfies the following conditions:
C1. f is monotone in the second parameter, i.e. j 1 ≤

j 2 implies f ( i , j 1 ) ≤ f ( i , j 2 )

for all i , j 1 , j 2 ∈ N ;

C2. for any i ∈ N , the limit lim j ₒ∞ f ( i , j ) exists;

C3. the partial sums S n = i = 0 lim j ₒ∞ f ( i , j ) are bounded, i.e. there exists some
c ∈ R ≥ 0 such that S n ≤ c for all n ≥ 0 .

Then the following equality holds:
∞ ∞

lim
j

f ( i , j ) = lim

j

f ( i , j ) .

ₒ∞ ₒ∞

i = 0 i = 0

= i = 0 f ( i , j ).
It is easy to see that g is monotone in both arguments. By C1 and C2 , we have that
f ( i , j )

Proof Let g : N × N ₒ R ≥ 0 be the function defined by g ( n , j )

≤ lim j ₒ∞ f ( i , j ) for any i , j ∈ N . So for any j , n ∈ N ,wehave

n n

g ( n , j ) = f ( i , j ) ≤ lim

j ₒ∞

f ( i , j ) ≤ c