deriv-conj-conj to isPathConnected-aux

Theoremderiv-conj-conj#

Let \(f : \mathbb{C} \to \mathbb{C}\) be a function at \(p \in \mathbb{C}\) with derivative \(a\). Then the derivative of the function \(g(z) = \overline{f(\overline{z})}\) at \(\overline{p}\) is \(\overline{a}\).

Proof

We proceed by case analysis on whether \(f\) is differentiable at \(p\). If \(f\) is differentiable at \(p\), then we can apply the previous theorem. If \(f\) is not differentiable at \(p\), then neither is \(g\), and both derivatives have the default value of zero.

Lean

Formalized as deriv_conj_conj'.

Sources
Leanderiv_conj_conj'
Used by 1
Used byderiv-riemannZeta-conj

Theoremderiv-riemannZeta-conj#

Conjugation symmetry of the derivative of the Riemann zeta function. Let \(s \in \mathbb{C}\). Then

\[ \zeta'(\overline{s}) = \overline{\zeta'(s)}. \]
Proof

We apply the derivative conjugation symmetry to the Riemann zeta function and use the conjugation symmetry of the Riemann zeta function itself.

Lean

Formalized as deriv_riemannZeta_conj.

Sources
Leanderiv_riemannZeta_conj
Uses 1 · Used by 4
Proof usesderiv-conj-conj
Used byI6GenBound · I7GenBound · I8I2 · I9Bound

TheoremintervalIntegral-conj#

The conjugation symmetry of the interval integral. Let \(f : \mathbb{R} \to \mathbb{C}\) be a measurable function, and let \(a, b \in \mathbb{R}\). Then

\[ \int_{a}^{b} \overline{f(x)} \, dx = \overline{\int_{a}^{b} f(x) \, dx}. \]
Proof

We unfold the interval integral into an integral over a uIoc and use the conjugation property of integrals.

Lean

Formalized as intervalIntegral_conj.

Sources
LeanintervalIntegral_conj
Used by 3
Used byI6GenBound · I7GenBound · I8I2

We record here some prelimiaries about the zeta function and general holomorphic functions.

TheoremResidueOfTendsTo#

If a function \(f\) is holomorphic in a neighborhood of \(p\) and \(\lim_{s\to p} (s-p)f(s) = A\), then \(f(s) = \frac{A}{s-p} + O(1)\) near \(p\).

Proof

The function \((s - p)\cdot f(s)\) bounded, so by Theorem existsDifferentiableOn-of-bddAbove, there is a holomorphic function, \(g\), say, so that \((s-p)f(s) = g(s)\) in a neighborhood of \(s=p\), and \(g(p)=A\). Now because \(g\) is holomorphic, near \(s=p\), we have \(g(s)=A+O(s-p)\). Then when you divide by \((s-p)\), you get \(f(s) = A/(s-p) + O(1)\).

Lean

Formalized as ResidueOfTendsTo.

Sources
LeanResidueOfTendsTo
Uses 1 · Used by 1
Proof usesexistsDifferentiableOn-of-bddAbove
Used byriemannZetaResidue

TheoremriemannZetaResidue#

The Riemann zeta function \(\zeta(s)\) has a simple pole at \(s=1\) with residue \(1\). In particular, the function \(\zeta(s) - \frac{1}{s-1}\) is bounded in a neighborhood of \(s=1\).

Proof

From riemannZeta_residue_one (in Mathlib), we know that \((s-1)\zeta(s)\) goes to \(1\) as \(s\to1\). Now apply Theorem ResidueOfTendsTo. (This can also be done using \(\zeta_0\) below, which is expressed as \(1/(s-1)\) plus things that are holomorphic for \(\Re(s)>0\)...)

Lean

Formalized as riemannZetaResidue.

Sources
LeanriemannZetaResidue
Uses 1 · Used by 1
Proof usesResidueOfTendsTo
Used byriemannZetaLogDerivResidue

TheoremnonZeroOfBddAbove#

If a function \(f\) has a simple pole at a point \(p\) with residue \(A \neq 0\), then \(f\) is nonzero in a punctured neighborhood of \(p\).

Proof

We know that \(f(s) = \frac{A}{s-p} + O(1)\) near \(p\), so we can write

\[ f(s) = \left(f(s) - \frac{A}{s-p}\right) + \frac{A}{s-p}. \]

The first term is bounded, say by \(M\), and the second term goes to \(\infty\) as \(s \to p\). Therefore, there exists a neighborhood \(V\) of \(p\) such that for all \(s \in V \setminus \{p\}\), we have \(f(s) \neq 0\).

Lean

Formalized as nonZeroOfBddAbove.

Sources
LeannonZeroOfBddAbove
Used by 1
Used byriemannZetaLogDerivResidue

TheoremlogDerivResidue#

