@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachWeightProduct (P : Prop) : Decidable P

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachWeightProduct P = Classical.propDecidable P

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightTwelveProductRHS (A : Finset ℕ) (N : ℕ) (ε z b c T Z : ℝ) : ℤ

Exact product-indexed source, with actual coefficients and moving q fibres.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightTwelveProductRHS A N ε z b c T Z = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightTwelveBase A N z b c T - ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10ProductSupport N b c, ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Coeff N b c m) * ↑{q ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProductQFiber N ε m | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalHPoint N 1 Z (N - m * q)}.card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_twelve_product_log_scale_eventually (ε δ θ : ℝ) (hε : 0 < ε) (hεu : ε < 2 / 15) (hδ : 0 < δ) (_hθ0 : 0 ≤ θ) (hθ1 : θ < 1) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (α β γ Z : ℝ), 1 / 18 < α → α < β → β < (1 - 3 * β) / 3 → (1 - 3 * β) / 3 < γ → γ < 1 / 3 → 1 ≤ Z → Z ≤ ↑N ^ θ → ↑(goldbachWeightTwelveProductRHS (goldbachDifferenceCarrier N ε) N ε (↑N ^ α) (↑N ^ β) (↑N ^ γ) (↑N ^ (9 / 19 - ε)) Z) - δ * ↑N / Real.log ↑N ^ 2 ≤ 4 * ↑(D19 N)