PrimeNumberTheoremAnd

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

From \texttt{riemannZeta_residue_one} (in Mathlib), we know that $(s-1)\zeta(s)$ goes to $1$ as $s\to1$. Now apply Theorem \ref{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$...) -/)] theorem riemannZetaResidue : ∃ U ∈ 𝓝 1, BddAbove (norm ∘ (ζ - (fun s ↦ (s - 1)⁻¹)) '' (U \ {1})) := by have zeta_holc : HolomorphicOn ζ (univ \ {1}) := by intro y hy exact DifferentiableAt.differentiableWithinAt <| differentiableAt_riemannZeta hy.2 convert ResidueOfTendsTo univ_mem zeta_holc riemannZeta_residue_one using 6 simp

-- Main theorem: if functions agree on a punctured set, their derivatives agree there too theorem deriv_eqOn_of_eqOn_punctured (f g : ℂ → ℂ) (U : Set ℂ) (p : ℂ) (hU_open : IsOpen U) (h_eq : EqOn f g (U \ {p})) : EqOn (deriv f) (deriv g) (U \ {p}) := by intro x hx apply EventuallyEq.deriv_eq filter_upwards [IsOpen.mem_nhds (hU_open.sdiff isClosed_singleton) hx] with t ht using h_eq ht

/- New two theorems to be proven

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$. -/)] theorem nonZeroOfBddAbove {f : ℂ → ℂ} {p : ℂ} {U : Set ℂ} (U_in_nhds : U ∈ 𝓝 p) {A : ℂ} (A_ne_zero : A ≠ 0) (f_near_p : BddAbove (norm ∘ (f - fun s ↦ A * (s - p)⁻¹) '' (U \ {p}))) : ∃ V ∈ 𝓝 p, IsOpen V ∧ ∀ s ∈ V \ {p}, f s ≠ 0 := by

-- Step 1: Rewrite f as the sum of two parts have h_decomp : ∀ s, f s = (f s - A * (s - p)⁻¹) + A * (s - p)⁻¹ := by intro s ring -- Get a bound for the first summand obtain ⟨M, hM⟩ := f_near_p -- Step 2: The second summand A * (s - p)⁻¹ goes to ∞ as s → p -- We need to find a neighborhood where |A * (s - p)⁻¹| > M + 1 have A_norm_pos : 0 < ‖A‖ := norm_pos_iff.mpr A_ne_zero -- Choose δ such that for |s - p| < δ, we have |A * (s - p)⁻¹| > M + 1 let δ := ‖A‖ / (‖M‖ + 1) have δ_pos : 0 < δ := by refine div_pos A_norm_pos (add_pos_of_nonneg_of_pos (norm_nonneg M) one_pos) -- Find an open neighborhood V contained in both U and the δ-ball around p obtain ⟨V, hV_open, hV_mem, hV_sub⟩ : ∃ V, IsOpen V ∧ p ∈ V ∧ V ⊆ U ∩ Metric.ball p δ := by -- rw [mem_nhds_iff] at U_in_nhds obtain ⟨W, hW_sub, hW_open, hW_mem⟩ := mem_nhds_iff.mp U_in_nhds let V := W ∩ Metric.ball p δ have VNp : V ∈ 𝓝 p := (𝓝 p).inter_mem (IsOpen.mem_nhds hW_open hW_mem) (Metric.ball_mem_nhds p δ_pos) exact ⟨V, IsOpen.inter hW_open Metric.isOpen_ball, mem_of_mem_nhds VNp, inter_subset_inter_left _ hW_sub⟩ use V, mem_nhds_iff.mpr ⟨V, subset_refl V, hV_open, hV_mem⟩, hV_open -- Show f ≠ 0 on V intro s hs have hs_in_U : s ∈ U := hV_sub hs.1 |>.1 have hs_near_p : dist s p < δ := hV_sub hs.1 |>.2 have hs_ne_p : s ≠ p := hs.2 -- Step 3: Therefore the sum of the two terms has large norm rw [h_decomp s] -- The first summand is bounded have bound_first : ‖f s - A * (s - p)⁻¹‖ ≤ M := by apply hM exact ⟨s, ⟨hs_in_U, hs_ne_p⟩, rfl⟩ -- The second summand has large norm have large_second : ‖M‖ + 1 < ‖A * (s - p)⁻¹‖ := by rw [norm_mul, norm_inv, ← div_eq_mul_inv] rw [lt_div_iff₀ (norm_pos_iff.mpr (sub_ne_zero.mpr hs_ne_p))] rw [mul_comm, ← lt_div_iff₀ (add_pos_of_nonneg_of_pos (norm_nonneg M) one_pos)] rw [dist_eq_norm_sub] at hs_near_p exact hs_near_p -- Step 4: Therefore the sum is nonzero near p by_contra h_zero -- If f s = 0, then the two summands are negatives of each other rw [add_eq_zero_iff_eq_neg] at h_zero rw [h_zero, norm_neg] at bound_first -- But this contradicts our bounds have : ‖M‖ + 1 < ‖M‖ := (lt_of_lt_of_le (lt_of_lt_of_le large_second bound_first) (Real.le_norm_self M)) norm_num at this

/- The set should be open so that f'(p) = O(1) for all p ∈ U

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)$.

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