theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9KernelBudget_low_nonneg : 0 ≤ fouvryG9RelaxedIntegralLow

Positivity of the literal production integral, not an auxiliary integral hypothesis.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedPairKernel_final (τ : ℝ) (hτ : 0 < τ) : ∃ (δ₀ : ℝ), 0 < δ₀ ∧ δ₀ < 1 / 4 ∧ ∃ (ρ₀ : ℝ), 1 < ρ₀ ∧ ρ₀ ≤ 5 / 4 ∧ ∀ (δ : ℝ), 0 ≤ δ → δ ≤ δ₀ → ∀ (ρ : ℝ), 1 < ρ → ρ ≤ ρ₀ → ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → ρ ^ 3 * fouvryG9RelaxedPairKernel N ρ δ ≤ 9 / 5 * fouvryG9RelaxedIntegralLow + τ

All perturbations, including the actual rho cube, are paid before the N threshold.