noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11BuchstabMass (y q : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11BuchstabMass y q = y * LiLiuPrereqBuchstab.buchstab (Real.log y / Real.log q) / Real.log q

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_buchstab_cutoff_identity {y q : ℝ} (hy : 1 < y) (hq : 1 < q) : q = y ^ (1 / (Real.log y / Real.log q))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_buchstab_source_mass_identity {y q : ℝ} (hy : 1 < y) (hq : 1 < q) : Real.log y / Real.log q * LiLiuPrereqBuchstab.buchstab (Real.log y / Real.log q) * y / Real.log y = goldbachG11BuchstabMass y q

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_buchstab_mass_pos_le {y q : ℝ} (hy : 1 < y) (hq : 1 < q) (hu : 1 ≤ Real.log y / Real.log q) : 0 < goldbachG11BuchstabMass y q ∧ goldbachG11BuchstabMass y q ≤ y / Real.log q

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_buchstab_relative_to_absolute {y q δ : ℝ} (hy : 1 < y) (hq : 1 < q) (hu : 1 ≤ Real.log y / Real.log q) (hδ : 0 < δ) (herr : |↑(LiLiuPrereqBuchstab.roughCount y q) / goldbachG11BuchstabMass y q - 1| < δ) : |↑(LiLiuPrereqBuchstab.roughCount y q) - goldbachG11BuchstabMass y q| ≤ δ * y / Real.log q

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_canonical_cofactor_lower_bound {N : ℕ} {v : GoldbachG11Label} (hN : 2 ≤ N) (hv : v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) : ↑N ^ (17 / 33) ≤ ↑N / ↑(goldbachG11LabelProd v)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_buchstab_endpoints (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1) (η : ℝ) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), have x := ↑N / ↑(goldbachG11LabelProd v); have l := ε * x; have q := ↑v.snd.snd.snd; 1 < l ∧ l ≤ x ∧ 0 < Real.log q ∧ 0 < goldbachG11BuchstabMass x q ∧ |↑(LiLiuPrereqBuchstab.roughCount x q) - goldbachG11BuchstabMass x q| ≤ η / 2 * x / Real.log q ∧ 0 < goldbachG11BuchstabMass l q ∧ |↑(LiLiuPrereqBuchstab.roughCount l q) - goldbachG11BuchstabMass l q| ≤ η / 2 * l / Real.log q

One source threshold, chosen before every canonical label, serves both endpoints. Each endpoint uses half the requested final window tolerance.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11CofactorWindow_buchstab_mass (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1) (η : ℝ) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), have x := ↑N / ↑(goldbachG11LabelProd v); have l := ε * x; have q := ↑v.snd.snd.snd; |↑(goldbachG11CofactorWindow N ε v).card - (goldbachG11BuchstabMass x q - goldbachG11BuchstabMass l q)| ≤ η * x / Real.log q

Absolute, not relative, window error: at epsilon one both the window and the difference of the two masses vanish. No output-prime counting is asserted.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11CofactorWindow_one (N : ℕ) (v : GoldbachG11Label) : goldbachG11CofactorWindow N 1 v = ∅

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11BuchstabMass_one_window (x q : ℝ) : goldbachG11BuchstabMass x q - goldbachG11BuchstabMass (1 * x) q = 0