theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ExpandedPrimeWindow_product_nat {N m p : ℕ} {ρ : ℝ} (hρ : 1 ≤ ρ) (hρu : ρ ≤ 5 / 4) (hp : p ∈ goldbachG11ExpandedPrimeWindow N ρ m) : m * p ≤ 2 * N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Expanded_divisor_cards {N : ℕ} (hN : 4 ≤ N) {ρ : ℝ} (hρ : 1 ≤ ρ) (hρu : ρ ≤ 5 / 4) : ∑ m ∈ goldbachG11ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), ↑{p ∈ goldbachG11ExpandedPrimeWindow N ρ m | p ∣ N}.card ≤ 42 * ↑N / ↑N ^ (4 / 53)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Expanded_divisor_mass {N : ℕ} (hN : 4 ≤ N) {ρ : ℝ} (hρ : 1 ≤ ρ) (hρu : ρ ≤ 5 / 4) (h : ℝ → ℝ) (H : ℝ) (hH : 0 ≤ H) (hh : ∀ (r : ℝ), h r ≤ H) : (goldbachG11ExpandedMotherSlice N ρ h fun (x p : ℕ) => p ∣ N) ≤ 16800 * H * ↑N / ↑N ^ (4 / 53)