AnalyticOn.norm-le-of-norm-le-on… to JBlaschke

LemmaAnalyticOn.norm-le-of-norm-le-on-sphere#

An application of the Maximum modulus principle.

Proof

This is standard in the literature.

Lean

Formalized as AnalyticOn.norm_le_of_norm_le_on_sphere.

Sources
LeanAnalyticOn.norm_le_of_norm_le_on_sphere
Used by 1
Used byDiskBound

TheoremborelCaratheodory'#

An application of

Complex.borelCaratheodory_zero.
Proof

This is standard in the literature.

Lean

Formalized as borelCaratheodory'.

Sources
LeanborelCaratheodory'
Used by 1
Used byDerivativeBound

This upstreamed from https://github.com/math-inc/strongpnt/tree/main

Lemmacauchy-formula-deriv#

Let \(f\) be analytic on \(|z|\leq R\). For any \(z\) with \(|z|\leq r\) and any \(r'\) with \(0 < r < r' < R\) we have

\[ f'(z)=\frac{1}{2\pi i}\oint_{|w|=r'}\frac{f(w)}{(w-z)^2}\,dw=\frac{1}{2\pi} \int_0^{2\pi}\frac{r'e^{it}\,f(r'e^{it})}{(r'e^{it}-z)^2}\,dt. \]
Proof

This is just Cauchy's integral formula for derivatives.

Lean

Formalized as cauchy_formula_deriv.

Sources
Leancauchy_formula_deriv
Used by 1
Used byDerivativeBound

LemmaDerivativeBound#

Let \(R,\,M>0\) and \(0 < r < r' < R\). Let \(f\) be analytic on \(|z|\leq R\) such that \(f(0)=0\) and suppose \(\Re f(z)\leq M\) for all \(|z|\leq R\). Then we have that

\[ |f'(z)|\leq\frac{2M(r')^2}{(R-r')(r'-r)^2} \]

for all \(|z|\leq r\).

Proof

By Lemma cauchy-formula-deriv we know that

\[ f'(z)=\frac{1}{2\pi i}\oint_{|w|=r'}\frac{f(w)}{(w-z)^2}\,dw =\frac{1}{2\pi }\int_0^{2\pi}\frac{r'e^{it}\,f(r'e^{it})}{(r'e^{it}-z)^2}\,dt. \]

Thus,

\[ |f'(z)|=\left|\frac{1}{2\pi}\int_0^{2\pi} \frac{r'e^{it}\,f(r'e^{it})}{(r'e^{it}-z)^2}\,dt\right| \leq\frac{1}{2\pi}\int_0^{2\pi} \left|\frac{r'e^{it}\,f(r'e^{it})}{(r'e^{it}-z)^2}\right|\,dt.\qquad\text{(1)} \]

Now applying Theorem borelCaratheodory', and noting that \(r'-r\leq|r'e^{it}-z|\), we have that

\[ \left|\frac{r'e^{it}\,f(r'e^{it})}{(r'e^{it}-z)^2}\right| \leq\frac{2M(r')^2}{(R-r')(r'-r)^2}. \]

Substituting this into Equation (1) and evaluating the integral completes the proof.

Lean

Formalized as DerivativeBound.

Sources
LeanDerivativeBound
Uses 2 · Used by 1
Proof usescauchy-formula-deriv · borelCaratheodory'
Used byBorelCaratheodoryDeriv

TheoremBorelCaratheodoryDeriv#

Let \(R,\,M>0\). Let \(f\) be analytic on \(|z|\leq R\) such that \(f(0)=0\) and suppose \(\Re f(z)\leq M\) for all \(|z|\leq R\). Then for any \(0 < r < R\),

\[ |f'(z)|\leq\frac{16MR^2}{(R-r)^3} \]

for all \(|z|\leq r\).

Proof

Using Lemma DerivativeBound with \(r'=(R+r)/2\), and noting that \(r < R\), we have that

\[ |f'(z)|\leq\frac{4M(R+r)^2}{(R-r)^3}\leq\frac{16MR^2}{(R-r)^3}. \]
Lean

Formalized as BorelCaratheodoryDeriv.

Sources
LeanBorelCaratheodoryDeriv
Uses 1 · Used by 1
Proof usesDerivativeBound
Used byJBlaschkeDerivBound

TheoremLogOfAnalyticFunction#

Let \(0\lt r\lt R\). Let \(B:\overline{\mathbb{D}_{R}}\to\mathbb{C}\) be analytic on neighborhoods of points in \(\overline{\mathbb{D}_{R}}\) with \(B(z)\neq 0\) for all \(z\in\overline{\mathbb{D}_{R}}\).Then there exists \(J_B:\mathbb{D}_R\to\mathbb{C}\) that is analytic on neighborhoods of points in \(\mathbb{D}_R\) such that

  • \(J_B(0)=0\)
  • \(J_B'(z)=B'(z)/B(z)\) for all \(z\in\overline{\mathbb{D}_r}\)
  • \(\log|B(z)|-\log|B(0)|=\mathfrak{R}J_B(z)\) for all \(z\in\mathbb{D}_R\).
Proof

We let \(J_B(z)=I_{B'/B}(z)\). Then clearly, \(J_B(0)=0\). Now note that

\[ \begin{aligned} I_{B'/B}(z)=z\int_0^1(B'/B)(tz)\,dt=\int_0^z(B'/B)(u)\,du. \end{aligned} \]

Thus by the fundamental theorem of calculus we have that \(J_B'(z)=B'(z)/B(z)\). Now let \(H(z)=\exp(J_B(z))/B(z)\) and note that

\[ H'(z)=(B(z)\,J_B'(z)-B'(z))\left(\frac{\exp(J_B(z))}{(B(z))^2}\right). \]

Thus, \(H\) is constant since we know that \(B(z)\,J_B'(z)-B'(z)=0\) from \(J_B'(z)=B'(z)/B(z)\). So since \(H(0)=\exp(J_B(0))/B(0)=1/B(0)\) we know \(H(z)=1/B(0)\) for all \(z\). So we have,

\[ \frac{1}{B(0)}=\frac{\exp(J_B(z))}{B(z)}\implies\left|\frac{B(z)}{B(0)}\right| =\exp(\mathfrak{R}J_B(z)). \]

Taking the logarithm of both sides completes the proof.

Lean

Formalized as LogOfAnalyticFunction.

Sources
LeanLogOfAnalyticFunction
Used by 1
Used byLogOfAnalyticFunction'

TheoremLogOfAnalyticFunction'#

A wrapper of the above theorem that will be useful later on.

Proof

See above.

Lean

Formalized as LogOfAnalyticFunction'.

Sources
LeanLogOfAnalyticFunction'
Uses 1 · Used by 3
Proof usesLogOfAnalyticFunction
Used byJBlaschke · FinalBound · JBlaschkeDerivBound

DefinitionSetOfZeros#

Let \(R>0\) and \(f:\mathbb{C}\to\mathbb{C}\). Define the set of zeros \(\mathcal{K}_f(R)=\{\rho\in\mathbb{C}:|\rho|\leq R,\,f(\rho)=0\}\).

Lean

Formalized as SetOfZeros.

Sources
LeanSetOfZeros
Used by 18
Used byBlaschkeAnalytic · BlaschkeB · BlaschkeNonZero · BlaschkeOfZero · CfAnalytic · CFunction · DiskBound · JBlaschke · norm-fOfZero-le-norm-BlaschkeOfZero · ZeroFactorization · ZerosBound · FinalBound · JBlaschkeDerivBound · LogDerivZetaFinalBound · SumBoundI · ZetaShiftFiniteZeros · LogDerivZetaUniformLogSquaredBoundStrip · SumBoundII

In LEAN, this corresponds exactly with analyticOrderAt/analyticOrderNatAt.

DefinitionZeroFactor#

Let \(f:\mathbb{C}\to\mathbb{C}\) and \(\rho\in\mathbb{C}\). Then there exists \(h_\rho\) such that

\[ f(z)=(z-\rho)^{m_f(\rho)}\,h_\rho(z). \]

In LEAN, this corresponds exactly with (-.analyticOrderAt-ne-top.mp -).choose, but this serves as a wrapper of that with the necessary conditions.

Lean

Formalized as ZeroFactor.

Sources
LeanZeroFactor
Used by 7
Used byBlaschkeNonZero · BlaschkeOfZero · CfAnalytic · CFunction · DiskBound · ZeroFactorization · FinalBound

LemmaZeroFactorization#

Let \(f:\mathbb{C}\to\mathbb{C}\) be analytic on \(\overline{\mathbb{D}_1}\) with \(f(0)\neq 0\). For all \(\rho\in\mathcal{K}_f(R)\) with \(R<1\) there exists \(h_\rho(z)\) such that \(h_\rho(z)\) is analytic at \(\rho\), \(h_\rho(\rho)\neq 0\), and \(f(z)=(z-\rho)^{m_f(\rho)}\,h_\rho(z)\).

Proof

Since \(f\) is analytic on neighborhoods of points in \(\overline{\mathbb{D}_1}\) we know that there exists a series expansion about \(\rho\):

\[ f(z)=\sum_{0\leq n}a_n\,(z-\rho)^n. \]

Now if we let \(m\) be the smallest number such that \(a_m\neq 0\), then

\[ f(z)=\sum_{0\leq n}a_n\,(z-\rho)^n=\sum_{m\leq n}a_n\,(z-\rho)^n =(z-\rho)^m\sum_{m\leq n}a_n\,(z-\rho)^{n-m}=(z-\rho)^m\,h_\rho(z). \]

Trivially, \(h_\rho(z)\) is analytic at \(\rho\) (we have written down the series expansion); now note that

\[ h_\rho(\rho)=\sum_{m\leq n}a_n(\rho-\rho)^{n-m}=\sum_{m\leq n}a_n0^{n-m}=a_m\neq 0. \]
Lean

Formalized as ZeroFactorization.

Sources
LeanZeroFactorization
Uses 2 · Used by 2
Statement usesSetOfZeros · ZeroFactor
Used byBlaschkeNonZero · CfAnalytic

DefinitionCFunction#

Let \(0 < r < 1\), and \(f:\mathbb{C}\to\mathbb{C}\) be analytic on \(\overline{\mathbb{D}_1}\) with \(f(0)\neq 0\). We define a function \(C_f:\mathbb{C}\to\mathbb{C}\) as follows. This function is constructed by dividing \(f(z)\) by a polynomial whose roots are the zeros of \(f\) inside \(\overline{\mathbb{D}_r}\).

\[ C_f(z)=\begin{cases} \displaystyle\frac{f(z)}{\prod_{\rho\in\mathcal{K}_f(r)}(z-\rho)^{m_f(\rho)}} \qquad\text{for }z\not\in\mathcal{K}_f(r) \\ \displaystyle\frac{h_z(z)}{\prod_{\rho\in\mathcal{K}_f(r)\setminus\{z\}} (z-\rho)^{m_f(\rho)}}\qquad\text{for }z\in\mathcal{K}_f(r) \end{cases} \]

where \(h_z(z)\) comes from Lemma ZeroFactorization.

Lean

Formalized as Cf.

Sources
LeanCf
Uses 2 · Used by 7
Statement usesSetOfZeros · ZeroFactor
Used byBlaschkeAnalytic · BlaschkeB · BlaschkeNonZero · BlaschkeOfZero · CfAnalytic · DiskBound · FinalBound

LemmaCfAnalytic#

If \(f:\mathbb{C}\to\mathbb{C}\) is analytic on \(\overline{\mathbb{D}_1}\) then so too is \(C_f\).

Proof

Look at the definition of \(C_f\) and apply ZeroFactorization.

Lean

Formalized as CfAnalytic.

Sources
LeanCfAnalytic
Uses 4 · Used by 1
Statement usesCFunction
Proof usesZeroFactorization · SetOfZeros · ZeroFactor
Used byBlaschkeAnalytic

DefinitionBlaschkeB#

Let \(0 < r < R < 1\), and \(f:\mathbb{C}\to\mathbb{C}\) be analytic \(\overline{\mathbb{D}_1}\) with \(f(0)\neq 0\). We define a function \(B_f:\mathbb{C}\to\mathbb{C}\) as follows.

\[ B_f(z)=C_f(z)\prod_{\rho\in\mathcal{K}_f(r)} \left(R-\frac{z\overline{\rho}}{R}\right)^{m_f(\rho)} \]
Lean

Formalized as BlaschkeB.

Sources
LeanBlaschkeB
Uses 2 · Used by 9
Statement usesCFunction · SetOfZeros
Used byBlaschkeAnalytic · BlaschkeNonZero · BlaschkeOfZero · DiskBound · JBlaschke · norm-fOfZero-le-norm-BlaschkeOfZero · ZerosBound · FinalBound · JBlaschkeDerivBound

LemmaBlaschkeAnalytic#

If \(f:\mathbb{C}\to\mathbb{C}\) is analytic on \(\overline{\mathbb{D}_R}\) then so too is \(B_f\).

Proof

Expand out \(B_f\) as a product, and observe that each part is analytic on \(\overline{\mathbb{D}_R}\).

Lean

Formalized as BlaschkeAnalytic.

Sources
LeanBlaschkeAnalytic
Uses 4 · Used by 4
Statement usesBlaschkeB · SetOfZeros
Proof usesCFunction · CfAnalytic
Used byDiskBound · JBlaschke · FinalBound · JBlaschkeDerivBound

LemmaBlaschkeOfZero#

Let \(0 < r < R<1\), and \(f:\mathbb{C}\to\mathbb{C}\) be analytic on \(\overline{\mathbb{D}_1}\) with \(f(0)\neq 0\). Then

\[ |B_f(0)|=|f(0)|\prod_{\rho\in\mathcal{K}_f(r)} \left(\frac{R}{|\rho|}\right)^{m_f(\rho)}. \]
Proof

Since \(f(0)\neq 0\), we know that \(0\not\in\mathcal{K}_f(r)\). Thus,

\[ C_f(0)=\frac{f(0)}{\displaystyle\prod_{\rho\in\mathcal{K}_f(r)}(-\rho)^{m_f(\rho)}}. \]

Thus, substituting this into Definition BlaschkeB,

\[ |B_f(0)|=|C_f(0)|\prod_{\rho\in\mathcal{K}_f(r)}R^{m_f(\rho)} =|f(0)|\prod_{\rho\in\mathcal{K}_f(r)}\left(\frac{R}{|\rho|}\right)^{m_f(\rho)}. \]
Lean

Formalized as BlaschkeOfZero.

Sources
LeanBlaschkeOfZero
Uses 4 · Used by 2
Statement usesBlaschkeB · SetOfZeros
Proof usesCFunction · ZeroFactor
Used bynorm-fOfZero-le-norm-BlaschkeOfZero · ZerosBound

Lemmanorm-fOfZero-le-norm-BlaschkeOfZero#

Let \(0 < r < R<1\), and \(f:\mathbb{C}\to\mathbb{C}\) be analytic on \(\overline{\mathbb{D}_1}\) with \(f(0)\neq 0\). Then

\[ |f(0)|\leq|B_f(0)|. \]
Proof

Applying lemma BlaschkeOfZero we know that

\[ |B_f(0)|=|f(0)|\prod_{\rho\in\mathcal{K}_f(r)} \left(\frac{R}{|\rho|}\right)^{m_f(\rho)}. \]

Note that for all \(\rho\in\mathcal{K}_f(r)\) that \(1\lt R/|\rho|\) since \(r\lt R\). Thus, the result follows.

Lean

Formalized as norm_fOfZero_le_norm_BlaschkeOfZero.

Sources
Leannorm_fOfZero_le_norm_BlaschkeOfZero
Uses 3 · Used by 1
Statement usesBlaschkeB · SetOfZeros
Proof usesBlaschkeOfZero
Used byJBlaschkeDerivBound

LemmaDiskBound#

Let \(0 < r < R<1\). If \(f:\mathbb{C}\to\mathbb{C}\) is a function analytic on \(\overline{\mathbb{D}_1}\) with \(f(0)\neq0\) such that \(|f(z)|\leq B\) for \(|z|\leq R\), then \(|B_f(z)|\leq B\) for \(|z|\leq R\) also.

Proof

For \(|z|=R\), we know that \(z\not\in\mathcal{K}_f(r)\). Thus,

\[ C_f(z)=\frac{f(z)}{\displaystyle\prod_{\rho\in\mathcal{K}_f(r)}(z-\rho)^{m_f(\rho)}}. \]

Thus, substituting this into Definition BlaschkeB,

\[ |B_f(z)|=|f(z)|\prod_{\rho\in\mathcal{K}_f(r)} \left|\frac{R-z\overline{\rho}/R}{z-\rho}\right|^{m_f(\rho)}. \]

But note that

\[ \left|\frac{R-z\overline{\rho}/R}{z-\rho}\right| =\frac{|R^2-z\overline{\rho}|/R}{|z-\rho|} =\frac{|z|\cdot|\overline{z-\rho}|/R}{|z-\rho|}=1. \]

So we have that \(|B_f(z)|=|f(z)|\leq B\) when \(|z|=R\). Now by the maximum modulus principle, we know that the maximum of \(|B_f|\) must occur on the boundary where \(|z|=R\). Thus \(|B_f(z)|\leq B\) for all \(|z|\leq R\).

Lean

Formalized as DiskBound.

Sources
LeanDiskBound
Uses 6 · Used by 2
Statement usesBlaschkeB · SetOfZeros
Proof usesCFunction · AnalyticOn.norm-le-of-norm-le-on-sphere · ZeroFactor · BlaschkeAnalytic
Used byZerosBound · JBlaschkeDerivBound

LemmaBlaschkeNonZero#

Let \(0 < r < R<1\) and \(f:\overline{\mathbb{D}_1}\to\mathbb{C}\) be analytic on neighborhoods of points in \(\overline{\mathbb{D}_1}\) with \(f(0)\neq 0\). Then \(B_f(z)\neq 0\) for all \(z\in\overline{\mathbb{D}_r}\).

Proof

Suppose that \(z\in\mathcal{K}_f(r)\). Then we have that

\[ C_f(z)=\frac{h_z(z)}{\displaystyle\prod_{\rho\in\mathcal{K}_f(r)\setminus\{z\}} (z-\rho)^{m_f(\rho)}}. \]

where \(h_z(z)\neq 0\) according to Lemma ZeroFactorization. Thus, substituting this into Definition BlaschkeB,

\[ |B_f(z)|=|h_z(z)|\cdot\left|R-\frac{|z|^2}{R}\right|^{m_f(z)} \prod_{\rho\in\mathcal{K}_f(r)\setminus\{z\}} \left|\frac{R-z\overline{\rho}/R}{z-\rho}\right|^{m_f(\rho)}.\qquad\text{(2)} \]

Trivially, \(|h_z(z)|\neq 0\). Now note that

\[ \left|R-\frac{|z|^2}{R}\right|=0\implies|z|=R. \]

However, this is a contradiction because \(z\in\overline{\mathbb{D}_r}\) tells us that \(|z|\leq r < R\). Similarly, note that

\[ \left|\frac{R-z\overline{\rho}/R}{z-\rho}\right|=0\implies|z|=\frac{R^2}{|\overline{\rho}|}. \]

However, this is also a contradiction because \(\rho\in\mathcal{K}_f(r)\) tells us that \(R < R^2/|\overline{\rho}|=|z|\), but \(z\in\overline{\mathbb{D}_r}\) tells us that \(|z|\leq r < R\). So, we know that

\[ \left|R-\frac{|z|^2}{R}\right|\neq 0\qquad\text{and}\qquad \left|\frac{R-z\overline{\rho}/R}{z-\rho}\right|\neq 0 \quad\text{for all}\quad\rho\in\mathcal{K}_f(r)\setminus\{z\}. \]

Applying this to Equation (2) we have that \(|B_f(z)|\neq 0\). So, \(B_f(z)\neq 0\).

Now suppose that \(z\not\in\mathcal{K}_f(r)\). Then we have that

\[ C_f(z)=\frac{f(z)}{\displaystyle\prod_{\rho\in\mathcal{K}_f(r)}(z-\rho)^{m_f(\rho)}}. \]

Thus, substituting this into Definition BlaschkeB,

\[ |B_f(z)|=|f(z)|\prod_{\rho\in\mathcal{K}_f(r)} \left|\frac{R-z\overline{\rho}/R}{z-\rho}\right|^{m_f(\rho)}.\qquad\text{(3)} \]

We know that \(|f(z)|\neq 0\) since \(z\not\in\mathcal{K}_f(r)\). Now note that

\[ \left|\frac{R-z\overline{\rho}/R}{z-\rho}\right|=0\implies|z|=\frac{R^2}{|\overline{\rho}|}. \]

However, this is a contradiction because \(\rho\in\mathcal{K}_f(r)\) tells us that \(R < R^2/|\overline{\rho}|=|z|\), but \(z\in\overline{\mathbb{D}_r}\) tells us that \(|z|\leq r < R\). So, we know that

\[ \left|\frac{R-z\overline{\rho}/R}{z-\rho}\right|\neq 0 \quad\text{for all}\quad\rho\in\mathcal{K}_f(r). \]

Applying this to Equation (3) we have that \(|B_f(z)|\neq 0\). So, \(B_f(z)\neq 0\).

We have shown that \(B_f(z)\neq 0\) for both \(z\in\mathcal{K}_f(r)\) and \(z\not\in\mathcal{K}_f(r)\), so the result follows.

Lean

Formalized as BlaschkeNonzero.

Sources
LeanBlaschkeNonzero
Uses 5 · Used by 3
Statement usesBlaschkeB · SetOfZeros
Proof usesCFunction · ZeroFactorization · ZeroFactor
Used byJBlaschke · FinalBound · JBlaschkeDerivBound

TheoremZerosBound#

Let \(0< r < R<1\). If \(f:\mathbb{C}\to\mathbb{C}\) is a function analytic on neighborhoods of points in \(\overline{\mathbb{D}_1}\) with \(f(0)=1\) and \(|f(z)|\leq B\) for \(|z|\leq R\), then

\[ \sum_{\rho\in\mathcal{K}_f(r)}m_f(\rho)\leq\frac{\log B}{\log(R/r)}. \]
Proof

Since \(f(0)=1\), by Lemma BlaschkeOfZero we know that

\[ |B_f(0)| =|f(0)|\prod_{\rho\in\mathcal{K}_f(r)}\left(\frac{R}{|\rho|}\right)^{m_f(\rho)} =\prod_{\rho\in\mathcal{K}_f(r)}\left(\frac{R}{|\rho|}\right)^{m_f(\rho)}. \]

Thus, substituting this into Definition BlaschkeB,

\[ (R/r)^{\sum_{\rho\in\mathcal{K}_f(r)}m_f(\rho)} =\prod_{\rho\in\mathcal{K}_f(r)}\left(\frac{R}{r}\right)^{m_f(\rho)} \leq\prod_{\rho\in\mathcal{K}_f(r)}\left(\frac{R}{|\rho|}\right)^{m_f(\rho)} =|B_f(0)|\leq B \]

whereby Lemma DiskBound we know that \(|B_f(z)|\leq B\) for all \(|z|\leq R\). Taking the logarithm of both sides and rearranging gives the desired result.

Lean

Formalized as ZerosBound.

Sources
LeanZerosBound
Uses 4 · Used by 2
Statement usesSetOfZeros
Proof usesBlaschkeB · DiskBound · BlaschkeOfZero
Used byFinalBound · LogDerivZetaUniformLogSquaredBoundStrip

DefinitionJBlaschke#

Let \(0 < r < R<1\). If \(f:\mathbb{C}\to\mathbb{C}\) is a function analytic on neighborhoods of points in \(\overline{\mathbb{D}_1}\) with \(f(0)=1\), define \(L_f(z)=J_{B_f}(z)\) where \(J\) is from Theorem LogOfAnalyticFunction and \(B_f\) is from Definition BlaschkeB.

Lean

Formalized as JBlaschke.

Sources
LeanJBlaschke
Uses 5 · Used by 2
Statement usesBlaschkeNonZero · BlaschkeB · SetOfZeros · BlaschkeAnalytic · LogOfAnalyticFunction'
Used byFinalBound · JBlaschkeDerivBound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.