Unfold definitions of \(\overline{{\mathbb D}}_R\) and \({\mathbb D}_1\). Calculate \(|z|\le R{\lt}1\).

Unfold definition of \(\mathcal{K}_f(R)\).

Unfold definition of \(\mathcal{K}_f(R)\).

Apply Lemmas 99, 241, 243 with \(D=\overline{{\mathbb D}}_R\) and \(Z = \mathcal{K}_f(R)\).

Apply Lemmas 245 and 239.

Apply Lemmas 246 and 242.

Apply Lemmas 247 and 244.

Contrapositive of Lemma 248.

Let \(\rho \) be an arbitrary element of \(\mathcal{K}_f(R_1)\). By the definition of \(\mathcal{K}_f(R_1)\) (see definition 240), any element \(\rho \in \mathcal{K}_f(R_1)\) is a zero of \(f\), which means \(f(\rho )=0\). The function \(f\) is assumed to be ‘AnalyticOnNhd‘ on \(\overline{{\mathbb D}}_1\). This implies that for any point \(w \in \overline{{\mathbb D}}_1\), there exists an open neighborhood of \(w\) where \(f\) is analytic. Since \(\rho \in \mathcal{K}_f(R_1) \subset \overline{{\mathbb D}}_{R_1} \subset \overline{{\mathbb D}}_1\), \(f\) is analytic in a neighborhood of \(\rho \). We are given that \(f(0) \neq 0\). This implies that the function \(f\) is not identically zero on any open connected set containing the origin. Since \(f\) is analytic on a connected open neighborhood of \(\overline{{\mathbb D}}_1\), if \(f\) were identically zero on any open subset of its domain, it would have to be identically zero on the entire connected component, which would contradict \(f(0) \neq 0\). Therefore, \(f\) is not identically zero in any neighborhood of \(\rho \) (this is the consequence of lemma 282). The quantity \(m_{\rho ,f}\) is defined as the analytic order of \(f\) at \(\rho \). For a function that is analytic at a point \(\rho \) but not identically zero in a neighborhood of \(\rho \), the order of a zero at \(\rho \) is a well-defined non-negative integer. Specifically, the order is the smallest integer \(n \ge 0\) such that the \(n\)-th derivative \(f^{(n)}(\rho )\) is non-zero. Since \(f\) is not identically zero around \(\rho \), not all derivatives can be zero. Thus, \(m_{\rho ,f}\) must be a non-negative integer, i.e., \(m_{\rho ,f} \in {\mathbb N}= \{ 0, 1, 2, \dots \} \).

Let \(\rho \) be an arbitrary element of \(\mathcal{K}_f(R_1)\). From lemma 251, we have established that \(m_{\rho ,f}\) is a non-negative integer. The analytic order of a function \(f\) at a point \(\rho \), \(m_{\rho ,f}\), is equal to 0 if and only if \(f(\rho ) \neq 0\). By the definition of the set of zeros \(\mathcal{K}_f(R_1)\) (see lemma 280), for any \(\rho \in \mathcal{K}_f(R_1)\), we have \(f(\rho ) = 0\). Since \(f(\rho ) = 0\), the order \(m_{\rho ,f}\) cannot be 0. Given that \(m_{\rho ,f}\) is a non-negative integer, it must be strictly greater than 0. Therefore, \(m_{\rho ,f} \ge 1\) for all \(\rho \in \mathcal{K}_f(R_1)\).

We are given that the functions \(h\) and \(g\) are analytic at \(w\). This means they are complex differentiable in a neighborhood of \(w\). We are also given the crucial assumption that \(g(w) \neq 0\). Since \(g\) is analytic at \(w\), it is also continuous at \(w\). By the definition of continuity, for any \(\epsilon {\gt} 0\), there exists a \(\delta {\gt} 0\) such that if \(|z-w| {\lt} \delta \), then \(|g(z)-g(w)| {\lt} \epsilon \). Let’s choose \(\epsilon = |g(w)|/2\). Since \(g(w) \neq 0\), \(\epsilon {\gt} 0\). Then there exists a neighborhood of \(w\), say \(U = D(w, \delta )\), such that for all \(z \in U\), \(|g(z)-g(w)| {\lt} |g(w)|/2\). This implies \(g(z) \neq 0\) for all \(z \in U\). Now consider the function \(q(z) = 1/g(z)\) defined on the neighborhood \(U\). The function \(z \mapsto 1/z\) is analytic on \({\mathbb C}\setminus \{ 0\} \). Since \(g\) is analytic at \(w\) and its image \(g(z)\) for \(z \in U\) is contained in \({\mathbb C}\setminus \{ 0\} \), the composition \(1/g\) is analytic at \(w\). The function we are interested in is \(h(z)/g(z)\), which can be written as the product of two functions: \(h(z)\) and \(q(z) = 1/g(z)\). The product of two functions that are analytic at a point \(w\) is also analytic at \(w\). Since both \(h(z)\) and \(1/g(z)\) are analytic at \(w\), their product \(h(z)/g(z)\) is also analytic at \(w\).

Let \(w\) be an arbitrary point in \({\mathbb C}\setminus S\). First, we show that \(P(z)\) is analytic at \(w\). For each \(s \in S\), consider the factor \(f_s(z) = (z-s)^{n_s}\). This is a polynomial in \(z\), and all polynomials are analytic on the entire complex plane \({\mathbb C}\). Therefore, each function \(f_s(z)\) is analytic at \(w\). The function \(P(z)\) is defined as the product of the functions \(f_s(z)\) for all \(s\) in the finite set \(S\). A finite product of functions that are analytic at a point \(w\) is itself analytic at \(w\). Therefore, \(P(z)\) is analytic at \(w\).

