11institutetext: NOVA School of Science and Technology 22institutetext: NOVA-
LINCS, Portugal

# Leroy and Blazy were right: their memory model soundness proof is
automatable
(Extended Version)

Pedro Barroso  Mário Pereira  António Ravara

###### Abstract

Xavier Leroy and Sandrine Blazy in 2007 conducted a formal verification, using
the Coq proof assistant, of a memory model for low-level imperative languages
such as C. Considering their formalization was performed essentially in first-
order logic, one question left open by the authors was whether their proofs
could be automated using a verification framework for first-order logic. We
took the challenge and automated their formalization using Why3, significantly
reducing the proof effort. We systematically followed the Coq proofs and
realized that in many cases at around one third of the way Why3 was able to
discharge all VCs. Furthermore, the proofs still requiring interactions (e.g.
induction, witnesses for existential proofs, assertions) were factorized
isolating auxiliary results that we stated explicitly. In this way, we
achieved an almost-automatic soundness and safety proof of the memory model.
Nonetheless, our development allows an extraction of a correct-by-construction
concrete memory model, going thus further than the preliminary Why version of
Leroy and Blazy.

###### Keywords:

C memory model Formal proof Theorem proving Why3

##  1 Introduction

Formal semantics are concerned with the process of building a mathematical
model to serve as a basis for understanding and reasoning about how programs
behave. A mathematical model is important because the activity of trying to
precisely define the behavior of program constructions can reveal all types of
subtleties of which it is crucial to be aware [9]. Many programs that require
formal verification are written in imperative languages that accommodate
pointer-based data structures with in-place modifications. To reason about the
contents of the memory or even the behavior of operations over it, one needs
to develop an adequate memory model.

##### Leroy and Blazy

in 2007 formalized and verified, using the Coq proof assistant, a memory model
for C-like imperative languages [4]. Coq proofs tend to be a very time
consuming task and in fact, Leroy and Blazy’s proof was almost the length of
the specification and theorems (970 and 1070 lines, respectively). Considering
their formalization was performed essentially in first-order logic, one
question the authors addressed was whether their proofs could be automated
using a verification framework for first-order logic, e.g. Why3 [2]. The
authors translated their memory model to Why (a former version of Why3), the
authors claim that at the time some recursive definitions were hard to define
in the Why syntax and therefore, they only translated the axiomatizations and
derived properties of the memory model. Their preliminary study (Table 1)
showed that could be automated, but no further study or complete formalization
of their memory model has been automated so far.

Figure 1: Leroy and Blazy’s Why formalization

Nonetheless, the problem we address here is:

> _Is it possible (15 years later) to automate the complete abstract and
> concrete implementation of the authors memory model?_

##### In this paper

we translate Leroy and Blazy’s memory model to Why3 and develop an almost-
automatic soundness and safety proof. Moreover, our code, implementing a
concrete memory model, is extractable. This requires some manual work, namely
re-organizing modules, that we believe with some refactoring of the WhyML code
could be avoided.

Concretely, our contributions are:

  * •

two Why3 versions (one containing interactive proofs and one “fully”
automatic) that reduce up to 90% the Coq proof effort;

  * •

general techniques to achieve a more automatic proof;

  * •

a proof effort comparison between ours and the original Coq ones;

  * •

a correct-by-construction memory model extracted from our development.

##### The rest of the article

is organized as follows. Section 2 describes memory models and briefly
presents the one of Leroy and Blazy. Also, Section 2 shows how to prove the
memory model sound and safe (which includes semantics preservation for three
passes of the Compcert compiler), and the Coq proof statistics that Leroy and
Blazy stated in their paper. Section 3 outlines our Why3 development and the
techniques used to explicitly state interactive transformations. Section 4
compares both versions with the Coq version and presents our approach to
extract correct-by-construction OCaml code, followed by conclusions in Section
6. Our Why3 development and OCaml extracted code is publicly
available111https://gitlab.com/p.barroso/memory-model-c-why3/.

##  2 The memory model

Memory models provide the necessary abstraction between the behavior of a
program and the behavior of the memory it reads and writes. When reasoning
about compilers and low-level code we need to account for several factors such
as memory management, concurrency behavior, casts, structured pointers,
overlapping locations, etc. Therefore, it is not sufficient to interpret
memory as a assignment of values to locations.

###  2.1 Concept

The generic idea behind a memory model is to explicitly describe and provide
some guarantees on the behavior of certain operations that manipulate memory
(e.g. read, write, allocation, free). This allows to make concrete assumptions
about the “state of the memory” at any time of the execution of a program. One
example is that reading after writing a value into a location should return
the value that was previously stored. Figure 2 shows this simple scenario and
the natural assertions one can make over the execution of the program.

Figure 2: Concrete assertion over a simple program

There are several ways to define a memory model: as a description of the set
of valid traces of operations fulfilled by the execution of a program (e.g.
IBM POWER multiprocessors [5]); as an abstract machine that receives and
replies to messages (e.g. CompCertTSO [8]); and as a set of functions that can
be invoked along with some guarantees on their results (e.g. Leroy and Blazy’s
memory model [4]). Note that in most cases a definition in one of these styles
is provably equivalent to a definition in another style [6].

The memory model presented by Leroy and Blazy is used in the formal
verification of the Compcert [3] compiler, which transforms the Clight subset
of the C programming language down to PowerPC assembly code.

###  2.2 Leroy and Blazy’s memory model

Leroy and Blazy start by giving an abstract, incomplete specification of a
memory model to formalize the memory-related aspects of C and related
languages. The abstract type val represents values, which includes the
constant vundef to describe an undefined value. To describe references to
memory blocks they use an abstract type block and to represent memory states
an abstract type mem.

##### Memory definitions.

A memory _state_ is a collection of separated blocks where each block behaves
as an array of bytes, and is addressed using byte offsets $i\in\mathbb{Z}$. A
memory _location_ is a pair (b, i) of a block reference b and an offset i
within this block. Lastly, the constant empty : mem represents the initial
memory state.

####  2.2.1 Operations.

They define four operations that manipulate memory states as total functions:

alloc
$\displaystyle:\texttt{mem}\times\mathbb{Z}\times\mathbb{Z}\rightarrow\texttt{option(block}\times\texttt{mem)}$
free $\displaystyle:\texttt{mem}\times\texttt{block}\rightarrow\texttt{option
mem}$ load
$\displaystyle:\texttt{memtype}\times\texttt{mem}\times\texttt{block}\times
Z\rightarrow\texttt{option val}$ store
$\displaystyle:\texttt{memtype}\times\texttt{mem}\times\texttt{block}\times
Z\times\texttt{val}\rightarrow\texttt{option mem}$

All these functions return option types to take into account potential
failures. The function alloc(m,l,h) allocates a fresh memory block, where m is
the initial memory state, $\texttt{l}\in\mathbb{Z}$ is the lower bound of the
block (inclusive), and $\texttt{h}\in\mathbb{Z}$ the upper bound (exclusive)
of the fresh block. Allocation can fail if not enough memory is available.
Otherwise, Some (b,m) is returned, where b is the reference to the new block
and m the updated memory state.

Contrarily, free(m,b) deallocates block b in memory m. In case of success, an
updated memory state is returned.

The function store($\tau$,m,b,i,v) writes value v of type $\tau$ at offset i
in block b of m. If successful, the updated memory state is returned.

Symmetrically, load($\tau$,m,b,i) reads a data type of $\tau$ from block b of
memory state m at byte offset i. If successful, the value from block b is
returned.

####  2.2.2 Axiomatization and additional properties.

The authors axiomatize the expected behavior of the operations.222The complete
set of hypotheses can be consulted online. Recall that any implementation of
the model must satisfy all these properties.

##### Good and not so good variables (axioms S5 to S8).

Define the correct behavior (operation succeeds) of a load after an alloc,
free or store operation. Concretely, these hypotheses specify that: alloc and
free preserve loads performed in any other disjoint block; reading from the
same location with a compatible type $\tau^{\prime}$ succeeds and returns the
value convert(v,$\tau^{\prime}$); and storing a value of type $\tau^{\prime}$
in block b at offset i commutes with loading. Furthermore, Leroy and Blazy
also specify when the load operation returns an undefined value.

##### Block validity (axioms S9 to S13).

The correct behavior of a load after an alloc, free or store depends on
separation properties between blocks. In order to capture such properties,
Leroy and Blazy axiomatize the relation m $\models$ b, which means that block
b is valid in memory m. A block is valid if it was previously allocated and
was not yet deallocated.

##### Bounds of block (axioms S14 to S17).

The authors also axiomatize the function $\mathcal{B}$(m, b) that associates
low and high bounds to a block b in memory state m. The axiomatization
specifies that a freshly allocated block has the bounds that were given as
argument to the alloc function and the bounds of a block are preserved by an
alloc, store or free operation over a different block.

##### Valid access (axiom S18 and derived properties D19 to D22).

Combining the definitions of block validity and of bounds of a block, Leroy
and Blazy define the “valid access” relation m $\models$ $\tau$ @ b, i, which
means that in state m, the block b is a valid block and the range of byte
offsets being accessed is included in the bounds of b. Intuitively, the store
and load operations succeeds if and only if the corresponding memory reference
is valid.

##### Freshness property (properties P30 to P34).

In Leroy and Blazy’s concrete memory model, alloc never reuses block
identifiers. Therefore, they define the relation m # b stating that block b is
fresh in memory m. This relation is mutually exclusive with block validity.

##### Alloc determinism (property P35).

Lastly, Leroy and Blazy state that alloc is deterministic with respect to the
domain of the current memory state, i.e. alloc chooses the same free block
when applied twice to memory states that have the same domain, but may differ
in block contents.

###  2.3 Compiler passes and their soundness proof

The axiomatization of the previous section specify precise handling of
undefined values, behavior of operations over memory states and “good-
variable” properties. This theory is used to prove the correctness of program
transformations performed by three passes of the Compcert compiler. Our
approach follows the same process presented by Leroy and Blazy and, therefore,
we also prove the correctness of these transformations.

To prove soundness and safety of each transformation, one need to guarantee
specific results between the memory operations performed by the original and
transformed program. For that, invariants are defined to describe the memory
states at every point of the execution of the original and transformed
programs.

Leroy and Blazy use four relations between memory states: memory embeddings;
memory extensions; refinement of stored values; and memory injections. For
each of them, they define several properties the program needs to hold in
order to prove soundness and safety. We decided to omit the exact definitions,
as the list is exhaustive and falls out of the scope of this paper.333The
authors did not presented a summarized list of properties for each of the four
relations.

###  2.4 Original Coq proof

