det2Factor

formal source

  91/-- The per-prime factor of det₂:
  92    det₂_factor(p, s) = (1 − p^{−s}) · exp(p^{−s}).
  93    This is entire in s. -/
  94noncomputable def det2Factor (p : ℕ) (σ : ℝ) : ℝ :=
  95  (1 - (p : ℝ) ^ (-σ)) * Real.exp ((p : ℝ) ^ (-σ))
  96
  97/-- The log of the per-prime factor:
  98    log det₂_factor = log(1 − p^{−σ}) + p^{−σ}.
  99    For |z| < 1: log(1−z) + z = −∑_{m≥2} z^m/m,
 100    so |log det₂_factor| ≤ p^{−2σ}/(1 − p^{−σ}). -/
 101noncomputable def det2LogFactor (p : ℕ) (σ : ℝ) : ℝ :=
 102  Real.log (1 - (p : ℝ) ^ (-σ)) + (p : ℝ) ^ (-σ)
 103
 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