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

The unchanged one-dimensional kernel, without its author weight.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorKernel r = ((Real.log (4 / 33 / r) ^ 2 - 2 * Real.log (4 / 33 / r) + 2) / r - 2 / (4 / 33)) / (2 * r)

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorPrimitive0 r = (-(Real.log (4 / 33 / r) ^ 2 - 4 * Real.log (4 / 33 / r) + 6) / r + 2 * Real.log (4 / 33 / r) / (4 / 33)) / 2

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorLog_hasDerivAt {r : ℝ} (hr : 0 < r) : HasDerivAt (fun (x : ℝ) => Real.log (4 / 33 / x)) (-1 / r) r

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorPrimitive0_hasDerivAt {r : ℝ} (hr : 0 < r) : HasDerivAt g11AuthorPrimitive0 (g11AuthorKernel r) r

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorPrimitive1 r = (-Real.log (4 / 33 / r) ^ 3 / 3 + Real.log (4 / 33 / r) ^ 2 - 2 * Real.log (4 / 33 / r) - 2 * r / (4 / 33)) / 2

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorPrimitiveN (n : ℕ) (r : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorPrimitiveN n r = (r ^ (n + 1) / (↑n + 1) * (Real.log (4 / 33 / r) ^ 2 + (2 / (↑n + 1) - 2) * Real.log (4 / 33 / r) + (2 / (↑n + 1) ^ 2 - 2 / (↑n + 1) + 2)) - 2 * r ^ (n + 2) / (4 / 33 * (↑n + 2))) / 2

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorPrimitive1_hasDerivAt {r : ℝ} (hr : 0 < r) : HasDerivAt g11AuthorPrimitive1 (r * g11AuthorKernel r) r

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorPrimitiveN_hasDerivAt (n : ℕ) {r : ℝ} (hr : 0 < r) : HasDerivAt (g11AuthorPrimitiveN n) (r ^ (n + 2) * g11AuthorKernel r) r

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorMajorant r = 1 + r + ∑ n ∈ Finset.range 10, r ^ (n + 2) + 10 / 9 * r ^ 12

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorMajorantPrimitive r = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorPrimitive0 r + MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorPrimitive1 r + ∑ n ∈ Finset.range 10, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorPrimitiveN n r + 10 / 9 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorPrimitiveN 10 r

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorMajorantPrimitive_hasDerivAt {r : ℝ} (hr : 0 < r) : HasDerivAt g11AuthorMajorantPrimitive (g11AuthorMajorant r * g11AuthorKernel r) r

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorMajorant_geometric {r : ℝ} (hr : 0 ≤ r) (hrc : r ≤ 1 / 10) : 1 / (1 - r) ≤ g11AuthorMajorant r

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorKernel_nonneg {r : ℝ} (hr : 0 < r) (hrb : r ≤ 4 / 33) : 0 ≤ g11AuthorKernel r

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorKernel_continuousOn {a b : ℝ} (ha : 0 < a) : ContinuousOn g11AuthorKernel (Set.Icc a b)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.continuous_g11AuthorMajorant : Continuous g11AuthorMajorant

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorMajorant_integral {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : ∫ (r : ℝ) in a..b, g11AuthorMajorant r * g11AuthorKernel r = g11AuthorMajorantPrimitive b - g11AuthorMajorantPrimitive a

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11AuthorKernel_integral {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : ∫ (r : ℝ) in a..b, g11AuthorKernel r = g11AuthorPrimitive0 b - g11AuthorPrimitive0 a

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeIntegral_author_le_primitives : goldbachG11PrimeIntegral goldbachG11AuthorWeight ≤ 36 / 5 * (g11AuthorMajorantPrimitive (1 / 10) - g11AuthorMajorantPrimitive (4 / 53)) + 8 * (g11AuthorPrimitive0 (4 / 33) - g11AuthorPrimitive0 (1 / 10))

An unconditional analytic upper bound by explicit endpoint primitives.