Coq uses Gallina, a functional programming language. The close connection
between functional languages and mathematical definitions eases the
implementation of mathematical theories. The Coq development of Leroy and
Blazy is very close to the definitions presented in their paper. In fact, most
of the definitions in their paper were transcribed directly from their Coq
development, which has approximately 1070 lines of theorems and
specifications, and 970 lines of proof scripts.

Coq does not grant much support for proof automation. Therefore, Leroy and
Blazy manually conducted most of the proofs. Yet, their proofs exhaustively
use the omega tactic, a procedure that automates reasoning about equations and
inequalities over the type nat of natural numbers. They also occasionally use
other tactics (e.g. eauto, congruence), which the authors say were useful.

##  3 Our approach in Why3

The formalization of Leroy and Blazy was conducted mostly in first-order
logic: the authors use functions as data, but only to implement finite maps,
which allows a first-order axiomatization. Henceforth, the definitions in Why3
are very similar to the fragment from Gallina (Coq’s language). In fact, our
development is very similar to the specification and theorems of the Coq
version.

##### Implementation.

The Why version of Leroy and Blazy only contained the axiomatization of the
abstract memory model. Our Why3 development have the axioms of the abstract
memory model and additionally, the implementation of a concrete memory model,
which allows an extraction of a correct-by-construction memory model. Our
formalization have approximately 1040 lines of theorems and specifications,
roughly the same amount of the Coq version.

##### Proofs.

The automatic theorem provers discharges automatically 114 from a total of 125
verification conditions using the auto level 3 tactic, which attempts to apply
recursively four transformations (split_all_full, introduce_premises,
inline_goal and split_vc) and calls the provers with a larger time and memory
limit (30 seconds and 4Gb of memory). Using the key 3 of the keyboard
(shortcut for the auto level 3 tactic) we automatically prove the equivalent
of approximately 870 lines of proof scripts in Coq (89.6% of the total proof
scripts lines). Appendix 0.A shows the corresponding proofs in Coq and Why3 of
one lemma of the 114.

For the remaining 9 verification conditions (VCs), we follow closely the Coq
proof script, applying transformations one by one and calling the solvers for
each transformation. Three of the VCs require simple induction; four case
analysis before applying the induction hypothesis; one additional properties
in the context that we introduce with assertions and the last one a mix of
induction, case analysis, assertions and additionally proves an existential
statement (Table B1 summarizes the results). Yet, in all nine, the amount of
transformations to complete the proof were significantly less than the steps
of the proof in Coq (circa 117 transformations versus a total of 220).

####  3.0.1 General strategies to achieve a more automatic proof.

The primary cons of Why3 regarding proofs with manually conducted interactions
are: it is hard to have a concise global view of all transformations applied,
especially on larger proof trees; moreover after making change in the code,
most of the times Why3 is not able to propagate the exact transformations
through the correct proof nodes, which quite often leads to losses of the
whole proof session [1].

To circumvent this, we present the following general techniques to explicitly
state the interactions required for the remaining 9 proofs as WhyML code. This
allows the reader to have the essence of the whole proof just by looking at
the source code. Bellow, we explain and illustrate the approaches namely in
the treatment of induction, assertions and existential properties. The
remainder 9 proofs use these techniques. These techniques can be used as
general recipes for provers.

##### Induction.

Why3 provides a way to define lemma functions, which are special functions
that serve not as actual code to execute but to prove the function’s contract
as a lemma. These are useful when proving properties by induction, as any
recursive call to the functions means an application of the induction
hypothesis. Lets consider the following lemma:

⬇

lemma set_cont_outside:

forall n, f:(int $\rightarrow$ option (fset ’a, fset ’a)) , ofs i.

We prove the lemma by induction on n. Let us now convert our lemma to a
recursive lemma function. Recursive lemma functions are declared with the
keywords let rec lemma and its parameters are the universally quantified
variables in the normal lemma:

⬇

let rec lemma set_cont_outside (n: int)

(f: (int $\rightarrow$ option (memtype, value))) (ofs i: int)

Now we give a contract to the lemma, where each premise is now a precondition
(declared with the requires keyword) and the conclusion a postcondition
(declared with the ensures keyword). To guarantee the function terminates we
state a variant, in this case n itself, which is the argument we are applying
induction:

⬇

let rec lemma set_cont_outside (n: int)

(f: (int $\rightarrow$ option (memtype, value))) (ofs i: int)

requires { n $\geq$ 0 }

requires { i $<$ ofs \/ i $\geq$ ofs + n }

ensures { set_cont f ofs n i = f i }

variant { n }

Finally, we construct the correct recursive call by looking at the definitions
of the functions within the postconditions. In this case we have the function
set_cont, which definition is as follows:

⬇

let rec ghost function set_cont (f: int $\rightarrow$ content)

(ofs: int) (n: int) : int $\rightarrow$ content

requires { n $\geq$ 0 }

variant { n }

= if n = 0 then f else set_cont (update ofs None f) (ofs + 1) (n-1)

The recursive call of the lemma uses the same argument modifications of the
recursive call of set_cont:

⬇

let rec lemma set_cont_outside (n: int)

(f: (int $\rightarrow$ option (memtype, value))) (ofs i: int) ...

= if n $>$ 0 then set_cont_outside (n-1) (update ofs None f) (ofs + 1) i

Why3 is now able to automatically generate a valid induction hypothesis and
prove the lemma. The technique can be used as a general recipe for provers.

##### Asserts.

We introduce assertions in the body of let lemmas. For example in the lemma
store_mapped_emb, we assert that b1 is a valid pointer in memory state m1 and
b2 is a valid pointer in memory state m2:

⬇

let lemma store_mapped_emb

(val_emb: (int $\rightarrow$ option (int, int)) $\rightarrow$ value
$\rightarrow$ value $\rightarrow$ bool)

(emb: int $\rightarrow$ option (int, int)) (m1 m2: mem_)

(b1 ofs b2 delta: int) (v1 v2: value) (ty: memtype) (m1’: mem_)

requires { ... }

ensures { ... }

= assert { valid_pointer_ ty m1 b1 ofs };

assert { valid_pointer_ ty m2 b2 (ofs + delta) }

The assertions are introduced in the hypotheses of the lemma and Why3
generates two new VCs to prove both the assertions are valid.

##### Witnesses for existential statements.

When one needs to prove an existentially quantified formula, sometimes the
automatic theorem provers are not able to easily find the specific witness.
Therefore, one needs to manually build it. Consider the following lemma:

⬇

lemma store_lessdef:

forall m1 m2 ty b ofs v1 m1’ v2. mem_lessdef m1 m2 $\rightarrow$

store_ ty m1 b ofs v1 = Some m1’ $\rightarrow$ val_lessdef v1 v2 $\rightarrow$

exists m2’. store_ ty m2 b ofs v2 = Some m2’ /\ mem_lessdef m1’ m2’

We convert the lemma to a let lemma and as the lemma now needs to return a
value, we change the signature of the function to return the type of the
witness:

⬇

let lemma store_lessdef (m1 m2: mem_) (ty: memtype) (b ofs: int)

(v1: value) (m1’: mem_) (v2: value) : (m2’: mem_)

We also need to change the postcondition, which should now ensure the same
properties over the result of the function. This is achieved by replacing the
existential quantified variable with the output value m2’:

⬇

ensures { store_ ty m2 b ofs v2 = Some m2’ /\ mem_lessdef m1’ m2’}

Lastly, the function needs to return a proper witness that satisfied the
postconditions. In this case, we manually build a new memory state with
updated fields:

⬇

let lemma store_lessdef (m1 m2: mem_) (ty: memtype) (b ofs: int)

(v1: value) (m1’: mem_) (v2: value) : (m2’: mem_)

... = ...

(mem_’mk (m2.nextblock) (m2.bounds_) (m2.freed)

(update b (store_contents (m2.contents @ b) ty (ofs + 0) v2)

(m2.contents)))

The proof is now automatic and again, the technique is general.

####  3.0.2 Outcome.

Applying these three techniques to the remainder 9 lemmas, we reduce 100% the
number of manually conducted transformations needed to complete the proofs.
Table 1 compares the before and after applying these techniques.

Lemma | Number of interactions (Why3)
---|---
Before | After
1\. check_cont_charact | 7 | 0
2\. set_cont_outside | 2 | 0
3\. set_cont_inside | 2 | 0
4\. free_list_left_emb | 6 | 0
5\. free_list_not_valid_block | 6 | 0
6\. embedding_no_overlap_free_list | 6 | 0
7\. free_list_fresh_block | 3 | 0
8\. alloc_list_left_inject | 75 | 0
9\. alloc_list_alloc_inject | 10 | 0

Table 1: Number of transformations before and after

##  4 Proof Effort

Coq support for proof automation is limited, as one needs to explicitly apply
a sequence of tactics and transformations to prove the desired goal. In
contrast, one of the main focus of Why3 is automation, linking with SMT
solvers to discharge proof obligations, what allows to develop proofs with
less effort.

In this section we present metrics to compare our proofs with the Coq version.
We used the original authors’ proof as we are not aware of any improved
version – nowadays Coq has much more support to automation and experts may
reduce significantly the amount of transformations. Anyway, our goal is not a
direct comparison between lines of proof scripts, but how much automation can
be achieved, being this actually the original challenge left by Leroy and
Blazy.

####  4.0.1 Why3 fully automatic proof.

All lemmas were automatically proved using the auto_level_3 tactic of Why3.
The detailed proof results are available here. The table 2 summarizes the
structure of the proof.

| Module | Total
---|---|---
Gen_Mem_Facts | Ref_Gen_Mem_Facts | Concrete_Mem | Rel_Mem | Mem_Extends | Mem_Lessdef | Mem_Inject
Number of lemmas | 7 | 12 | 61 | 16 | 7 | 6 | 15 | 124

Table 2: Number of lemmas per module

These results take into consideration the interactions stated explicitly in
the code. Although the automatic theorem provers were able to prove all the
lemmas automatically, we had to use the techniques in Section 3.0.1 to aid the
verification process. One might think these techniques do exactly the same
thing as the transformations in the Coq proof scripts. In some sense that is
true, we closely followed the Coq proof script and applied transformations one
by one. However, when explicitly stating the transformations, one gives
auxiliary results (e.g. auxiliary lemmas, assertions, concrete definitions)
not a sequence of transformations/tactics as in Coq. On one hand, in Why3 we
have the certainty that all auxiliary results are required to complete the
proof (without them it is not possible to prove the lemmas). On the other, in
Coq, one does not have the certainty that all the tactics are essential to the
proof (one just knows that specific sequence completes the proof).
Nonetheless, even without explicitly stating the interactive proofs, the
effort to prove the lemmas in Why3 was way less than in Coq. Let us compare
the non-fully automatic Why3 proof with the Coq version.

