eigenvalue_pos

formal source

  82  exact Real.rpow_lt_one_of_one_lt_of_neg hp_one (by linarith)
  83
  84/-- Each eigenvalue p^{−s} is positive for σ > 0. -/
  85theorem eigenvalue_pos {σ : ℝ} (hσ : 0 < σ) (p : Nat.Primes) :
  86    0 < (p : ℝ) ^ (-σ) := by
  87  exact Real.rpow_pos_of_pos (by exact_mod_cast p.prop.pos) _
  88
  89/-! ### §2. The regularized Fredholm determinant -/
  90
  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]