Next, we show that \(P(w) \neq 0\). The value of the function at \(w\) is given by \(P(w) = \prod _{s \in S} (w-s)^{n_s}\). A product of complex numbers is zero if and only if at least one of the factors is zero. Let’s examine an arbitrary factor \((w-s)^{n_s}\) for some \(s \in S\). We are given the assumption that \(w \notin S\). This means that for any \(s \in S\), we have \(w \neq s\), which implies \(w-s \neq 0\). Since \(n_s\) is a positive integer, \((w-s)^{n_s}\) is also non-zero. As this holds for every \(s \in S\), none of the factors in the product \(P(w)\) are zero. Therefore, the product \(P(w)\) is not zero.

Let \(F(z) = \frac{h(z)}{\prod _{s \in S} (z-s)^{n_s}}\). We want to show that \(F(z)\) is analytic at an arbitrary point \(w \in \overline{{\mathbb D}}_1 \setminus S\). Let’s define the denominator as \(g(z) = \prod _{s \in S} (z-s)^{n_s}\). Then \(F(z) = h(z)/g(z)\). We will use lemma 253. To do so, we must verify its hypotheses for the point \(w\): 1. \(h(z)\) is analytic at \(w\). This is given as an assumption in the lemma statement. 2. \(g(z)\) is analytic at \(w\). 3. \(g(w) \neq 0\).

We can verify the second and third hypotheses using lemma 254. The function \(g(z)\) has the precise form required by lemma 254, with the set of roots being \(S\) and the exponents being \(n_s\). The assumptions of lemma 254 are: a. \(S\) is a finite set. This is given in the current lemma’s assumptions. b. For each \(s \in S\), \(n_s\) is a positive integer. This is also given. c. The point of evaluation \(w\) is not in \(S\). Our assumption is \(w \in \overline{{\mathbb D}}_1 \setminus S\), which explicitly states \(w \notin S\).

Since all assumptions of lemma 254 are met, we can conclude that the function \(g(z)\) is analytic at \(w\) and that \(g(w) \neq 0\). Now we have verified all three hypotheses for lemma 253. Therefore, we can conclude that the ratio \(F(z) = h(z)/g(z)\) is analytic at \(w\).

Let \(\sigma \) be an arbitrary zero in \(\mathcal{K}_f(R_1)\). By assumption, \(f\) is ‘AnalyticOnNhd‘ \(\overline{{\mathbb D}}_1\). This means there is an open neighborhood \(U\) of \(\sigma \) where \(f\) is analytic. On this neighborhood, \(f\) can be represented by its Taylor series centered at \(\sigma \): \(f(z) = \sum _{n=0}^\infty a_n (z-\sigma )^n\), where \(a_n = \frac{f^{(n)}(\sigma )}{n!}\). Let \(m = m_{\sigma ,f}\). By definition 250, \(m\) is the analytic order of \(f\) at \(\sigma \). By definition of analytic order, this means that \(m\) is the smallest non-negative integer such that \(f^{(m)}(\sigma ) \neq 0\). Since \(\sigma \in \mathcal{K}_f(R_1)\), we have \(f(\sigma )=0\). This implies that \(m \ge 1\). The definition of order \(m\) implies that \(f^{(k)}(\sigma ) = 0\) for all integers \(0 \le k {\lt} m\), and \(f^{(m)}(\sigma ) \neq 0\). Consequently, the Taylor coefficients \(a_k = f^{(k)}(\sigma )/k!\) are zero for \(k {\lt} m\), and \(a_m = f^{(m)}(\sigma )/m! \neq 0\). The Taylor series for \(f(z)\) can thus be written as: \(f(z) = a_m(z-\sigma )^m + a_{m+1}(z-\sigma )^{m+1} + a_{m+2}(z-\sigma )^{m+2} + \dots \) We can factor out the term \((z-\sigma )^m\) from the series: \(f(z) = (z-\sigma )^m \left( a_m + a_{m+1}(z-\sigma ) + a_{m+2}(z-\sigma )^2 + \dots \right)\). This holds for all \(z\) in the disk of convergence of the Taylor series, which is a neighborhood of \(\sigma \). Let us define the function \(h_\sigma (z)\) as the series in the parenthesis: \(h_\sigma (z) = \sum _{j=0}^\infty a_{m+j} (z-\sigma )^j\). A power series defines an analytic function within its radius of convergence. This series for \(h_\sigma (z)\) has the same radius of convergence as the series for \(f(z)\), so \(h_\sigma (z)\) is analytic in a neighborhood of \(\sigma \), i.e., it is ‘AnalyticAt‘ \(\sigma \). By our construction, the identity \(f(z) = (z-\sigma )^m h_\sigma (z)\) holds in this neighborhood. Finally, we must verify that \(h_\sigma (\sigma ) \neq 0\). We evaluate \(h_\sigma (z)\) at \(z=\sigma \): \(h_\sigma (\sigma ) = a_m + a_{m+1}(\sigma -\sigma ) + a_{m+2}(\sigma -\sigma )^2 + \dots = a_m\). As we established that \(a_m \neq 0\), we have \(h_\sigma (\sigma ) \neq 0\). This completes the proof.

