noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.g9TransportMu (δ η : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.g9TransportMu δ η = (1 / 2 - δ) * η ^ 2 / 4

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.g9TransportMu_pos {δ η : ℝ} (hδ : δ < 1 / 2) (hη : 0 < η) : 0 < g9TransportMu δ η

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.g9Transport_internal_power {N T δ η : ℝ} (hN : 1 ≤ N) (hT : 1 ≤ T) (hTup : T ≤ N ^ (1 / 10)) (hδ : 0 ≤ δ) (hδu : δ < 1 / 2) (hη : 0 < η) (hηu : η < 1 / 8) : N ^ (2 * g9TransportMu δ η) ≤ externalInternalLevel (N ^ (5 / 9 - δ) / T ^ (5 / 9)) η ^ η ^ 2

The original external level, not a rescaled replacement, gives twice the required saving.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.g9Transport_one {N : ℕ} {T δ η C : ℝ} (hN : 1 ≤ ↑N) (hlog : 1 ≤ Real.log ↑N) (hT : 1 ≤ T) (hTup : T ≤ ↑N ^ (1 / 10)) (hδ : 0 ≤ δ) (hδu : δ < 1 / 2) (hη : 0 < η) (hηu : η < 1 / 8) (hC : 0 ≤ C) : have Q := ↑N ^ (5 / 9 - δ) / T ^ (5 / 9); Real.exp (8 * η⁻¹ ^ 3) * (C * ↑N ^ (1 + g9TransportMu δ η)) * (4 / externalInternalLevel Q η ^ η ^ 2) * (1 + Real.log ↑⌊Q⌋₊) ^ 2 ≤ 16 * Real.exp (8 * η⁻¹ ^ 3) * C * ↑N ^ (1 - g9TransportMu δ η) * Real.log ↑N ^ 2

Per-cell envelope, uniform over the whole occupied short-scale window.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.g9Transport_eventually_envelope (K : ℝ) (A : ℕ) {μ : ℝ} (hμ : 0 < μ) : ∀ᶠ (x : ℝ) in Filter.atTop, 1 ≤ x ∧ 1 ≤ Real.log x ∧ K * x ^ (1 - μ) * Real.log x ^ 5 ≤ x / Real.log x ^ A

Fixed constants and the positive power saving pay the five logarithms and any target A.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.g9Transport_grid_log_payment (δ η ρ C : ℝ) (A : ℕ) (hδ : 0 ≤ δ) (hδu : δ < 1 / 2) (hη : 0 < η) (hηu : η < 1 / 8) (hρ : 1 < ρ) (hC : 0 < C) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → ∀ (eps : ℝ) (T : ℕ × ℕ × ℕ → ℝ), (∀ k ∈ LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridUsed N eps ρ, 1 ≤ T k ∧ T k ≤ ↑N ^ (1 / 10)) → (∑ k ∈ LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridUsed N eps ρ, have Q := ↑N ^ (5 / 9 - δ) / T k ^ (5 / 9); Real.exp (8 * η⁻¹ ^ 3) * (C * ↑N ^ (1 + g9TransportMu δ η)) * (4 / externalInternalLevel Q η ^ η ^ 2) * (1 + Real.log ↑⌊Q⌋₊) ^ 2) ≤ ↑N / Real.log ↑N ^ A

Actual occupied-grid exceptional transport at the original external level. The threshold precedes arbitrary eps and all cell scales.