noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11WeightedGridMass (N : ℕ) (ε ρ : ℝ) (h : ℝ → ℝ) : ℝ

Literal expanded prime-box mass with the original product multiplicity and a weight on the actual short-prime logarithmic coordinate.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11WeightedGridMass N ε ρ h = ∑ k ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridUsed N ε ρ, ∑ v ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridLong N ε ρ k ×ˢ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridShort N ρ k, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AllPrimeWeight N v * h (Real.log ↑v.2 / Real.log ↑N)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedTotal_le_authorGrid (τ : ℝ) (hτ : 0 < τ) (A : ℕ) {ε ρ : ℝ} (hε : 0 < ε) (hεu : ε ≤ 1) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachG11GoodSwitchedTotal N ε (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ (SingularSeries.liuSingularSeries N / Real.log ↑N * goldbachG11WeightedGridMass N ε ρ fun (r : ℝ) => goldbachG11AuthorWeight r + τ) + 5 * ↑N / Real.log ↑N ^ A

Actual good G11 count with the author's weight. All distribution, sieve, level, Euler and small-output errors are supplied internally. The remaining expanded-box-to-original-Buchstab comparison is deliberately visible.