theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.integrable_fouvryG9WeightedScaledSource : MeasureTheory.Integrable (fouvryG9WeightedSource.indicator fun (x : ℝ × ℝ) => 9 / 5 * fouvryG9WeightedIntegrand x) MeasureTheory.volume

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegralUpperSum_le_low_add_error (n : ℕ) (hn : 0 < n) (h : ℝ) (hh : 0 ≤ h) : fouvryG9RelaxedIntegralUpperSum n h 0 ≤ 9 / 5 * fouvryG9RelaxedIntegralLow + 30000 * (h + 1 / ↑n)

Uniform in every positive mesh, with the actual integral as the main term.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.exists_fouvryG9RelaxedIntegralUpperSum_le_low_add (τ : ℝ) (hτ : 0 < τ) : ∃ (n : ℕ), 0 < n ∧ ∃ (h : ℝ), 0 < h ∧ h ≤ 1 / 20 ∧ fouvryG9RelaxedIntegralUpperSum n h 0 ≤ 9 / 5 * fouvryG9RelaxedIntegralLow + τ

The mesh and boundary width are fixed before any prime-size limit.