theorem
proved
tactic proof
det2_log_factor_bound
show as:
view Lean formalization →
formal statement (Lean)
107theorem det2_log_factor_bound {σ : ℝ} (hσ : 1/2 < σ) (p : Nat.Primes) :
108 |det2LogFactor p σ| ≤ (p : ℝ) ^ (-2 * σ) / (1 - (p : ℝ) ^ (-σ)) := by
proof body
Tactic-mode proof.
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. -/