theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12WeightedSource_eq_good_add_bad (N : ℕ) (ε : ℝ) (w : ℕ → ℝ) : goldbachG12WeightedSource N ε w = goldbachG12WeightedGood N ε w + goldbachG12WeightedBad N ε w

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12WeightedBad_le {N : ℕ} (hN : 4 ≤ N) (ε C : ℝ) (hC : 0 ≤ C) (w : ℕ → ℝ) (hw : ∀ (r : ℕ), w r ≤ C) : goldbachG12WeightedBad N ε w ≤ C * (21 * ↑N / ↑N ^ (4 / 53))

Only the exceptional prime-divisor part is replaced by a constant weight.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12WeightedSource_le_fullRough {N : ℕ} (hN : 4 ≤ N) (ε C : ℝ) (hC : 0 ≤ C) (w : ℕ → ℝ) (hw : ∀ (r : ℕ), 0 ≤ w r) (hwC : ∀ (r : ℕ), w r ≤ C) : 400 * goldbachG12WeightedSource N ε w ≤ goldbachG12WeightedRough N w + 8400 * C * ↑N / ↑N ^ (4 / 53)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorPrimeWeight (N r : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorPrimeWeight N r = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorWeight (Real.log ↑r / Real.log ↑N)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorSource_le_fullRough {N : ℕ} (hN : 4 ≤ N) (ε : ℝ) : 400 * goldbachG12WeightedSource N ε (goldbachG12AuthorPrimeWeight N) ≤ goldbachG12WeightedRough N (goldbachG12AuthorPrimeWeight N) + 67200 * ↑N / ↑N ^ (4 / 53)

Author weight retained in the entire good mother; eight occurs only in the error.