noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logLower (r : ℝ) : ℝ

Fixed odd-log expansion; the order is fixed before endpoint arithmetic.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logLower r = 2 * ∑ i ∈ Finset.range 32, ((r - 1) / (r + 1)) ^ (2 * i + 1) / ↑(2 * i + 1)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logUpper (r : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logUpper r = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logLower r + 2 * ((r - 1) / (r + 1)) ^ 65 / (1 - ((r - 1) / (r + 1)) ^ 2)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.log_bounds {r : ℝ} (hr : 1 ≤ r) : logLower r ≤ Real.log r ∧ Real.log r ≤ logUpper r

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.scaled_log_bounds {r : ℝ} (hr : 1 ≤ r) (m : ℕ) : logLower r - ↑m * logUpper 2 ≤ Real.log (r / 2 ^ m) ∧ Real.log (r / 2 ^ m) ≤ logUpper r - ↑m * logLower 2