Let \(z\) be an arbitrary point in the set \(\overline{{\mathbb D}}_R \setminus \mathcal{K}_f(R_1)\). By the definition of this set, \(z \notin \mathcal{K}_f(R_1)\). According to definition 257, for such a point \(z\), the function \(C_f(z)\) is defined by the first case: \(C_f(z) = \frac{f(z)}{\prod _{\rho \in \mathcal{K}_f(R_1)}(z-\rho )^{m_{\rho ,f}}}\). We can prove this function is analytic at \(z\) by applying lemma 255. Let’s verify its hypotheses:

• Let \(h(z) = f(z)\), \(S = \mathcal{K}_f(R_1)\), and for each \(\rho \in S\), let \(n_\rho = m_{\rho ,f}\). The point of evaluation is \(w=z\).

• The function \(h(z)=f(z)\) is ‘AnalyticOnNhd‘ \(\overline{{\mathbb D}}_1\), so it is analytic at \(z \in \overline{{\mathbb D}}_R \subset \overline{{\mathbb D}}_1\).

• The set \(S = \mathcal{K}_f(R_1)\) is the set of zeros of a non-zero analytic function in a compact set \(\overline{{\mathbb D}}_{R_1}\), and is therefore a finite set, as stated by lemma 249.

• For each \(\rho \in S\), the exponent \(n_\rho = m_{\rho ,f}\) is a positive integer by lemma 252.

• The point of evaluation \(w=z\) is in \(\overline{{\mathbb D}}_R \setminus S\), which is a subset of \(\overline{{\mathbb D}}_1 \setminus S\).

All hypotheses of lemma 255 are satisfied. Therefore, we conclude that \(C_f(z)\) is analytic at \(z\). Since \(z\) was an arbitrary point in \(\overline{{\mathbb D}}_R \setminus \mathcal{K}_f(R_1)\), the statement holds for all such points.

Let \(\sigma \) be an arbitrary point in \(\mathcal{K}_f(R_1)\). We are interested in the case where \(z=\sigma \). By definition 257, when \(z = \sigma \), \(C_f(z)\) is defined by the second case: \(C_f(\sigma ) = \frac{h_\sigma (\sigma )}{\prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(\sigma -\rho )^{m_{\rho ,f}}}\). The expression we are asked to prove is \(C_f(z) = \frac{h_\sigma (z)}{\prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(z-\rho )^{m_{\rho ,f}}}\). Evaluating the right-hand side at \(z=\sigma \) gives: \(\frac{h_\sigma (\sigma )}{\prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(\sigma -\rho )^{m_{\rho ,f}}}\). This is precisely the definition of \(C_f(\sigma )\). Thus, the equality holds at \(z=\sigma \). The phrase "Eventually for \(z\) in nbhds of \(\sigma \)" is satisfied trivially, as the statement only concerns the point \(z=\sigma \) itself and holds true at that point regardless of the neighborhood.

The statement "Eventually for \(z\) in nbhds of \(\sigma \), we have \(z\neq \rho \)" means that there exists a neighborhood of \(\sigma \) that does not contain \(\rho \). Let \(\sigma \) and \(\rho \) be two distinct points in \(\mathcal{K}_f(R_1)\). Let \(d = |\sigma - \rho |\) be the distance between them. Since \(\sigma \neq \rho \), we have \(d {\gt} 0\). Consider the open disk \(U = D(\sigma , d)\) centered at \(\sigma \) with radius \(d\). This is a neighborhood of \(\sigma \). For any point \(z \in U\), the distance from \(z\) to \(\sigma \) is less than \(d\), i.e., \(|z - \sigma | {\lt} d\). The distance from any such \(z\) to \(\rho \) is \(|z - \rho |\). By the reverse triangle inequality, \(|z - \rho | = |(z - \sigma ) - (\rho - \sigma )| \ge ||\rho - \sigma | - |z - \sigma || = |d - |z - \sigma ||\). Since \(|z - \sigma | {\lt} d\), the value \(d - |z - \sigma |\) is positive. Thus, \(|z - \rho | {\gt} 0\), which implies \(z \neq \rho \). Therefore, the neighborhood \(U\) of \(\sigma \) does not contain the point \(\rho \). This proves the claim.

Let \(\sigma \) be an arbitrary point in \(\mathcal{K}_f(R_1)\). By lemma 249, the set \(\mathcal{K}_f(R_1)\) is finite. Let \(\mathcal{K}_f(R_1) \setminus \{ \sigma \} = \{ \rho _1, \rho _2, \dots , \rho _k\} \). For each \(\rho _i\) in this set, since \(\rho _i \neq \sigma \), by lemma 260 there exists a neighborhood \(U_i\) of \(\sigma \) such that for all \(z \in U_i\), \(z \neq \rho _i\). Let \(U = \bigcap _{i=1}^k U_i\). As a finite intersection of neighborhoods of \(\sigma \), \(U\) is also a neighborhood of \(\sigma \). For any \(z \in U\), we have \(z \neq \rho _i\) for all \(i=1, \dots , k\). Now, consider a point \(z\) in this neighborhood \(U\) such that \(z \neq \sigma \). For such a \(z\), we have \(z \notin \{ \rho _1, \dots , \rho _k\} \) and \(z \neq \sigma \), which means \(z \notin \mathcal{K}_f(R_1)\). By the first case of definition 257, for such a \(z\), we have \(C_f(z) = \frac{f(z)}{\prod _{\rho \in \mathcal{K}_f(R_1)}(z-\rho )^{m_{\rho ,f}}}\). From lemma 256, there exists a neighborhood of \(\sigma \), say \(V\), and a function \(h_\sigma (z)\) such that \(f(z) = (z-\sigma )^{m_{\sigma ,f}} h_\sigma (z)\) for all \(z \in V\). Let \(W = U \cap V\). This is also a neighborhood of \(\sigma \). For any \(z \in W\) with \(z \neq \sigma \), both of the above representations are valid. Substituting the expression for \(f(z)\) into the one for \(C_f(z)\), we get: \(C_f(z) = \frac{(z-\sigma )^{m_{\sigma ,f}} h_\sigma (z)}{\prod _{\rho \in \mathcal{K}_f(R_1)}(z-\rho )^{m_{\rho ,f}}}\). This holds for all \(z\) in the punctured neighborhood \(W \setminus \{ \sigma \} \), which satisfies the "Eventually" condition.

