noncomputable def G12FineGrid.cutoffOutput (N : ℕ) (ε : ℝ) : ℝ

The original prime-output count on the retained integer cutoff slice.

Equations

• G12FineGrid.cutoffOutput N ε = 400 * ∑ p ∈ G12FineGrid.cutoffSlice N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0

theorem G12FineGrid.cutoffSlice_card {N : ℕ} (hN : 1 ≤ N) (ε : ℝ) : (cutoffSlice N ε).card ≤ N / lowCut N

A fixed short coordinate leaves at most N/r positive long coordinates.

theorem G12FineGrid.cutoffOutput_le {N : ℕ} (hN : 1 ≤ N) (ε : ℝ) : cutoffOutput N ε ≤ 400 * ↑N / ↑(lowCut N)

Dropping the output primality test is an inequality, not deletion of the slice.

theorem G12FineGrid.cutoffOutput_power {N : ℕ} (hN : 1 ≤ N) (ε : ℝ) : cutoffOutput N ε ≤ 400 * ↑N / ↑N ^ (4 / 53)

The rounded cutoff is paid by its exact positive-power lower bound.

theorem G12FineGrid.cutoffOutput_log_saving (B : ℝ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ), cutoffOutput N ε ≤ ↑N / Real.log ↑N ^ B

Arbitrary real logarithmic saving, uniformly in the original prefix.

theorem G12FineGrid.cutoffOutput_normalized (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ), cutoffOutput N ε ≤ δ * (MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The physical coefficient 400 and actual singular series both remain present.