TITLE: $\frac{\sqrt{9+x}{-3}}{x}$ for $x = 10^{-n}$, $n \in \{4,...,13\}$ and interpret the observations
QUESTION [1 upvotes]: I am looking for some help with the following question. I am really stuck!
I am trying to use python to evaluate
$$\frac{\sqrt{9+x}{-3}}{x}$$
for $x = 10^{-n}$, $n \in \{4,...,13\}$ and interpret the observations. Is there a better way to evaluate this expression?
I am not sure how to proceed with this, maybe multiplying by a conjugate and evaluating would be better?

REPLY [3 votes]: Obviously if you multiply the numerator and denominator by the conjugate expression$\sqrt{9+x}+3$, you can prove that the limiting value is $1/6$.  To wit:
$\frac{\sqrt{9+x}-3}{x}=\frac{9+x-3^2}{x(\sqrt{9+x}+3)}=\frac{1}{\sqrt{9+x}+3}\rightarrow 1/6 \text{ as }x\rightarrow 0$
But I suspect this is a computer exercise, meaning you should just punch the expression into your computer or calculator and see what happens.
If your machine is like most machines (all machines if you keep trying lower powers of ten), you seem to approach $0.16666...$ with no problem ... until, when the absolute value of the exponent gets large enough, there are suddenly random deviations that keep getting worse.  That is what you should be looking for, and interpreting as ill conditioning when you subtract numbers close to each other.
If you put in the conjugate factor in the numerator and denominator and try again, you kill the deviations.  This is an example of removing the ill-conditioned operation.


text:
(*
  File:     Furstenberg_Topology.thy
  Author:   Manuel Eberl, TU München
*)
section \<open>Furstenberg's topology and his proof of the infinitude of primes\<close>
theory Furstenberg_Topology
  imports
    "HOL-Real_Asymp.Real_Asymp"
    "HOL-Analysis.Analysis"
    "HOL-Number_Theory.Number_Theory"
begin

text \<open>
  This article gives a formal version of Furstenberg's topological proof of the infinitude of
  primes~\cite{furstenberg}. He defines a topology on the integers based on arithmetic progressions
  (or, equivalently, residue classes).

  Apart from yielding a short proof of the infinitude of primes, this topology is also fairly
  `nice' in general: it is second countable, metrizable, and perfect. All of these (well-known)
  facts will be formally proven below.
\<close>

subsection \<open>Arithmetic progressions of integers\<close>

text \<open>
  We first define `bidirectional infinite arithmetic progressions' on \<open>\<int>\<close> in the sense that
  to an integer \<open>a\<close> and a positive integer \<open>b\<close>, we associate all the integers \<open>x\<close> such that
  $x \equiv a\ (\text{mod}\ b)$, or, equivalently, $\{a + nb\mid n\in\mathbb{Z}\}$.
\<close>

definition arith_prog :: "int \<Rightarrow> nat \<Rightarrow> int set" where
  "arith_prog a b = {x. [x = a] (mod int b)}"

lemma arith_prog_0_right [simp]: "arith_prog a 0 = {a}"
  by (simp add: arith_prog_def)

lemma arith_prog_Suc_0_right [simp]: "arith_prog a (Suc 0) = UNIV"
  by (auto simp: arith_prog_def)

lemma in_arith_progI [intro]: "[x = a] (mod b) \<Longrightarrow> x \<in> arith_prog a b"
  by (auto simp: arith_prog_def)

text \<open>
  Two arithmetic progressions with the same period and noncongruent starting points are
  disjoint.
\<close>
lemma arith_prog_disjoint:
  assumes "[a \<noteq> a'] (mod int b)" and "b > 0"
  shows   "arith_prog a b \<inter> arith_prog a' b = {}"
  using assms by (auto simp: arith_prog_def cong_def)

text \<open>
  Multiplying the period gives us a subset of the original progression.
\<close>
lemma arith_prog_dvd_mono: "b dvd b' \<Longrightarrow> arith_prog a b' \<subseteq> arith_prog a b"
  by (auto simp: arith_prog_def cong_dvd_modulus)

text \<open>
  The following proves the alternative definition mentioned above.
\<close>
lemma bij_betw_arith_prog:
  assumes "b > 0"
  shows   "bij_betw (\<lambda>n. a + int b * n) UNIV (arith_prog a b)"
proof (rule bij_betwI[of _ _ _ "\<lambda>x. (x - a) div int b"], goal_cases)
  case 1
  thus ?case
    by (auto simp: arith_prog_def cong_add_lcancel_0 cong_mult_self_right mult_of_nat_commute)
next
  case 4
  thus ?case
    by (auto simp: arith_prog_def cong_iff_lin)
qed (use \<open>b > 0\<close> in \<open>auto simp: arith_prog_def\<close>)

lemma arith_prog_altdef: "arith_prog a b = range (\<lambda>n. a + int b * n)"
proof (cases "b = 0")
  case False
  thus ?thesis
    using bij_betw_arith_prog[of b] by (auto simp: bij_betw_def)
qed auto

text \<open>
  A simple corollary from this is also that any such arithmetic progression is infinite.
\<close>
lemma infinite_arith_prog: "b > 0 \<Longrightarrow> infinite (arith_prog a b)"
  using bij_betw_finite[OF bij_betw_arith_prog[of b]] by simp

subsection \<open>The Furstenberg topology on \<open>\<int>\<close>\<close>

text \<open>
  The typeclass-based topology is somewhat nicer to use in Isabelle/HOL, but the integers,
  of course, already have a topology associated to them. We therefore need to introduce a type
  copy of the integers and furnish them with the new topology. We can easily convert between
  them and the `proper' integers using Lifting and Transfer.
\<close>
typedef fbint = "UNIV :: int set"
  morphisms int_of_fbint fbint ..

setup_lifting type_definition_fbint

lift_definition arith_prog_fb :: "int \<Rightarrow> nat \<Rightarrow> fbint set" is "arith_prog" .

instantiation fbint :: topological_space
begin

text \<open>
  Furstenberg defined the topology as the one generated by all arithmetic progressions.
  We use a slightly more explicit equivalent formulation that exploits the fact that
  the intersection of two arithmetic progressions is again an arithmetic progression (or empty).
\<close>
lift_definition open_fbint :: "fbint set \<Rightarrow> bool" is
  "\<lambda>U. (\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U)" .

text \<open>
  We now prove that this indeed forms a topology.
\<close>
instance proof
  show "open (UNIV :: fbint set)"
    by transfer auto
next
  fix U V :: "fbint set"
  assume "open U" and "open V"
  show "open (U \<inter> V)"
  proof (use \<open>open U\<close> \<open>open V\<close> in transfer, safe)
    fix U V :: "int set" and x :: int
    assume U: "\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U" and V: "\<forall>x\<in>V. \<exists>b>0. arith_prog x b \<subseteq> V"
    assume x: "x \<in> U" "x \<in> V"
    from U x obtain b1 where b1: "b1 > 0" "arith_prog x b1 \<subseteq> U" by auto
    from V x obtain b2 where b2: "b2 > 0" "arith_prog x b2 \<subseteq> V" by auto
    from b1 b2 have "lcm b1 b2 > 0" "arith_prog x (lcm b1 b2) \<subseteq> U \<inter> V"
      using arith_prog_dvd_mono[of b1 "lcm b1 b2" x] arith_prog_dvd_mono[of b2 "lcm b1 b2" x]
      by (auto simp: lcm_pos_nat)
    thus "\<exists>b>0. arith_prog x b \<subseteq> U \<inter> V" by blast
  qed
next
  fix F :: "fbint set set"
  assume *: "\<forall>U\<in>F. open U"
  show "open (\<Union>F)"
  proof (use * in transfer, safe)
    fix F :: "int set set" and U :: "int set" and x :: int
    assume F: "\<forall>U\<in>F. \<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U"
    assume "x \<in> U" "U \<in> F"
    with F obtain b where b: "b > 0" "arith_prog x b \<subseteq> U" by blast
    with \<open>U \<in> F\<close> show "\<exists>b>0. arith_prog x b \<subseteq> \<Union>F"
      by blast
  qed
qed

end

text \<open>
  Since any non-empty open set contains an arithmetic progression and arithmetic progressions
  are infinite, we obtain that all nonempty open sets are infinite.
\<close>
lemma open_fbint_imp_infinite:
  fixes U :: "fbint set"
  assumes "open U" and "U \<noteq> {}"
  shows   "infinite U"
  using assms
proof transfer
  fix U :: "int set"
  assume *: "\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U" and "U \<noteq> {}"
  from \<open>U \<noteq> {}\<close> obtain x where "x \<in> U" by auto
  with * obtain b where b: "b > 0" "arith_prog x b \<subseteq> U" by auto
  from b have "infinite (arith_prog x b)"
    using infinite_arith_prog by blast
  with b show "infinite U"
    using finite_subset by blast
qed

lemma not_open_finite_fbint [simp]:
  assumes "finite (U :: fbint set)" "U \<noteq> {}"
  shows   "\<not>open U"
  using open_fbint_imp_infinite assms by blast

text \<open>
  More or less by definition, any arithmetic progression is open.
\<close>
lemma open_arith_prog_fb [intro]:
  assumes "b > 0"
  shows   "open (arith_prog_fb a b)"
  using assms
proof transfer
  fix a :: int and b :: nat
  assume "b > 0"
  show "\<forall>x\<in>arith_prog a b. \<exists>b'>0. arith_prog x b' \<subseteq> arith_prog a b"
  proof (intro ballI exI[of _ b] conjI)
    fix x assume "x \<in> arith_prog a b"
    thus "arith_prog x b \<subseteq> arith_prog a b"
      using cong_trans by (auto simp: arith_prog_def )
  qed (use \<open>b > 0\<close> in auto)
qed

text \<open>
  Slightly less obviously, any arithmetic progression is also closed.
  This can be seen by realising that for a period \<open>b\<close>, we can partition the integers
  into \<open>b\<close> congruence classes and then the complement of each congruence class is the
  union of the other \<open>b - 1\<close> classes, and unions of open sets are open.
\<close>
lemma closed_arith_prog_fb [intro]:
  assumes "b > 0"
  shows   "closed (arith_prog_fb a b)"
proof -
  have "open (-arith_prog_fb a b)"
  proof -
    have "-arith_prog_fb a b = (\<Union>i\<in>{1..<b}. arith_prog_fb (a+i) b)"
    proof (transfer fixing: b)
      fix a :: int
      have disjoint: "x \<notin> arith_prog a b" if "x \<in> arith_prog (a + int i) b" "i \<in> {1..<b}" for x i
      proof -
        have "[a \<noteq> a + int i] (mod int b)"
        proof
          assume "[a = a + int i] (mod int b)"
          hence "[a + 0 = a + int i] (mod int b)" by simp
          hence "[0 = int i] (mod int b)" by (subst (asm) cong_add_lcancel) auto
          with that show False by (auto simp: cong_def)
        qed
        thus ?thesis using arith_prog_disjoint[of a "a + int i" b] \<open>b > 0\<close> that by auto
      qed

      have covering: "x \<in> arith_prog a b \<or> x \<in> (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)" for x
      proof -
        define i where "i = nat ((x - a) mod (int b))"
        have "[a + int i = a + (x - a) mod int b] (mod int b)"
          unfolding i_def using \<open>b > 0\<close> by simp
        also have "[a + (x - a) mod int b = a + (x - a)] (mod int b)"
          by (intro cong_add) auto
        finally have "[x = a + int i] (mod int b)"
          by (simp add: cong_sym_eq)
        hence "x \<in> arith_prog (a + int i) b"
          using \<open>b > 0\<close> by (auto simp: arith_prog_def)
        moreover have "i < b" using \<open>b > 0\<close>
          by (auto simp: i_def nat_less_iff)
        ultimately show ?thesis using \<open>b > 0\<close>
          by (cases "i = 0") auto
      qed

      from disjoint and covering show "- arith_prog a b = (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)"
        by blast
    qed
    also from \<open>b > 0\<close> have "open \<dots>"
      by auto
    finally show ?thesis .
  qed
  thus ?thesis by (simp add: closed_def)
qed

subsection \<open>The infinitude of primes\<close>

text \<open>
  The infinite of the primes now follows quite obviously: The multiples of any prime form a
  closed set, so if there were only finitely many primes, the union of all of these would also
  be open. However, since any number other than \<open>\<plusminus>1\<close> has a prime divisor, the union of all these
  sets is simply \<open>\<int>\<setminus>{\<plusminus>1}\<close>, which is obviously \<^emph>\<open>not\<close> closed since the finite set \<open>{\<plusminus>1}\<close> is not
  open.
\<close>
theorem "infinite {p::nat. prime p}"
proof
  assume fin: "finite {p::nat. prime p}"
  define A where "A = (\<Union>p\<in>{p::nat. prime p}. arith_prog_fb 0 p)"
  have "closed A"
    unfolding A_def using fin by (intro closed_Union) (auto simp: prime_gt_0_nat)
  hence "open (-A)"
    by (simp add: closed_def)
  also have "A = -{fbint 1, fbint (-1)}"
    unfolding A_def
  proof transfer
    show "(\<Union>p\<in>{p::nat. prime p}. arith_prog 0 p) = - {1, - 1}"
    proof (intro equalityI subsetI)
      fix x :: int assume x: "x \<in> -{1, -1}"
      hence "\<bar>x\<bar> \<noteq> 1" by auto
      show "x \<in> (\<Union>p\<in>{p::nat. prime p}. arith_prog 0 p)"
      proof (cases "x = 0")
        case True
        thus ?thesis
          by (auto simp: A_def intro!: exI[of _ 2])
      next
        case [simp]: False
        obtain p where p: "prime p" "p dvd x"
          using prime_divisor_exists[of x] and \<open>\<bar>x\<bar> \<noteq> 1\<close> by auto
        hence "x \<in> arith_prog 0 (nat p)" using prime_gt_0_int[of p]
          by (auto simp: arith_prog_def cong_0_iff)
        thus ?thesis using p
          by (auto simp: A_def intro!: exI[of _ "nat p"])
      qed
    qed (auto simp: A_def arith_prog_def cong_0_iff)
  qed
  also have "-(-{fbint 1, fbint (-1)}) = {fbint 1, fbint (-1)}"
    by simp
  finally have "open {fbint 1, fbint (-1)}" .
  thus False by simp
qed

subsection \<open>Additional topological properties\<close>

text \<open>
  Just for fun, let us also show a few more properties of Furstenberg's topology.
  First, we show the equivalence to the above to Furstenberg's original definition
  (the topology generated by all arithmetic progressions).
\<close>

theorem topological_basis_fbint: "topological_basis {arith_prog_fb a b |a b. b > 0}"
  unfolding topological_basis_def
proof safe
  fix a :: int and b :: nat
  assume "b > 0"
  thus "open (arith_prog_fb a b)"
    by auto
next
  fix U :: "fbint set" assume "open U"
  hence "\<forall>x\<in>U. \<exists>b. b > 0 \<and> arith_prog_fb (int_of_fbint x) b \<subseteq> U"
    by transfer
  hence "\<exists>f. \<forall>x\<in>U. f x > 0 \<and> arith_prog_fb (int_of_fbint x) (f x) \<subseteq> U"
    by (subst (asm) bchoice_iff)
  then obtain f where f: "\<forall>x\<in>U. f x > 0 \<and> arith_prog_fb (int_of_fbint x) (f x) \<subseteq> U" ..
  define B where "B = (\<lambda>x. arith_prog_fb (int_of_fbint x) (f x)) ` U"
  have "B \<subseteq> {arith_prog_fb a b |a b. b > 0}"
    using f by (auto simp: B_def)
  moreover have "\<Union>B = U"
  proof safe
    fix x assume "x \<in> U"
    hence "x \<in> arith_prog_fb (int_of_fbint x) (f x)"
      using f by transfer auto
    with \<open>x \<in> U\<close> show "x \<in> \<Union>B" by (auto simp: B_def)
  qed (use f in \<open>auto simp: B_def\<close>)
  ultimately show "\<exists>B'\<subseteq>{arith_prog_fb a b |a b. 0 < b}. \<Union> B' = U" by auto