####  4.0.2 Why3 semi-automatic proof.

The implementation and proofs without explicit interaction in the code can be
consulted here. Even without stating explicitly the interactions, the theorem
provers were able to prove 115 VCs automatically, which translates into a gain
of automation circa 93%. Table 3 summarizes the results.

| Module | Total
---|---|---
Gen_Mem_Facts | Ref_Gen_Mem_Facts | Concrete_Mem | Rel_Mem | Mem_Extends | Mem_Lessdef | Mem_Inject
Number of lemmas | 7 | 12 | 61 | 16 | 7 | 6 | 15 | 124
Automatically proved | 7 (100%) | 12 (100%) | 58 (95%) | 14 (87.5%) | 7 (100%) | 6 (100%) | 11 (73.3%) | 115 (92.7%)

Table 3: Number of lemmas proved automatically

These 115 VCs corresponds to a total of approximately 870 lines of the Coq
proof script, which in turn consists of 89.6% of the total lines of the entire
Coq proof script. Table C2 compares the amount of transformations used in
interactive proofs in Why3 and Coq. One can see that in Why3 we have a
reduction of 46.8% of the transformations compared to the Coq version, which
means significantly less proof effort.

##  5 Code extraction

One extra contribution of our work is the extraction of a correct-by-
construction OCaml implementation of the memory model.

The implementation of Leroy and Blazy uses several undefined functions (e.g.
enough_free_memory, alignof). In order to extract OCaml code, we need to
organize the code involving these functions and insert them into a
parameterized module (functor). For example, considering the function
enough_free_memory, we include its signature in the scope of the following
Make functor:

⬇

scope Make

scope X

val function enough_free_memory (mem: mem_) (i: int) : bool

end = struct ... end

With this manual transformation in the WhyML code (with the respect to the one
we originally used for the proofs), the extraction becomes automatic in the
sense that the obtained OCaml code compiles.

##  6 Conclusions

In this paper we present two versions in Why3 of the memory model of Leroy and
Blazy, which is used in the Compcert compiler: from the proof point of view
one is semi-automatic and the other results from an engineering effort to
attain full automation (e.g. turning tactics into auxiliary results). Using
the Why3 code extraction mechanism [7], from both versions we get correct-by-
construction OCaml implementations of the memory model.

The first version is a direct translation from the Coq development to Why3. We
immediately gain 93% of automation. The remaining 7% were proved following
closely the Coq proof script. Nonetheless, in Why3 the amount of
transformations required for the theorem provers to validate the proofs were
significantly less (117 transformations versus a total of 220).

The second version is a fully automatic proof. We performed general techniques
(explained in Section 3.0.1) to explicitly define the interactive proofs of
the first version within the WhyML code. This improves readability, as one
does not need to open the Why3 IDE to verify which transformations are used,
it is possible to have the essence of the proof just by analyzing the code.
Furthermore, as the proof is fully automatic, this approach also preserves the
proof-sessions, allowing a simple replay to check the reproducibility of the
results.

####  6.0.1 Lessons learned.

Nothing of the memory model was inexpressible in WhyML. This confirms the
premise that automatic verification tools are well-good candidates to defiant
proofs of complex programs without losing expressiveness.

Furthermore, most of the proofs required a handful of transformations and
nevertheless 93% of the proof was performed by merely pressing a button (hence
using automatic tactics, like split, etc). It is possible to save time and
effort to the proofs that are actually challenging.

It is undoubtedly that we are, at some point, limited to first order logic,
however if one reaches the limits of these type of provers, one can still
prove the remaining goals in Coq for example. In fact, Why3 provides a Coq
tactic to call external theorem provers as oracles.

Nonetheless, to achieve an even higher level of automation we performed some
refactoring to expose properties to the WhyML code: created auxiliary lemmas
from patterns that constantly appear in the Coq proof script; defined
inductive predicates to avoid proofs by induction; and transformed existential
proofs to lemma functions which return the desired witness.

### Acknowledgements

Work partially supported by the Portuguese Fundação para a Ciência e
Tecnologia via NOVA LINCS (UIDB/04516/2020) and by the first author PhD grant
(UI/BD/151265/2021).

## References

  * [1] Bobot, F., Filliâtre, J.C., Marché, C., Melquiond, G., Paskevich, A.: Preserving user proofs across specification changes. In: Cohen, E., Rybalchenko, A. (eds.) Verified Software: Theories, Tools, Experiments. pp. 191–201. Springer Berlin Heidelberg, Berlin, Heidelberg (2014)
  * [2] Filliâtre, J.C., Paskevich, A.: Why3—where programs meet provers. In: European symposium on programming. pp. 125–128. Springer (2013)
  * [3] Leroy, X.: A formally verified compiler back-end. Journal of Automated Reasoning 43(4), 363–446 (nov 2009). https://doi.org/10.1007/s10817-009-9155-4, https://doi.org/10.1007%2Fs10817-009-9155-4
  * [4] Leroy, X., Blazy, S.: Formal verification of a c-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning 41 (07 2008). https://doi.org/10.1007/s10817-008-9099-0
  * [5] Mador-Haim, S., Maranget, L., Sarkar, S., Memarian, K., Alglave, J., Owens, S., Alur, R., Martin, M.M.K., Sewell, P., Williams, D.: An axiomatic memory model for power multiprocessors. In: Madhusudan, P., Seshia, S.A. (eds.) Computer Aided Verification. pp. 495–512. Springer Berlin Heidelberg, Berlin, Heidelberg (2012)
  * [6] Mansky, W., Garbuzov, D., Zdancewic, S.: An axiomatic specification for sequential memory models. In: Kroening, D., Păsăreanu, C.S. (eds.) Computer Aided Verification. pp. 413–428. Springer International Publishing, Cham (2015)
  * [7] Pereira, M.J.P.: Tools and Techniques for the Verification of Modular Stateful Code. (Outils et techniques pour la vérification de programmes impératives modulaires). Ph.D. thesis, University of Paris-Saclay, France (2018), https://tel.archives-ouvertes.fr/tel-01980343
  * [8] Ševčík, J., Vafeiadis, V., Zappa Nardelli, F., Jagannathan, S., Sewell, P.: Compcerttso: A verified compiler for relaxed-memory concurrency. J. ACM 60(3) (jun 2013). https://doi.org/10.1145/2487241.2487248, https://doi.org/10.1145/2487241.2487248
  * [9] Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge, MA, USA (1993)

##  Appendix 0.A Comparison of an automatic proof

Coq

⬇

Lemma store_mapped_emb:

...

Proof: (*@ \color{red}(166 transformations/tactics) @*)

assert (valid_pointer ty m1 b1 ofs).

eapply M.store_valid_pointer; eauto.

assert (valid_pointer ty m2 b2 (ofs + delta)).

eapply valid_pointer_emb; eauto.

destruct (M.valid_pointer_store _ _ _ _ v2 H6)

as [m2’ STORE2].

exists m2’; split. auto.

red. intros ty’ b1’ ofs’ v b2’ delta’ CP LOAD1.

assert (valid_pointer ty’ m1 b1’ ofs’).

rewrite $\leftarrow\;$ (store_valid_pointer_inv (...) ).

eapply M.load_valid_pointer; eauto.

generalize (load_store_characterization (...) ).

destruct (load_store_classification (...) );

intro.

... (*@ \color{red} (+50 lines) @*)

Qed

Why3

⬇

lemma store_mapped_emb:

...

  * •

The proof is immediate

  * •

Proved in 0.15 seconds

##  Appendix 0.B Types of proofs

Type | Lemma | Number of transformations
---|---|---
Why3
$\bullet$ | 1\. check_cont_charact | 7
$\bullet$ | 2\. set_cont_outside | 2
$\bullet$ | 3\. set_cont_insid | 2
$\bullet$ | 4\. free_list_left_emb | 6
$\bullet$ | 5\. free_list_not_valid_block | 6
$\bullet$ | 6\. embedding_no_overlap_free_list | 6
$\bullet$ | 7\. free_list_fresh_block | 3
$\bullet$ | 8\. alloc_list_left_inject | 75
$\bullet$ | 9\. alloc_list_alloc_inject | 10

  * $\bullet$

Simple induction

  * $\bullet$

Induction and case analysis

  * $\bullet$

Assertions

  * $\bullet$

The two above + proof of an existential statement

Table B1: Number of transformations per type of proof

##  Appendix 0.C Amount of transformations used in interactive proofs

Lemma | Number of transformations
---|---
Coq | Why3
1\. check_cont_charact | 26 | 7 (27%)
2\. set_cont_outside | 9 | 2 (22%)
3\. set_cont_inside | 15 | 2 (13%)
4\. free_list_left_emb | 10 | 6 (60%)
5\. free_list_not_valid_block | 16 | 6 (38%)
6\. embedding_no_overlap_free_list | 11 | 6 (55%)
7\. free_list_fresh_block | 11 | 3 (27%)
8\. alloc_list_left_inject | 85 | 75 (88%)
9\. alloc_list_alloc_inject | 37 | 10 (27%)
Total | 220 | 117 (53.2%)
Table C2: Number of transformations in interactive proofs


# Pick interpolation and invariant distances

Anindya Biswas  Department of Mathematics and Statistics, Masaryk University,
Brno<EMAIL_ADDRESS>
###### Abstract.

In this article, we study the role of invariant distances in the Pick
interpolation problem. Given a Carathéodory hyperbolic domain $\Omega$ in some
$\mathbb{C}^{m}$, we have introduced a notion of an invariant object that
gives a necessary and sufficient condition for any Pick interpolation problem
to be solvable on $\Omega$. This invariant object plays the same role as that
of Carathéodory pseudodistance in the two-point Pick interpolation problem.
Furthermore, a full description of the invariant object is given when $\Omega$
is the open unit disc.

###### Key words and phrases:

Invariant pseudodistance, Carathéodory pseudodistance, Pick interpolation

###### 2010 Mathematics Subject Classification:

Primary 32F45 , Secondary 32E30

##  1\. Introduction

We start with a Carathéodory hyperbolic domain $\Omega$ in some
$\mathbb{C}^{m}$, $z_{1},z_{2}\in\Omega$ and $w_{1},w_{2}\in\mathbb{D}$. It is
well known that there is an $f\in H^{\infty}_{1}(\Omega)$ satisfying
$f(z_{1})=w_{1}$ and $f(z_{2})=w_{2}$ if and only if

$m(w_{1},w_{2})=\Big{|}\frac{w_{1}-w_{2}}{1-\overline{w_{1}}w_{2}}\Big{|}\leq
c^{*}_{\Omega}(z_{1},z_{2})$

