theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LowGrid_internal_gates {δ θ ρ : ℝ} (hδ : 0 ≤ δ) (hδu : δ < 1 / 2) (hθ : 0 < θ) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ∀ (ε : ℝ), ∀ k ∈ goldbachG11LowGridUsed N ε ρ, 1 ≤ ↑N ∧ 4 ≤ ↑N ^ (4 / 53) ∧ 1 ≤ goldbachG11GridLowLevel N δ ρ k ∧ 2 ≤ LiLiuPrereqWF.externalInternalLevel (goldbachG11GridLowLevel N δ ρ k) θ ∧ goldbachG11GridLowLevel N δ ρ k ≤ ↑N

All elementary source gates are internal and uniform in the retained epsilon.

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

A common envelope for the actual primorial-to-full costs, after the tag cardinality bound, at the original N-relative level.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LowGridTransportEnvelope N ε δ θ ρ C = ∑ k ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LowGridUsed N ε ρ, Real.exp (8 * θ⁻¹ ^ 3) * (C * ↑N ^ (1 + MathlibNt.SieveTheory.LiLiuPrereqWF.g9TransportMu δ θ)) * (4 / MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridLowLevel N δ ρ k) θ ^ θ ^ 2) * (1 + Real.log ↑⌊MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridLowLevel N δ ρ k⌋₊) ^ 2

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LowGrid_transport_envelope_paid (A : ℕ) {δ θ ρ C : ℝ} (hδ : 0 ≤ δ) (hδu : δ < 1 / 2) (hθ : 0 < θ) (hθu : θ < 1 / 8) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hC : 0 < C) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ∀ (ε : ℝ), goldbachG11LowGridTransportEnvelope N ε δ θ ρ C ≤ ↑N / Real.log ↑N ^ A