det2_log_factor_bound

formal source

 104/-- The bound on each log-factor:
 105    |log det₂_factor(p,σ)| ≤ p^{−2σ}/(1 − p^{−σ}).
 106    This is summable over primes for σ > 1/2. -/
 107theorem det2_log_factor_bound {σ : ℝ} (hσ : 1/2 < σ) (p : Nat.Primes) :
 108    |det2LogFactor p σ| ≤ (p : ℝ) ^ (-2 * σ) / (1 - (p : ℝ) ^ (-σ)) := by
 109  let x : ℝ := (p : ℝ) ^ (-σ)
 110  have hσ_pos : 0 < σ := by linarith
 111  have hx_pos : 0 < x := by
 112    dsimp [x]
 113    exact eigenvalue_pos hσ_pos p
 114  have hx_lt : x < 1 := by
 115    dsimp [x]
 116    exact eigenvalue_lt_one hσ_pos p
 117  have hx_abs : |x| < 1 := by
 118    simpa [abs_of_pos hx_pos] using hx_lt
 119  have hbound := Real.abs_log_sub_add_sum_range_le hx_abs 1
 120  have hsum1 : (∑ i ∈ Finset.range 1, x ^ (i + 1) / (i + 1 : ℝ)) = x := by
 121    simp
 122  have hmain : |Real.log (1 - x) + x| ≤ x ^ 2 / (1 - x) := by
 123    have htmp : |x + Real.log (1 - x)| ≤ |x| ^ 2 / (1 - |x|) := by
 124      simpa [hsum1, add_comm] using hbound
 125    simpa [add_comm, abs_of_pos hx_pos, x] using htmp
 126  have hx_sq : x ^ 2 = (p : ℝ) ^ (-2 * σ) := by
 127    dsimp [x]
 128    rw [← Real.rpow_natCast, ← Real.rpow_mul (by positivity)]
 129    ring_nf
 130  simpa [det2LogFactor, x, hx_sq] using hmain
 131
 132/-- The log-factor sum converges absolutely for σ > 1/2.
 133    This is the key convergence theorem for the regularized determinant. -/
 134theorem det2_log_summable {σ : ℝ} (hσ : 1/2 < σ) :
 135    Summable (fun (p : Nat.Primes) => |det2LogFactor p σ|) := by
 136  let C : ℝ := 1 / (1 - (2 : ℝ) ^ (-σ))
 137  have hσ_pos : 0 < σ := by linarith