where $c^{*}_{\Omega}(z_{1},z_{2})$ stands for the Carathéodory pseudodistance
between $z_{1}$ and $z_{2}$. This condition does not have an analogous form
for the case where one is interested in three or more points. In 1916, Pick
gave a necessary and sufficient condition for $n$-point interpolation problem
to be solvable when $\Omega=\mathbb{D}$ ([13]). In 1919, Nevanlinna gave an
independent proof of the same fact (see [12]). Their result states the
following: Suppose $z_{1},\ldots,z_{n}\in\mathbb{D}$ are distinct points and
$w_{1},\ldots,w_{n}\in\mathbb{D}$. Then the interpolation problem
$z_{j}\mapsto w_{j}$ is solvable by a function in $H^{\infty}_{1}(\mathbb{D})$
if and only if the (Pick-)matrix

(1.1)
$\displaystyle\begin{pmatrix}\frac{1-w_{i}\overline{w_{j}}}{1-z_{i}\overline{z_{j}}}\end{pmatrix}_{1\leq
i,j\leq n}$

is positive semi-definite. Considering the set

(1.2) $\displaystyle D(z_{1},\ldots,z_{n})=\\{(f(z_{1}),\ldots,f(z_{n})):f\in
H^{\infty}_{1}(\mathbb{D})\\},$

it is equivalent to saying that the interpolation problem $z_{j}\mapsto w_{j}$
is solvable if and only if

$(w_{1},\ldots,w_{n})\in D(z_{1},\ldots,z_{n})$

if and only if the matrix (1.1) is positive semi-definite. The set
$D(z_{1},\ldots,z_{n})$ is called the Pick body or the interpolation body
associated with the tuple $(z_{1},\ldots,z_{n})$. Further works on the Pick
body have been carried out by Cole, Lewis, and Wermer (see [4], [5], [6], [7],
[8]).

Our attention will be on a set that is somewhat similar to (1.2). We consider
an arbitrary Carathéodory hyperbolic domain $\Omega$ and $n$ distinct points
$z_{1},\ldots,z_{n}\in\Omega$. Let $B^{\infty}_{1}$ denote the interior of
$H^{\infty}_{1}(\Omega)$, that is, the set of all bounded holomorphic
functions on $\Omega$ with norm strictly less than one. We now construct the
following set

(1.3)
$\displaystyle\mathscr{D}_{\Omega}(z_{1},\ldots,z_{n})=\\{(f(z_{1})\ldots,f(z_{n})):f\in
B^{\infty}_{1}\\}.$

We will often write $\mathscr{D}_{n}$ for
$\mathscr{D}_{\Omega}(z_{1},\ldots,z_{n})$ when it is clear from the context.
Note that

$\overline{\mathscr{D}_{n}}=\\{(f(z_{1})\ldots,f(z_{n})):f\in
H^{\infty}_{1}(\Omega)\\},$

and the boundary of $\mathscr{D}_{n}$, denoted by $\partial\mathscr{D}_{n}$,
consists of the points $(w_{1},\ldots,w_{n})$ such that, if $f\in
H^{\infty}_{1}(\Omega)$ satisfies $f(z_{j})=w_{j}$, then $||f||=1$, that is,
$\partial\mathscr{D}_{n}$ consists of the points that can not be interpolated
by functions with norm strictly less than one.

The main part of the article is divided into two sections. In Section 2, we
describe the invariant object and some familiar notions connected to the
object. In Section 3, we give a way of finding the invariant object for
$\mathbb{D}$.

##  2\. Description of the invariant object

Let us begin with describing a few properties of the set $\mathscr{D}_{n}$.

######  Proposition 2.1.

$\mathscr{D}_{n}$ is an open balanced convex subset of the unit polydisc
$\mathbb{D}^{n}$.

###### Proof.

For any $f,g\in B^{\infty}_{1}$ we have $(1-t)f+tg\in B^{\infty}_{1}$ for all
$t\in[0,1]$ and $\lambda f\in B^{\infty}_{1}$ for all
$\lambda\in\overline{\mathbb{D}}$. So $\mathscr{D}_{n}$ is balanced and
convex. Obviously $\mathscr{D}_{n}$ is a subset of $\mathbb{D}^{n}$ and it
contains $0$. Note that, if the standard basis for $\mathbb{C}^{n}$ is denoted
by $e_{j},1\leq j\leq n$ , we can always find nonzero
$\lambda_{j}\in\mathbb{C}$ such that $\lambda_{j}e_{j}\in\mathscr{D}_{n}$ (so
convexity implies that $\mathscr{D}_{n}$ contains a small neighborhood of
$0$). To see that $\mathscr{D}_{n}$ is open, we consider the linear map
$H:H^{\infty}(\Omega)\rightarrow\mathbb{C}^{n}$ defined by
$H(f)=(f(z_{1})\ldots,f(z_{n}))$. Note that $||H||\leq\sqrt{n}$. So $H$ is a
bounded onto linear map. By open mapping theorem, $H$ is an open map and
$H(B^{\infty}_{1})=\mathscr{D}_{n}$. This completes our proof. ∎

Since we have that $\mathscr{D}_{n}$ is a balanced convex open set, let us
talk about the Minkowski functional $\mu_{\mathscr{D}_{n}}$ of
$\mathscr{D}_{n}$. We recall the following facts ([11], Chapter 2):

  1. (1)

$\mu_{\mathscr{D}_{n}}$ is a norm on $\mathbb{C}^{n}$.

  2. (2)

The boundary of $\mathscr{D}_{n}$ is given by
$\partial\mathscr{D}_{n}=\\{X\in\mathbb{C}^{n}:\mu_{\mathscr{D}_{n}}(X)=1\\}$.

  3. (3)

Since $\mathscr{D}_{n}$ is a balanced convex (hence pseudoconvex),
$\mu_{\mathscr{D}_{n}}$ is plurisubharmonic (Proposition 2.2.15 in [11]).
Consequently, $\mathscr{D}_{n}$ is hyperconvex.

Let $Aut(\mathbb{D})$ denote the group of automorphisms of $\mathbb{D}$. We
consider a $\varphi\in Aut(\mathbb{D})$ and define
$\Phi_{\varphi}:\mathbb{D}^{n}\rightarrow\mathbb{D}^{n}$ as

(2.1)
$\displaystyle\Phi_{\varphi}(w_{1},\ldots,w_{n})=(\varphi(w_{1}),\ldots,\varphi(w_{n})).$

Since $f\in B^{\infty}_{1}$ if and only if $\varphi\circ f\in B^{\infty}_{1}$,
we conclude that the restriction $\Phi_{\varphi}|_{\mathscr{D}_{n}}$ is an
automorphism of $\mathscr{D}_{n}$.

Our next result gives a description of $\mu_{\mathscr{D}_{n}}$ in terms of
$H^{\infty}(\Omega)$.

######  Theorem 2.2.

For any $\underline{w}=(w_{1},\ldots,w_{n})\in\mathbb{C}^{n}$,

$\mu_{\mathscr{D}_{n}}(\underline{w})=inf\\{||g||:g\in
H^{\infty}(\Omega),g(z_{j})=w_{j},j=1,\ldots,n\\}.$

###### Proof.

Observe that the map $H$ in Proposition 2.1 is onto. So for any
$\underline{w}\in\mathbb{C}^{n}$, there is a $g\in H^{\infty}(\Omega)$ such
that $w_{j}=g(z_{j})$ for all $j=1,\ldots,n$. For such a $g$ we have
$\frac{1}{||g||}\underline{w}\in\overline{\mathscr{D}_{n}}$. And hence, we
have $\mu_{\mathscr{D}_{n}}(\underline{w})\leq||g||$ for all such $g$.

Let $l=\inf\\{||g||:g\in H^{\infty}(\Omega),g(z_{j})=w_{j},j=1,\ldots,n\\}$
and suppose that $\mu_{\mathscr{D}_{n}}(\underline{w})<l$. Then
$\mu_{\mathscr{D}_{n}}(\frac{1}{l}\underline{w})<1$ and hence
$\frac{1}{l}\underline{w}\in\mathscr{D}_{n}$. By definition, there is an $f\in
B^{\infty}_{1}$ such that $\frac{w_{j}}{l}=f(z_{j})$ So $w_{j}=lf(z_{j})$ for
all $j$, $lf\in H^{\infty}(\Omega)$ and $||lf||<l$. This contradicts our
assumption. Hence $\mu_{\mathscr{D}_{n}}(\underline{w})=l$ and this concludes
the proof. ∎

######  Corollary 2.3.

Let $I=I(z_{1},\ldots,z_{n})$ be the ideal in the Banach algebra
$H^{\infty}(\Omega)$ consisting of the functions that vanish at each
$z_{j},1\leq j\leq n$. Then the normed spaces
$(\mathbb{C}^{n},\mu_{\mathscr{D}_{n}})$ and
$(H^{\infty}(\Omega)/I,||\cdot||_{q})$ are isometrically isomorphic, where
$||\cdot||_{q}$ is the quotient norm. Moreover, $\mu_{\mathscr{D}_{n}}$ is a
Banach algebra norm (i.e., sub-multiplicative) on $\mathbb{C}^{n}$ with
component-wise product.

Using Montel’s theorem, it is not hard to see that $\mu_{\mathscr{D}_{n}}$ is
attained, that is, for a given $\underline{w}\in\mathbb{C}^{n}$, there exists
a $g\in H^{\infty}(\Omega)$ such that $g(z_{j})=w_{j}$ for all $j$ and
$\mu_{\mathscr{D}_{n}}(\underline{w})=||g||$.

We now want to focus on an old domain introduced by H. Cartan [3] and later
studied by several mathematicians in different context and form (see [2], [4],
[10]). The domain is given by

(2.2)
$\displaystyle\mathbb{D}^{2}_{r}=\Big{\\{}(w_{1},w_{2})\in\mathbb{D}^{2}:m(w_{1},w_{2})=\Big{|}\frac{w_{1}-w_{2}}{1-\overline{w_{1}}w_{2}}\Big{|}<r\Big{\\}},r\in(0,1).$

The following theorem will lead us to our invariant object.

######  Theorem 2.4.

For two distinct points $z_{1},z_{2}\in\Omega$ we have

$\displaystyle\mathscr{D}_{\Omega}(z_{1},z_{2})=\mathscr{D}_{2}=\mathbb{D}^{2}_{c^{*}_{\Omega}(z_{1},z_{2})}.$

###### Proof.

This follows from the fact that $c^{*}_{\Omega}(z_{1},z_{2})$ is always
attained by functions of norm one, and $m(aw_{1},aw_{2})\leq m(bw_{1},bw_{2})$
if and only if $|a|\leq|b|$ whenever $w_{1}\neq w_{2}$,
$a,b\in\mathbb{C},aw_{j},bw_{j}\in\mathbb{D}$, and $j=1,2$. ∎

