noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MixedLevel (N : ℕ) (δ ρ : ℝ) (k : ℕ × ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MixedLevel N δ ρ k = if ρ ^ k.1 ≤ ↑N ^ (1 / 10) then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridLowLevel N δ ρ k else MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryLevel N δ

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridAnalyticMain (N : ℕ) (ε ρ δ θ C K : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridAnalyticMain N ε ρ δ θ C K = ∑ k ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridUsed N ε ρ, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9UpperFactor N (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MixedLevel N δ ρ k) C K θ * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9BaseEuler N √↑N * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EulerCorrection N * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridPlainMass N ε ρ k

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MixedDensity_analytic_upper : ∃ (C : ℝ), 0 < C ∧ ∃ (K : ℝ), 1 < K ∧ ∀ (δ θ : ℝ), 0 ≤ δ → δ < 1 / 4 → 0 < θ → θ < 1 / 8 → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (ε ρ : ℝ), 1 < ρ → ρ ≤ 5 / 4 → goldbachG11MixedDensityMain N ε ρ δ θ √↑N ≤ goldbachG11GridAnalyticMain N ε ρ δ θ C K

Both actual main terms are evaluated through the existing external-family analytic theorem. No progression-density gate remains on the right. All its large-level gates are proved before epsilon and the changing mesh are supplied.