eigenvalue_lt_one

formal source

  75
  76/-- Each eigenvalue p^{−s} has modulus < 1 for σ > 0.
  77    This ensures each factor (1 − p^{−s}) is nonzero. -/
  78theorem eigenvalue_lt_one {σ : ℝ} (hσ : 0 < σ) (p : Nat.Primes) :
  79    (p : ℝ) ^ (-σ) < 1 := by
  80  have hp_one : (1 : ℝ) < p := by
  81    exact_mod_cast p.prop.one_lt
  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