This gives us that for any $r\in(0,1)$, $\mathbb{D}^{2}_{r}$ is convex. Note
that, the boundary of $\mathbb{D}^{2}_{r}$ can be given by

$\displaystyle\partial\mathbb{D}^{2}_{r}=\\{(e^{i\theta},e^{i\theta}):\theta\in\mathbb{R}\\}\cup\\{(w_{1},w_{2})\in\mathbb{D}^{2}:m(w_{1},w_{2})=r\\}.$

When $n\geq 3$, there is no analogous description of $\mathscr{D}_{n}$. To
address this issue, let us consider the following procedure: Let
$\underline{\alpha}=(\alpha_{1},\ldots,\alpha_{n})\in\mathbb{C}^{n}-\\{\mathbf{0}\\}$.
For this $\underline{\alpha}$ and $z_{1},\ldots,z_{n}\in\Omega$, we define

(2.3) $\displaystyle
d^{\Omega}_{(\underline{z},{\underline{\alpha}})}(z_{i},z_{j})=d_{\underline{\alpha}}(z_{i},z_{j})=sup\\{m(f(z_{i}),f(z_{j})):f\in
H^{\infty}_{1}(\Omega),\underline{f}\in\mathbb{C}\cdot\underline{\alpha}\\}$

where $\underline{z}=(z_{1},\ldots,z_{n})\in\Omega^{n}$,
$\underline{f}=(f(z_{1}),\ldots,f(z_{n}))\in\mathbb{D}^{n}$ and
$\mathbb{C}\cdot\underline{\alpha}$ denotes the one dimensional subspace
generated by the nonzero element $\underline{\alpha}$. The following facts are
easy to deduce.

  1. (1)

Since $\mathbf{0}\in\mathscr{D}_{n}\cap\mathbb{C}\cdot\underline{\alpha}$ and
$H^{\infty}_{1}(\Omega)$ contains the zero function, the set we used to define
$d$ is nonempty. So the supremum exists. Also, for any fixed
$\underline{\alpha}$ we have

$\displaystyle 0\leq d_{\underline{\alpha}}(z_{i},z_{j})\leq
c^{*}_{\Omega}(z_{i},z_{j}).$

  2. (2)

$d_{\underline{\alpha}}(z_{i},z_{j})$ is contractible under holomorphic maps,
that is, if $F:\Omega_{1}\rightarrow\Omega_{2}$ is a holomorphic map between
two Carathéodory hyperbolic domains, then

$\displaystyle
d^{\Omega_{2}}_{(\underline{F(z)},{\underline{\alpha}})}(F(z_{i}),F(z_{j}))\leq
d^{\Omega_{1}}_{(\underline{z},{\underline{\alpha}})}(z_{i},z_{j})$

where $\underline{z}=(z_{1},\ldots,z_{n})\in\Omega_{1}^{n}$ and
$\underline{F(z)}=(F(z_{1}),\ldots,F(z_{n}))\in\Omega_{2}^{n}$. If $F$
injective on $\\{z_{1},\ldots,z_{n}\\}$, then the fact is clear. If
$F(z_{i})=F(z_{j})$, then we use the argument as in (1).

  3. (3)

For any $\underline{\beta}\in\mathbb{C}\cdot\underline{\alpha}$ and
$\underline{\beta}\neq\mathbf{0}$,
$d_{\underline{\alpha}}(z_{i},z_{j})=d_{\underline{\beta}}(z_{i},z_{j})$.
Furthermore, if $\alpha_{i}=\alpha_{j}$, then
$d_{\underline{\alpha}}(z_{i},z_{j})=0$.

  4. (4)

If we consider only two points $z_{1},z_{2}\in\Omega$ and an
$\underline{\alpha}=(\alpha_{1},\alpha_{2})$ with $\alpha_{1}\neq\alpha_{2}$,
then $d_{\underline{\alpha}}(z_{1},z_{2})=c^{*}_{\Omega}(z_{1},z_{2})$. This
holds because for $\alpha_{1}\neq\alpha_{2}$, there is a positive $t$ such
that $t\alpha_{1},t\alpha_{2}\in\mathbb{D}$ and
$m(t\alpha_{1},t\alpha_{2})=c^{*}_{\Omega}(z_{1},z_{2})$, and
$c^{*}_{\Omega}(z_{1},z_{2})$ is always attained by some function in
$H^{\infty}_{1}(\Omega)$. Observe that, this $t$ is nothing but
$\frac{1}{\mu_{\mathscr{D}_{2}}(\alpha_{1},\alpha_{2})}$.

  5. (5)

For any $i$ and $j$,
$d_{\underline{\alpha}}(z_{i},z_{j})=m(t\alpha_{i},t\alpha_{j})$ where
$t=\frac{1}{\mu_{\mathscr{D}_{n}}(\underline{\alpha})}$. Consequently, for any
$\underline{\alpha}$ there is an $f\in H^{\infty}_{1}(\Omega)$ such that
$\underline{f}\in\mathbb{C}\cdot\underline{\alpha}$ and
$d_{\underline{\alpha}}(z_{i},z_{j})=m(f(z_{i}),f(z_{j}))$ for all $i$ and
$j$. To see this, note that $\mu_{\mathscr{D}_{n}}(t\underline{\alpha})=1$. If
$\alpha_{i}=\alpha_{j}$, the result is clear. Therefore, let us assume
$\alpha_{i}\neq\alpha_{j}$, and hence
$t\underline{\alpha}\in\partial\mathscr{D}_{n}\cap\mathbb{D}^{n}$. By
definition of $\overline{\mathscr{D}_{n}}$, there is an $f\in
H^{\infty}_{1}(\Omega)$ such that $t\underline{\alpha}=\underline{f}$. Also
suppose that $g\in H^{\infty}_{1}(\Omega)$ satisfies
$d_{\underline{\alpha}}(z_{i},z_{j})=m(g(z_{i}),g(z_{j}))$ and
$\underline{g}=\lambda\underline{\alpha}$ for some $\lambda\in\mathbb{C}$. We
now have

$\displaystyle m(t\alpha_{i},t\alpha_{j})$
$\displaystyle=m(f(z_{i}),f(z_{j}))$ $\displaystyle\leq
d_{\underline{\alpha}}(z_{i},z_{j})$ $\displaystyle=m(g(z_{i}),g(z_{j}))$
$\displaystyle=m(\lambda\alpha_{i},\lambda\alpha_{j}).$

So $t\leq|\lambda|$. On the other hand
$\frac{|\lambda|}{t}=|\lambda|\mu_{\mathscr{D}_{n}}(\underline{\alpha})=\mu_{\mathscr{D}_{n}}(\underline{g})\leq
1$, that is, $|\lambda|\leq t$.

  6. (6)

For $\Omega=\mathbb{D}$, we have
$d_{\underline{z}}(z_{i},z_{j})=m(z_{i},z_{j})$ for all $i$ and $j$.

Let us now give a description of $\mathscr{D}_{n}$ in terms of $d$.

######  Theorem 2.5.

Suppose $z_{1},\ldots,z_{n}$ are $n$ distinct points in $\Omega$. Then
$\mathscr{D}_{\Omega}(z_{1},\ldots,z_{n})=\mathscr{D}_{n}$ is given by

$\displaystyle\mathscr{D}_{n}=$
$\displaystyle\\{(\alpha,\ldots,\alpha):\alpha\in\mathbb{D}\\}$
$\displaystyle\cup\big{[}\cup_{1\leq i<j\leq
n}\\{(\alpha_{1},\ldots,\alpha_{n})\in\mathbb{D}^{n}:\alpha_{i}\neq\alpha_{j},m(\alpha_{i},\alpha_{j})<d_{\underline{\alpha}}(z_{i},z_{j})\\}\big{]}$

###### Proof.

Let $\underline{w}=(w_{1},\ldots,w_{n})\in\mathscr{D}_{n}$. By definition,
there is an $f\in B^{\infty}_{1}$ such that $w_{j}=f(z_{j})$ for all $j$, and
hence $(f(z_{1}),\ldots,f(z_{n}))\in\mathbb{C}\cdot\underline{w}$. If
$w_{1}=\ldots=w_{n}$, then
$\underline{w}\in\\{(\alpha,\ldots,\alpha):\alpha\in\mathbb{D}\\}$. If
$w_{i}\neq w_{j}$ for some $i\neq j$, then we have $m(w_{i},w_{j})\leq
d_{\underline{w}}(z_{i},z_{j})$. Suppose we have
$m(w_{i},w_{j})=d_{\underline{w}}(z_{i},z_{j})$. Note that $f\in
B^{\infty}_{1}$ and hence there is a $t>1$ such that $tf\in B^{\infty}_{1}$.
But then we have $(tf(z_{1}),\ldots,tf(z_{n}))\in\mathbb{C}\cdot\underline{w}$
and $d_{\underline{w}}(z_{i},z_{j})<m(tf(z_{i}),tf(z_{j}))$. This is a
contradiction. Therefore, we obtain
$m(w_{i},w_{j})<d_{\underline{w}}(z_{i},z_{j})$.

Now suppose we have $\underline{x}=(x_{1},\ldots,x_{n})\in\mathbb{D}^{n}$. If
$x_{1}=\ldots=x_{n}$, then clearly the constant function $f(z)=x_{1}$ takes
$z_{j}$ to $x_{j}$ and has norm strictly less than one. Now suppose $x_{i}\neq
x_{j}$ and $m(x_{i},x_{j})<d_{\underline{x}}(z_{i},z_{j})$. Using Montel’s
theorem, we can claim that there is a $g\in H^{\infty}_{1}(\Omega)$ such that
$||g||=1$, $d_{\underline{x}}(z_{i},z_{j})=m(g(z_{i}),g(z_{j}))$ and
$(g(z_{1}),\ldots,g(z_{n}))\in\mathbb{C}\cdot\underline{x}$. We can find
$t\in(0,1)$ and $\lambda\in\mathbb{C}$ such that
$m(x_{i},x_{j})=m(tg(z_{i}),tg(z_{j}))$ and
$(g(z_{1}),\ldots,g(z_{n}))=\lambda\cdot\underline{x}$. This gives us
$m(x_{i},x_{j})=m(t\lambda x_{i},t\lambda x_{j})$. This holds if and only if
$|t\lambda|=1$. So $t\lambda=e^{-i\theta}$ for some $\theta\in\mathbb{R}$. Let
$h=e^{i\theta}tg$. Then $||h||=t<1$ and
$(h(z_{1}),\ldots,h(z_{n}))=(x_{1},\ldots,x_{n})$, that is,
$(x_{1},\ldots,x_{n})\in\mathscr{D}_{n}$, and we are done. ∎

