noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12WeightedSource (N : ℕ) (ε : ℝ) (w : ℕ → ℝ) : ℝ

Each individual first-prime coordinate keeps its weight.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12WeightedSource N ε w = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m * ∑ r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m, w r

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12WeightedGood (N : ℕ) (ε : ℝ) (w : ℕ → ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12WeightedGood N ε w = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m * ∑ r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m with ¬r ∣ N, w r

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12WeightedBad (N : ℕ) (ε : ℝ) (w : ℕ → ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12WeightedBad N ε w = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m * ∑ r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m with r ∣ N, w r

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12WeightedRough (N : ℕ) (w : ℕ → ℝ) : ℝ

Full unconditioned rough cofactor mother on the original closed cross.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12WeightedRough N w = ∑ v ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)), w v.snd.snd.fst * ↑(LiLiuPrereqBuchstab.roughCount (↑N / ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v)) ↑v.snd.snd.snd)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12GoodCross_sum_product_real (N : ℕ) (z b c : ℝ) (f : ℕ → ℝ) : ∑ u ∈ goldbachG12GoodCrossBodies N z b c, f (goldbachG11SwitchedBodyProd u) = ∑ m ∈ goldbachG12ProductSupport N z b c, ↑(goldbachG12ProductCoefficient N z b c m) * f m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12WeightedGood_le_fullRough (N : ℕ) (ε : ℝ) (w : ℕ → ℝ) (hw : ∀ (r : ℕ), 0 ≤ w r) : 400 * goldbachG12WeightedGood N ε w ≤ goldbachG12WeightedRough N w