Let \(S = \mathcal{K}_f(R_1)\). By lemma 249, \(S\) is a finite set. Let \(\sigma \) be any element of \(S\). The set \(S\) can be partitioned into two disjoint subsets: \(\{ \sigma \} \) and \(S \setminus \{ \sigma \} \). The product over the finite set \(S\) can be split into the product of the terms corresponding to these two subsets. Let \(a_\rho (z) = (z-\rho )^{m_{\rho ,f}}\). The product over \(S\) is \(\prod _{\rho \in S} a_\rho (z)\). By the commutative property of multiplication, we can separate the term for \(\rho =\sigma \): \(\prod _{\rho \in S} a_\rho (z) = a_\sigma (z) \cdot \left( \prod _{\rho \in S \setminus \{ \sigma \} } a_\rho (z) \right)\). Substituting the definition of \(a_\rho (z)\) back into this identity gives: \(\prod _{\rho \in \mathcal{K}_f(R_1)}(z-\rho )^{m_{\rho ,f}} = (z-\sigma )^{m_{\sigma ,f}} \cdot \left( \prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(z-\rho )^{m_{\rho ,f}} \right)\). This is a fundamental property of products over finite sets.

From lemma 262, we have the identity: \(\prod _{\rho \in \mathcal{K}_f(R_1)}(z-\rho )^{m_{\rho ,f}} = (z-\sigma )^{m_{\sigma ,f}} \prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(z-\rho )^{m_{\rho ,f}}\). To manipulate this equation by division, we must ensure the terms we divide by are non-zero. The crucial assumption is that \(z \notin \mathcal{K}_f(R_1)\). This means that for every \(\rho \in \mathcal{K}_f(R_1)\), we have \(z \neq \rho \), and therefore \(z-\rho \neq 0\). Since \(m_{\rho ,f} \ge 1\), it follows that \((z-\rho )^{m_{\rho ,f}} \neq 0\) for all \(\rho \in \mathcal{K}_f(R_1)\). This implies that all factors in the products are non-zero. In particular, the denominator on the left-hand side, \(\prod _{\rho \in \mathcal{K}_f(R_1)}(z-\rho )^{m_{\rho ,f}}\), is non-zero. Also, the term \((z-\sigma )^{m_{\sigma ,f}}\) is non-zero. We can therefore divide both sides of the identity from lemma 262 by the non-zero quantity \((z-\sigma )^{m_{\sigma ,f}} \cdot \left(\prod _{\rho \in \mathcal{K}_f(R_1)}(z-\rho )^{m_{\rho ,f}}\right)\). Starting with the identity and dividing by \(\prod _{\rho \in \mathcal{K}_f(R_1)}(z-\rho )^{m_{\rho ,f}}\) gives: \(1 = \frac{(z-\sigma )^{m_{\sigma ,f}} \prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(z-\rho )^{m_{\rho ,f}}}{\prod _{\rho \in \mathcal{K}_f(R_1)}(z-\rho )^{m_{\rho ,f}}}\). Now, dividing by the non-zero term \(\prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(z-\rho )^{m_{\rho ,f}}\) yields the desired result: \(\frac{1}{\prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(z-\rho )^{m_{\rho ,f}}} = \frac{(z-\sigma )^{m_{\sigma ,f}}}{\prod _{\rho \in \mathcal{K}_f(R_1)}(z-\rho )^{m_{\rho ,f}}}\).

By lemma 261, there exists a neighborhood \(W\) of \(\sigma \) such that for all \(z \in W\) with \(z \neq \sigma \), we have the identity: \(C_f(z) = \frac{(z-\sigma )^{m_{\sigma ,f}} h_\sigma (z)}{\prod _{\rho \in \mathcal{K}_f(R_1)}(z-\rho )^{m_{\rho ,f}}}\). We can rewrite the right-hand side as a product: \(C_f(z) = h_\sigma (z) \cdot \left( \frac{(z-\sigma )^{m_{\sigma ,f}}}{\prod _{\rho \in \mathcal{K}_f(R_1)}(z-\rho )^{m_{\rho ,f}}} \right)\). For a point \(z \in W\) with \(z \neq \sigma \), we established in the proof of lemma 261 that \(z \notin \mathcal{K}_f(R_1)\). Therefore, the conditions for lemma 263 are met for such a point \(z\). Applying this lemma, we can replace the fractional part: \(\frac{(z-\sigma )^{m_{\sigma ,f}}}{\prod _{\rho \in \mathcal{K}_f(R_1)}(z-\rho )^{m_{\rho ,f}}} = \frac{1}{\prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(z-\rho )^{m_{\rho ,f}}}\). Substituting this back into the expression for \(C_f(z)\) gives: \(C_f(z) = h_\sigma (z) \cdot \frac{1}{\prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(z-\rho )^{m_{\rho ,f}}} = \frac{h_\sigma (z)}{\prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(z-\rho )^{m_{\rho ,f}}}\). This equality holds for all \(z \in W \setminus \{ \sigma \} \), which satisfies the "Eventually" condition.