qed

lemma open_fbint_altdef: "open = generate_topology {arith_prog_fb a b |a b. b > 0}"
  using topological_basis_imp_subbasis[OF topological_basis_fbint] .

text \<open>
  From this, we can immediately see that it is second countable:
\<close>
instance fbint :: second_countable_topology
proof
  have "countable ((\<lambda>(a,b). arith_prog_fb a b) ` (UNIV \<times> {b. b > 0}))"
    by (intro countable_image) auto
  also have "\<dots> = {arith_prog_fb a b |a b. b > 0}"
    by auto
  ultimately show "\<exists>B::fbint set set. countable B \<and> open = generate_topology B"
    unfolding open_fbint_altdef by auto
qed

text \<open>
  A trivial consequence of the fact that nonempty open sets in this topology are infinite
  is that it is a perfect space:
\<close>
instance fbint :: perfect_space
  by standard auto

text \<open>
  It is also Hausdorff, since given any two distinct integers, we can easily
  construct two non-overlapping arithmetic progressions that each contain one of them.
  We do not \<^emph>\<open>really\<close> have to prove this since we will get it for free later on when we
  show that it is a metric space, but here is the proof anyway:
\<close>
instance fbint :: t2_space
proof
  fix x y :: fbint
  assume "x \<noteq> y"
  define d where "d = nat \<bar>int_of_fbint x - int_of_fbint y\<bar> + 1"
  from \<open>x \<noteq> y\<close> have "d > 0"
    unfolding d_def by transfer auto
  define U where "U = arith_prog_fb (int_of_fbint x) d"
  define V where "V = arith_prog_fb (int_of_fbint y) d"

  have "U \<inter> V = {}" unfolding U_def V_def d_def
  proof (use \<open>x \<noteq> y\<close> in transfer, rule arith_prog_disjoint)
    fix x y :: int
    assume "x \<noteq> y"
    show "[x \<noteq> y] (mod int (nat \<bar>x - y\<bar> + 1))"
    proof
      assume "[x = y] (mod int (nat \<bar>x - y\<bar> + 1))"
      hence "\<bar>x - y\<bar> + 1 dvd \<bar>x - y\<bar>"
        by (auto simp: cong_iff_dvd_diff algebra_simps)
      hence "\<bar>x - y\<bar> + 1 \<le> \<bar>x - y\<bar>"
        by (rule zdvd_imp_le) (use \<open>x \<noteq> y\<close> in auto)
      thus False by simp
    qed
  qed auto
  moreover have "x \<in> U" "y \<in> V"
    unfolding U_def V_def by (use \<open>d > 0\<close> in transfer, fastforce)+
  moreover have "open U" "open V"
    using \<open>d > 0\<close> by (auto simp: U_def V_def)
  ultimately show "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}" by blast
qed

(* TODO Move? *)
text \<open>
  Next, we need a small lemma: Given an additional assumption, a $T_2$ space is also $T_3$:
\<close>
lemma t2_space_t3_spaceI:
  assumes "\<And>(x :: 'a :: t2_space) U. x \<in> U \<Longrightarrow> open U \<Longrightarrow>
             \<exists>V. x \<in> V \<and> open V \<and> closure V \<subseteq> U"
  shows   "OFCLASS('a, t3_space_class)"
proof
  fix X :: "'a set" and z :: 'a
  assume X: "closed X" "z \<notin> X"
  with assms[of z "-X"] obtain V where V: "z \<in> V" "open V" "closure V \<subseteq> -X"
    by auto
  show "\<exists>U V. open U \<and> open V \<and> z \<in> U \<and> X \<subseteq> V \<and> U \<inter> V = {}"
    by (rule exI[of _ V], rule exI[of _ "-closure V"])
       (use X V closure_subset[of V] in auto)
qed

text \<open>
  Since the Furstenberg topology is $T_2$ and every arithmetic progression is also closed,
  we can now easily show that it is also $T_3$ (i.\,e.\ regular).
  Again, we do not really need this proof, but here it is:
\<close>
instance fbint :: t3_space
proof (rule t2_space_t3_spaceI)
  fix x :: fbint and U :: "fbint set"
  assume "x \<in> U" and "open U"
  then obtain b where b: "b > 0" "arith_prog_fb (int_of_fbint x) b \<subseteq> U"
    by transfer blast
  define V where "V = arith_prog_fb (int_of_fbint x) b"
  have "x \<in> V"
    unfolding V_def by transfer auto
  moreover have "open V" "closed V"
    using \<open>b > 0\<close> by (auto simp: V_def)
  ultimately show "\<exists>V. x \<in> V \<and> open V \<and> closure V \<subseteq> U"
    using b by (intro exI[of _ V]) (auto simp: V_def)
qed

subsection \<open>Metrizability\<close>

text \<open>
  The metrizability of Furstenberg's topology (i.\,e.\ that it is induced by some metric) can
  be shown from the fact that it is second countable and $T_3$ using Urysohn's Metrization Theorem,
  but this is not available in Isabelle yet. Let us therefore give an \<^emph>\<open>explicit\<close> metric,
  as described by Zulfeqarr~\cite{zulfeqarr}. We follow the exposition by Dirmeier~\cite{dirmeier}.

  First, we define a kind of norm on the integers. The norm depends on a real parameter \<open>q > 1\<close>.
  The value of \<open>q\<close> does not matter in the sense that all values induce the same topology
  (which we will show). For the final definition, we then simply pick \<open>q = 2\<close>.
\<close>

locale fbnorm =
  fixes q :: "real"
  assumes q_gt_1: "q > 1"
begin

definition N :: "int \<Rightarrow> real" where
  "N n = (\<Sum>k. if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k)"

lemma N_summable: "summable (\<lambda>k. if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k)"
  by (rule summable_comparison_test[OF _ summable_geometric[of "1/q"]])
     (use q_gt_1 in \<open>auto intro!: exI[of _ 0] simp: power_divide\<close>)

lemma N_sums: "(\<lambda>k. if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k) sums N n"
  using N_summable unfolding N_def by (rule summable_sums)

lemma N_nonneg: "N n \<ge> 0"
  by (rule sums_le[OF _ sums_zero N_sums]) (use q_gt_1 in auto)

lemma N_uminus [simp]: "N (-n) = N n"
  by (simp add: N_def)

lemma N_minus_commute: "N (x - y) = N (y - x)"
  using N_uminus[of "x - y"] by (simp del: N_uminus)

lemma N_zero [simp]: "N 0 = 0"
  by (simp add: N_def)

lemma not_dvd_imp_N_ge:
  assumes "\<not>n dvd a" "n > 0"
  shows   "N a \<ge> 1 / q ^ n"
  by (rule sums_le[OF _ sums_single[of n] N_sums]) (use q_gt_1 assms in auto)

lemma N_lt_imp_dvd:
  assumes "N a < 1 / q ^ n" and "n > 0"
  shows   "n dvd a"
  using not_dvd_imp_N_ge[of n a] assms by auto

lemma N_pos:
  assumes "n \<noteq> 0"
  shows   "N n > 0"
proof -
  have "0 < 1 / q ^ (nat \<bar>n\<bar>+1)"
    using q_gt_1 by simp
  also have "\<not>1 + \<bar>n\<bar> dvd \<bar>n\<bar>"
    using zdvd_imp_le[of "1 + \<bar>n\<bar>" "\<bar>n\<bar>"] assms by auto
  hence "1 / q ^ (nat \<bar>n\<bar>+1) \<le> N n"
    by (intro not_dvd_imp_N_ge) (use assms in auto)
  finally show ?thesis .
qed

lemma N_zero_iff [simp]: "N n = 0 \<longleftrightarrow> n = 0"
  using N_pos[of n] by (cases "n = 0") auto

lemma N_triangle_ineq: "N (n + m) \<le> N n + N m"
proof (rule sums_le)
  let ?I = "\<lambda>n k. if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k"
  show "?I (n + m) sums N (n + m)"
    by (rule N_sums)
  show "(\<lambda>k. ?I n k + ?I m k) sums (N n + N m)"
    by (intro sums_add N_sums)
qed (use q_gt_1 in auto)

