Uniform envelopes for the actual transport costs

The family-size factor is the cardinality of the actual signed tags, bounded by the proved source estimate, not by a cardinality assumption. The remaining envelopes involve only the consumer scale and the positive power saving.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.TransportAbsorption.log_nat_le {T N : ℕ} (hTN : T ≤ N) : Real.log ↑T ≤ Real.log ↑N

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.TransportAbsorption.floor_log_bound {Q : ℝ} {N : ℕ} (hQ : Q ≤ ↑N) (hN : 1 ≤ Real.log ↑N) : 0 ≤ 1 + Real.log ↑⌊Q⌋₊ ∧ 1 + Real.log ↑⌊Q⌋₊ ≤ 2 * Real.log ↑N

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.TransportAbsorption.eventually_log_power_budget (C A : ℝ) {s : ℝ} (hs : 0 < s) : ∀ᶠ (x : ℝ) in Filter.atTop, C * Real.log x ^ A ≤ x ^ s

A fixed multiple of any real logarithmic power is eventually smaller than any positive power. The constant may in particular be exponential in ε⁻³.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.fullModulusTransportCost_le_power_envelope (upper : Bool) (P : Finset ℕ) {D ε σ : ℝ} (label : ℕ → ℕ) (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (N : ℕ) (hN : 1 ≤ Real.log ↑N) (hQ : D ^ (1 + ε + ε ^ 9) ≤ ↑N) (hpower : ↑N ^ σ ≤ D ^ ε ^ 2) {X : ℝ} (hX0 : 0 ≤ X) (hXN : X ≤ ↑N) : fullModulusTransportCost upper P D ε label N X ≤ 32 * Real.exp (8 * ε⁻¹ ^ 3) * ↑N * Real.log ↑N ^ 2 / ↑N ^ σ

A consumer-scale envelope with the actual J already paid. It is uniform in the side, prime carrier, and labelling; no primality premise is needed.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.primeProgressionTransportCost_le_power_envelope (upper : Bool) (P : Finset ℕ) {D ε σ : ℝ} (label : ℕ → ℕ) (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (I : Finset ℕ) (N : ℕ) (hI : ∀ p ∈ I, p < N) (hN : 1 ≤ Real.log ↑N) (hQ : D ^ (1 + ε + ε ^ 9) ≤ ↑N) (hpower : ↑N ^ σ ≤ D ^ ε ^ 2) : primeProgressionTransportCost upper P D ε label I N ↑I.card ≤ 32 * Real.exp (8 * ε⁻¹ ^ 3) * ↑N * Real.log ↑N ^ 2 / ↑N ^ σ + 16 * Real.exp (8 * ε⁻¹ ^ 3) * Real.log ↑N ^ 4

With the exact mass X = #I, the prime correction is at most J log⁴ N. The estimate concerns the actual cost, not a distribution discrepancy.