Let \(\sigma \) be an arbitrary point in \(\mathcal{K}_f(R_1)\). Let us define the function \(g_\sigma (z) = \frac{h_\sigma (z)}{\prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(z-\rho )^{m_{\rho ,f}}}\). From lemma 264, we know there exists a neighborhood of \(\sigma \), let’s call it \(W\), such that for all \(z \in W \setminus \{ \sigma \} \), the equality \(C_f(z) = g_\sigma (z)\) holds. From lemma 259, we know that at the point \(z=\sigma \), the equality \(C_f(\sigma ) = g_\sigma (\sigma )\) also holds. Combining these two results, we see that \(C_f(z) = g_\sigma (z)\) for all points \(z\) in the neighborhood \(W\). This proves the statement.

Let \(\sigma \) be an arbitrary point in \(\mathcal{K}_f(R_1)\). We want to prove that the function \(g_\sigma (z) = \frac{h_\sigma (z)}{\prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(z-\rho )^{m_{\rho ,f}}}\) is analytic at \(\sigma \). We will use lemma 255 with the point of evaluation \(w=\sigma \). Let’s identify the components and verify the hypotheses:

• The numerator function is \(h(z) = h_\sigma (z)\).

• The set of roots in the denominator is \(S = \mathcal{K}_f(R_1) \setminus \{ \sigma \} \).

• The exponents are \(n_\rho = m_{\rho ,f}\) for each \(\rho \in S\).

Now we check the conditions of lemma 255:

1. \(h(z)\) must be analytic at \(\sigma \). By lemma 256, the function \(h_\sigma (z)\) is analytic at \(\sigma \). This condition is met.

2. \(S\) must be a finite set. Since \(\mathcal{K}_f(R_1)\) is finite (by lemma 249), its subset \(S\) is also finite. This condition is met.

3. For each \(\rho \in S\), \(n_\rho \) must be a positive integer. For \(\rho \in S\), \(n_\rho = m_{\rho ,f}\). By lemma 252, \(m_{\rho ,f} \ge 1\). This condition is met.

4. The point of evaluation \(\sigma \) must not be in \(S\). By definition, \(S = \mathcal{K}_f(R_1) \setminus \{ \sigma \} \), so \(\sigma \notin S\). This condition is met.

Since all hypotheses of lemma 255 are satisfied, we can conclude that the function \(g_\sigma (z)\) is analytic at \(\sigma \).

Let \(\sigma \) be an arbitrary point in \(\mathcal{K}_f(R_1)\). By lemma 265, there exists a neighborhood of \(\sigma \), say \(W\), such that for all \(z \in W\), \(C_f(z)\) is equal to the function \(g_\sigma (z) = \frac{h_\sigma (z)}{\prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(z-\rho )^{m_{\rho ,f}}}\). By lemma 266, the function \(g_\sigma (z)\) is analytic at \(\sigma \). A function is defined to be analytic at a point \(\sigma \) if it is equal to a function known to be analytic at \(\sigma \) in a neighborhood of \(\sigma \). Since \(C_f(z) = g_\sigma (z)\) on the neighborhood \(W\) and \(g_\sigma (z)\) is analytic at \(\sigma \), it follows directly that \(C_f(z)\) is also analytic at \(\sigma \). As \(\sigma \) was an arbitrary element of \(\mathcal{K}_f(R_1)\), this holds for all points in that set.

Let \(z\) be an arbitrary point in the closed disk \(\overline{{\mathbb D}}_R\). We must show that \(C_f\) is analytic at \(z\). We can partition the domain \(\overline{{\mathbb D}}_R\) into two disjoint sets: those points that are in \(\mathcal{K}_f(R_1)\) and those that are not. Note that \(\mathcal{K}_f(R_1) \subset \overline{{\mathbb D}}_{R_1} \subset \overline{{\mathbb D}}_R\). Case 1: The point \(z\) is not in \(\mathcal{K}_f(R_1)\). In this case, \(z \in \overline{{\mathbb D}}_R \setminus \mathcal{K}_f(R_1)\). By lemma 258, the function \(C_f\) is analytic at \(z\). Case 2: The point \(z\) is in \(\mathcal{K}_f(R_1)\). In this case, let’s call the point \(\sigma = z\). By lemma 267, the function \(C_f\) is analytic at \(\sigma \). Since any point \(z \in \overline{{\mathbb D}}_R\) must fall into one of these two cases, and we have shown that \(C_f\) is analytic at \(z\) in both cases, we conclude that \(C_f(z)\) is analytic for all \(z \in \overline{{\mathbb D}}_R\).