lemma N_1: "N 1 = 1 / (q * (q - 1))"
proof (rule sums_unique2)
  have "(\<lambda>k. if k = 0 \<or> int k dvd 1 then 0 else 1 / q ^ k) sums N 1"
    by (rule N_sums)
  also have "(\<lambda>k. if k = 0 \<or> int k dvd 1 then 0 else 1 / q ^ k) =
               (\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k)"
    by (simp add: power_divide cong: if_cong)
  finally show "(\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums N 1" .

  have "(\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums
                 (1 / (1 - 1 / q) + (- (1 / q) - 1))"
    by (rule sums_If_finite_set'[OF geometric_sums]) (use q_gt_1 in auto)
  also have "\<dots> = 1 / (q * (q - 1))"
    using q_gt_1 by (simp add: field_simps)
  finally show "(\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums \<dots>" .
qed

text \<open>
  It follows directly from the definition that norms fulfil a kind of monotonicity property
  with respect to divisibility: the norm of a number is at most as large as the norm of any of
  its factors:
\<close>
lemma N_dvd_mono:
  assumes "m dvd n"
  shows   "N n \<le> N m"
proof (rule sums_le[OF _ N_sums N_sums])
  fix k :: nat
  show "(if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k) \<le>
        (if k = 0 \<or> int k dvd m then 0 else 1 / q ^ k)"
    using q_gt_1 assms by auto
qed

text \<open>
  In particular, this means that 1 and -1 have the greatest norm.
\<close>
lemma N_le_N_1: "N n \<le> N 1"
  by (rule N_dvd_mono) auto

text \<open>
  Primes have relatively large norms, almost reaching the norm of 1:
\<close>
lemma N_prime:
  assumes "prime p"
  shows   "N p = N 1 - 1 / q ^ nat p"
proof (rule sums_unique2)
  define p' where "p' = nat p"
  have p: "p = int p'"
    using assms by (auto simp: p'_def prime_ge_0_int)
  have "prime p'"
    using assms by (simp add: p)

  have "(\<lambda>k. if k = 0 \<or> int k dvd p then 0 else 1 / q ^ k) sums N p"
    by (rule N_sums)
  also have "int k dvd p \<longleftrightarrow> k \<in> {1, p'}" for k
    using assms by (auto simp: p prime_nat_iff)
  hence "(\<lambda>k. if k = 0 \<or> int k dvd p then 0 else 1 / q ^ k) =
         (\<lambda>k. if k \<in> {0, 1, p'} then 0 else (1 / q) ^ k)"
    using assms q_gt_1 by (simp add: power_divide cong: if_cong)
  finally show "\<dots> sums N p" .

  have "(\<lambda>k. if k \<in> {0, 1, p'} then 0 else (1 / q) ^ k) sums
                 (1 / (1 - 1 / q) + (- (1 / q) - (1 / q) ^ p' - 1))"
    by (rule sums_If_finite_set'[OF geometric_sums])
       (use \<open>prime p'\<close> q_gt_1 prime_gt_Suc_0_nat[of p'] in \<open>auto simp: \<close>)
  also have "\<dots> = N 1 - 1 / q ^ p'"
    using q_gt_1 by (simp add: field_simps N_1)
  finally show "(\<lambda>k. if k \<in> {0, 1, p'} then 0 else (1 / q) ^ k) sums \<dots>" .
qed

lemma N_2: "N 2 = 1 / (q ^ 2 * (q - 1))"
  using q_gt_1 by (auto simp: N_prime N_1 field_simps power2_eq_square)

lemma N_less_N_1:
  assumes "n \<noteq> 1" "n \<noteq> -1"
  shows   "N n < N 1"
proof (cases "n = 0")
  case False
  then obtain p where p: "prime p" "p dvd n"
    using prime_divisor_exists[of n] assms by force
  hence "N n \<le> N p" by (intro N_dvd_mono)
  also from p have "N p < N 1"
    using q_gt_1 by (simp add: N_prime)
  finally show ?thesis .
qed (use q_gt_1 in \<open>auto simp: N_1\<close>)

text \<open>
  Composites, on the other hand, do not achieve this:
\<close>
lemma nonprime_imp_N_lt:
  assumes "\<not>prime_elem n" "\<bar>n\<bar> \<noteq> 1" "n \<noteq> 0"
  shows   "N n < N 1 - 1 / q ^ nat \<bar>n\<bar>"
proof -
  obtain p where p: "prime p" "p dvd n"
    using prime_divisor_exists[of n] assms by auto
  define p' where "p' = nat p"
  have p': "p = int p'"
    using p by (auto simp: p'_def prime_ge_0_int)
  have "prime p'"
    using p by (simp add: p')

  define n' where "n' = nat \<bar>n\<bar>"
  have "n' > 1"
    using assms by (auto simp: n'_def)

  have "N n \<le> 1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n'"
  proof (rule sums_le)
    show "(\<lambda>k. if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k) sums N n"
      by (rule N_sums)
  next
    from assms p have "n' \<noteq> p'"
      by (auto simp: n'_def p'_def nat_eq_iff)
    hence "(\<lambda>k. if k \<in> {0, 1, p', n'} then 0 else (1 / q) ^ k) sums
                   (1 / (1 - 1 / q) + (- (1 / q) - (1 / q) ^ p' - (1 / q) ^ n' - 1))"
      by (intro sums_If_finite_set'[OF geometric_sums])
         (use \<open>prime p'\<close> q_gt_1 prime_gt_Suc_0_nat[of p'] \<open>n' > 1\<close> in \<open>auto simp: \<close>)
    also have "\<dots> = 1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n'"
      using q_gt_1 by (simp add: field_simps)
    finally show "(\<lambda>k. if k \<in> {0, 1, p', n'} then 0 else (1 / q) ^ k) sums \<dots>" .
  next
    show "\<And>k. (if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k)
         \<le> (if k \<in> {0, 1, p', n'} then 0 else (1 / q) ^ k)"
      using q_gt_1 p by (auto simp: p'_def n'_def power_divide)
  qed
  also have "\<dots> < 1 / (q * (q - 1)) - 1 / q ^ n'"
    using q_gt_1 by simp
  finally show ?thesis by (simp add: n'_def N_1)
qed

text \<open>
  This implies that one can use the norm as a primality test:
\<close>
lemma prime_iff_N_eq:
  assumes "n \<noteq> 0"
  shows   "prime_elem n \<longleftrightarrow> N n = N 1 - 1 / q ^ nat \<bar>n\<bar>"
proof -
  have *: "prime_elem n \<longleftrightarrow> N n = N 1 - 1 / q ^ nat \<bar>n\<bar>" if "n > 0" for n
  proof -
    consider "n = 1" | "prime n" | "\<not>prime n" "n > 1"
      using \<open>n > 0\<close> by force
    thus ?thesis
    proof cases
      assume "n = 1"
      thus ?thesis using q_gt_1
        by (auto simp: N_1)
    next
      assume n: "\<not>prime n" "n > 1"
      with nonprime_imp_N_lt[of n] show ?thesis by simp
    qed (auto simp: N_prime prime_ge_0_int)
  qed

  show ?thesis
  proof (cases "n > 0")
    case True
    with * show ?thesis by blast
  next
    case False
    with *[of "-n"] assms show ?thesis by simp
  qed
qed

text \<open>
  Factorials, on the other hand, have very small norms:
\<close>
lemma N_fact_le: "N (fact m) \<le> 1 / (q - 1) * 1 / q ^ m"
proof (rule sums_le[OF _ N_sums])
  have "(\<lambda>k. 1 / q ^ k / q ^ Suc m) sums (q / (q - 1) / q ^ Suc m)"
    using geometric_sums[of "1 / q"] q_gt_1
    by (intro sums_divide) (auto simp: field_simps)
  also have "(q / (q - 1) / q ^ Suc m) = 1 / (q - 1) * 1 / q ^ m"
    using q_gt_1 by (simp add: field_simps)
  also have "(\<lambda>k. 1 / q ^ k / q ^ Suc m) = (\<lambda>k. 1 / q ^ (k + Suc m))"
    using q_gt_1 by (simp add: field_simps power_add)
  also have "\<dots> = (\<lambda>k. if k + Suc m \<le> m then 0 else 1 / q ^ (k + Suc m))"
    by auto
  finally have "\<dots> sums (1 / (q - 1) * 1 / q ^ m)" .
  also have "?this \<longleftrightarrow> (\<lambda>k. if k \<le> m then 0 else 1 / q ^ k) sums (1 / (q - 1) * 1 / q ^ m)"
    by (rule sums_zero_iff_shift) auto
  finally show \<dots> .
next
  fix k :: nat
  have "int k dvd fact m" if "k > 0" "k \<le> m"
  proof -
    have "int k dvd int (fact m)"
      unfolding int_dvd_int_iff using that by (simp add: dvd_fact)
    thus "int k dvd fact m"
      unfolding of_nat_fact by simp
  qed
  thus "(if k = 0 \<or> int k dvd fact m then 0 else 1 / q ^ k) \<le>
        (if k \<le> m then 0 else 1 / q ^ k)" using q_gt_1 by auto
qed

lemma N_prime_mono:
  assumes "prime p" "prime p'" "p \<le> p'"
  shows   "N p \<le> N p'"
  using assms q_gt_1 by (auto simp add: N_prime field_simps nat_le_iff prime_ge_0_int)

lemma N_prime_ge:
  assumes "prime p"
  shows   "N p \<ge> 1 / (q\<^sup>2 * (q - 1))"
proof -
  have "1 / (q ^ 2 * (q - 1)) = N 2"
    using q_gt_1 by (auto simp: N_prime N_1 field_simps power2_eq_square)
  also have "\<dots> \<le> N p"
    using assms by (intro N_prime_mono) (auto simp: prime_ge_2_int)
  finally show ?thesis .
qed

lemma N_prime_elem_ge:
  assumes "prime_elem p"
  shows   "N p \<ge> 1 / (q\<^sup>2 * (q - 1))"
proof (cases "p \<ge> 0")
  case True
  with assms N_prime_ge show ?thesis by auto
next
  case False
  with assms N_prime_ge[of "-p"] show ?thesis by auto
qed

text \<open>
  Next, we use this norm to derive a metric:
\<close>

lift_definition dist :: "fbint \<Rightarrow> fbint \<Rightarrow> real" is
  "\<lambda>x y. N (x - y)" .

lemma dist_self [simp]: "dist x x = 0"
  by transfer simp

lemma dist_sym [simp]: "dist x y = dist y x"
  by transfer (simp add: N_minus_commute)

lemma dist_pos: "x \<noteq> y \<Longrightarrow> dist x y > 0"
  by transfer (use N_pos in simp)

lemma dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
  using dist_pos[of x y] by (cases "x = y") auto

lemma dist_triangle_ineq: "dist x z \<le> dist x y + dist y z"
proof transfer
  fix x y z :: int
  show "N (x - z) \<le> N (x - y) + N (y - z)"
    using N_triangle_ineq[of "x - y" "y - z"] by simp
qed

text \<open>
  Lastly, we show that the metric we defined indeed induces the Furstenberg topology.
\<close>
theorem dist_induces_open:
  "open U \<longleftrightarrow> (\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U)"
proof (transfer, safe)
  fix U :: "int set" and x :: int
  assume *: "\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U"
  assume "x \<in> U"
  with * obtain b where b: "b > 0" "arith_prog x b \<subseteq> U" by blast
  define e where "e = 1 / q ^ b"

  show "\<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U"
  proof (rule exI; safe?)
    show "e > 0" using q_gt_1 by (simp add: e_def)
  next
    fix y assume "N (x - y) < e"
    also have "\<dots> = 1 / q ^ b" by fact
    finally have "b dvd (x - y)"
      by (rule N_lt_imp_dvd) fact
    hence "y \<in> arith_prog x b"
      by (auto simp: arith_prog_def cong_iff_dvd_diff dvd_diff_commute)
    with b show "y \<in> U" by blast
  qed

next

  fix U :: "int set" and x :: int
  assume *: "\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U"
  assume "x \<in> U"
  with * obtain e where e: "e > 0" "\<forall>y. N (x - y) < e \<longrightarrow> y \<in> U" by blast
  have "eventually (\<lambda>N. 1 / (q - 1) * 1 / q ^ N < e) at_top"
    using q_gt_1 \<open>e > 0\<close> by real_asymp
  then obtain m where m: "1 / (q - 1) * 1 / q ^ m < e"
    by (auto simp: eventually_at_top_linorder)
  define b :: nat where "b = fact m"

  have "arith_prog x b \<subseteq> U"
  proof
    fix y assume "y \<in> arith_prog x b"
    show "y \<in> U"
    proof (cases "y = x")
      case False
      from \<open>y \<in> arith_prog x b\<close> obtain n where y: "y = x + int b * n"
        by (auto simp: arith_prog_altdef)
      from y and \<open>y \<noteq> x\<close> have [simp]: "n \<noteq> 0" by auto
      have "N (x - y) = N (int b * n)" by (simp add: y)
      also have "\<dots> \<le> N (int b)"
        by (rule N_dvd_mono) auto
      also have "\<dots> \<le> 1 / (q - 1) * 1 / q ^ m"
        using N_fact_le by (simp add: b_def)
      also have "\<dots> < e" by fact
      finally show "y \<in> U" using e by auto
    qed (use \<open>x \<in> U\<close> in auto)
  qed
  moreover have "b > 0" by (auto simp: b_def)
  ultimately show "\<exists>b>0. arith_prog x b \<subseteq> U"
    by blast
qed

end

text \<open>
  We now show that the Furstenberg space is a metric space with this metric (with \<open>q = 2\<close>),
  which essentially only amounts to plugging together all the results from above.
\<close>

interpretation fb: fbnorm 2
  by standard auto

instantiation fbint :: dist
begin

definition dist_fbint where "dist_fbint = fb.dist"

instance ..

end

instantiation fbint :: uniformity_dist
begin

definition uniformity_fbint :: "(fbint \<times> fbint) filter" where
  "uniformity_fbint = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"

instance by standard (simp add: uniformity_fbint_def)

end

instance fbint :: open_uniformity
proof
  fix U :: "fbint set"
  show "open U = (\<forall>x\<in>U. eventually (\<lambda>(x',y). x' = x \<longrightarrow> y \<in> U) uniformity)"
    unfolding eventually_uniformity_metric dist_fbint_def
    using fb.dist_induces_open by simp
qed

instance fbint :: metric_space
  by standard (use fb.dist_triangle_ineq in \<open>auto simp: dist_fbint_def\<close>)

text \<open>
  In particular, we can now show that the sequence \<open>n!\<close> tends to 0 in the Furstenberg topology:
\<close>
lemma tendsto_fbint_fact: "(\<lambda>n. fbint (fact n)) \<longlonglongrightarrow> fbint 0"
proof -
  have "(\<lambda>n. dist (fbint (fact n)) (fbint 0)) \<longlonglongrightarrow> 0"
  proof (rule tendsto_sandwich[OF always_eventually always_eventually]; safe?)
    fix n :: nat
    show "dist (fbint (fact n)) (fbint 0) \<le> 1 / 2 ^ n"
      unfolding dist_fbint_def by (transfer fixing: n) (use fb.N_fact_le[of n] in simp)
    show "dist (fbint (fact n)) (fbint 0) \<ge> 0"
      by simp
    show "(\<lambda>n. 1 / 2 ^ n :: real) \<longlonglongrightarrow> 0"
      by real_asymp
  qed simp_all
  thus ?thesis
    using tendsto_dist_iff by metis
qed

end

subset_name: curated


text:
\begin{document}
\preprint{}
\title[]{
Entanglement-breaking channels with general outcome operator algebras
}
\author{Yui Kuramochi}
\affiliation{Laboratory of Quantum Engineering and Quantum Metrology, School of Physics and Astronomy, Sun Yat-Sen University (Zhuhai Campus), Zhuhai 519082, China}
\email{yui.tasuke.kuramochi@gmail.com}
\date{}

\begin{abstract}
A unit-preserving and completely positive linear map, or a channel,
$\Lambda \colon \mathcal{A} \to \mathcal{A}_{\mathrm{in}}$
between $C^\ast$-algebras $\mathcal{A}$ and $\mathcal{A}_{\mathrm{in}}$
is called entanglement-breaking (EB) if
$\omega \circ( \Lambda \otimes \mathrm{id}_{\mathcal{B}} ) $
is a separable state for any $C^\ast$-algebra $\mathcal{B}$
and any state $\omega$ on
the injective $C^\ast$-tensor product $\mathcal{A}_{\mathrm{in}} \otimes \mathcal{B} .$
In this paper, we establish the equivalence of the following conditions for a channel
$\Lambda$ with a quantum input space and
with a general outcome $C^\ast$-algebra, generalizing
known results in finite dimensions:
(i) $\Lambda$ is EB;
(ii) $\Lambda$ has a measurement-prepare form (Holevo form);
(iii) $n$ copies of $\Lambda$ are compatible for all $2 \leq n < \infty ;$
(iv) countably infinite copies of $\Lambda$ are compatible.
By using this equivalence,
we also show that the set of randomization-equivalence classes of
normal EB channels with a fixed input von Neumann algebra
is upper and lower Dedekind-closed,
i.e.\ the supremum or infimum of
any randomization-increasing or decreasing net of EB channels
is also EB.
As an example, we construct an injective normal EB channel with an arbitrary outcome operator algebra $\mathcal{M}$ acting on an infinite-dimensional separable Hilbert space
by using the coherent states and the Bargmann measure.
\end{abstract}
\pacs{03.67.-a, 02.30.Tb}
\keywords{entanglement-breaking channel, Holevo form,
channel compatibility, randomization order, no-broadcasting theorem, Dedekind-closedness}
\maketitle

\section{Introduction} \label{sec:intro}
A quantum channel $\Lambda$ is called entanglement-breaking (EB)
if $\Lambda$ tensored with the identity on any state space maps
any entangled state to a separable state.
In Ref.~\onlinecite{Horodecki2003} some useful characterizations
of finite-dimensional EB channels were established.

Later EB condition is considered in the infinite-dimensional quantum
systems in Refs.~\onlinecite{holevo2005separability,0036-0279-60-2-L12,Holevo2008,Holevo2011,He2013}
and the operator algebraic setup in
Refs.~\onlinecite{STORMER20082303,Stoermer_2009,doi:10.1063/1.5024385}.
Among them, in Ref.~\onlinecite{holevo2005separability},
it was shown that a channel with input and outcome separable Hilbert spaces
is EB if and only if the channel has a measurement-prepare form (Holevo form).
Recently,
another characterization of the EB condition in terms of
channel compatibility was given in Ref.~\onlinecite{1751-8121-50-13-135302}
(Proposition~12):
a finite-dimensional channel is EB if and only if
$n$ copies of the channel have a joint channel
for all $2 \leq n < \infty .$
The proof in Ref.~\onlinecite{1751-8121-50-13-135302} is based on
an upper bound~\cite{10.1007/978-3-642-18073-6_2}
on the diamond norm distance
that explicitly depends on the dimension of the system
and is not applicable to the infinite-dimensional case.

The purpose of this paper is to generalize these characterizations of the EB condition
to the case of channels with (possibly non-separable) quantum input spaces
and with general outcome operator algebras.
The main finding of this paper is Theorem~\ref{theo:main},
which, roughly speaking, establishes the equivalence of
the following conditions for a channel $\Lambda$
with quantum input and operator algebraic outcome spaces:
\begin{enumerate}[(i)]
\item
$\Lambda$ is EB;
\item
$\Lambda$ has a measurement-prepare form;
\item
$n$-copies of $\Lambda$ are compatible for all $2 \leq n < \infty ;$
\item
countably infinite copies of $\Lambda$ are compatible.
\end{enumerate}
The equivalence of the first three conditions generalizes known results in finite-dimensions,~\cite{Horodecki2003,1751-8121-50-13-135302}
while the last infinite-self-compatibility condition is a new characterization.

This paper is organized as follows.
After mathematical preliminaries in Section~\ref{sec:prel},
we consider in Section~\ref{sec:sep} general properties of separable states on
injective \cstar-tensor product algebras and show
that any separable state is represented as a barycentric integral of
product states (Corollary~\ref{coro:sep}),
which is a \cstar-algebra version of the corresponding integral representation
given in Ref.~\onlinecite{holevo2005separability}.
In Section~\ref{sec:main} we prove Theorem~\ref{theo:main},
the main result of this paper.
In Section~\ref{sec:dedekind},
as an application of the characterizations given in Theorem~\ref{theo:main},
we show that
the supremum or infimum of
any randomization-increasing or decreasing net of normal EB channels with
a fixed input von Neumann algebra is also EB
(Theorem~\ref{theo:dc}).
In Section~\ref{sec:ex} we construct a normal injective EB channel
that has an arbitrary outcome von Neumann algebra acting on a separable
Hilbert space.
Section~\ref{sec:conclusion} concludes the paper.

\section{Preliminaries} \label{sec:prel}
This section introduces mathematical preliminaries needed in the main part
and fixes the notation.
For general references of operator algebra we refer to
Refs.~\onlinecite{takesakivol1,sakaibook}.

\subsection{States and channels on operator algebras}
Throughout this paper every \cstar-algebra $\A$ is assumed to have
a unit element which we write as $\unit_\A .$
For a \cstar-algebra $\A ,$ a positive and normalized linear functional
$\phi \in \A^\ast$ is called a state on $\A .$
We denote by $\cS (\A) $ the set of states on $\A ,$
which is a compact convex subset of the dual space $\A^\ast$
in the weak-$\ast$ topology $\sigma (\A^\ast , \A)$.
We also denote by $\Sp (\A)$ the set of pure states on $\A .$
Since $\Sp (\A)$ coincides with the set of extreme points of $\cS (\A) ,$
the Krein-Milman theorem implies that $\cS (\A) = \cco ( \Sp (\A) ) ,$
where $\cco (\cdot)$ denotes the closed convex hull in the weak-$\ast$ topology.
For a Hilbert space $\cH ,$
$\LH$ and $\unit_\cH$ denote the algebra of bounded linear operators
and the unit operator on $\cH ,$
respectively.
We also write the inner product of a Hilber space $\cH$ as $\braket{\xi | \eta } $
$(\xi , \eta \in \cH) ,$
which is linear and anti-linear with respect to $\eta$ and $\xi ,$ respectively.

A channel (in the Heisenberg picture)
is a unit-preserving and completely positive (CP) map
$\Lambda \colon \A \to \B$
between \cstar-algebras $\A$ and $\B .$
The algebras $\A$ and $\B$ are called the outcome and input spaces, or algebras,
of $\Lambda ,$
respectively.
In the Schr\"odinger picture, an input state
$\phi \in \cS (\B)$ is mapped to the outcome state
$\Lambda^\ast (\phi) = \phi \circ \Lambda \in \cS (\A) .$
For \cstar-algebras $\A$ and $\B ,$
the set of channels from $\A $ to $\B$ is denoted by $\chset{\A}{\B} .$

A channel $\Lambda \in \chset{\M}{\N}$ between von Neumann algebras
$\M$ and $\N$ is called normal if $\Lambda$ is continuous with respect to
the $\sigma$-weak topologies of $\M$ and $\N ,$ respectively.
The set of normal channels from $\M$ to $\N$ is denoted by
$\nchset{\M}{\N}  .$
A normal channel with a commutative outcome von Neumann algebra is called
a quantum-classical (QC) channel.

Let $\Lambda \in \chset{\A}{\Ain}$
and $\Gamma \in \chset{\B}{\Ain}$
be channels with the common input space $\Ain .$
We define the randomization (or coarse-graining or concatenation)
relations~\cite{1751-8121-50-13-135302,kuramochi2018incomp}
for channels as follows:
\begin{itemize}
\item
$\Lambda \cocp \Gamma$
($\Lambda$ is a randomization of $\Gamma$)
$: \defarrow$
there exists a channel $\alpha \in \chset{\A}{\B}$
such that $\Lambda = \Gamma \circ \alpha ;$
\item
$\Lambda \eqcp \Gamma $
($\Lambda$ is randomization-equivalent to $\Gamma$)
$:\defarrow$
$\Lambda \cocp \Gamma$ and $\Gamma \cocp \Lambda .$
\end{itemize}
The relations $\cocp $ and $\eqcp$ are binary preorder and equivalence relations,
respectively,
defined on the class of channels with a fixed input algebra.
In the above definition, if $\A , $ $\B ,$ and $\Ain$ are von Neumann algebras
and $\Lambda $ and $\Gamma$ are normal,
$\Lambda \cocp \Gamma$
if and only if
there exists a normal channel
$\alpha \in \nchset{\A}{\B}$ such that
$\Lambda = \Gamma \circ \alpha .$~\cite{kuramochi2018incomp}

Let $\A$ be a \cstar-algebra
and let $\pi_\A \colon \A \to \calL (\cH_\A)$ be the universal representation of $\A ,$
which is the direct sum of the Gelfand-Naimark-Segal
(GNS) representations of
all the states on $\A .$
The von Neumann algebra $\pi_\A (\A)^{\prime \prime} ,$
where the prime denotes the commutant,
generated by $\pi_\A (\A)$ is called the universal enveloping von Neumann algebra
of $\A .$
The algebra $\pi_\A (\A)^{\prime \prime}$ is isometrically isomorphic to
the double dual space $\A^{\ast \ast}$
and we identify $\pi_\A (\A)^{\prime \prime}$ with $\A^{\ast \ast } .$
By identifying $\A$ with $\pi_\A (\A) ,$
we also regard $\A$ as a $\sigma$-weakly dense
\cstar-subalgebra of $\A^{\ast \ast} .$

Let $\A$ be a \cstar-algebra and let $\Min$ be a von Neumann algebra.
Then any channel $\Lambda \in \chset{\A}{\Min}$
uniquely extends to a normal channel
$\bL \in \nchset{\A^{\ast \ast }}{\Min} $
which we call the normal extension of $\Lambda .$\cite{kuramochi2018incomp}
The normal extension $\bL$ is the least normal channel that upper bounds $\Lambda$
in the randomization order $\cocp .$
Specifically, $\Lambda \cocp \bL$ and for any normal channel
$\Gamma \in \nchset{\N}{\Min} ,$
$\Lambda \cocp \Gamma$ if and only if
$\bL \cocp \Gamma $
(Ref.~\onlinecite{kuramochi2018incomp}, Lemma 7).
This also implies that $\Lambda \eqcp \bL$ if $\Lambda$ is normal.

\subsection{Positive-operator valued measures}
A positive-operator valued measure (POVM)~\cite{davieslewisBF01647093,holevo2011probabilistic}
on a Hilbert space $\cH$ is a triple $(\Omega ,\Sigma , \oM)$
such that $(\Omega , \Sigma)$ is a measurable space, i.e.\
$\Sigma$ is a $\sigma$-algebra on a set $\Omega ,$
and $\oM \colon \Sigma \to \LH$ is a map satisfying
\begin{enumerate}[(i)]
\item
$\oM (E) \geq 0$
$(E \in \Sigma) ;$
\item
$\oM (\Omega) = \unit_{\cH} ;$
\item
for any disjoint sequence $\{ E_n \}_{n \in \natn} \subset \Sigma ,$
$\oM (\bigcup_{n \in \natn} E_n) = \sum_{n \in \natn} \oM(E_n) .$
\end{enumerate}
A POVM describes the classical outcome statistics of a general quantum measurement.
For a measurable space $(\Omega , \Sigma) ,$
we denote by $B(\Omega , \Sigma)$ the set of bounded, complex valued,
$\Sigma$-measurable functions on $\Omega ,$
which is a commutative \cstar-algebra under the supremum norm
$\| f \| := \sup_{x \in \Omega} | f(x) | .$
If $(\Omega , \Sigma , \oM)$ is a POVM on $\cH ,$
for each $f \in B(\Omega , \Sigma) $ we can define the integral
$\int_{\Omega} f (x) d \oM (x) \in \LH$
in the weak sense.

Let $\Omega$ be a compact Hausdorff space.
We denote by $C (\Omega)$ and $\B (\Omega)$
the commutative \cstar-algebra of bounded complex-valued continuous functions on
$\Omega $
and the Borel $\sigma$-algebra generated by the set of open subsets of $\Omega ,$
respectively.
A POVM $(\Omega , \B (\Omega) , \oM)$ on a Hilbert space $\cH$
is called regular
if
\[
	\B (\Omega) \ni E
	\longmapsto
	\braket{\xi | \oM(E) \eta}
	\in \cmplx
\]
is a regular complex measure for any $\xi , \eta \in \cH .$
According to the Riesz-Markov-Kakutani representation theorem
we have a one-to-one correspondence
\[
	\cS (C(\Omega)) \ni \phi
	\longmapsto
	\mu_\phi \in
	\bfMpo (\Omega)
\]
between the state space $\cS (C(\Omega))$
and the set $\bfMpo (\Omega)$ of regular probability measures on $\Omega$
such that
\[
	\phi (f)
	=
	\int_\Omega
	f(x) d\mu_\phi (x)
	\quad
	(f \in C(\Omega)) .
\]
A similar representation theorem also holds for
channels as follows.
\begin{proposition}[Ref.~\onlinecite{busch2016quantum}, Theorem~4.4]
\label{prop:RMK}
Let $\Omega$ be a compact Hausdorff space and let $\cH$ be a Hilbert space.
Then for any channel $\Gamma \in \chset{C(\Omega)}{\LH}$
there exists a unique regular POVM $(\Omega , \B (\Omega) , \oM)$ on $\cH$
such that
\[
	\Gamma (f)
	=
	\int_\Omega f (x) d\oM (x)
	\quad
	(f \in C (\Omega)) .
\]
\end{proposition}

\subsection{Tensor products}
Let $\A$ and $\B$ be \cstar-algebras.
We denote the algebraic tensor and the injective \cstar-tensor
products by $\A \atensor \B$ and $\A \otimes \B ,$
respectively.
If $\A$ and $\B$ are faithfully represented on Hilbert spaces
$\cH$ and $\cK ,$ respectively,
then $\A \otimes \B$ coincides with the norm closure
of $\A \atensor \B$ on $\calL (\cH \otimes \cK) $
up to isomorphism.
For \cstar-algebras $\A , $ $\B ,$ and $\C ,$
the associative law
\[
(\A  \otimes \B) \otimes \C = \A \otimes(\B \otimes \C)
=:
\A \otimes \B \otimes \C
\]
holds
(again up to isomorphism)
and the \cstar-algebra $\A \otimes \B \otimes \C$
coincides with the norm closure of $\A \atensor \B \atensor \C$
on $\calL (\cH \otimes \cK \otimes \mathcal{J})$
if $\A ,$ $\B ,$ and $\C$ are faithfully represented on Hilbert spaces
$\cH , $ $\cK ,$ and $\mathcal{J} ,$ respectively.
The injective \cstar-tensor product of arbitrary finite number of
\cstar-algebras can be defined similarly.

Let $\Lambda \in \chset{\A}{\B}$ and $\Gamma \in \chset{\C}{\D}$
be channels.
Then there exists a unique CP channel
$\Lambda \otimes \Gamma \in \chset{\A \otimes \C}{\B \otimes \D},$
called the tensor product channel,
such that
$\Lambda \otimes \Gamma ( A \otimes C) = \Lambda (A) \otimes \Gamma (C)$
$(A \in \A , C \in \C) .$

By the inductive limit procedure,
we can also define the injective \cstar-tensor product of
infinite number of \cstar-algebras.~\cite{takeda1955}
In this paper we only need the countably infinite tensor product
$\A^{\otimes \infty}$
of identical \cstar-algebras,
which is defined as follows.
For each \cstar-algebra $\A$
and each integer $1 \leq n < \infty ,$ we write
\[
	\A^{\otimes n}
	:=
	\underbrace{\A \otimes \dots \otimes \A}_{\text{$n$ elements}} .
\]
For each $1 \leq m <n < \infty ,$
the representation
$
\pi_{n \gets m} \colon
\A^{\otimes m} \ni X
\mapsto
X \otimes \unit_{\A^{\otimes (n-m)}}
\in \A^{\otimes n}
$
is faithful and the family $(\pi_{n \gets m})_{1 \leq m < n < \infty}$
satisfies the consistency condition
$\pi_{n \gets k} = \pi_{n \gets m} \circ \pi_{m \gets k}$
$(1 \leq k <m < n < \infty) .$
Then there exist a \cstar-algebra
$\A^{\otimes \infty}$
and faithful representations $\pi_n \colon \A^{\otimes n} \to \A^{\otimes \infty}$
$(1 \leq n < \infty) $
such that
$\pi_m = \pi_n \circ \pi_{n\gets m}$
$(1 \leq m<n<\infty)$
and
$\bigcup_{1 \leq n < \infty} \pi_n (\A^{\otimes n})$
is a norm dense $\ast$-subalgebra of $\A^{\otimes \infty} .$
Such $\Ainf$ and $(\pi_n)_{n \geq 1}$ are unique up to isomorphism.
The \cstar-algebra $\A^{\otimes \infty} $
is called the (countably) infinite injective \cstar-tensor product of $\A .$
The element $\pi_n (X) \in \A^{\otimes \infty}$ $(X \in \A^{\otimes n})$
and the \cstar-subalgebra $\pi_n (\A^{\otimes n}) \subset \A^{\otimes \infty}$
are written as $X \otimes \unit_{\A^{\otimes \infty}}$ and
$\A^{\otimes n} \otimes \unit_{\A^{\otimes \infty}} ,$
respectively.

Let $\A$ and $\B$ be \cstar-algebras
and let $ 2 \leq n < \infty .$
A channel $\Lambda \in \chset{\A^{\otimes n}}{\B}$
is called symmetric if
$\Lambda = \Lambda \circ \pi_\sigma$
for all $\sigma \in \Sn ,$
where $\Sn$ is the symmetric group of
the finite set $\{ 1, \dots , n\} $
and $\pi_\sigma \colon \A^{\otimes n} \to \A^{\otimes n}$
$(\sigma \in \Sn)$
is a representation defined by
\[
	\pi_\sigma (A_1 \otimes \dots \otimes A_n)
	:=
	A_{\sigma(1)} \otimes \dots \otimes A_{\sigma(n)}
	\quad
	(A_1 , \dots , A_n \in \A) .
\]
The representation $\pi_\sigma$
$(\sigma \in \Sn )$
extends to the representation
$\pi_\sigma \otimes \id_{\Ainf} \colon \Ainf \to \Ainf$ defined by
\[
	\pi_\sigma \otimes \id_{\Ainf}
	(X \otimes Y \otimes \unit_{\Ainf})
	:=
	\pi_\sigma (X) \otimes Y \otimes \unit_{\Ainf}
	\quad
	(1\leq m < \infty , X \in \A^{\otimes n } , Y \in \A^{\otimes m}).
\]
A channel $\tL \in \chset{\Ainf}{\B}$ is called symmetric
if $\tL \circ (\pi_\sigma \otimes \id_{\Ainf}) = \tL$
for all $2 \leq n < \infty$
and all $\sigma \in \Sn .$
A channel $\tL \in \chset{\Ainf}{\B}$ is symmetric if and only if
the restriction
\[
	\tL_n \colon \Atn \ni X \longmapsto \tL (X \otimes \unit_{\Ainf}) \in \B
\]
is symmetric for all $2 \leq n <\infty .$

\subsection{Self-compatibility of channels}
Let $\Lambda \in \chset{\A}{\Ain}$ be a channel.
For $2 \leq n < \infty ,$
a channel $\Theta \in \chset{\Atn}{\Ain}$
is called an $n$-joint channel~\cite{1751-8121-50-13-135302}
of $\Lambda$ if
\[
	\Lambda(A)
	=
	\Theta (A \otimes \unit_{\A^{\otimes (n-1)}})
	=
	\dots
	=
	\Theta (\unit_{\A^{\otimes k}} \otimes A \otimes \unit_{\A^{\otimes (n-k-1)}} )
	=\dots =
	\Theta ( \unit_{\A^{\otimes (n-1)}} \otimes A)
\]
for all $A \in \A ,$
i.e.\ the $n$ marginal channels of $\Theta$ are identical to $\Lambda .$

An $n$-joint channel $\Theta$ of $\Lambda ,$ if exists,
can always be taken to be symmetric by retaking $\Theta$
as~\cite{1751-8121-50-13-135302}
\[
	\frac{1}{n!}
	\sum_{\sigma \in \Sn}
	\Theta \circ \pi_\sigma .
\]
A channel $\Theta_\infty \in \chset{\Ainf}{\Ain}$ is called an
$\omega$-joint channel of $\Lambda$ if
\[
	\Lambda (A)
	=
	\Theta_\infty
	(A \otimes \unit_{\Ainf})
	=
	\Theta_\infty
	( \unit_{\Atn} \otimes   A \otimes \unit_{\Ainf})
\]
for all $A \in \A$ and all $1 \leq n < \infty .$

\subsection{No-broadcasting theorem}
Let $\Lambda \in \chset{\A}{\Ain}$ be a channel
and let $\A \otimes_x \A$ be either
$\A \atensor \A $ or $\A \otimes \A .$
Then a channel $\Psi \in \chset{\A \otimes_x \A}{\A}$
is called a broadcasting channel of $\Lambda$ if
\[
	\Lambda (A)
	=
	\Lambda \circ \Psi (A \otimes \unit_\A)
	=
	\Lambda \circ \Psi (  \unit_\A \otimes  A)
\]
for all $A \in \A ,$
where a linear map
$\Phi \colon \A \atensor \A \to \B$
for a \cstar-algebra $\B$ is called a channel if $\Phi$
is unit-preserving and CP, i.e.\
\[
	\sum_{i,j=1}^n B_i^\ast \Phi (X_i^\ast X_j) B_j
	\geq 0
\]
for all $1 \leq n < \infty ,$
$\{ B_i \}_{i=1}^n \subset \B ,$
and
$\{  X_i \}_{i=1}^n \subset \A \atensor \A .$
If $\Lambda$ has a broadcasting channel
$\Psi \in \chset{\A \otimes \A}{\A}$
(respectively, $\Psi \in \chset{\A \atensor \A}{\A}$),
then $\Lambda$ is called broadcastable in the sense of injective \cstar-tensor product
(respectively, algebraic tensor product).

The following theorem, which is immediate from Corollary~1 of
Ref.~\onlinecite{kuramochi2018access},
is an operator algebraic version of the quantum no-broadcasting theorem
and will play an important role in the proof of the main result.
\begin{theorem}[No-broadcasting theorem for normal channels]
\label{theo:nb}
Let $\Lambda \in \nchset{\M}{\Min}$ be a normal channel.
Then the following conditions are equivalent.
\begin{enumerate}[(i)]
\item
$\Lambda$ is broadcastable in the sense of algebraic tensor product.
\item
$\Lambda$ is broadcastable in the sense of injective \cstar-tensor product.
\item
$\Lambda$ is randomization-equivalent to a QC channel with the input space $\Min .$
\end{enumerate}
\end{theorem}

For the broadcastability for channels with outcome \cstar-algebras,
we have the following lemma.

\begin{lemma}\label{lemm:bc}
Let $\A$ be a \cstar-algebra,
let $\Min$ be a von Neumann algebra,
and let $\Lambda \in \chset{\A }{\Min}$
be a channel.
Suppose that $\Lambda$ has a broadcasting channel
$\Psi \in \chset{\A \otimes \A}{\A} .$
Then the normal extension $\bL \in \nchset{\A^{\ast \ast}}{\Min}$
of $\Lambda$ satisfies the conditions (i)-(iii) of Theorem~\ref{theo:nb}.
\end{lemma}
\begin{proof}
It is sufficient to show that $\bL$ satisfies the condition (i) of
Theorem~\ref{theo:nb}.
Let $(\cH_\A , \pi_\A)$ be the universal representation of $\A .$
From the complete positivity of
$\Psi \colon \A \otimes \A \to \A \subset \calL (\cH_\A) ,$
we can take a Stinespring representation $(\cK , \pi ,V)$ of $\Psi ,$
namely
$\cK$ is a Hilbert space, $\pi \colon \A \otimes \A \to \LK$
is a representation,
and $V \colon \cH_\A \to \cK$ is a linear isometry such that
\[
	\Psi (X)
	=
	V^\ast \pi (X) V
	\quad
	(X \in \A \otimes \A) .
\]
We define representations $\pi_L$ and $\pi_R$ by
\[
	\pi_L (A)
	:=
	\pi (A \otimes \unit_\A) ,
	\quad
	\pi_R (A)
	:=
	\pi (\unit_\A \otimes A )
	\quad
	(A \in \A) .
\]
By the universality of the enveloping algebra $\A^{\ast \ast}$
the representations $\pi_L$ and $\pi_R$ uniquely extend to
normal representations
$\bpi_L \colon \A^{\ast \ast} \to \LK$
and
$\bpi_R \colon \A^{\ast \ast} \to \LK ,$
respectively.
Since $\pi_L (\A)$ and $\pi_R (\A)$ commute,
so do the von Neumann algebras
$\bpi_L (\A^{\ast \ast}) = \pi_L (\A)^{\prime \prime}$
and
$\bpi_R (\A^{\ast \ast}) = \pi_R (\A)^{\prime \prime} .$
Thus we can define a representation
$\tpi \colon \A^{\ast \ast} \atensor \A^{\ast \ast} \to \LK$
and a channel $\tPsi \colon \A^{\ast \ast} \atensor \A^{\ast \ast} \to \A^{\ast \ast}$ by
\begin{gather*}
	\tpi \left(
	\sum_i A_i^{\prime \prime} \otimes B_i^{\prime \prime}
	\right)
	:=
	\sum_i
	\bpi_L (A_i^{\prime \prime})
	\bpi_R (B_i^{\prime \prime})
	\quad
	(A_i^{\prime \prime}, B_i^{\prime \prime} \in \A^{\ast \ast}) ,
	\\
	\tPsi (X) := V^\ast  \tpi (X) V
	\quad (X \in \A^{\ast \ast} \atensor \A^{\ast \ast} ) .
\end{gather*}
Then for each $A \in \A ,$
\[
	\bL \circ \tPsi (A \otimes \unit_{\A^{\ast \ast}})
	=
	\Lambda \circ \Psi (A \otimes \unit_\A) = \Lambda (A) = \bL (A) ,
\]
and similarly $\bL \circ \tPsi (\unit_{\A^{\ast \ast}} \otimes A) = \bL (A) .$
Since the channels
\begin{gather*}
	\A^{\ast \ast} \ni A^{\prime \prime} \longmapsto
	\bL \circ \tPsi (A^{\prime \prime} \otimes \unit_{\A^{\ast \ast}})
	\in \Min
	\\
	\A^{\ast \ast} \ni A^{\prime \prime} \longmapsto
	\bL \circ \tPsi (\unit_{\A^{\ast \ast}} \otimes A^{\prime \prime}  )
	\in \Min
\end{gather*}
are normal and $\A$ is $\sigma$-weakly dense in $\A^{\ast \ast} ,$
this implies that $\tPsi$ is a broadcasting channel of $\bL .$
\end{proof}

\section{Separable states} \label{sec:sep}
For \cstar-algebras $\A$ and $\B$ and for states
$\phi \in \cS (\A)$ and $\psi \in \cS (\B) ,$
there exists a unique state $\phi \otimes \psi \in \cS (\A \otimes \B)$
such that
$( \phi \otimes \psi ) (A \otimes B) = \phi(A) \psi (B) $
$(A \in \A , B \in \B) .$
For subsets $X \subset \cS(\A)$ and $Y \subset \cS (\B) ,$
we write
\[
	X \otimes Y
	:=
	\set{
	\phi \otimes \psi \in \cS (\A \otimes \B)
	|
	\phi \in X, \,
	\psi \in Y
	} .
\]
The states in $\cS (\A) \otimes \cS (\B)$

are called the product states.
We define
\[
	\Ssep (\A \otimes \B)
	:=
	\cco ( \cS (\A) \otimes \cS (\B) ) ,
\]
where the closed convex hull is with respect to the weak-$\ast$
topology $\sigma ((\A \otimes \B)^\ast , \A \otimes \B) .$
Each element of $\Ssep (\A \otimes \B)$ is called a separable state,
while each element of the complement
$\cS (\A \otimes \B) \setminus \Ssep (\A \otimes \B)$
is called an entangled state.

\begin{lemma}\label{lemm:prodch}
Let $\Lambda \in \chset{\A}{\B}$
and
$\Gamma \in \chset{\C}{\D}$
be channels.
Then $\omega \circ (\Lambda \otimes \Gamma) \in \Ssep (\A \otimes \C)$
for any $\omega \in \Ssep (\B \otimes \D) .$
\end{lemma}
\begin{proof}
The claim immediately follows from that
$\Lambda \otimes \Gamma$
maps any input product state $\phi \otimes \psi \in \cS (\B) \otimes \cS (\D)$
to the product state
$(\phi \circ \Lambda) \otimes ( \psi \circ  \Gamma) \in \cS (\A) \otimes  \cS (\C) .$
\end{proof}

\begin{lemma}\label{lemm:comm}
Let $\A$ and $\B$ be \cstar-algebras.
Suppose that $\A$ is commutative.
Then
$\cS (\A \otimes \B) = \Ssep (\A \otimes \B) .$
\end{lemma}
\begin{proof}
By Theorem~4.4 of Ref.~\onlinecite{takesakivol1},
we have
$\Sp (\A \otimes \B) = \Sp (\A) \otimes \Sp (\B) .$
Hence by the Krein-Milman theorem,
$\cS (\A \otimes \B) = \cco (  \Sp (\A) \otimes \Sp (\B)  )
\subset
\cco (  \cS (\A) \otimes \cS(\B)  )
=
\Ssep (\A \otimes \B)
\subset
\cS (\A \otimes \B) ,
$
which proves the claim.
\end{proof}

\begin{lemma}
\label{lemm:iso}
Let $\A$ and $\B$ be \cstar-algebras.
Then the map
\[
	f \colon \cS (\A) \times \cS (\B)
	\ni
	(\phi , \psi)
	\longmapsto
	\phi \otimes \psi
	\in
	\cS (\A) \otimes \cS (\B)
\]
is a topological isomorphism,
where the topologies of
$ \cS (\A) \times \cS (\B)$
and
$ \cS (\A) \otimes \cS (\B)$
are defined as the product topology of the weak-$\ast$ topologies of
$\cS (\A)$ and $\cS(\B) ,$
and the weak-$\ast$ topology on $\cS (\A \otimes \B) ,$
respectively.
\end{lemma}
\begin{proof}
We can easily see that $f$ is bijective.
Since $\cS (\A) \times \cS (\B)$ is a compact Hausdorff space,
we have only to prove the continuity of $f .$
Let $(\phi_i , \psi_i)_{i \in I}$ be a net on $\cS (\A) \times \cS (\B)$
converging to $(\phi , \psi) \in \cS (\A) \times \cS (\B) .$
Then $(\phi_i \otimes \psi_i) (X) \to (\phi \otimes \psi) (X)$
for all $X \in \A \atensor \B .$
Since the net $(\phi_i \otimes \psi_i)_{i \in I}$
is uniformly bounded
and $\A \atensor \B$ is norm dense in $\A \otimes \B ,$
this implies
$(\phi_i \otimes \psi_i) (X) \to (\phi \otimes \psi) (X)$
for all $X \in \A \otimes \B ,$
which proves the continuity of $f .$
\end{proof}

\begin{corollary}\label{coro:compact}
For \cstar-algebras $\A $ and $\B ,$
the set $\cS (\A) \otimes \cS(\B)$ of product states
is a weakly-$\ast$ compact subset of $\cS (\A \otimes \B) .$
\end{corollary}

To prove the integral representation for separable states,
we need some results of barycentric integrals on compact subsets of general
locally convex Hausdorff spaces.~\cite{phelps2001lectures}
Let $E$ be a locally convex Hausdorff space and let $K \subset E$
be a compact subset.
A regular probability measure $ \mu \in \bfMpo (K)$
is said to represent a point $\bar{x} \in E$ if
\[
	f (\bar{x}) = \int_K f(x) d\mu (x)
\]
for any continuous linear functional $f \in E^\ast .$
By using the Hahn-Banach separation theorem,
we can show that such a point $\bar{x} $ is,
if exists,
unique for given $\mu \in \bfMpo (K)$
and called the barycenter of $\mu .$
For $\mu \in \bfMpo (K) ,$
we denote the barycenter of $\mu $
by
\[
	\int_K x d \mu (x) ,
\]
if it exists.

\begin{proposition}[Ref.~\onlinecite{phelps2001lectures}, Proposition~1.2]
\label{prop:barycenter}
Let $E$ be a locally convex Hausdorff space and let
$K \subset E$ be a compact subset.
Then for a point $x \in E ,$
$x \in \cco (K)$ if and only if there exists a regular probability measure
$\mu \in \bfMpo (K)$ that represents $x .$
\end{proposition}

From Corollary~\ref{coro:compact} and Proposition~\ref{prop:barycenter}
we obtain

\begin{corollary}\label{coro:sep}
Let $\A$ and $\B$ be \cstar-algebras.
Then for any separable state $\omega \in \Ssep (\A \otimes \B)$
there exists a regular probability measure
$\nu \in \bfMpo (\cS (\A) \otimes \cS (\B))$
such that
\[
	\omega
	=
	\int_{\cS (\A) \otimes \cS (\B)}
	\phi \otimes \psi \,
	d\nu
	(\phi \otimes \psi ) .
\]
\end{corollary}
Corollary~\ref{coro:sep} is a \cstar-algebra version of the integral representation
for infinite-dimensional separable density operators
obtained in Ref.~\onlinecite{holevo2005separability}.

In the case of state space on a \cstar-algebra,
the barycentric integral can be generalized to the weakly-$\ast$ measurable
state-valued maps as follows.
Let $\A $ be a \cstar-algebra and let $(\Omega , \Sigma , \mu)$
be a probability space.
A map $\Omega \ni x \mapsto \phi_x \in \cS (\A)$ is called
weakly-$\ast$ measurable if
$\Omega \ni x \mapsto \phi_x (A) \in \cmplx$
is $\Sigma$-measurable for all $A \in \A .$
For such a map $\Omega \ni x \mapsto \phi_x \in \cS (\A)$
we define the integral state
$\int_\Omega \phi_x d\mu (x) \in \cS (\A)$ by
\[
	\left(
	\int_\Omega \phi_x d\mu (x)
	\right)
	(A)
	:=
	\int_\Omega
	\phi_x (A) d\mu (x)
	\quad
	(A\in \A) .
\]

\section{Characterizations of EB channels} \label{sec:main}
In this section, we give equivalent characterizations
of the EB condition for a channel (Theorem~\ref{theo:main}).

\begin{definition}\label{defi:eb}
A channel $\Lambda \in \chset{\A}{\Ain}$ is called EB if
$\omega \circ (\Lambda \otimes \id_\B) \in \Ssep (\A \otimes \B)$
for any \cstar-algebra $\B$ and
any input state $\omega \in \cS (\Ain \otimes \B) .$
We denote by $\chseteb{\A}{\Ain}$ the set of EB channels
from $\A$ to $\Ain .$
\end{definition}
In what follows in this section, we fix an input Hilbert space $\Hin ,$
which may be separable or non-separable,
and an orthonormal basis $(\xi_i)_{i \in I}$ of $\Hin .$
We write the set of finite subsets of $I$ as $\FI ,$
which is directed by the set inclusion,
and for each $F \in \FI ,$ define $P_F, $ $\cH_F ,$
$\eta_F \in \cH_F \otimes \cH_F ,$
and $\omega_F \in \cS (\LHin \otimes \calL (\cH_F))$ by
\begin{gather*}
	P_F :=
	\sum_{i \in F}
	\ket{\xi_i} \bra{\xi_i} ,
	\\
	\cH_F := P_F \Hin ,
	\\
	\eta_F
	:=
	|F|^{-1/2}
	\sum_{i \in F}
	\xi_i \otimes \xi_i ,
	\\
	\omega_F (A)
	:=
	\braket{\eta_F | A \eta_F}
	=
	|F|^{-1}
	\sum_{i,j\in F}
	\braket{\xi_i \otimes \xi_i | A (\xi_j \otimes \xi_j)}
	\quad
	(A \in \LHin \otimes \calL (\cH_F)) ,
\end{gather*}
where $| F |$ denotes the number of elements of $F .$
Since $\omega_F (P_F \otimes P_F) = 1 ,$
we can regard $\omega_F$ as a state in
$\cS (\calL (\cH_F) \otimes \calL (\cH_F) ) ,$
which we also write as $\omega_F .$
The state $\omega_F$ is a maximally entangled state on $\cH_F \otimes \cH_F .$

Now we are in a position to prove the main result of this paper:
\begin{theorem}\label{theo:main}
Let $\Ain$ be a unital \cstar-subalgebra of $\LHin ,$
let $\A$ be a \cstar-algebra,
let $\Lambda \in \chset{\A}{\Ain} \subset \chset{\A}{\LHin}$
be a channel,
and let $\bL \in \nchset{\A^{\ast \ast}}{\LHin}$ be the normal extension of
$\Lambda .$
Then the following conditions are equivalent.
\begin{enumerate}[(i)]
\item \label{it:eb1}
$\Lambda \in \chseteb{\A}{\Ain} .$
\item \label{it:eb2}
$\Lambda \in \chseteb{\A}{\LHin} .$
\item \label{it:eb3}
$\bL \in \chseteb{\A^{\ast \ast}}{\LHin} .$
\item \label{it:bell}
$\omega_F \circ (\Lambda \otimes \id_{\LHF}) \in \Ssep (\A \otimes \LHF)$
for all $F \in \FI .$
\item \label{it:rand1}
There exists a channel $\Gamma \in \chset{\C}{\LHin}$
with a commutative outcome \cstar-algebra $\C$
such that $\Lambda \cocp \Gamma .$
\item \label{it:rand2}
There exists a QC channel
$\tG \in \nchset{\M}{\LHin}$
with a commutative outcome von Neumann algebra $\M$ such that
$\Lambda \cocp \tG .$
\item \label{it:holevo}
(Measurement-prepare form).
There exists a POVM $(\Omega , \Sigma , \oM)$
on $\Hin $ and a weakly-$\ast$ measurable map
$\Omega \ni x \mapsto \phi_x \in \cS (\A)$
such that
\begin{equation}
	\Lambda (A)
	=
	\int_\Omega \phi_x (A) d \oM (x)
	\quad
	(A \in \A) .
	\label{eq:holevo}
\end{equation}
\item \label{it:njoint}
$\Lambda$ has an $n$-joint channel
$\Theta_n \in \chset{\A^{\otimes n}}{\LHin}$
for all $2 \leq n < \infty .$
\item \label{it:ijoints}
$\Lambda$ has a symmetric $\omega$-joint channel
$\Theta_\infty \in \chset{\A^{\otimes \infty}}{\LHin} .$
\item \label{it:ijoint}
$\Lambda$ has an $\omega$-joint channel
$\Theta_\infty^\prime \in \chset{\A^{\otimes \infty}}{\LHin} .$
\end{enumerate}
\end{theorem}
\begin{proof}
\eqref{it:eb1}$\implies$\eqref{it:eb2}.
Assume \eqref{it:eb1} and take a \cstar-algebra $\B$
and a state $\omega \in \cS (\LHin \otimes \B) .$
Since $\Ain \otimes \B \subset \LHin \otimes \B ,$
by the assumption we have
$\omega \circ (\Lambda \otimes \id_\B)
= \omega \rvert_{\Ain \otimes \B} \circ (\Lambda \otimes \id_\B)
\in \Ssep (\A \otimes \B) ,
$
which implies \eqref{it:eb2}.

\eqref{it:eb2}$\implies$\eqref{it:eb1}.
Assume \eqref{it:eb2} and take a \cstar-algebra $\B$
and a state $\omega \in \cS (\Ain \otimes \B) .$
From $\Ain \otimes \B \subset \LHin \otimes \B $
and the Hahn-Banach theorem,
$\omega$ extends to a linear functional $\tomega \in (\LHin \otimes \B)^\ast$
such that $\| \tomega \| = \| \omega \| =1 .$
Since
$\tomega (\unit_{\LHin \otimes \B})
=  \omega( \unit_{\Ain \otimes \B})
= 1 = \| \tomega \| ,$
$\tomega$ is a state on $\LHin \otimes \B $
by Proposition~1.5.2 of Ref.~\onlinecite{sakaibook}.
Thus by the assumption we have
$\omega \circ (\Lambda \otimes \id_\B) = \tomega \circ (\Lambda \otimes \id_\B)
\in \Ssep (\A \otimes \B),
$
which implies \eqref{it:eb1}.

\eqref{it:eb2}$\implies$\eqref{it:bell} is obvious.

\eqref{it:bell}$\implies$\eqref{it:rand1}.
Assume \eqref{it:bell}.
For each $F \in \FI ,$ we define $\LF \in \chset{\A}{\LHF}$ by
$\LF (A) := P_F \Lambda (A) P_F $
$(A\in \A ) .$
By assumption we have
$\omega_F \circ (\Lambda_F \otimes \id_{\LHF})
= \omega_F \circ (\Lambda \otimes \id_{\LHF})
\in \Ssep (\A \otimes \LHF) .
$
Therefore by Corollary~\ref{coro:sep} there exists a regular probability measure
$\nu_F \in \bfMpo (\cS (\A) \otimes \cS (\LHF))$
such that
\[
	\omega_F \circ (\Lambda_F \otimes \id_{\LHF})
	=
	\int_{\cS (\A) \otimes \cS (\LHF)}
	\phi \otimes \psi \,
	d\nu_F (\phi \otimes \psi).
\]
For each Borel set $E \in \B (\SA),$
we define a positive linear functional
$\tphi_E \in \LHF^\ast$ by
\[
	\tphi_E (B)
	:=
	\int_{E \otimes \cS (\LHF )}
	\psi(B)
	d\nu_F
	(\phi \otimes \psi)
	\quad
	(B \in \LHF).
\]
We write $\tphi := \tphi_{\SA} ,$
which is a state on $\LHF$
given by
\begin{equation}
	\tphi (B)
	=
	\omega_F
	\circ
	(\Lambda_F \otimes \id_{\LHF})
	(\unit_{\A} \otimes B )
	=
	\braket{\eta_F | (P_F \otimes B) \eta_F}
	\quad (B \in \LHF) .
	\label{eq:tphi}
\end{equation}
Then the RHS of \eqref{eq:tphi}
is a GNS representation of $\tphi .$
Furthermore, by the $\sigma$-additivity of $\nu_F ,$
the map
$\B (\SA) \ni E \mapsto \tphi_E (B) \in \cmplx$
is also $\sigma$-additive for all $B \in \LHF .$
Therefore application of the Radon-Nikodym theorem
for CP maps (e.g.\ Theorem~III.1 of Ref.~\onlinecite{doi:10.1063/1.1615697})
to $\tphi \in \chset{\LHF}{\cmplx} $
yields that
there exists a unique POVM $(\SA , \B (\SA) , \oM_F)$
on $\cH_F$ such that
\[
	\tphi_E (B)
	=
	\braket{\eta_F | (\oM_F (E) \otimes B) \eta_F}
	\quad
	(E \in \B (\SA) , B \in \LHF  ) .
\]
We define channels
$\alpha \in \chset{\A}{C (\SA)}$
and
$\Gamma_F \in \chset{C ( \SA )}{\LHF}$
by
\begin{gather*}
	\alpha (A) (\phi)
	:=
	\phi (A)
	\quad
	(A \in \A , \phi \in \SA) ,
	\\
	\Gamma_F (f)
	:=
	\int_{\SA}
	f (\phi)
	d \oM_F (\phi)
	\quad
	(f \in C (\SA ) ) .
\end{gather*}
Then for each $i,j \in F$
and each
$E \in \B (\SA ) ,$
\[
	\braket{\eta_F|
	(\oM_F (E) \otimes \ket{\xi_i} \bra{\xi_j})
	\eta_F
	}
	=
	\tphi_E (\ket{\xi_i } \bra{\xi_j})
	=
	\int_{E \otimes \cS (\LHF)}
	\psi (\ket{\xi_i } \bra{\xi_j})
	d\nu_F (\phi \otimes \psi) .
\]
Hence for each $i, j \in F $
and each $A \in \A  ,$
\begin{align*}
	\braket{\xi_i | \Gamma_F \circ \alpha (A) \xi_j}
	&=
	\int_{\SA}
	\phi(A)
	d \braket{\xi_i| \oM_F (\phi) \xi_j}
	\\
	&=
	| F |
	\int_{\SA}
	\phi (A)
	d \braket{\eta_F|
	(\oM_F (\phi) \otimes \ket{\xi_i} \bra{\xi_j})
	\eta_F
	}
	\\
	&= |F|
	\int_{\SA \otimes \cS (\LHF )}
	\phi (A)
	\psi(\ket{\xi_i} \bra{\xi_j})
	d \nu_F (\phi \otimes \psi)
	\\
	&=
	|F|
	\left(
	\omega_F \circ (\Lambda_F \otimes \id_{\LHF})
	\right)
	(A \otimes \ket{\xi_i} \bra{\xi_j} )
	\\
	&=
	\braket{\xi_i | \Lambda_F (A) \xi_j} .
\end{align*}
Therefore
$\Lambda_F = \Gamma_F \circ \alpha .$
Since a closed ball in $\LHin$ is $\sigma$-weakly compact,
Tychonoff\rq{}s theorem implies that
there exist
a subnet $(\Gamma_{F(j)})_{j \in J}$
and a bounded linear map
$\Gamma \colon C (\SA) \to \LHin$
such that
$\Gamma_{F(j)} (f)
\xrightarrow{\text{$\sigma$-weakly}}
\Gamma (f)
$
for all $f \in C (\SA ) .$
By the complete positivity of each $\Gamma_F ,$
$\Gamma $ is also CP.
From
\[
	\Gamma (\unit_{C (\SA )})
	=
	\swlim_{j \in J} \Gamma_{F(j)}
	(\unit_{C (\SA )})
	=
	\swlim_{j \in J} P_{F(j)}
	= \unit_{\Hin} ,
\]
where $\swlim$ denotes the $\sigma$-weak limit,
we have
$\Gamma \in \chset{C(\SA ) }{\LHin} .$
Moreover for each $A \in \A $
\[
	\Gamma \circ \alpha (A)
	=
	\swlim_{j \in J}
	\Gamma_{F(j)} \circ \alpha (A)
	=
	\swlim_{j \in J}
	\Lambda_{F(j)} (A)
	= \Lambda (A),
\]
where we used
$P_F B P_F \xrightarrow{\text{$\sigma$-strongly}}
B$
$(B \in \LHin)$
in the third equality.
Therefore
$\Lambda = \Gamma \circ \alpha \cocp \Gamma .$
Since the outcome space $C (\SA ) $
of $\Gamma$ is commutative,
this implies \eqref{it:rand1}.

\eqref{it:rand1}$\implies$\eqref{it:rand2}.
Let $\Gamma \in \chset{\C}{\LHin}$ be a channel
such that $\C$ is commutative and
$\Lambda \cocp \Gamma .$
Then the outcome space $\C^{\ast \ast}$
of the normal extension
$\tG \in \nchset{\C^{\ast \ast}}{\LHin}$
of $\Gamma $
is also commutative
and hence $\tG$ is a QC channel.
Moreover we have
$\Lambda \cocp \Gamma \cocp \tG ,$
which implies \eqref{it:rand2}.

\eqref{it:rand2}$\implies$\eqref{it:rand1} is obvious.

\eqref{it:rand1}$\implies$\eqref{it:holevo}.
Assume \eqref{it:rand1} and take channels
$\Gamma \in \chset{\C}{\LHin}$
and
$\beta \in \chset{\A}{\C}$
such that $\C$ is commutative
and $\Lambda = \Gamma \circ \beta .$
By the Gelfand representation we may assume that
$\C = C(\Omega)$ for some compact Hausdorff space $\Omega .$
Then by Proposition~\ref{prop:RMK} there exists a unique
regular POVM $(\Omega , \B (\Omega) , \oM)$
on $\Hin$ such that
\[
	\Gamma (f)
	= \int_\Omega f (x) d\oM (x)
	\quad
	(f \in C (\Omega)) .
\]
If we define $\phi_x \in \SA$ by $\phi_x (A) := \beta(A) (x) $
$(A \in \A)$
for each $x \in \Omega ,$
the map $\Omega \ni x \mapsto \phi_x \in \SA$
is weakly-$\ast$ measurable.
Moreover for each $A \in \A$
\[
	\Lambda (A)
	=
	\Gamma \circ \beta (A)
	=
	\int_\Omega \beta (A) (x) d \oM (x)
	=
	\int_\Omega \phi_x (A) d \oM (x),
\]
which implies \eqref{it:holevo}.

\eqref{it:holevo}$\implies$\eqref{it:rand1}.
Assume \eqref{it:holevo} and take a POVM $(\Omega , \Sigma , \oM)$ on $\Hin$
and a weakly-$\ast$ measurable map
$\Omega \ni x \mapsto \phi_x \in \SA $
satisfying \eqref{eq:holevo}.
We define channels $\gamma \in \chset{\A}{B(\Omega , \Sigma)}$
and $\Gamma^\prime \in \chset{B(\Omega , \Sigma)}{\LHin}$
by
\begin{gather*}
	\gamma (A) (x)
	:=
	\phi_x (A)
	\quad
	(A \in \A , x \in \Omega),
	\\
	\Gamma^\prime (f)
	:=
	\int_\Omega
	f (x) d \oM (x)
	\quad
	(f \in B(\Omega , \Sigma)) .
\end{gather*}
Then by the assumption~\eqref{eq:holevo}
we have $\Lambda = \Gamma^\prime \circ \gamma \cocp \Gamma^\prime .$
Since $B(\Omega, \Sigma)$ is commutative,
this implies \eqref{it:rand1}.

\eqref{it:rand1}$\implies$\eqref{it:eb2}.
Assume \eqref{it:rand1} and take channels
$\Gamma \in \chset{\C}{\LHin}$
and
$\alpha \in \chset{\A}{\C}$
such that $\C$ is commutative
and $\Lambda = \Gamma \circ \alpha .$
Then for any \cstar-algebra $\B$
and any state $\omega \in \cS (\LHin \otimes \B) ,$
Lemma~\ref{lemm:comm} implies
$\omega \circ (\Gamma \otimes \id_\B) \in \Ssep (\C \otimes \B) .$
Hence by Lemma~\ref{lemm:prodch}
\[
	\omega \circ (\Lambda \otimes \id_\B)
	=
	\omega \circ
	(\Gamma \otimes \id_\B)
	\circ
	(\alpha \otimes \id_\B)
	\in \Ssep (\A \otimes \B) ,
\]
which proves \eqref{it:eb2}.

\eqref{it:rand1}$\implies$\eqref{it:njoint}.
Assume \eqref{it:rand1} and take channels
$\Gamma \in \chset{\C}{\LHin}$
and
$\alpha \in \chset{\A}{\C}$
such that $\C$ is commutative
and $\Lambda = \Gamma \circ \alpha .$
By the commutativity of $\C , $
for each $2 \leq n < \infty $
there exists a channel
$\alpha_n \in \chset{\Atn}{\C}$ such that
\[
	\alpha_n (A_1 \otimes A_2 \otimes \dots \otimes A_n)
	=
	\alpha (A_1) \alpha (A_2) \cdots \alpha (A_n)
	\quad
	(A_1 , A_2 , \dots , A_n \in \A) .
\]
Then $\Gamma \circ \alpha_n \in \chset{\Atn}{\LHin}$
is an $n$-joint channel of $\Lambda .$

\eqref{it:njoint}$\implies$\eqref{it:ijoints}.
Assume \eqref{it:njoint} and take a symmetric $n$-joint channel
$\Theta_n \in \chset{\Atn}{\LHin}$
of $\Lambda$ for each $2 \leq n < \infty .$
We write $\tA_0 := \bigcup_{n \geq 1} \Atn \otimes \unit_{\Ainf} ,$
which is a norm dense $\ast$-subalgebra of $\Ainf ,$
and for each $2\leq n < \infty$
define a map $\Xi_n \colon \tA_0 \to \LHin$
by
\[
	\Xi_n (Y)
	:=
	\begin{cases}
	\Theta_n (X)
	&
	\text{if $Y = X \otimes \unit_{\Ainf}$ and $ X \in \Atn  ;$}
	\\
	0
	&
	\text{otherwise .}
	\end{cases}
\]
Since $\| \Xi_n (Y) \| \leq  \| Y \|$ for all $Y \in \tA_0$
and all $2 \leq n < \infty ,$
by Tychonoff\rq{}s theorem there exists a subnet
$(\Xi_{n(k)})_{k \in K}$
such that the $\sigma$-weak limit
$\Theta_0 (Y) := \swlim_{k \in K} \Xi_{n(k)} (Y)$
exists for all $Y \in \tA_0 .$
Since $\Xi_{n(k)} (c_1 Y_1 + c_2 Y_2) = c_1 \Xi_{n(k)} (Y_1) + c_2 \Xi_{n(k)} (Y_2)$
eventually for each $Y_1 , Y_2 \in \tA_0$
and each $c_1 , c_2 \in \cmplx ,$
$\Theta_0 \colon \tA_0 \to \LHin$ is a bounded linear map
and hence uniquely extends to a bounded linear map
$\Theta_\infty \colon \Ainf \to \LHin .$
Then,
by the complete positivity of each $\Theta_n ,$
$\Theta_\infty $ is a channel in
$\chset{\Ainf}{\LHin} .$
By the symmetry of each $\Theta_n ,$
$\Theta_\infty$ is also symmetric.
Moreover
\begin{equation}
	\Theta_\infty
	(A \otimes \unit_{\Ainf})
	=
	\swlim_{k \in K}
	\Theta_{n(k)}
	(A \otimes \unit_{\A^{\otimes (n(k)-1)}})
	=\Lambda (A)
	\quad
	(A \in \A) .
	\label{eq:thinf}
\end{equation}
From the symmetry of $\Theta_\infty ,$
Eq.~\eqref{eq:thinf}
implies that $\Theta_\infty$
is a symmetric $\omega$-joint channel of $\Lambda, $
which proves \eqref{it:ijoints}.

\eqref{it:ijoints}$\implies$\eqref{it:ijoint} is obvious.

\eqref{it:ijoint}$\implies$\eqref{it:njoint} is immediate from that
for an $\omega$-joint channel $\Theta_\infty^\prime \in \chset{\Ainf}{\LHin}$
and each $2 \leq n< \infty ,$
the map
\[
	\Atn \ni X \longmapsto \Theta_\infty^\prime (X \otimes \unit_{\Ainf})
	\in \LHin
\]
is an $n$-joint channel of $\Lambda .$

\eqref{it:ijoints}$\implies$\eqref{it:rand2}.
Let $\Theta_\infty \in \chset{\Ainf}{\LHin}$
be a symmetric $\omega$-joint channel of $\Lambda .$
If $\Theta_\infty$ has a broadcasting channel
$\Psi_\infty \in \chset{\Ainf \otimes \Ainf}{\Ainf} ,$
by Lemma~\ref{lemm:bc}
the normal extension $\bTh_\infty \in \chset{(\Ainf)^{\ast \ast}}{\LHin}$
of $\Theta_\infty$
is randomization-equivalent to a QC channel
and, from $\Lambda \cocp \Theta_\infty \cocp \bTh_\infty ,$
this implies \eqref{it:rand2}.
Thus it suffices to construct a broadcasting channel of $\Theta_\infty .$
For each $1 \leq n < \infty$
we define a representation
\[
\rho_n \colon (\Atn \otimes \unit_{\Ainf}) \otimes (\Atn \otimes \unit_{\Ainf})
\to
\A^{\otimes (2n)} \otimes \unit_{\Ainf}
\]
by
\begin{align*}
	&\rho_n \left(
	(A_1 \otimes A_2 \otimes \cdots \otimes A_n \otimes \unit_{\Ainf})
	\otimes
	(B_1 \otimes B_2 \otimes \cdots \otimes B_n \otimes \unit_{\Ainf})
	\right)
	\\
	&:=
	A_1 \otimes B_1 \otimes A_2 \otimes B_2 \otimes
	\cdots
	A_n \otimes B_n \otimes \unit_{\Ainf}
	\\
	&( A_1 , \dots , A_n , B_1 , \dots , B_n \in \A) .
\end{align*}
Let $\B_n :=  (\Atn \otimes \unit_{\Ainf}) \otimes (\Atn \otimes \unit_{\Ainf})$
and $\B_\infty := \bigcup_{1 \leq n < \infty} \B_n ,$
which are \cstar- and $\ast$-subalgebras of $\Ainf \otimes \Ainf, $
respectively.
Since $\rho_n \rvert_{\B_m} = \rho_m$
for $1 \leq m < n < \infty ,$
there exists a representation
$\trho_0 \colon \B_\infty \to \Ainf$
such that $\trho_0 \rvert_{\B_n} = \rho_n$
for all $1 \leq n < \infty .$
Now we show that $\B_\infty$ is norm dense in $\Ainf \otimes \Ainf .$
Take an arbitrary product element $X_1 \otimes X_2 \in \Ainf \otimes \Ainf$
$(X_1 , X_2 \in \Ainf) .$
Then there exist sequences $(X_{j,m})_{m \geq 1}$
$(j=1,2)$
in $\bigcup_{n \geq 1} \Atn \otimes \unit_{\Ainf}$
such that
$ \| X_{j,m} - X_j \| \to 0  $
and
$\sup_{m \geq 1} \| X_{j,m} \| \leq \| X_j \| .$
Then $(X_{1,m} \otimes X_{2,m})_{m \geq 1}$
is a sequence in $\B_\infty$ and satisfies
\begin{align*}
	\| X_{1,m} \otimes X_{2,m} - X_{1} \otimes X_{2} \|
	&\leq
	\|  (X_{1,m} - X_1) \otimes X_{2,m} \|
	+
	\| X_1 \otimes (X_{2,m} - X_2) \|
	\\
	&\leq
	\| X_{1,m} - X_1 \| \| X_2 \|
	+
	\| X_1 \|
	\| X_{2,m} - X_2 \|
	\\
	&\to 0 .
\end{align*}
Therefore $\B_\infty$ is norm dense in $\Ainf \otimes \Ainf .$
Hence $\trho_0$ uniquely extends to a representation
$\trho \colon \Ainf \otimes \Ainf \to \Ainf .$
Then by the symmetry of $\Theta_\infty ,$
for each $2 \leq n < \infty$
and each $X \in \Atn ,$
\[
	\Theta_{\infty} (X \otimes \unit_{\Ainf})
	=
	\Theta_\infty \circ \trho
	\left(
	(X \otimes \unit_{\Ainf}) \otimes \unit_{\Ainf}
	\right)
	=
	\Theta_\infty \circ \trho
	\left(
	 \unit_{\Ainf} \otimes  (X \otimes \unit_{\Ainf})
	\right) .
\]
Since $\bigcup_{n \geq 1} \Atn \otimes \unit_{\Ainf}$
is norm dense in $\Ainf ,$
this implies that $\trho$ is a broadcasting channel of $\Theta_\infty ,$
which proves \eqref{it:rand2}.

\eqref{it:eb2}$\iff$\eqref{it:eb3} follows from the equivalence
\eqref{it:eb2}$\iff$\eqref{it:rand2}
and from that $\Lambda \cocp \tG$ if and only if
$\bL \cocp \tG$ for any QC channel $\tG .$
\end{proof}
From the proof of \eqref{it:ijoints}$\implies$\eqref{it:rand2}
in Theorem~\ref{theo:main},
we obtain
\begin{corollary}\label{coro:sym}
Let $\A$ be a \cstar-algebra.
Then any symmetric channel
$\Theta \in \chset{\Ainf}{\LHin}$
has a broadcasting channel $\Psi \in \chset{\Ainf \otimes \Ainf}{\Ainf} .$
Furthermore the normal extension
$\bTh \in \nchset{(\Ainf)^{\ast \ast}}{\LHin}$
of $\Theta$ is randomization-equivalent to a QC channel.
\end{corollary}

\begin{remark} \label{rem:refs}
Related results to the equivalence of the EB condition and \eqref{it:rand1}
of Theorem~\ref{theo:main} were obtained in
Ref.~\onlinecite	{STORMER20082303} (Corollary~3)
and
Ref.~\onlinecite{doi:10.1063/1.5024385} (Lemma~III.1).
\end{remark}

\section{Dedekind-closedness of EB channels} \label{sec:dedekind}
In this section we prove that the supremum or infimum
of any randomization-monotone net of normal EB channels
with a fixed input von Neumann algebra is also EB
(Theorem~\ref{theo:dc}).
Before going to Theorem~\ref{theo:dc},
we need to review some results from Ref.~\onlinecite{kuramochi2018directed}.

For a von Neumann algebra $\Min$
we denote by $\nchset{}{\Min}$
the class of normal channels with the input space $\Min$
and with arbitrary outcome von Neumann algebras.
Since the class of von Neumann algebras is a proper class,
so is $\nchset{}{\Min} .$

\begin{proposition}[Ref.~\onlinecite{kuramochi2018directed}, Section~3]
\label{prop:class}
Let $\Min$ be a von Neumann algebra.
Then there exist a set $\CH (\Min)$
and a class-to-set surjection
\begin{equation}
	\nchset{}{\Min} \ni \Lambda \longmapsto [\Lambda] \in \CH (\Min)
	\label{eq:csmap}
\end{equation}
such that for any $\Lambda , \Gamma \in \nchset{}{\Min} ,$
$\Lambda \eqcp \Gamma$ if and only if $[\Lambda] = [\Gamma] .$
\end{proposition}

For each von Neumann algebra $\Min$ we fix such a set
$\CH (\Min)$ and a map \eqref{eq:csmap}.
We call $\CH (\Min)$ the set of randomization-equivalence classes of normal channels.
We define a partial order $\cocp $ on $\CH (\Min)$ by
$[\Lambda] \cocp [\Gamma] $
$:\defarrow$
$\Lambda \cocp \Gamma $
$([\Lambda ] , [\Gamma] \in \CH (\Min)) .$
We also define
\begin{gather*}
	\CHqc (\Min)
	:=
	\set{ [\Lambda] \in \CH (\Min) |
	\text{the outcome algebra of $\Lambda$ is commutative}} ,
	\\
	\CHeb (\Min ):=
	\set{ [\Lambda] \in \CH (\Min) |
	\text{$\Lambda$ is EB}
	 },
\end{gather*}
which are the sets of equivalence classes of QC and EB normal channels,
respectively.

Let $(X , \leq )$ be a partially ordered set (poset).
We adopt the following terminology as in Ref.~\onlinecite{kuramochi2018directed}
\begin{itemize}
\item
A net $(x_i)_{i \in I}$ on $X$ is called increasing
(respectively, decreasing)
if for $i,j \in I ,$
$i \leq j$ implies $x_i \leq x_j$
(respectively, $x_j \leq x_i$).
\item
$X$ is called an upper (respectively, lower)
directed-complete partially ordered set (dcpo)
if any increasing (respectively, decreasing) net $(x_i)_{i \in I}$
on $X$ has a supremum $\sup_{i \in I} x_i \in X$
(respectively, infimum $\inf_{i \in I} x_i \in X $).
\item
A subset $A \subset X$ is said to be an upper (respectively, lower)
Dedekind-closed subset of $X$
if whenever an increasing (respectively, decreasing)
net $(x_i)_{i \in I}$ on $A$
has a supremum $\sup_{i \in } x_i \in X $
(respectively, infimum $\inf_{i \in I }x_i \in X$),
then $\sup_{i\in I} x_i \in A$
(respectively, $\inf_{i \in I}x_i \in A$).
\end{itemize}

The following theorem is the \lq\lq{}channel part\rq\rq{}
of the main results of Ref.~\onlinecite{kuramochi2018directed}.
\begin{theorem}[Ref.~\onlinecite{kuramochi2018directed}, Theorem~3]
\label{theo:prev}
Let $\Min$ be a von Neumann algebra.
\begin{enumerate}[(i)]
\item
$\CH (\Min)$ is an upper and lower dcpo.
\item
$\CHqc (\Min)$ is an upper and lower Dedekind-closed subset of $\CH (\Min) .$
\end{enumerate}
\end{theorem}

Now we are in a position to prove the following theorem.

\begin{theorem}\label{theo:dc}
Let $\Min$ be a von Neumann algebra.
Then $\CHeb (\Min)$ is an upper and lower Dedekind-closed subset
of $\CH (\Min) .$
\end{theorem}
\begin{proof}
Suppose that $\Min$ acts on a Hilbert space $\Hin .$
We first show the claim when $\Min = \LHin .$

By Theorem~\ref{theo:main}, we can write
\[
	\CHeb (\LHin)
	=
	\set{[\Lambda] \in \CH (\LHin)|
	\exists [\Gamma]\in \CHqc (\LHin) \text{ s.t. }
	[\Lambda] \cocp [\Gamma]
	} ,
\]
from which the lower Dedekind-closedness of $\CHeb (\LHin)$ immediately follows.
Now we show the upper Dedekind-closedness of $\CHeb (\LHin) .$
According to Lemma~4 of Ref.~\onlinecite{kuramochi2018directed},
we have only to prove
$\sup_{\alpha< \alpha_0} [\Lambda_\alpha] \in \CHeb (\LHin)$
for any increasing transfinite sequence $([\Lambda_\alpha])_{\alpha <\alpha_0}$
in $\CHeb (\LHin) $
indexed by ordinals $\alpha$
smaller than $\alpha_0$ and greater than or equal to $0 .$
From the proof of Lemma~7 of Ref.~\onlinecite{kuramochi2018directed}
we can take channels $\tL_\alpha \in \chset{\A_\alpha}{\LHin}$
$(\alpha < \alpha_0)$
and
$\Lambda \in \chset{\A}{\LHin}$ such that
\begin{itemize}
\item
$\Lambda_\alpha \eqcp \tL_\alpha $
$(\alpha < \alpha_0) ;$
\item
$(\A_\alpha)_{\alpha < \alpha_0}$ is an increasing transfinite sequence of
unital \cstar-subalgebras of $\A$
such that $\bigcup_{\alpha < \alpha_0} \A_\alpha$
is a norm dense $\ast$-subalgebra of $\A ;$
\item
$\tL_\alpha$ is the restriction of $\Lambda$ to $\A_\alpha$
$(\alpha < \alpha_0) ;$
\item
if we denote by $\bL \in \nchset{\A^{\ast \ast}}{\LHin}$ the normal extension of
$\Lambda, $
we have $[\bL] = \sup_{\alpha < \alpha_0} [\Lambda_\alpha ] .$
\end{itemize}
Therefore by
the equivalence \eqref{it:eb2}$\iff$\eqref{it:eb3} of Theorem~\ref{theo:main},
it suffices to show that $\Lambda$ is EB.
For each $\alpha < \alpha_0 ,$
since $\Lambda_\alpha$ is EB,
so is $\tL_\alpha .$
Hence there exists a symmetric $n$-joint channel
$\Theta_{n ,\alpha} \in \chset{\Atn_\alpha}{\LHin}$
of $\tL_\alpha$
for each $2 \leq n < \infty .$
We define a $\ast$-subalgebra $\tA_n \subset \Atn$
and a map $\Xi_{n, \alpha} \colon \tA_n \to \LHin$
by
\begin{gather*}
	\tA_n := \bigcup_{\alpha < \alpha_0} \Atn_\alpha ,
	\\
	\Xi_{n,\alpha}(X)
	:=
	\begin{cases}
	\Theta_{n,\alpha} (X)
	& \text{if $X \in \Atn_\alpha;$}
	\\
	0 & \text{otherwise.}
	\end{cases}
\end{gather*}
By Tychonoff's theorem,
there exists a subnet $(\Xi_{n , \alpha (i)})_{i \in I}$
such that the limit
$\Theta^\prime_n (X) := \swlim_{i \in I} \Xi_{n, \alpha (i)} (X)$
exists for all $X \in \tA_n .$
Similarly as in the proofs of
\eqref{it:njoint}$\implies$\eqref{it:ijoints}
and
\eqref{it:ijoints}$\implies$\eqref{it:rand2}
of Theorem~\ref{theo:main},
we can show that $\tA_n$ is norm dense in $\Atn$
and $\Theta_n^\prime$ uniquely extends to a
symmetric channel $\Theta_n \in \chset{\Atn}{\LHin} .$
Since
\[
	\Theta_n (A \otimes \unit_{\A^{\otimes (n-1)}})
	=\swlim_{i \in I , \alpha(i) \geq \alpha}
	\Theta_{n, \alpha (i)}
	(A \otimes \unit_{\A^{\otimes (n-1)}_{\alpha(i)}})
	=
	\Lambda(A)
\]
for each $\alpha <\alpha_0$ and each
$A \in \A_\alpha ,$
the norm denseness of
$\bigcup_{\alpha < \alpha_0} \A_\alpha$
in $\A$
implies
$\Theta_n (A \otimes \unit_{\A^{\otimes (n-1)}}) = \Lambda (A)$
for all $A\in \A .$
Thus by the symmetry of  $\Theta_n, $
$\Theta_n$ is an $n$-joint channel of $\Lambda .$
Therefore by Theorem~\ref{theo:main}, $\Lambda$ is EB,
which proves the upper Dedekind-closedness of $\CHeb (\LHin) .$

Finally we consider general $\Min .$
We can regard the set $\CH (\Min)$ as the lower subset
\[
	\set{[\Lambda] \in \CH (\LHin) | [\Lambda] \cocp [\id_{\Min}]}
\]
of $\CH (\LHin) .$
Furthermore, by the equivalence \eqref{it:eb1}$\iff$\eqref{it:eb2}
of Theorem~\ref{theo:main},
$\CHeb (\Min)$
can be identified with the lower subset
\[
	\set{[\Lambda] \in \CHeb (\LHin) | [\Lambda] \cocp [\id_{\Min}]}
\]
of $\CHeb (\LHin) \subset \CH (\LHin) .$
Therefore the claim for general $\Min$ follows from that for $\LHin .$
\end{proof}

\section{Example} \label{sec:ex}
In this section, we construct injective normal EB channels
with arbitrary outcome von Neumann algebras on an infinite-dimensional separable Hilbert space.
We first remark that if we omit the injectivity requirement,
we have a trivial example of such a channel:
for each von Neumann algebra $\M$ acting on a Hilbert space $\cH $
and a fixed normal state $\vph$ on $\M ,$
the channel
\[
	\M \ni A \mapsto \vph (A) \unit_{\cH} \in  \LH
\]
is an EB channel with the outcome algebra $\M .$
Indeed, the above channel is trivial in the sense
that it is minimal in the randomization order $\cocp $
among $\nchset{}{\LH}.$

In what follows in this section,
we fix an infinite-dimensional separable Hilbert space $\cH $
and an orthonormal basis $(x_n)_{n \in \natz}$ of $\cH ,$
where $\natz$ is the set of natural numbers containing $0 .$
For each $\alpha \in \cmplx$ we define the coherent state vector~\cite{PhysRev.131.2766} by
\[
	\psi_\alpha
	:=
	e^{- |\alpha|^2 /2} \sum_{n \in \natz} \frac{\alpha^n}{\sqrt{n!}} x_n .
\]
The coherent state vectors satisfy the overcompleteness relation~\cite{PhysRev.138.B274}
\[
	\pi^{-1} \int_\cmplx \ket{\psi_\alpha} \bra{\psi_\alpha} d^2 \alpha
	= \unit_{\cH} ,
\]
where
$d^2 \alpha = d \Real (\alpha) d \Imag (\alpha) $
is the $2$-dimensional Lebesgue measure and
the integral is in the weak sense.
We denote by $L^p (\cmplx)$ the $L^p$ space of $\cmplx$
with respect to $d^2 \alpha .$
We define normal channels
$\gbarg \in \nchset{L^\infty(\cmplx)}{\LH} ,$
$\Psi \in \nchset{\LH}{L^\infty(\cmplx)},$
and $\Lambda \colon \nchset{\LH}{\LH}$
by
\begin{gather*}
	\gbarg (f)
	:=
	\pi^{-1} \int_\cmplx f (\alpha) \ket{\psi_\alpha} \bra{\psi_\alpha} d^2 \alpha
	\quad (f \in L^\infty(\cmplx)) ,
	\\
	\Psi (A) (\alpha) := \braket{\psi_\alpha | A \psi_\alpha}
	\quad
	(A \in \LH , \alpha \in \cmplx) ,
	\\
	\Lambda := \gbarg \circ \Psi .
\end{gather*}
The QC channel $\gbarg$ corresponds to the POVM
$\pi^{-1} \ket{\psi_\alpha} \bra{\psi_{\alpha}} d^2 \alpha$
on $\cmplx$ called the Bargmann measure.~\cite{bargmann1961,klauder1968fundamentals}
For each von Neumann algebra $\M$ acting on $\cH ,$
we also define $\Lambda_\M \in \nchset{\M}{\LH} $
as the restriction of $\Lambda$ to $\M .$
Then we immediately have
$\Lambda_\M \cocp \Lambda \cocp \gbarg $
and hence $\Lambda_\M$ is EB.
Now we have
\begin{proposition}\label{prop:ex}
$\Lambda_\M$ is an injective EB channel for any von Neumann algebra $\M$ acting on $\cH .$
\end{proposition}
\begin{proof}
It suffices to establish the injectivity of $\Lambda .$
Since the injectivity of $\Psi$ is well-known (e.g.\ Ref.~\onlinecite{PhysRev.138.B274}),
we have only to prove the injectivity of $\gbarg .$
Take $f \in L^\infty (\cmplx)$ such that $\gbarg (f) = 0 .$
Then by noting $| \braket{\psi_\alpha | \psi_\beta} |^2 = e^{-|\beta-\alpha|^2} ,$
we have
\[
	\int_\cmplx f(\beta) e^{- | \beta - \alpha |^2} d^2 \beta
	=
	\pi \braket{ \psi_\alpha| \gbarg (f) \psi_\alpha }
	=
	0
	\quad (\forall \alpha \in \cmplx)
\]
and hence
\begin{equation}
	\int_\cmplx
	f(\beta)
	(h \ast g) (\beta) d^2 \beta
	=
	\int_\cmplx \int_\cmplx
	f(\beta)
	e^{-| \beta - \alpha|^2 }
	g(\alpha)
	d^2 \beta d^2 \alpha
	=0
	\label{eq:fg}
\end{equation}
for any $g \in L^1 (\cmplx) ,$
where $h(\alpha) := e^{- |\alpha |^2}$ and
\[
	F \ast G (\beta)
	=
	\int_\cmplx F(\beta - \alpha) G(\alpha) d^2 \alpha
\]
is the convolution.
If we take
$g(\alpha) = e^{- | \alpha |^2 + 2ik_1 \Real(\alpha) + 2ik_2 \Imag (\alpha)}$
for each $(k_1, k_2) \in \realn^2 ,$ then a straightforward calculation gives
\[
	h \ast g(\beta)
	=\frac{\pi}{2}
	\exp \left[
	- \frac{| \beta|^2}{2}
	- \frac{1}{2} (k_1^2 + k_2^2)
	+ i k_1 \Real (\beta) + i k_2 \Imag (\beta)
	\right] .
\]
Hence \eqref{eq:fg} implies
\begin{equation}
	\int_\cmplx f(\beta)
	e^{- \frac{| \beta|^2}{2} + i k_1 \Real (\beta) + i k_2 \Imag (\beta) }
	d^2 \beta
	= 0
	\label{eq:fourier}
\end{equation}
for any $(k_1 , k_2 ) \in \realn^2 .$
Equation~\eqref{eq:fourier} implies that the Fourier transform
of the integrable function $f(\beta) e^{- \frac{| \beta|^2}{2} }$ is zero.
Hence, by the injectivity of the Fourier transform, we obtain $f(\alpha) =0$
for almost all $\alpha \in \cmplx, $
proving the injectivity of $\gbarg . $
\end{proof}

By using the concept of the minimal sufficiency of channels,~\cite{kuramochi2017minimal}
we can show that $\Lambda_\M$ is not randomization-equivalent to
any QC channel if $\M$ is not commutative.
A normal channel $\Gamma \in \nchset{\N}{\Min}$ is called minimal sufficient if
$\Gamma \circ \Phi = \Gamma$ implies $\Phi = \id_{\N}$
for any $\Phi \in \nchset{\N}{\N} .$
Any normal channel $\Gamma$ is randomization-equivalent to a minimal sufficient
channel and such a minimal sufficient channels is unique up to normal isomorphism
between outcome algebras.
It is immediate from the definition that any injective normal channel is minimal sufficient
and hence so is $\Lambda_\M .$
By following the construction of the minimal sufficient channel equivalent to a given channel (Ref.~\onlinecite{kuramochi2017minimal}, Theorem~1),
we can also show that the minimal sufficient channel equivalent to a QC channel
is also QC.
Therefore $\Lambda_\M$ cannot be randomization-equivalent to a QC channel
if $\M$ is not commutative.

Finally we remark that the injectivity of $\Lambda_\M$ still holds when
$\Psi$ is generalized to
$\Psi (A) (\alpha)= \braket{\psi_{f(\alpha)} | A \psi_{f(\alpha)}} ,$
where $f : \cmplx \to \cmplx$ is a non-degenerate real affine map.
In specific, if $f (\alpha) = c \overline{\alpha}$ for some positive constant $c ,$
the EB channel $\gbarg \circ \Psi$ corresponds to the conjugate channel of the ideal quantum linear amplification channel
(Ref.~\onlinecite{kuramochi2018directed}, Eq.~(7)).

\section{Concluding remark} \label{sec:conclusion}
In this paper we have investigated the EB condition of channels
in the infinite-dimensional general operator algebraic framework
and found equivalent characterizations in Theorem~\ref{theo:main},
generalizing known results in finite dimensions.
Among the conditions, the infinite-self-compatibility condition involves
the infinite \cstar-tensor product of operator algebras and
is intrinsically infinite-dimensional.
We have also shown the Dedekind-closedness of normal EB channels
in the context of results of Ref.~\onlinecite{kuramochi2018directed}
and constructed injective normal EB channel with an arbitrary outcome
von Neumann algebra.

One of the natural generalizations of the present work will be
the EB condition for positive channels between general(ized) probabilistic theories (GPTs).~\cite{1751-8121-47-32-323001}
In an attempt to such generalization,
one new problem will be the non-uniqueness of tensor products:~\cite{namioka1969}
in the GPT framework,
the tensor product corresponding to a composite system
is not unique even in finite-dimensions,
which is not the case for operator algebraic theories.
This kind of problem is related to the definition of EB condition
and the self-compatibility conditions \eqref{it:njoint}-\eqref{it:ijoint}
in Theorem~\ref{theo:main},
while the condition~\eqref{it:rand1} can be straightforwardly generalized.

\begin{acknowledgements}
This work was supported by the National Natural Science Foundation of China
(Grants No.~11374375 and No.~11574405).
The author would like to thank Erkka Haapasalo for
helpful comments on the manuscript.
\end{acknowledgements}

config: arxiv


TITLE: Integral divisors of $a^n-b^n$ - misinterpretation
QUESTION [2 upvotes]: I am reading Birkhoff and Vandiver (1904) Integral divisors of $a^n-b^n$ and I am a bit confused.
From Fermat we know that $$x\equiv y \mod \phi(n) \Rightarrow a^x\equiv a^y \mod n$$
or
$$n\equiv 0 \mod (p-1) \Rightarrow m^n\equiv 1 \mod p$$
but on page 2, what I read seems to be something like
...$ \mathit{m^n\equiv1 \mod p}$. It now follows from the definition of p, that m appertains to n, modulo p, so that $\mathit{p - 1\equiv 0\mod n}$...
which I interpret (in thoose particular conditions) as
$$ m^n\equiv 1 \mod p\Rightarrow (p-1)\equiv 0 \mod n$$
What am I missing? Because it would mean
$$n\equiv 0 \mod (p-1) \Rightarrow (p-1)\equiv 0 \mod n$$
or $n=(p-1)$ which is not the case.
Thanks

REPLY [2 votes]: It isn't necessary that if $m^n \equiv 1 \pmod{p} \implies n \equiv 0 \pmod{p-1}$. For example, we can take $$2^3 \equiv 1 \pmod{7}$$
The smallest value $n$ can take, say $d$ is the order of $m$ modulo $p$. Here, we say that $3$ is the order of $2$ modulo $7$. It is not necessary that the order takes the value $p-1$. However, we can see that by definition of minimality of $d$, if $p-1=dq+r$ by division algorithm, then:
$$m^{p-1-dq} \equiv 1 \pmod{p} \implies m^r \equiv 1 \pmod{p} \implies r=0$$
as $0<r<d$ would contradict the minimality of $d$. That is why it follows that $p-1 \equiv 0 \pmod{d}$. In the above context, I guess that $n$ was referring to the order.


text:
\section{Omitted Details for Experiments in Section~\ref{sec:expts}}
\label{app:expts}

Now, we provide details for our experimental setup that were omitted from the main body due to space constraints.

\mypar{Dataset} Following~\citep{jain2014near}, we use the Cod-RNA dataset~\citep{codrna} which contains $59,535$ training and $271,617$ validation (used as test set) samples, each with $8$ features and a binary label.
To preprocess the data, we normalize each feature to range from $[-0.5, 0.5]$ using $f(x) = (x - \text{min}) / (\text{max} - \text{min}) - 0.5$, where $\text{min}$ and $\text{max}$ is the minimum and maximum value, respectively, of the feature in the training set. We then project each sample to the $\ell_2$-ball of radius $\sqrt{8/9}$, and append a constant feature of value $1/3$, such that each sample has $9$ dimensions and the $\ell_2$ norm is upper bounded by $1$.

To illustrate the effect of data dimensionality on accuracy, following~\citep{jain2014near} we append zero-valued features to the data samples, such that the accuracy of a non-private classifier does not change. We consider data dimensionality as $9$ (the original data) and

$\cup_{i=1}^{4}\{1,2,5\} \times 10^{i}  \setminus \{10\}$.

\mypar{Model} We use logistic regression to solve the binary classification problem, i.e., for $d$-dimensional feature $x$ and label $y \in \{-1, 1\}$, the loss function is $\ell = \log(1 + e^{-y\theta^\top x})$ for model $\theta$. The gradient of the loss function is $\nabla \ell = {-yx}/(1 + e^{y\theta^\top x})$, which has bounded $\ell_2$ norm: $\|\nabla \ell\|_2 \leq \|x\|_2 \leq 1$.

\mypar{Algorithm}
To solve this problem privately, we consider DP-SGD with mini-batch gradient and Gaussian noise. Specifically, we use batch size $250$, and iterate over the training data for $10$ epochs.

As a comparison, we consider another algorithm with random noise drawn from $\Pr(Z=z) \propto e^{-\epsilon_0 \|z\|_2}$, i.e., the direction of the noise is uniform, and the magnitude of the noise follows from Gamma distribution with shape $d$ and scale $1/\epsilon_0$.
Adding this random noise to the stochastic gradient (averaged over one batch) guarantees $\epsilon_0$-differential privacy. Thus, by privacy amplification, if one batch is formed by selecting each sample with probability $q < 0.5$, it guarantees $\epsilon = \log(1 + q(e^{\epsilon_0}-1))$-differential privacy~\citep{Ullman-lecturenotes}. By properties of R\'enyi differential privacy (RDP)~\citep{mironov2017renyi}, this converts to $(\alpha, \alpha\epsilon^2/2)$-RDP, and we can then use RDP composition to account privacy for multiple iterations.

\mypar{Privacy parameters and hyperparameter}
We consider $\epsilon \approx 5.0$ and $\delta=10^{-5}$, which, under batch size $250$ and number of epochs $10$, can be achieved by setting the standard deviation of the Gaussian noise to be $\sigma=0.63$, and the scale parameter of the Gamma noise to be $0.57$.

The only hyperparameter in the experiment is the learning rate of DP-SGD. We search in the grid

$\cup_{i=-1}^1\{1, 2, 5\} \times 10^{i}$.
We run with every learning rate once, and pick the one with the highest averaged test accuracy over the last $5$ epochs. None of the chosen learning rate lies on the boundary of the grid.
Finally, we repeat each experiment for $5$ times with the chosen learning rate.