noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9SmallOutputRectangle (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ × ℕ) (z : ℝ) : ℝ

The literal weighted rectangle of outputs below the real cutoff, including zero.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9SmallOutputRectangle N ρ k z = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongProducts N ρ k, ∑ n ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectanglePrimeSupport N ρ k, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongAlpha N ρ k m * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleBeta N n * if ↑(↑N - ↑m * ↑n).natAbs < z then 1 else 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g9SmallOutput_fibre_sum {ι : Type u_1} (S : Finset ι) (a : ι → ℕ) (w : ι → ℝ) (z J : ℝ) (hf : ∀ r ∈ Finset.range ⌈z⌉₊, (∑ x ∈ S, if a x = r then w x else 0) ≤ J) : (∑ x ∈ S, w x * if ↑(a x) < z then 1 else 0) ≤ ↑⌈z⌉₊ * J

Sum all small fibres; the range starts at zero and labels need not be injective.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9SmallOutputRectangle_bound {C₀ : ℝ} (hC₀ : 0 < C₀) (hfib : ∀ (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ × ℕ) (U V : Finset ℕ), ∀ r ≤ 4 * N, (∑ p ∈ U ×ˢ V, if (↑N - ↑p.1 * ↑p.2).natAbs = r then fouvryG9LongAlpha N ρ k p.1 * fouvryG9RectangleBeta N p.2 else 0) ≤ 2 * C₀ * (5 * ↑N) ^ (1 / 4)) {N : ℕ} (hN : 1 ≤ ↑N) (ρ : ℝ) (k : ℕ × ℕ × ℕ) {z : ℝ} (hz : 0 ≤ z) (hzu : z ≤ √↑N) : fouvryG9SmallOutputRectangle N ρ k z ≤ 4 * C₀ * 5 ^ (1 / 4) * ↑N ^ (1 - 1 / 4)

A single actual rectangle has the uniform three-quarter power bound.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9SmallOutput_total (A : ℕ) {ρ : ℝ} (hρ : 1 < ρ) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → ∀ (e z : ℝ), 0 ≤ z → z ≤ √↑N → ∑ k ∈ fouvryG9GridUsed N e ρ, fouvryG9SmallOutputRectangle N ρ k z ≤ ↑N / Real.log ↑N ^ A

Uniform in every real e and every cutoff in the square-root window.