We prove this by contraposition. The contrapositive statement is: if \(z \in \overline{{\mathbb D}}_{R_1}\) and \(f(z)=0\), then \(z \in \mathcal{K}_f(R_1)\). Let \(z\) be a point in \(\overline{{\mathbb D}}_{R_1}\) such that \(f(z)=0\). The set \(\mathcal{K}_f(R_1)\) is defined (in definition 240) as the set of all points \(w\) in the closed disk \(\overline{{\mathbb D}}_{R_1}\) for which \(f(w)=0\). Since \(z \in \overline{{\mathbb D}}_{R_1}\) and \(f(z)=0\), \(z\) satisfies the condition for membership in \(\mathcal{K}_f(R_1)\). Therefore, \(z \in \mathcal{K}_f(R_1)\). This proves the contrapositive, and thus the original statement is true.

Let \(z\) be an arbitrary point in the set \(\overline{{\mathbb D}}_{R_1} \setminus \mathcal{K}_f(R_1)\). By definition, \(z \notin \mathcal{K}_f(R_1)\). According to the first case of definition 257, \(C_f(z)\) is given by the ratio: \(C_f(z) = \frac{f(z)}{\prod _{\rho \in \mathcal{K}_f(R_1)}(z-\rho )^{m_{\rho ,f}}}\). A fraction is non-zero if and only if its numerator is non-zero and its denominator is finite and non-zero. Numerator: The numerator is \(f(z)\). Since \(z \in \overline{{\mathbb D}}_{R_1} \setminus \mathcal{K}_f(R_1)\), by lemma 269, we have \(f(z) \neq 0\). Denominator: The denominator is the product \(P(z) = \prod _{\rho \in \mathcal{K}_f(R_1)}(z-\rho )^{m_{\rho ,f}}\). Since \(\mathcal{K}_f(R_1)\) is finite, this is a finite product. For the product to be non-zero, each of its factors must be non-zero. A factor is of the form \((z-\rho )^{m_{\rho ,f}}\). Since we assumed \(z \notin \mathcal{K}_f(R_1)\), we have \(z \neq \rho \) for all \(\rho \in \mathcal{K}_f(R_1)\). This means \(z-\rho \neq 0\). As \(m_{\rho ,f} \ge 1\), it follows that \((z-\rho )^{m_{\rho ,f}} \neq 0\). Since every factor is non-zero, the denominator is non-zero. Since the numerator is non-zero and the denominator is non-zero, their ratio \(C_f(z)\) must be non-zero.

Let \(\sigma \) be an arbitrary point in \(\mathcal{K}_f(R_1)\). By the second case of definition 257, the value of \(C_f\) at \(\sigma \) is given by: \(C_f(\sigma ) = \frac{h_\sigma (\sigma )}{\prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(\sigma -\rho )^{m_{\rho ,f}}}\). We must show this expression is non-zero. Numerator: The numerator is \(h_\sigma (\sigma )\). By lemma 256, the function \(h_\sigma \) is constructed specifically to satisfy \(h_\sigma (\sigma ) \neq 0\). Denominator: The denominator is the product \(\prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(\sigma -\rho )^{m_{\rho ,f}}\). This is a finite product. For any \(\rho \) in the indexing set \(\mathcal{K}_f(R_1) \setminus \{ \sigma \} \), we have \(\rho \neq \sigma \), which implies \(\sigma -\rho \neq 0\). Since \(m_{\rho ,f} \ge 1\), the factor \((\sigma -\rho )^{m_{\rho ,f}}\) is also non-zero. As a finite product of non-zero terms, the denominator is non-zero. Since the numerator is non-zero and the denominator is non-zero, their ratio \(C_f(\sigma )\) is non-zero.

Let \(z\) be an arbitrary point in the closed disk \(\overline{{\mathbb D}}_{R_1}\). We partition the domain \(\overline{{\mathbb D}}_{R_1}\) into two disjoint sets: \(\mathcal{K}_f(R_1)\) and \(\overline{{\mathbb D}}_{R_1} \setminus \mathcal{K}_f(R_1)\). Any point \(z \in \overline{{\mathbb D}}_{R_1}\) must belong to exactly one of these sets. Case 1: \(z \in \overline{{\mathbb D}}_{R_1} \setminus \mathcal{K}_f(R_1)\). By lemma 270, we have \(C_f(z) \neq 0\). Case 2: \(z \in \mathcal{K}_f(R_1)\). By lemma 271, we have \(C_f(z) \neq 0\). In both possible cases, \(C_f(z)\) is non-zero. Therefore, we conclude that \(C_f(z) \neq 0\) for all \(z \in \overline{{\mathbb D}}_{R_1}\).

By lemma 354. Note \(\mathcal K_f(R_1)\) is finite by lemma 249

By lemma 354. Note \(\mathcal K_f(R_1)\) is finite by lemma 249

By ??

By Mathlib: Finset.prod_div_distrib Note \(\mathcal K_f(R_1)\) is finite by lemma 249.

By lemma 277 and Mathlib: div_pow Note \(m_{\rho ,f}\in {\mathbb N}\). Note \(\mathcal K_f(R_1)\) is finite by lemma 249.

By lemma 276 and ??

Unfold definition 240.

Contrapositive of lemma 280

By definition of the identically zero function.

By definition 240, as \(\mathcal{K}_f(R_1)\) is a subset of \(\overline{{\mathbb D}}_{R_1}\).

By lemma 281.

By lemma 284, as \(\rho \) is an element of \(\mathcal{K}_f(R_1)\).

Shown in lemma 35

By lemma 285 and lemma 286.

By definition 240, as \(\mathcal{K}_f(R_1)\) is a subset of \(\overline{{\mathbb D}}_{R_1}\).

