@[instance_reducible]

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

Equations

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

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8CoeffReal (N m : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8CoeffReal N m = ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Coeff N m)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8CoeffReal_eq_one_of_mem {N m : ℕ} (hm : m ∈ goldbachC8ProductSupport N) : goldbachC8CoeffReal N m = 1

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8CoeffReal_eq_zero_of_not_mem {N m : ℕ} (hm : m ∉ goldbachC8ProductSupport N) : goldbachC8CoeffReal N m = 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.abs_goldbachC8CoeffReal_le_one (N m : ℕ) : |goldbachC8CoeffReal N m| ≤ 1

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusGatedMainMass (N d : ℕ) : ℝ

The gate is retained for every modulus, not only for sieve divisors.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusGatedMainMass N d = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8ProductSupport N, if m.Coprime d then MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) (↑N / ↑m) else 0

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusRemainder (N d : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusRemainder N d = ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusDivCount N d) - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusGatedMainMass N d / ↑d.totient

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Product_mul_ne_self {N m q : ℕ} (hm : m ∈ goldbachC8ProductSupport N) : m * q ≠ N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Product_mul_lt_iff_le {N m q : ℕ} (hm : m ∈ goldbachC8ProductSupport N) : m * q < N ↔ m * q ≤ N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Product_coprime_of_dvd_output {N m q d : ℕ} (hm : m ∈ goldbachC8ProductSupport N) (hle : m * q ≤ N) (hd : d ∣ N - m * q) : m.Coprime d

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusAtom_output_dvd_iff_residue {N d : ℕ} {x : (_ : ℕ × ℕ) × ℕ} (hx : x ∈ goldbachB8PlusAtoms N) : d ∣ goldbachB8PlusOutput N x ↔ (goldbachC8Prod x.fst).Coprime d ∧ ↑x.snd = ↑N * (↑(goldbachC8Prod x.fst))⁻¹

The inverse residue is coupled to the product label, including modulus one.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusDivCount_eq_product_sum (N d : ℕ) : ↑(goldbachB8PlusDivCount N d) = ∑ m ∈ goldbachC8ProductSupport N, if m.Coprime d then ↑(AnalyticNumberTheory.Sieve.primesInAPBelow N m d (N % d)) else 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8CoeffReal_sum_eq_support {N A₁ A₂ : ℕ} (f : ℕ → ℝ) (hsupp : goldbachC8ProductSupport N ⊆ Finset.Ioc A₁ A₂) : ∑ m ∈ Finset.Ioc A₁ A₂, goldbachC8CoeffReal N m * f m = ∑ m ∈ goldbachC8ProductSupport N, f m

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusPanAPPrefixCount (N A₁ A₂ d : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusPanAPPrefixCount N A₁ A₂ d = ∑ m ∈ Finset.Ioc A₁ A₂, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8CoeffReal N m * if m.Coprime d then ↑(AnalyticNumberTheory.Sieve.primesInAPBelow N m d (N % d)) else 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusDivCount_eq_panAPPrefixCount {N A₁ A₂ d : ℕ} (_hd : 1 ≤ d) (_hdN : d.Coprime N) (hsupp : goldbachC8ProductSupport N ⊆ Finset.Ioc A₁ A₂) : ↑(goldbachB8PlusDivCount N d) = goldbachB8PlusPanAPPrefixCount N A₁ A₂ d

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusRemainder_eq_panError {N A₁ A₂ d : ℕ} (_hd : 1 ≤ d) (_hdN : d.Coprime N) (hsupp : goldbachC8ProductSupport N ⊆ Finset.Ioc A₁ A₂) : goldbachB8PlusRemainder N d = LiuWeight.liuMainPanCoprimeIntervalSum (LiuWeight.liuLogarithmicIntegral (2 / Real.log 2)) N A₁ A₂ d (N % d) (goldbachC8CoeffReal N)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8ProductSupport_mem_panInterval {N : ℕ} {B : ℝ} (hN : 2 ≤ N) (hlow : LiuWeight.liuPanSourceIntervalLower N B < LiuWeight.liuSourceZ10 N) : goldbachC8ProductSupport N ⊆ Finset.Ioc (LiuWeight.liuPanSourceIntervalLower N B) (LiuWeight.liuPanSourceIntervalUpper N)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8ProductSupport_eventually_panInterval (B : ℝ) : ∀ᶠ (N : ℕ) in Filter.atTop, goldbachC8ProductSupport N ⊆ Finset.Ioc (LiuWeight.liuPanSourceIntervalLower N B) (LiuWeight.liuPanSourceIntervalUpper N)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusRemainder_abs_le_maxL {N A₁ A₂ d : ℕ} (hd : 1 ≤ d) (hdN : d.Coprime N) (hsupp : goldbachC8ProductSupport N ⊆ Finset.Ioc A₁ A₂) : |goldbachB8PlusRemainder N d| ≤ LiuWeight.liuMainPanCoprimeIntervalMaxL (LiuWeight.liuLogarithmicIntegral (2 / Real.log 2)) N A₁ A₂ d (goldbachC8CoeffReal N)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusRemainder_log_saving (U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∑ d ∈ Finset.Icc 1 (LiuWeight.panModulusCutoff N B) with d.Coprime N, |goldbachB8PlusRemainder N d| ≤ C * ↑N / Real.log ↑N ^ U

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8ProductSupport_coprime_of_dvd_prodPrimes {N m d : ℕ} {Z : ℝ} (hm : m ∈ goldbachC8ProductSupport N) (hZ : Z ≤ ↑N ^ (3 / 11)) (hd : d ∣ goldbachB10ProdPrimes N Z) : m.Coprime d

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusGatedMainMass_eq_mainMass_of_dvd_prodPrimes {N d : ℕ} {Z : ℝ} (hZ : Z ≤ ↑N ^ (3 / 11)) (hd : d ∣ goldbachB10ProdPrimes N Z) : goldbachB8PlusGatedMainMass N d = goldbachB8PlusMainMass N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusBoundingSieve_rem_eq_remainder {N d : ℕ} (hEven : Even N) {Z : ℝ} (hZ : Z ≤ ↑N ^ (3 / 11)) (hd : d ∣ goldbachB10ProdPrimes N Z) : BoundingSieve.rem d = goldbachB8PlusRemainder N d

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusBoundingSieve_remainder_log_saving (U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N), ∀ Z ≤ ↑N ^ (3 / 11), ∑ d ∈ Finset.Icc 1 (LiuWeight.panModulusCutoff N B) with d ∣ goldbachB10ProdPrimes N Z, |BoundingSieve.rem d| ≤ C * ↑N / Real.log ↑N ^ U

The actual sieve remainder contract for the next upper-sieve step.