######  Corollary 2.6.

An $n$-point Nevanlinna-Pick interpolation problem $\Omega\ni z_{j}\mapsto
w_{j}\in\mathbb{D},1\leq j\leq n$, is solvable if and only if either
$w_{1}=\ldots=w_{n}\in\mathbb{D}$ or with $w_{i}\neq w_{j}$ (for at least one
pair $(i,j)$) the condition $m(w_{i},w_{j})\leq
d_{\underline{w}}(z_{i},z_{j})$ is satisfied.

We can consider this Corollary 2.6 as a generalized or multi-point Schwarz-
Pick lemma for Carathéodory hyperbolic domains. For multi-point Schwarz-Pick
lemma on $\mathbb{D}$ see [1] and [9].

##  3\. Values of $d^{\mathbb{D}}$

Here we will describe the values of $d^{\mathbb{D}}_{\underline{\alpha}}$ for
all nonzero $\underline{\alpha}$s. First we consider the following
$\underline{\alpha}$:

  1. (1)

$\underline{\alpha}=(0,0,\ldots,0,1)$.

  2. (2)

$\underline{\alpha}=(0,0,\ldots,0,\alpha_{n-1},\alpha_{n})$ with
$\alpha_{n-1}\alpha_{n}\neq 0$.

######  Proposition 3.1.

If $\underline{\alpha}=(0,0,\ldots,0,1)$ then

$\displaystyle d_{\underline{\alpha}}(z_{i},z_{j})$
$\displaystyle=0,\,\,\text{for}\,\,1\leq i,j\leq n-1,$
$\displaystyle=\prod_{l=1}^{n-1}\Big{|}\frac{z_{l}-z_{n}}{1-\overline{z_{l}}z_{n}}\Big{|},\,\,\text{for}\,\,1\leq
i\leq n-1\,\,\text{and}\,\,j=n.$

###### Proof.

It is easy to see that for $1\leq i,j\leq n-1$,
$d_{\underline{\alpha}}(z_{i},z_{j})=0$. Now suppose $j=n$ and $1\leq i\leq
n-1$. There is an $f\in H^{\infty}_{1}(\mathbb{D})$ such that
$\underline{f}=(f(z_{1}),\ldots,f(z_{n}))\in\mathbb{C}\cdot\underline{\alpha}$
and $d_{\underline{\alpha}}(z_{i},z_{n})=m(f(z_{i}),f(z_{n}))$. Since
$f(z_{1})=\cdots=f(z_{n-1})=0$, there is an $f_{n}\in
H^{\infty}_{1}(\mathbb{D})$ such that

$f(z)=f_{n}(z)\prod_{l=1}^{n-1}\Big{(}\frac{z_{l}-z}{1-\overline{z_{l}}z}\Big{)}.$

Note that this $f$ satisfies
$m(f(z_{i}),f(z_{n}))\leq\prod_{l=1}^{n-1}\Big{|}\frac{z_{l}-z_{n}}{1-\overline{z_{l}}z_{n}}\Big{|}$.
Now the function

$\varphi(z)=\prod_{l=1}^{n-1}\Big{(}\frac{z_{l}-z}{1-\overline{z_{l}}z}\Big{)}$

is in $H^{\infty}_{1}(\mathbb{D})$ and
$\underline{\varphi}\in\mathbb{C}\cdot\alpha$. Hence

$\displaystyle m(\varphi(z_{i}),\varphi(z_{n}))\leq
d_{\underline{\alpha}}(z_{i},z_{n})=m(f(z_{i}),f(z_{n}))\leq\prod_{l=1}^{n-1}\Big{|}\frac{z_{l}-z_{n}}{1-\overline{z_{l}}z_{n}}\Big{|}=m(\varphi(z_{i}),\varphi(z_{n}))$

and this completes the proof. ∎

Before proceeding with the other $\underline{\alpha}$, we want to point out
that for a given pair $(\beta_{1},\beta_{2})$ of distinct complex numbers and
any two distinct $z_{1},z_{2}$ in $\Omega$, there is a $t>0$ such that
$m(t\beta_{1},t\beta_{2})=c^{*}_{\Omega}(z_{1},z_{2})$. This $t$ is just
$\frac{1}{\mu_{\mathscr{D}_{\Omega}(z_{1},z_{2})}(\beta_{1},\beta_{2})}$.

Now for a given $\underline{\alpha}=(0,0,\ldots,0,\alpha_{n-1},\alpha_{n})$
with $\alpha_{n-1}\alpha_{n}\neq 0$, suppose

(3.1)
$\displaystyle\alpha^{\prime}_{n-1}=\frac{\alpha_{n-1}}{\prod_{l=1}^{n-2}\big{(}\frac{z_{l}-z_{n-1}}{1-\overline{z_{l}}z_{n-1}}\big{)}}\neq\frac{\alpha_{n}}{\prod_{l=1}^{n-2}\big{(}\frac{z_{l}-z_{n}}{1-\overline{z_{l}}z_{n}}\big{)}}=\alpha^{\prime}_{n-1}.$

Then there is a $t>0$, depending only on $\underline{\alpha}$ and $z_{j}$s
such that

$m(t\alpha^{\prime}_{n-1},t\alpha^{\prime}_{n})=c^{*}_{\mathbb{D}}(z_{n-1},z_{n})=m(z_{n-1},z_{n}).$

By the Schwarz-Pick lemma, there is a $\varphi_{t}\in Aut(\mathbb{D})$ such
that $\varphi_{t}(z_{n-1})=t\alpha^{\prime}_{n-1}$ and
$\varphi_{t}(z_{n})=t\alpha^{\prime}_{n}$. Now consider the function

(3.2) $\displaystyle
f_{t}(z)=\varphi_{t}(z)\prod_{l=1}^{n-2}\Big{(}\frac{z_{l}-z}{1-\overline{z_{l}}z}\Big{)}.$

This $f_{t}$ is in $H^{\infty}_{1}(\mathbb{D})$ and
$\underline{f_{t}}=(0,0,\ldots,0,t\alpha_{n-1},t\alpha_{n})\in\mathbb{C}\cdot\underline{\alpha}$.

######  Proposition 3.2.

Suppose we are given
$\underline{\alpha}=(0,0,\ldots,0,\alpha_{n-1},\alpha_{n})$ with
$\alpha_{n-1}\alpha_{n}\neq 0$. Then we have the following.

  1. (1)

$d_{\underline{\alpha}}(z_{i},z_{j})=0,\,\,\text{for}\,\,1\leq i,j\leq n-2.$

  2. (2)

If
$\frac{\alpha_{n-1}}{\prod_{l=1}^{n-2}\big{(}\frac{z_{l}-z_{n-1}}{1-\overline{z_{l}}z_{n-1}}\big{)}}=\frac{\alpha_{n}}{\prod_{l=1}^{n-2}\big{(}\frac{z_{l}-z_{n}}{1-\overline{z_{l}}z_{n}}\big{)}}$,
then

$\displaystyle d_{\underline{\alpha}}(z_{i},z_{j})$
$\displaystyle=|f_{0}(z_{j})|,\,\,\text{for}\,\,1\leq i\leq n-2,j=n-1,n,$
$\displaystyle=m(f_{0}(z_{n-1}),f_{0}(z_{n})),\,\,\text{for}\,\,i=n-1,j=n$

where
$f_{0}(z)=\prod_{l=1}^{n-2}\big{(}\frac{z_{l}-z}{1-\overline{z_{l}}z}\big{)}$.

  3. (3)

If
$\frac{\alpha_{n-1}}{\prod_{l=1}^{n-2}\big{(}\frac{z_{l}-z_{n-1}}{1-\overline{z_{l}}z_{n-1}}\big{)}}\neq\frac{\alpha_{n}}{\prod_{l=1}^{n-2}\big{(}\frac{z_{l}-z_{n}}{1-\overline{z_{l}}z_{n}}\big{)}}$,
then

$\displaystyle d_{\underline{\alpha}}(z_{i},z_{j})$
$\displaystyle=|f_{t}(z_{j})|,\,\,\text{for}\,\,1\leq i\leq n-2,j=n-1,n,$
$\displaystyle=m(f_{t}(z_{n-1}),f_{t}(z_{n})),\,\,\text{for}\,\,i=n-1,j=n$

where $f_{t}(z)$ is given by (3.2).

###### Proof.

  1. (1)

The first statement is trivial.

  2. (2)

For proving the second statement, let us suppose we have
$\frac{\alpha_{n-1}}{f_{0}(z_{n-1})}=\frac{\alpha_{n}}{f_{0}(z_{n})}$, that
is, $\mathbb{C}\cdot\underline{\alpha}=\mathbb{C}\cdot\underline{f}$. Let
$f\in H^{\infty}_{1}(\mathbb{D})$ be such that
$\underline{f}\in\mathbb{C}\cdot\underline{f_{0}}$. Then there is an $f_{1}\in
H^{\infty}_{1}(\mathbb{D})$ such that $f(z)=f_{0}(z)f_{1}(z)$ for all
$z\in\mathbb{D}$. Hence, for any $i\neq n-1,n$, we have
$m(f(z_{i}),f(z_{n-1}))=|f(z_{n-1})|\leq|f_{0}(z_{n-1})|$. Also
$|f_{0}(z_{n-1})|\leq d_{\underline{\alpha}}(z_{i},z_{n-1})$. Since
$d_{\underline{\alpha}}(z_{i},z_{n-1})$ is attained by some function in $\in
H^{\infty}_{1}(\mathbb{D})$, we obtain that
$d_{\underline{\alpha}}(z_{i},z_{n-1})=|f_{0}(z_{n-1})|$. Similarly we can
show that $d_{\underline{\alpha}}(z_{i},z_{n})=|f_{0}(z_{n})|$.

Now suppose $f\in H^{\infty}_{1}(\mathbb{D})$ satisfies
$\underline{f}=\lambda\underline{f_{0}}$ for some $\lambda\in\mathbb{C}$ and
$d_{\underline{\alpha}}(z_{n-1},z_{n})=m(f(z_{n-1}),f(z_{n}))$. So we have

$\displaystyle m(f_{0}(z_{n-1}),f_{0}(z_{n}))$ $\displaystyle\leq
d_{\underline{\alpha}}(z_{n-1},z_{n})$ $\displaystyle=m(\lambda
f_{0}(z_{n-1}),\lambda f_{0}(z_{n}))$

which implies $1\leq|\lambda|$. On the other hand, if $f_{1}\in
H^{\infty}_{1}(\mathbb{D})$ is the function that satisfies $f=f_{0}f_{1}$,
then we have