By lemma 287, lemma 288, and lemma 289.

By lemma 290 and lemma 291, using the hypothesis \(R{\gt}0\).

By lemma 279 and lemma 293 with \(I=\mathcal K_f(R_1)\) and \(w_\rho = (\frac{R-z\bar\rho /R}{z-\rho })^{m_\rho }\).

By lemma 295 with \(n=m_\rho \) and \(w=\frac{R-z\bar\rho /R}{z-\rho }\).

By ??.

By evaluating the expression in lemma 294 at \(z=0\).

By ?? with \(w_1=R\) and \(\rho \).

By applying ?? to the expression in lemma 298.

By applying lemma 303 with \(x=R{\gt}0\) to the expression in lemma 302.

Apply lemma 306, and then assumption \(1 \le c\).

By lemma 305 \(c_{\rho } \le c_{\rho }^{n_\rho }\). Then apply lemma 306 with \(a_{\rho }=c_{\rho }\), \(b_{\rho }=c_{\rho }^{n_\rho }\).

By ??.

First \(m_\rho \in {\mathbb N}\) and \(m_\rho \ge 1\) by ??. Also \(\mathcal K_f(R_1)\) is finite by lemma 249. Now apply lemma 310 with \(K=\mathcal K_f(R_1)\), \(b_\rho =3/2\), and \(n=m_\rho \).

By lemma 268.

By lemma 313 and the hypothesis \(|f(z)| \le B\).

By applying lemma 110 with \(h(z)=B_f(z)\).

By lemma 312 and lemma 315.

By lemma 314 and lemma 316.

By evaluating the inequality in lemma 317 at \(z=0\).

By lemma 318 and lemma 319.

By applying lemma 321 to the inequality in lemma 320.

Note \(\log (R/R_1){\gt}0\) since \(R/R_1{\gt}1\). By lemma 322, and then divide both sides by \(\log (R/R_1)\).

\(\mathcal K_f(R_1)\) is finite by lemma 249. Now apply ?? with \(K=\mathcal K_f(R_1)\), \(a_\rho =1\), and \(b_{\rho }=m_\rho \).

By ??.

\(\mathcal K_f(R_1)\) is finite by lemma 249. Now apply ?? with \(S=\mathcal K_f(R_1)\)

By ??

By ??

By lemma 332 with \(z=0\).

By ??.

By ??.

By ?? and lemma 237

By lemma 321 with \(x=|B_f(z)|\) and \(y=B\).

By ??.

By ??.

By lemma 321 with \(x=1\) and \(y=|B_f(0)|\), giving \(\log |B_f(0)| \ge \log (1)=0\).

By ??.

By theorem 198.

By lemma 342 with \(r:=r\), \(r_1:= r_1\), \(L(z)=L_f(z)\) and \(M=\log B\), using ??.

Mathlib: logDeriv_const_mul

By lemma 331 and lemma 333

By ?? with \(g(z)=B_f(z)\) and \(a=1/B_f(0)\).

Mathlib: logDeriv_mul

Mathlib: logDeriv_prod

Mathlib: logDeriv_div

Mathlib: logDeriv_fun_pow

By definition \(z \notin \mathcal{K}_f(R_1)\) and \(\rho \in \mathcal{K}_f(R_1)\). This implies that \(z \neq \rho \), and therefore \(z-\rho \neq 0\). The function \(z\mapsto z-\rho \) is a linear function, therefore differentiableAt \(z\).

\(R-\bar\rho z/R \neq 0\) for all \(z\in \overline{D}_R \setminus \mathcal{K}_f(R_1)\).

The function \(R-\bar\rho z/R\) is a linear function, therefore differentiableAt \(z\).

By ??

By lemma 353. Note \(m_{\rho ,f}\in {\mathbb N}\).

By lemma 354. Note \(\mathcal K_f(R_1)\) is finite by lemma 249

By definition of \(\mathcal{K}_f(R_1)\) in definition 240.

By ??, recalling definition 275.

By lemma 347 with \(g(z)=\prod _{\rho \in \mathcal K_f(R_1)}\left(\frac{R-z\bar\rho /R}{z-\rho }\right)^{m_{\rho ,f}}\).

Note diffAt, nonzero conditions hold by lemma 355.

By ??.

By definition of logDeriv in Mathlib.

By lemma 346, lemma 359, and lemma 360.

By lemma 348 with \(K=\mathcal K_f(R_1)\) and \(g_\rho (z) = \left(\frac{R-z\bar\rho /R}{z-\rho }\right)^{m_{\rho ,f}}\).

Note \(K=\mathcal K_f(R_1)\) is finite by lemma 249. The diffAt, nonzero conditions hold by lemma 354.

By lemma 350 with \(m=m_{\rho ,f}\) and \(g(z) = \frac{R-z\bar\rho /R}{z-\rho }\). Note \(m_{\rho ,f}\in {\mathbb N}\). The diffAt, nonzero conditions hold by lemma 353.

By lemma 362 and lemma 363.

By lemma 361 and lemma 364.

By lemma 349 with \(h(z)=R-z\bar\rho /R\) and \(g(z)=z-\rho \).

Note diffAt, nonzero conditions hold by ??.

