Source indexedlemma · leanprover/lean4:v4.32.0

hs_lo

PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries · PrimeNumberTheoremAnd/IEANTN/LnFactorialSeries.lean:50 to 59

Mathematical statement

Exact Lean statement

lemma hs_lo : (0.834438 : ℝ) ≤
    ∑' n : ℕ, (Real.log 2) ^ (n + 1) / ((↑(n + 1) : ℝ) * ↑(n + 1).factorial)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma hs_lo : (0.834438 : ℝ) ≤    ∑' n : ℕ, (Real.log 2) ^ (n + 1) / ((↑(n + 1) : ℝ) * ↑(n + 1).factorial) := by  have h_sum_le_tsum : (∑ n ∈ Finset.range 8, (Real.log 2) ^ (n + 1) / ((↑(n + 1) : ℝ) * ↑(n + 1).factorial)) ≤      ∑' n : ℕ, (Real.log 2) ^ (n + 1) / ((↑(n + 1) : ℝ) * ↑(n + 1).factorial) :=    Summable.sum_le_tsum _ (fun _ _ => div_nonneg (by positivity) (by positivity)) summable_series  norm_num [Finset.sum_range_succ, Nat.factorial] at *  have := Real.log_two_gt_d9; norm_num at *  nlinarith [pow_pos (Real.log_pos one_lt_two) 2, pow_pos (Real.log_pos one_lt_two) 3,    pow_pos (Real.log_pos one_lt_two) 4, pow_pos (Real.log_pos one_lt_two) 5,    pow_pos (Real.log_pos one_lt_two) 6]