$f_{1}(z_{n-1})=\frac{f(z_{n-1})}{f_{0}(z_{n-1})}=\lambda=\frac{f(z_{n})}{f_{0}(z_{n})}=f_{1}(z_{n}).$

Thus $|\lambda|\leq 1$. This concludes the proof.

  3. (3)

Let
$\frac{\alpha_{n-1}}{\prod_{l=1}^{n-2}\big{(}\frac{z_{l}-z_{n-1}}{1-\overline{z_{l}}z_{n-1}}\big{)}}\neq\frac{\alpha_{n}}{\prod_{l=1}^{n-2}\big{(}\frac{z_{l}-z_{n}}{1-\overline{z_{l}}z_{n}}\big{)}}$
hold. We consider $f_{t}$ and $\varphi_{t}$ as constructed in (3.2), and
$f_{0}$ as above. For $i\neq n-1,n$, there is an $f\in H^{\infty}_{1}(\Omega)$
such that $\underline{f}\in\mathbb{C}\cdot\underline{\alpha}$ and
$d_{\underline{\alpha}}(z_{i},z_{n-1})=m(f(z_{i}),f(z_{n-1}))=|f(z_{n-1})|$.
Moreover, there is a $\lambda\in\mathbb{C}$ and an $f_{1}\in
H^{\infty}_{1}(\Omega)$ such that $\underline{f}=\lambda\underline{f_{t}}$ and
$f=f_{0}f_{1}$. Clearly, $f_{1}(z_{n-1})=\lambda\varphi_{t}(z_{n-1})$ (and
similarly $f_{1}(z_{n})=\lambda\varphi_{t}(z_{n})$). So we can write

$\displaystyle m(\lambda\varphi_{t}(z_{n-1}),\lambda\varphi_{t}(z_{n}))$
$\displaystyle=m(f_{1}(z_{n-1}),f_{1}(z_{n}))$ $\displaystyle\leq
m(z_{n-1},z_{n})$ $\displaystyle=m(\varphi_{t}(z_{n-1}),\varphi_{t}(z_{n}))$

which suggests $|\lambda|\leq 1$. Also $|f_{t}(z_{n-1})|\leq
d_{\underline{\alpha}}(z_{i},z_{n-1})=|f(z_{n-1})|=|\lambda f_{t}(z_{n-1})|$
implies $1\leq|\lambda|$. Similarly, one can show that
$d_{\underline{\alpha}}(z_{i},z_{n})=|f_{t}(z_{n})|$.

Now we show that
$d_{\underline{\alpha}}(z_{n-1},z_{n})=m(f_{t}(z_{n-1}),f_{t}(z_{n}))$. We
find $g,g_{1}\in H^{\infty}_{1}(\mathbb{D})$ and $\lambda\in\mathbb{C}$ such
that $\underline{g}=\lambda\underline{f_{t}}$,
$d_{\underline{\alpha}}(z_{n-1},z_{n})=m(g(z_{n-1}),g(z_{n}))$ and
$g=f_{0}g_{1}$. This gives us $g_{1}(z_{n-1})=\lambda\varphi_{t}(z_{n-1})$ and
$g_{1}(z_{n})=\lambda\varphi_{t}(z_{n})$. So we have

$\displaystyle m(\lambda\varphi_{t}(z_{n-1}),\lambda\varphi_{t}(z_{n}))$
$\displaystyle=m(g_{1}(z_{n-1}),g_{1}(z_{n}))$ $\displaystyle\leq
m(z_{n-1},z_{n})$ $\displaystyle=m(\varphi_{t}(z_{n-1}),\varphi_{t}(z_{n}))$

and hence $|\lambda|\leq 1$. On the other hand

$\displaystyle m(f_{t}(z_{n-1}),f_{t}(z_{n}))$ $\displaystyle\leq
d_{\underline{\alpha}}(z_{n-1},z_{n})$ $\displaystyle=m(g(z_{n-1}),g(z_{n}))$
$\displaystyle=m(\lambda f_{t}(z_{n-1}),\lambda f_{t}(z_{n}))$

implies $|\lambda|\geq 1$. The proof is now complete.

∎

Next let us describe the boundary of $\mathscr{D}_{n}$. It can be shown that

$\displaystyle\partial\mathscr{D}_{n}=$
$\displaystyle\\{(w,\ldots,w):w\in\partial\mathbb{D}\\}$
$\displaystyle\cup\big{[}\cup_{1\leq i<j\leq
n}\\{(w_{1},\ldots,w_{n})\in\mathbb{D}^{n}:w_{i}\neq
w_{j},m(w_{i},w_{j})=d_{\underline{w}}(z_{i},z_{j})\\}\big{]}.$

######  Lemma 3.3.

$(w_{1},\ldots,w_{n})\in\partial\mathscr{D}_{n}\cap\mathbb{D}^{n}$ if and only
if

$\Big{(}\frac{\varphi_{w_{n}}(w_{1})}{\varphi_{z_{n}}(z_{1})},\ldots,\frac{\varphi_{w_{n}}(w_{n-1})}{\varphi_{z_{n}}(z_{n-1})}\Big{)}\in\partial\mathscr{D}_{n-1}$

where
$\varphi_{u}(v)=\frac{u-v}{1-\overline{u}v},\mathscr{D}_{n}=\mathscr{D}_{\mathbb{D}}(z_{1},\ldots,z_{n}),$
and $\mathscr{D}_{n-1}=\mathscr{D}_{\mathbb{D}}(z_{1},\ldots,z_{n-1})$.

###### Proof.

The proof follows from making the following observations:

  1. (1)

$\partial\mathscr{D}_{n}$ consists of the points that can be attained by
functions of norm one but not by functions of norm strictly less than one.

  2. (2)

$\partial\mathscr{D}_{n}$ is invariant under the action of the elements of
$Aut(\mathscr{D}_{n})$ described in (2.1).

  3. (3)

For any $f\in H^{\infty}_{1}(\mathbb{D})$ with $f(u)=0$, there is an $f_{1}\in
H^{\infty}_{1}(\mathbb{D})$ such that $f(z)=\varphi_{u}(z)f_{1}(z)$.

∎

The implication of the following two results are previously known in some
other form. However, we produce new proofs which provide new insight of the
things that are taking place underneath.

######  Theorem 3.4.

$(w_{1},\ldots,w_{n})\in\partial\mathscr{D}_{n}$ if and only if there is a
finite Blaschke product $\varphi$ of degree at most $(n-1)$ such that
$\varphi(z_{j})=w_{j},1\leq j\leq n$.

###### Proof.

($\Leftarrow$): We apply induction on $n$. Let $\varphi_{n-1}$ be a finite
Blaschke product of degree at most $(n-1)$ and
$\varphi_{n-1}(z_{j})=w_{j},1\leq j\leq n$.

For $n=1$ we have $\varphi_{0}(z)=e^{i\theta}$, so
$\varphi_{0}(z_{1})\in\partial\mathscr{D}_{1}=\partial\mathbb{D}$.

For $n=2$, $\varphi_{1}$ is either the constant function with modulus one or
is an element of $Aut(\mathbb{D})$. In any case,
$(\varphi_{1}(z_{1}),\varphi_{1}(z_{2}))\in\mathscr{D}_{2}$.

Let the statement be true for $n=m$. Suppose $\varphi_{m}$ is a Blaschke
product of degree at most $m$ and
$(w_{1},\ldots,w_{m+1})=(\varphi_{m}(z_{1}),\ldots,\varphi_{m}(z_{m+1}))$. If
the degree of $\varphi_{m}$ is zero, the result is clear. To see the other
case, consider the function $\psi_{m}=\varphi_{w_{m+1}}\circ\varphi_{m}(z)$.
Then $\psi_{m}$ is a Blaschke product of degree at most $m$ with a zero at
$z_{m+1}$. Hence the function
$\psi_{m-1}(z)=\frac{\psi_{m}(z)}{\varphi_{z_{m+1}}(z)}$ is a Blaschke product
of degree at most $m-1$. By induction hypothesis
$(\psi_{m-1}(z_{1}),\ldots,\psi_{m-1}(z_{m}))\in\partial\mathscr{D}_{m}$, that
is,

$\Big{(}\frac{\varphi_{w_{m+1}}(w_{1})}{\varphi_{z_{m+1}}(z_{1})},\ldots,\frac{\varphi_{w_{m+1}}(w_{m})}{\varphi_{z_{m+1}}(z_{m})}\Big{)}\in\partial\mathscr{D}_{m}.$

Now Lemma 3.3 gives rest of the argument.

($\Rightarrow$): We again apply induction on $n$.

For $n=1$ and $2$, the result is clear. Suppose that the statement is true for
$n=m$ and let $(w_{1},\ldots,w_{m+1})\in\partial\mathscr{D}_{m+1}$. If
$|w_{m+1}|=1$, the constant function $\varphi_{m}(z)=w_{m+1}$ works. For
$|w_{m+1}|<1$, we have
$(w_{1},\ldots,w_{m+1})\in\partial\mathscr{D}_{m+1}\cap\mathbb{D}^{n}$. So by
Lemma 3.3 we obtain

$\Big{(}\frac{\varphi_{w_{m+1}}(w_{1})}{\varphi_{z_{m+1}}(z_{1})},\ldots,\frac{\varphi_{w_{m+1}}(w_{m})}{\varphi_{z_{m+1}}(z_{m})}\Big{)}\in\partial\mathscr{D}_{m}.$

By induction hypothesis there is a Blaschke product $\varphi_{m-1}$ of degree
at most $m-1$ such that
$\varphi_{m-1}(z_{j})=\frac{\varphi_{w_{m+1}}(w_{j})}{\varphi_{z_{m+1}}(z_{j})},1\leq
j\leq m$. We now take the Blaschke product

$\varphi_{m}(z)=\varphi_{w_{m+1}}(\varphi_{z_{m+1}}(z)\varphi_{m-1}(z))$

which is of degree at most $m$ and satisfies $\varphi_{m}(z_{j})=w_{j},1\leq
j\leq m+1$.

This completes our proof. ∎

######  Theorem 3.5.

The solution to a solvable interpolation problem $\mathbb{D}\ni z_{j}\mapsto
w_{j}\in\mathbb{D},1\leq j\leq n,$ is unique if and only if
$(w_{1},\ldots,w_{n})\in\partial\mathscr{D}_{n}$.

###### Proof.

The result is clear if $n=1$. Let the statement be true for $n=m$.

($\Leftarrow$): Let $(w_{1},\ldots,w_{m+1})\in\partial\mathscr{D}_{m+1}$. If
$|w_{m+1}|=1$, then the unique solution is the constant function
$\varphi(z)=w_{m+1}$. For the other case, Lemma 3.3 gives us

