@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableB10CommonRemainder (P : Prop) : Decidable P

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableB10CommonRemainder P = Classical.propDecidable P

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10CommonRemainder (N d : ℕ) (ε b c : ℝ) : ℝ

The actual common main-term remainder, with the divisor gate removed from the main mass.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10CommonRemainder N d ε b c = ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10DivisorAtoms N d ε b c).card - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainMass N ε b c / ↑d.totient

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainWeight_sum_gateLoss_le_logCube (ε γ : ℝ) (hε : 0 < ε) (hεlt : ε < 1) (hγ : γ < 1 / 3) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (β : ℝ), 1 / 18 < β → ∀ Q ≤ N, ∑ d ∈ Finset.Icc 1 Q, gateLoss N (↑N ^ β) (↑N ^ γ) (goldbachB10MainWeight N ε) d ≤ 4 * (↑N / Real.log 2) / ↑N ^ β * (1 + Real.log ↑N) ^ 3

Instantiation of the generic gate-loss budget to the actual floor-endpoint B10 main weight.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainWeight_sum_gateLoss_log_saving (ε γ U : ℝ) (hε : 0 < ε) (hεlt : ε < 1) (hγ : γ < 1 / 3) (_hU : 0 < U) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (β : ℝ), 1 / 18 < β → ∀ Q ≤ N, ∑ d ∈ Finset.Icc 1 Q, gateLoss N (↑N ^ β) (↑N ^ γ) (goldbachB10MainWeight N ε) d ≤ ↑N / Real.log ↑N ^ U

The actual main-weight gate loss is uniformly absorbed by any prescribed log-saving, without requiring beta to stay a fixed distance away from 1 / 18.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10CommonRemainder_eq_panPrefixRemainder_sub_deletedMain {N A₁ A₂ d : ℕ} {ε b c : ℝ} (hsupp : ∀ ⦃m : ℕ⦄, m ∈ goldbachC10ProductSupport N b c → m ∈ Finset.Ioc A₁ A₂) : goldbachB10CommonRemainder N d ε b c = goldbachB10PanPrefixRemainder N d A₁ A₂ ε b c - (∑ m ∈ goldbachC10ProductSupport N b c with ¬m.Coprime d, goldbachB10MainWeight N ε m) / ↑d.totient

Exact bridge from the production Pan remainder to the common remainder, retaining the signed deleted main-term contribution.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.abs_goldbachB10CommonRemainder_le {N A₁ A₂ d : ℕ} {ε b c : ℝ} (hsupp : ∀ ⦃m : ℕ⦄, m ∈ goldbachC10ProductSupport N b c → m ∈ Finset.Ioc A₁ A₂) : |goldbachB10CommonRemainder N d ε b c| ≤ |goldbachB10PanPrefixRemainder N d A₁ A₂ ε b c| + gateLoss N b c (goldbachB10MainWeight N ε) d

Triangle-inequality comparison between the common remainder and the production Pan-prefix remainder plus the explicit gate-loss term.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10CommonRemainder_log_saving (U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∀ (ε γ : ℝ), 0 < ε → ε < 1 → γ < 1 / 3 → ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (β : ℝ), 1 / 18 < β → ∑ d ∈ Finset.Icc 1 (LiuWeight.panModulusCutoff N (B + 1)) with d.Coprime N, |goldbachB10CommonRemainder N d ε (↑N ^ β) (↑N ^ γ)| ≤ C * ↑N / Real.log ↑N ^ U

Final actual common-remainder bound, obtained by combining the production Pan remainder estimate with the finite gate-loss budget for the removed non-coprime main mass.