PrimeNumberTheoremAnd

If f is holomorphic on the disk ‖·‖ < r and bounded by C on the circle ‖·‖ = r, then ‖f z‖ ≤ C for every z in the disk.

A continuous complex-valued function is bounded on a closed ball.

If a < re z, nested open balls around z stay in the half-plane re · ≥ a.

Variant of borelCaratheodory_zero for a uniform bound on a closed ball and ‖z‖ ≤ r.

The canonical product converges uniformly on compact sets under the standard summability hypothesis.

The canonical product is holomorphic on ℂ under the standard summability hypothesis.

Genus-one Weierstrass factors contribute the usual 1 / (z - a) + 1 / a term to the logarithmic derivative.

The canonical product vanishes at each prescribed zero a n.

Away from the prescribed zero set Set.range a, the canonical product is nonzero.

The logarithmic derivative of a genus-one sequence-indexed canonical product is the expected sum of the logarithmic derivatives of the Weierstrass factors, away from the prescribed zero set.

The one-dimensional logarithmic singularity used in the Cartan/dyadic averaging argument. -/ noncomputable def φ (t : ℝ) : ℝ := log⁺ (1 / |1 - t|)

lemma measurable_phi : Measurable φ := by unfold φ simpa [Real.posLog_def, Real.posLog] using (by fun_prop : Measurable fun t : ℝ => max 0 (Real.log (1 / |1 - t|)))

lemma phi_le_log_two_of_le_half {t : ℝ} (ht : t ≤ (1 / 2 : ℝ)) : φ t ≤ Real.log 2 := by have hnonneg : 0 ≤ (1 - t : ℝ) := by linarith have hden : (1 / 2 : ℝ) ≤ |1 - t| := by have : (1 / 2 : ℝ) ≤ (1 - t : ℝ) := by linarith simpa [abs_of_nonneg hnonneg] using this have hfrac : (1 / |1 - t| : ℝ) ≤ 2 := by have hhalfpos : (0 : ℝ) < (1 / 2 : ℝ) := by norm_num have := one_div_le_one_div_of_le hhalfpos hden simpa [one_div, div_eq_mul_inv] using this have hposLog : log⁺ (1 / |1 - t|) ≤ log⁺ (2 : ℝ) := Real.posLog_le_posLog (by positivity) hfrac have habs : (1 : ℝ) ≤ |(2 : ℝ)| := by simp have hposLog2 : (log⁺ (2 : ℝ)) = Real.log 2 := by simpa using (Real.posLog_eq_log habs) simpa [φ, hposLog2] using hposLog

lemma phi_eq_zero_of_one_le_abs_one_sub {t : ℝ} (ht : (1 : ℝ) ≤ |1 - t|) : φ t = 0 := by have hpos : 0 < |1 - t| := lt_of_lt_of_le (by norm_num) ht have hfrac : (1 / |1 - t| : ℝ) ≤ 1 := (div_le_one hpos).2 ht have habs : |(1 / |1 - t| : ℝ)| ≤ 1 := by have hnonneg : 0 ≤ (1 / |1 - t| : ℝ) := by positivity simpa [abs_of_nonneg hnonneg] using hfrac have : log⁺ (1 / |1 - t|) = 0 := (Real.posLog_eq_zero_iff _).2 habs simpa [φ] using this

lemma φ_nonneg (t : ℝ) : 0 ≤ φ t := by simpa [φ] using (Real.posLog_nonneg (x := (1 / |1 - t|)))

lemma φ_le_sqrt (t : ℝ) : φ t ≤ Real.sqrt (2 / |1 - t|) := by simpa [φ, Real.posLog] using posLog_log_one_div_abs_one_sub_le_sqrt (t := t)

lemma ae_restrict_norm_phi_le_of_forall_mem {A B : ℝ} (hAB : A ≤ B) {g : ℝ → ℝ} (hg : ∀ t, 0 ≤ g t) (h : ∀ t ∈ Set.Icc A B, φ t ≤ g t) : (fun t : ℝ => ‖φ t‖) ≤ᶠ[ae (volume.restrict (Set.uIoc A B))] fun t => ‖g t‖ := by refine MeasureTheory.ae_restrict_of_forall_mem (μ := (volume : MeasureTheory.Measure ℝ)) (s := Set.uIoc A B) (by simpa using (measurableSet_uIoc : MeasurableSet (Set.uIoc A B))) ?_ intro t ht have htIoc : t ∈ Set.Ioc A B := by simpa [Set.uIoc_of_le hAB] using ht have htIcc : t ∈ Set.Icc A B := ⟨le_of_lt htIoc.1, htIoc.2⟩ have hle : φ t ≤ g t := h t htIcc have hφ0 : 0 ≤ φ t := φ_nonneg t have hg0 : 0 ≤ g t := hg t simpa [Real.norm_eq_abs, abs_of_nonneg hφ0, abs_of_nonneg hg0] using hle

/-!

Bridge lemma: from the 1D singularity φ to a complex lower bound

On a circle ‖u‖ = r, the quantity log ‖1 - u/a‖ is bounded below in terms of φ(r/‖a‖). This is the local estimate in the probabilistic-radius argument.