If \(f\) is holomorphic in a neighborhood of \(p\), and there is a simple pole at \(p\), then \(f'/ f\) has a simple pole at \(p\) with residue \(-1\):

\[ \frac{f'(s)}{f(s)} = \frac{-1}{s - p} + O(1). \]
Proof

Using Theorem existsDifferentiableOn-of-bddAbove, there is a function \(g\) holomorphic near \(p\), for which \(f(s) = A/(s-p) + g(s) = h(s)/ (s-p)\). Here \(h(s):= A + g(s)(s-p)\) which is nonzero in a neighborhood of \(p\) (since \(h\) goes to \(A\) which is nonzero). Then \(f'(s) = (h'(s)(s-p) - h(s))/(s-p)^2\), and we can compute the quotient:

\[ \frac{f'(s)}{f(s)}+1/(s-p) = \frac{h'(s)(s-p) - h(s)}{h(s)} \cdot \frac{1}{(s-p)}+1/(s-p) = \frac{h'(s)}{h(s)}. \]

Since \(h\) is nonvanishing near \(p\), this remains bounded in a neighborhood of \(p\).

Lean

Formalized as logDerivResidue.

Sources
LeanlogDerivResidue
Uses 1 · Used by 1
Proof usesexistsDifferentiableOn-of-bddAbove
Used byriemannZetaLogDerivResidue

TheoremBddAbove-to-IsBigO#

If \(f\) is bounded above in a punctured neighborhood of \(p\), then \(f\) is \(O(1)\) in that neighborhood.

Proof

Elementary.

Lean

Formalized as BddAbove_to_IsBigO.

Sources
LeanBddAbove_to_IsBigO
Used by 2
Used bySmoothedChebyshevPull1 · ShiftZeroBound

Let's also record that if a function \(f\) has a simple pole at \(p\) with residue \(A\), and \(g\) is holomorphic near \(p\), then the residue of \(f \cdot g\) is \(A \cdot g(p)\).

TheoremResidueMult#

If \(f\) has a simple pole at \(p\) with residue \(A\), and \(g\) is holomorphic near \(p\), then the residue of \(f \cdot g\) at \(p\) is \(A \cdot g(p)\). That is, we assume that

\[ f(s) = \frac{A}{s - p} + O(1) \]

near \(p\), and that \(g\) is holomorphic near \(p\). Then

\[ f(s) \cdot g(s) = \frac{A \cdot g(p)}{s - p} + O(1). \]
Proof

Elementary calculation.

\[ f(s) * g(s) - \frac{A * g(p)}{s - p} = \left(f(s) * g(s) - \frac{A * g(s)}{s - p}\right) + \left(\frac{A * g(s) - A * g(p)}{s - p}\right). \]

The first term is \(g(s)(f(s) - \frac{A}{s - p})\), which is bounded near \(p\) by the assumption on \(f\) and the fact that \(g\) is holomorphic near \(p\). The second term is \(A\) times the log derivative of \(g\) at \(p\), which is bounded by the assumption that \(g\) is holomorphic.

Lean

Formalized as ResidueMult.

Sources
LeanResidueMult
Used by 1
Used bySmoothedChebyshevPull1

As a corollary, the log derivative of the Riemann zeta function has a simple pole at \(s=1\):

TheoremriemannZetaLogDerivResidue#

The log derivative of the Riemann zeta function \(\zeta(s)\) has a simple pole at \(s=1\) with residue \(-1\): \(-\frac{\zeta'(s)}{\zeta(s)} - \frac{1}{s-1} = O(1)\).

Proof

This follows from Theorem logDerivResidue and Theorem riemannZetaResidue.

Lean

Formalized as riemannZetaLogDerivResidue.

Sources
LeanriemannZetaLogDerivResidue
Uses 3 · Used by 4
Proof useslogDerivResidue · nonZeroOfBddAbove · riemannZetaResidue
Used byI1Bound · SmoothedChebyshevPull1 · LogDerivZetaBndUnif99 · ShiftZeroBound

DefinitionriemannZeta0#

For any natural \(N\ge1\), we define

\[ \zeta_0(N,s) := \sum_{1\le n \le N} \frac1{n^s} + \frac{- N^{1-s}}{1-s} + \frac{-N^{-s}}{2} + s \int_N^\infty \frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx \]
Lean

Formalized as riemannZeta0.

Sources
LeanriemannZeta0
Used by 6
Used byHolomorphicOn-riemannZeta0 · Zeta0EqZeta · ZetaDerivUpperBnd · ZetaUpperBnd · Zeta1AltFormula · ZetaAltFormula

Lemmasum-eq-int-deriv#

Let \(a < b\), and let \(\phi\) be continuously differentiable on \([a, b]\). Then

\[ \sum_{a < n \le b} \phi(n) = \int_a^b \phi(x) \, dx + \left(\lfloor b \rfloor + \frac{1}{2} - b\right) \phi(b) - \left(\lfloor a \rfloor + \frac{1}{2} - a\right) \phi(a) - \int_a^b \left(\lfloor x \rfloor + \frac{1}{2} - x\right) \phi'(x) \, dx. \]
Proof

This is first order Euler-Maclaurin.

Lean

Formalized as sum_eq_int_deriv.

Sources
Leansum_eq_int_deriv
Used by 1
Used byZetaSum-aux1

LemmaZetaSum-aux1#

Let \(0 < a < b\) be natural numbers and \(s\in \mathbb{C}\) with \(s \ne 1\) and \(s \ne 0\). Then

\[ \sum_{a < n \le b} \frac{1}{n^s} = \frac{b^{1-s} - a^{1-s}}{1-s} + \frac{b^{-s}-a^{-s}}{2} + s \int_a^b \frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx. \]
Proof

Apply Lemma sum-eq-int-deriv to the function \(x \mapsto x^{-s}\).

Lean

Formalized as ZetaSum_aux1.

Sources
LeanZetaSum_aux1
Uses 1 · Used by 1
Proof usessum-eq-int-deriv
Used byZetaSum-aux2

LemmaZetaBnd-aux1a#

For any \(0 < a < b\) and \(s \in \mathbb{C}\) with \(\sigma=\Re(s)>0\),

\[ \int_a^b \left|\frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx\right| \le \frac{a^{-\sigma}-b^{-\sigma}}{\sigma}. \]
Proof

Apply the triangle inequality

\[ \left|\int_a^b \frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx\right| \le \int_a^b \frac{1}{x^{\sigma+1}} \, dx, \]

and evaluate the integral.

Lean

Formalized as ZetaBnd_aux1a.

Sources
LeanZetaBnd_aux1a
Used by 1
Used byZetaBnd-aux1b

LemmaZetaSum-aux2#

Let \(N\) be a natural number and \(s\in \mathbb{C}\), \(\Re(s)>1\). Then

\[ \sum_{N < n} \frac{1}{n^s} = \frac{- N^{1-s}}{1-s} + \frac{-N^{-s}}{2} + s \int_N^\infty \frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx. \]
Proof

Apply Lemma ZetaSum-aux1 with \(a=N\) and \(b\to \infty\).

Lean

Formalized as ZetaSum_aux2.

Sources
LeanZetaSum_aux2
Uses 1 · Used by 1
Proof usesZetaSum-aux1
Used byZeta0EqZeta

LemmaZetaBnd-aux1b#

For any \(N\ge1\) and \(s = \sigma + tI \in \mathbb{C}\), \(\sigma > 0\),

\[ \left| \int_N^\infty \frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx \right| \le \frac{N^{-\sigma}}{\sigma}. \]
Proof

Apply Lemma ZetaBnd-aux1a with \(a=N\) and \(b\to \infty\).

Lean

Formalized as ZetaBnd_aux1b.

Sources
LeanZetaBnd_aux1b
Uses 1 · Used by 2
Proof usesZetaBnd-aux1a
Used byZetaBnd-aux1 · ZetaBnd-aux1p

LemmaZetaBnd-aux1#

For any \(N\ge1\) and \(s = \sigma + tI \in \mathbb{C}\), \(\sigma=\in(0,2], 2 < |t|\),

\[ \left| s\int_N^\infty \frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx \right| \le 2 |t| \frac{N^{-\sigma}}{\sigma}. \]
Proof

Apply Lemma ZetaBnd-aux1b and estimate \(|s|\ll |t|\).

Lean

Formalized as ZetaBnd_aux1.

Sources
LeanZetaBnd_aux1
Uses 1 · Used by 2
Proof usesZetaBnd-aux1b
Used byZetaDerivUpperBnd · ZetaUpperBnd

Big-Oh version of Lemma ZetaBnd-aux1.

LemmaZetaBnd-aux1p#

For any \(N\ge1\) and \(s = \sigma + tI \in \mathbb{C}\), \(\sigma=\in(0,2], 2 < |t|\),

\[ \left| s\int_N^\infty \frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx \right| \ll |t| \frac{N^{-\sigma}}{\sigma}. \]
Proof

Apply Lemma ZetaBnd-aux1b and estimate \(|s|\ll |t|\).

Lean

Formalized as ZetaBnd_aux1p.

Sources
LeanZetaBnd_aux1p
Uses 1
Proof usesZetaBnd-aux1b

TheoremHolomorphicOn-riemannZeta0#

For any \(N\ge1\), the function \(\zeta_0(N,s)\) is holomorphic on \(\{s\in \mathbb{C}\mid \Re(s)>0 ∧ s \ne 1\}\).

Proof

The function \(\zeta_0(N,s)\) is a finite sum of entire functions, plus an integral that's absolutely convergent on \(\{s\in \mathbb{C}\mid \Re(s)>0 ∧ s \ne 1\}\) by Lemma ZetaBnd-aux1b.

Lean

Formalized as HolomorphicOn_riemannZeta0.

Sources
LeanHolomorphicOn_riemannZeta0
Uses 1 · Used by 1
Statement usesriemannZeta0
Used byZeta0EqZeta

LemmaisPathConnected-aux#

The set \(\{s\in \mathbb{C}\mid \Re(s)>0 ∧ s \ne 1\}\) is path-connected.

Proof

Construct explicit paths from \(2\) to any point, either a line segment or two joined ones.

Lean

Formalized as isPathConnected_aux.

Sources
LeanisPathConnected_aux
Used by 1
Used byZeta0EqZeta

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.