noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.highL (x : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.highL x = 2 * ∑ k ∈ Finset.range 10, x ^ (2 * k + 1) / (2 * ↑k + 1) + 9 / 4 * x ^ 21

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.highG (x : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.highG x = 3 * (∑ k ∈ Finset.range 96, (3 * x) ^ k + 9 / 2 * (3 * x) ^ 96)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.highF (x : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.highF x = Real.log ((1 + x) / (1 - x)) * (3 / (1 - 3 * x))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.highL_bounds {x : ℝ} (hx : x ∈ Set.Icc 0 (7 / 27)) : Real.log ((1 + x) / (1 - x)) ≤ highL x ∧ highL x ≤ Real.log ((1 + x) / (1 - x)) + 1 / 1000000000

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.highG_identity (x : ℝ) : highG x * (1 - 3 * x) = 3 + 3 / 2 * (3 * x) ^ 96 * (7 - 27 * x)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.highG_bounds {x : ℝ} (hx : x ∈ Set.Icc 0 (7 / 27)) : 3 / (1 - 3 * x) ≤ highG x ∧ highG x ≤ 3 / (1 - 3 * x) + 1 / 100000000

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.highF_enclosure {x : ℝ} (hx : x ∈ Set.Icc 0 (7 / 27)) : highF x ≤ highL x * highG x ∧ highL x * highG x ≤ highF x + 1 / 10000000