Note linear polynomial has derivative \((az+b)'=a\).

Now unfold logDeriv definition and calculate \(\text{logDeriv}(az+b) = \frac{(az+b)'}{az+b} =\frac{a}{az+b}\).

By lemma 367 with \(a=1\) and \(b=-\rho \).

By lemma 367 with \(a=-\bar\rho /R\) and \(b=R\).

This is an algebraic simplification. For the expression to be well-defined, we must make some assumptions that are implicit in the context of the larger proof:

• \(R \neq 0\) and \(\bar\rho \neq 0\) (which implies \(\rho \neq 0\)), so that the fractions are defined.

• The denominator \(R-z\bar\rho /R \neq 0\).

• The denominator \(z-R^2/\bar\rho \neq 0\).

These conditions hold in the domains where this lemma is applied.

Our goal is to show the equality of the two fractions. We will start with the left-hand side (LHS) and manipulate it to obtain the right-hand side (RHS). The strategy is to multiply the numerator and the denominator of the LHS by the same non-zero quantity, chosen to simplify the expression. A suitable choice is the factor \(-R/\bar\rho \).

Let’s start with the LHS:

Now, we multiply the numerator and the denominator by \(-R/\bar\rho \):

Let’s simplify the new numerator and denominator separately.

Numerator simplification:

Denominator simplification: We distribute the factor \((-R/\bar\rho )\) across the terms in the denominator:

Conclusion: Substituting the simplified numerator and denominator back into the fraction, we get:

This is exactly the RHS of the equation we wanted to prove.

By ??

The proof proceeds by first applying the division rule for the logarithmic derivative and then evaluating each resulting term. This is valid for any \(z \in \overline{{\mathbb D}}_{R_1} \setminus \mathcal{K}_f(R_1)\) and any \(\rho \in \mathcal{K}_f(R_1)\).

Step 1: Apply the division rule for logDeriv We use lemma 366, which is an application of the general rule \(\text{logDeriv}(h/g) = \text{logDeriv}(h) - \text{logDeriv}(g)\). Let \(h(z) = R-z\bar\rho /R\) and \(g(z) = z-\rho \). To apply this rule, we must ensure that \(h(z)\) and \(g(z)\) are differentiable and non-zero at \(z\).

• For \(h(z) = R-z\bar\rho /R\): Lemma 352 confirms that this function is differentiable and non-zero for all \(z \in \overline{{\mathbb D}}_1\), which includes our domain of interest.

• For \(g(z) = z-\rho \): Lemma 351 confirms that this function is differentiable and non-zero for all \(z \in \overline{{\mathbb D}}_{R_1} \setminus \mathcal{K}_f(R_1)\), given \(\rho \in \mathcal{K}_f(R_1)\).

Since the conditions are met, we can apply lemma 366 to get:

Step 2: Evaluate the first term, \(\text{logDeriv}(R-z\bar\rho /R)\) We use lemma 371. This lemma states:

This is valid provided \(R \neq 0\) and \(\rho \neq 0\), which are true under our assumptions (\(0{\lt}R{\lt}1\) and \(\rho \in \mathcal{K}_f(R_1)\) implies \(\rho \neq 0\) as \(f(0)=1\)).

Step 3: Evaluate the second term, \(\text{logDeriv}(z-\rho )\) We use lemma 368. This lemma states:

This is valid for \(z \neq \rho \). This condition is satisfied, as our domain for \(z\) is \(\overline{{\mathbb D}}_{R_1} \setminus \mathcal{K}_f(R_1)\) and \(\rho \) is an element of \(\mathcal{K}_f(R_1)\), so \(z\) cannot be equal to \(\rho \).

Step 4: Substitute the results back Now we substitute the expressions found in Step 2 and Step 3 into the equation from Step 1:

This gives the final desired formula.

The proof is a direct substitution into a previously established formula. The assumptions on \(R\) and \(f\) are used to justify the application of the necessary lemmas. The result holds for all \(z \in \overline{{\mathbb D}}_{R_1} \setminus \mathcal{K}_f(R_1)\).

Step 1: Recall the formula for \(L'_f(z)\) from lemma 365 Lemma 365 provides an expression for \(L'_f(z)\) under the same assumptions as the current lemma. The formula is:

This equation holds for all \(z \in \overline{{\mathbb D}}_{R_1} \setminus \mathcal{K}_f(R_1)\).

Step 2: Find a replacement for the \(\text{logDeriv}\) term Our goal is to replace the term \(\text{logDeriv}\left(\frac{R-z\bar\rho /R}{z-\rho }\right)\) inside the summation. We look to lemma 372. This lemma gives the following identity for each \(\rho \in \mathcal{K}_f(R_1)\) and for all \(z \in \overline{{\mathbb D}}_{R_1} \setminus \mathcal{K}_f(R_1)\):

Step 3: Substitute the expression into the formula for \(L'_f(z)\) We now substitute the expression from Step 2 into the formula from Step 1. The substitution is valid because the domains for \(z\) and \(\rho \) match in both lemmas. Starting with the formula from Step 1:

We replace the parenthesized term with its equivalent from Step 2:

This is the final expression we aimed to prove.

By the distributive property of summation.

By lemma 374. Note \(K=\mathcal K_f(R_1)\) is finite by lemma 249

By lemma 373 and lemma 375.

By algebraic rearrangement of the equality in lemma 376.

By the triangle inequality.

By applying the modulus and lemma 378 to the equality in lemma 377.

Note \(K=\mathcal K_f(R_1)\) is finite by lemma 249.

By lemma 380, and lemma 324.

By lemma 379, lemma 381, and lemma 343.

By lemma 382, factoring out \(\log B\) from both terms.