noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LowGridUsed (N : ℕ) (ε ρ : ℝ) : Finset (ℕ × ℕ)

The branch decision belongs to the occupied short cell, not a changed coefficient.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LowGridUsed N ε ρ = {k ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridUsed N ε ρ | ρ ^ k.1 ≤ ↑N ^ (1 / 10)}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11HighGridUsed (N : ℕ) (ε ρ : ℝ) : Finset (ℕ × ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11HighGridUsed N ε ρ = {k ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridUsed N ε ρ | ¬ρ ^ k.1 ≤ ↑N ^ (1 / 10)}

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

The actual original-N level, with the true buffered short scale.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridLowLevel N δ ρ k = ↑N ^ (5 / 9 - δ) / (2 / 3 * ρ ^ k.1) ^ (5 / 9)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LowGrid_short_upper {N : ℕ} {ε ρ : ℝ} (hρ : 1 < ρ) {k : ℕ × ℕ} (hk : k ∈ goldbachG11LowGridUsed N ε ρ) : 2 / 3 * ρ ^ k.1 ≤ ↑N ^ (1 / 10)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LowGrid_actual_rectangle_error (j A : ℕ) {ε δ : ℝ} (hε : 0 < ε) (hεu : ε ≤ 1) (hδ : 0 < δ) (hδu : δ < 1 / 2) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ∀ (ρ : ℝ), 1 < ρ → ρ ≤ 5 / 4 → ∀ k ∈ goldbachG11LowGridUsed N ε ρ, ∀ (c : ℕ → ℝ), AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable j (goldbachG11GridLowLevel N δ ρ k) c → |AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError (goldbachG11GridLong N ε ρ k) (goldbachG11GridShort N ρ k) (Finset.Ioc 0 ⌊goldbachG11GridLowLevel N δ ρ k⌋₊) (fun (m : ℕ) => ↑(goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m)) (fun (p : ℕ) => if p.Coprime N then AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta p else 0) c ↑N| ≤ goldbachG11GridPhysicalScale ρ k / Real.log (goldbachG11GridPhysicalScale ρ k) ^ A

The original-N low level and the physical Fouvry level have the same signed error for the same supported member. All geometry and the smaller analytic epsilon are supplied internally from occupied G11 cells.