$\Big{(}\frac{\varphi_{w_{m+1}}(w_{1})}{\varphi_{z_{m+1}}(z_{1})},\ldots,\frac{\varphi_{w_{m+1}}(w_{m})}{\varphi_{z_{m+1}}(z_{m})}\Big{)}\in\partial\mathscr{D}_{m}.$

By induction hypothesis and Theorem 3.4, there is a unique Blaschke product
$\varphi_{m-1}$ of degree at most $m-1$ such that $\varphi_{m-1}$ takes
$z_{j}$ to $\frac{\varphi_{w_{m+1}}(w_{j})}{\varphi_{z_{m+1}}(z_{j})},1\leq
j\leq m$. If $g\in H^{\infty}_{1}(\mathbb{D})$ is a solution to the problem
$z_{j}\mapsto w_{j},1\leq j\leq m+1$, then
$\frac{\varphi_{w_{m+1}}(g(z))}{\varphi_{z_{m+1}}(z)}$ sends $z_{j}$ to
$\frac{\varphi_{w_{m+1}}(w_{j})}{\varphi_{z_{m+1}}(z_{j})},1\leq j\leq m$.
Using the uniqueness of $\varphi_{m-1}$ we find that
$g(z)=\varphi_{w_{m+1}}(\varphi_{z_{m+1}}(z)\varphi_{m-1}(z))$. So this $g$ is
unique.

($\Rightarrow$): Let the solution to the interpolation problem $z_{j}\mapsto
w_{j},1\leq j\leq m+1$, be unique and let $g$ be the solution. Clearly, the
problem
$z_{j}\mapsto\frac{\varphi_{w_{m+1}}(w_{j})}{\varphi_{z_{m+1}}(z_{j})},1\leq
j\leq m,$ is solvable. If $h_{0}$ is a solution to this problem, then it is
easy to see that the function
$h(z)=\varphi_{w_{m+1}}(\varphi_{z_{m+1}}(z)h_{0}(z))$ solves the
interpolation problem $z_{j}\mapsto w_{j},1\leq j\leq m+1,$ and hence, $h=g$.
This gives us $h_{0}(z)=\frac{\varphi_{w_{m+1}}(g(z))}{\varphi_{z_{m+1}}(z)}$
(note that $\varphi_{w_{m+1}}(g(z))$ has a zero at $z_{m+1}$). So the
uniqueness of $g$ passes onto $h_{0}$ and induction hypothesis together with
Lemma 3.3 imply that $(w_{1},\ldots,w_{m+1})\in\partial\mathscr{D}_{m+1}$.

This completes the proof. ∎

The theorems above give us a way to relate the domain $\mathscr{D}_{n}$ and
the degree of the Blaschke product interpolating the boundary points of
$\mathscr{D}_{n}$.

######  Corollary 3.6.

Let $(w_{1},\ldots,w_{n})\in\partial\mathscr{D}_{n}$ and $\varphi$ a Blaschke
product sending $z_{j}$ to $w_{j}$, $1\leq j\leq n$. Then $\varphi$ is of
degree at most $k-1$ if and only if $k$ is the least positive integer for
which there are $w_{i_{1}},\ldots,w_{i_{k}}\in\\{w_{1},\ldots,w_{n}\\}$ such
that

$\displaystyle(w_{i_{1}},\ldots,w_{i_{k}})\in\partial\mathscr{D}_{\mathbb{D}}(z_{i_{1}},\ldots,z_{i_{k}}).$

###### Proof.

($\Rightarrow$): Let $\varphi$ has degree $k-1$. Then using Theorem 3.4, we
see that for any $z_{i_{1}},\ldots,z_{i_{k}}\in\\{z_{1},\ldots,z_{n}\\}$ we
have

$\displaystyle(w_{i_{1}},\ldots,w_{i_{k}})=(\varphi(z_{i_{1}}),\ldots,\varphi(z_{i_{k}}))\in\partial\mathscr{D}_{\mathbb{D}}(z_{i_{1}},\ldots,z_{i_{k}}).$

($\Leftarrow$): Let $k$ be the least positive integer for which there are
$w_{i_{1}},\ldots,w_{i_{k}}\in\\{w_{1},\ldots,w_{n}\\}$ such that

$\displaystyle(w_{i_{1}},\ldots,w_{i_{k}})\in\partial\mathscr{D}_{\mathbb{D}}(z_{i_{1}},\ldots,z_{i_{k}}).$

Then by Theorem 3.4, there is a Blaschke product $\psi$ of degree at most
$k-1$ such that $\psi(z_{i_{j}})=w_{i_{j}}$, $1\leq j\leq k$. Note that $k$ is
the least positive integer satisfying the above. If $\psi$ is a Blaschke
product of degree less than $k-1$, then it contradicts with the minimality of
$k$ (this follows from Theorem 3.4). By Theorem 3.5, $\psi$ is unique. Thus,
$\psi$ is a Blaschke product of degree $k-1$ and $\psi=\varphi$. Thus he
stated claim therefore holds true. ∎

Lastly, let us now describe the values of
$d_{\underline{\alpha}}^{\mathbb{D}}$ for arbitrary $\underline{\alpha}$. We
recall that if $\underline{\alpha}\in\mathbb{C}^{n}$ is a nonzero element and
$t=\frac{1}{\mu_{\mathscr{D}_{n}}(\underline{\alpha})}$, then for any $i$ and
$j$, $d_{\underline{\alpha}}(z_{i},z_{j})=m(t\alpha_{i},t\alpha_{j})$ and
$t\cdot\underline{\alpha}\in\partial\mathscr{D}_{n}$. Once one finds $t$,
$d_{\underline{\alpha}}$ can easily be computed. We know that an interpolation
problem $\mathbb{D}\ni z_{j}\mapsto w_{j}\in\mathbb{D},1\leq i,j\leq n$, is
solvable if and only if the matrix

$\displaystyle\mathcal{M}=\begin{pmatrix}\frac{1-w_{i}\overline{w_{j}}}{1-z_{i}\overline{z_{j}}}\end{pmatrix}_{1\leq
i,j\leq n}$

is positive semidefinite. Also, the solution is a unique if and only if
$det(\mathcal{M})=0$. By Theorem 3.4 and 3.5 we can say that the positive
number $t=\frac{1}{\mu_{\mathscr{D}_{n}}(\underline{\alpha})}$ is a root of
the equation

(3.3) $\displaystyle
det\begin{pmatrix}\frac{1-x^{2}\alpha_{i}\overline{\alpha_{j}}}{1-z_{i}\overline{z_{j}}}\end{pmatrix}=0.$

Since the left hand side is a polynomial in the single variable $x$, it is
solvable. Let us now consider the following quantity

(3.4) $\displaystyle t=max\Big{\\{}x\geq 0:x\,\,\text{is a root
of}\,\,(\ref{EquationGivingMinkowski})\,\,\text{and}\,\,\begin{pmatrix}\frac{1-x^{2}\alpha_{i}\overline{\alpha_{j}}}{1-z_{i}\overline{z_{j}}}\end{pmatrix}\geq\mathbf{0}\Big{\\}}.$

######  Theorem 3.7.

The quantity $t$ given by (3.4) is
$\frac{1}{\mu_{\mathscr{D}_{n}}(\underline{\alpha})}$.

###### Proof.

We have

$\displaystyle
det\begin{pmatrix}\frac{1-t^{2}\alpha_{i}\overline{\alpha_{j}}}{1-z_{i}\overline{z_{j}}}\end{pmatrix}=0\,\,\text{and}\,\,\begin{pmatrix}\frac{1-t^{2}\alpha_{i}\overline{\alpha_{j}}}{1-z_{i}\overline{z_{j}}}\end{pmatrix}\geq\mathbf{0}.$

So the interpolation problem $z_{j}\mapsto t\alpha_{j}$ is solvable and its
solution is unique. Theorem 3.5 implies that
$t\cdot\underline{\alpha}\in\partial\mathscr{D}_{n}$. Since
$\partial\mathscr{D}_{n}=\\{\mu_{\mathscr{D}_{n}}=1\\}$, the proof follows. ∎

Acknowledgements: The author’s research is supported by GACR (Czech grant
agency) grant 22-15012J. The author thanks Dr. Anwoy Maitra for fruitful
discussions.

## References

  * [1] A. F. Beardon, D. Minda, A multi-point Schwarz-Pick lemma, J. Anal. Math. 92 (2004), 81–104.
  * [2] A. Biswas, A. Maitra, A characterization of the bidisc by a subgroup of its automorphism group, J. Math. Anal. Appl. 504 (2021), no. 2, Paper No. 125434.
  * [3] H. Cartan, Sur les transformations analytiques des domaines cerclés et semi-cerclés bornés. Math. Ann. 106, 540–573 (1932)
  * [4] B. Cole, K. Lewis, J. Wermer, Pick conditions on a uniform algebra and von Neumann inequalities J. Funct. Anal. 107 (1992), no. 2, $235-254$
  * [5] B. Cole, K. Lewis, J. Wermer, A characterization of Pick bodies, J. London Math. Soc. (2) 48 (1993), no. 2, $316-328$.
  * [6] B. Cole, J. Wermer, Pick interpolation, von Neumann inequalities, and hyperconvex sets, Complex potential theory (Montreal, PQ, 1993), NATO Adv. Sci. Inst. Ser. C: Math. Phys. Sci., 439, Kluwer Acad. Publ., Dordrecht, 1994, $89-129$.
  * [7] B. Cole, J. Wermer, Interpolation in the bidisk J. Funct. Anal. 140 (1996), no. 1, $194-217$.
  * [8] B. Cole, J. Wermer, Boundaries of interpolation bodies, Houston J. Math. 23 (1997), no. 3, $499-527$.
  * [9] M. Elin, F. Jacobzon, M. Levenshtein, D. Shoikhet, The Schwarz lemma: rigidity and dynamics, Harmonic and complex analysis and its applications, 135–230, Trends Math., Birkhäuser/Springer, Cham, 2014.
  * [10] A. V. Isaev, Hyperbolic 2-dimensional manifolds with 3-dimensional automorphism group, Geometry and Topology 12 (2008), no. 2, $643-711$.
  * [11] M. Jarnicki, P. Pflug, Invariant Distances and Metrics in Complex Analysis, 2nd extended edition, De Gruyter, Berlin, 2013.
  * [12] R. Nevanlinna, Über beschränkte Funktionen, die in gegeben Punkten vorgeschrieben Werte annehmen. Ann. Acad. Sci. fenn. Ser. A, 13, no. 1., 1919.
  * [13] G. Pick, Über die Beschränkungen analytischer Funktionen, welche durch vorgegebene Funktionswerte bewirkt werden, Math. Ann. 11 (1916),$7-23$.