@[instance_reducible]

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

Equations

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

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10CoeffReal (N : ℕ) (b c : ℝ) (m : ℕ) : ℝ

The literal real-valued C10 coefficient used by the finite Pan bridge.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10CoeffReal N b c m = ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Coeff N b c m)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10CoeffReal_eq_one_of_mem_productSupport {N : ℕ} {b c : ℝ} {m : ℕ} (hm : m ∈ goldbachC10ProductSupport N b c) : goldbachC10CoeffReal N b c m = 1

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.abs_goldbachC10CoeffReal_le_one (N : ℕ) (b c : ℝ) (m : ℕ) : |goldbachC10CoeffReal N b c m| ≤ 1

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10CoeffReal_ne_zero_iff {N : ℕ} {b c : ℝ} {m : ℕ} : goldbachC10CoeffReal N b c m ≠ 0 ↔ m ∈ goldbachC10ProductSupport N b c

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10CoeffReal_ne_zero_imp_one_lt {N : ℕ} {b c : ℝ} {m : ℕ} (hm0 : goldbachC10CoeffReal N b c m ≠ 0) : 1 < m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10CoeffReal_ne_zero_imp_coprime {N : ℕ} {b c : ℝ} {m : ℕ} (hm0 : goldbachC10CoeffReal N b c m ≠ 0) : m.Coprime N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProductQFiber_card_eq_primePrefix_sub {N : ℕ} {ε b c : ℝ} {m : ℕ} (hm : m ∈ goldbachC10ProductSupport N b c) (hε0 : 0 < ε) (hε1 : ε < 1) : (goldbachB10ProductQFiber N ε m).card = AnalyticNumberTheory.Sieve.primesInAPBelow N m 1 0 - AnalyticNumberTheory.Sieve.primesInAPBelow ⌊ε * ↑N⌋₊ m 1 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProductResidueQFiber_card_eq_primePrefix_sub {N d : ℕ} {ε b c : ℝ} {m : ℕ} (hm : m ∈ goldbachC10ProductSupport N b c) (hmd : m.Coprime d) (hε0 : 0 < ε) (hε1 : ε < 1) : (goldbachB10ProductResidueQFiber N d ε m).card = AnalyticNumberTheory.Sieve.primesInAPBelow N m d (N % d) - AnalyticNumberTheory.Sieve.primesInAPBelow ⌊ε * ↑N⌋₊ m d (N % d)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PanAPPrefixCount (N Y A₁ A₂ d l : ℕ) (b c : ℝ) : ℝ

The fixed-source Pan AP prefix count with the actual real coefficient goldbachC10CoeffReal N b c.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PanAPPrefixCount N Y A₁ A₂ d l b c = ∑ m ∈ Finset.Ioc A₁ A₂, if m.Coprime d then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10CoeffReal N b c m * ↑(AnalyticNumberTheory.Sieve.primesInAPBelow Y m d l) else 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10DivisorAtoms_card_eq_panAPPrefixCount_sub {N d A₁ A₂ : ℕ} {ε b c : ℝ} (hd : 1 ≤ d) (hdN : d.Coprime N) (hε0 : 0 < ε) (hε1 : ε < 1) (hsupp : ∀ ⦃m : ℕ⦄, m ∈ goldbachC10ProductSupport N b c → m ∈ Finset.Ioc A₁ A₂) : ↑(goldbachB10DivisorAtoms N d ε b c).card = goldbachB10PanAPPrefixCount N N A₁ A₂ d (N % d) b c - goldbachB10PanAPPrefixCount N ⌊ε * ↑N⌋₊ A₁ A₂ d (N % d) b c

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PanKappa0 : ℝ

The Pan main-term normalization used for the exact B10 remainder bridge.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PanKappa0 = 2 / Real.log 2

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PanMainPrefix (N Y A₁ A₂ d : ℕ) (b c : ℝ) : ℝ

The interval main-term prefix built from the literal coefficient goldbachC10CoeffReal N b c.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PanMainPrefix N Y A₁ A₂ d b c = ∑ m ∈ Finset.Ioc A₁ A₂, if m.Coprime d then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10CoeffReal N b c m * (MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PanKappa0 (↑Y / ↑m) / ↑d.totient) else 0

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PanPrefixRemainder (N d A₁ A₂ : ℕ) (ε b c : ℝ) : ℝ

The actual finite B10 remainder written with the same source coefficient goldbachC10CoeffReal N b c and the same lower residue N % d.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PanPrefixRemainder N d A₁ A₂ ε b c = ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10DivisorAtoms N d ε b c).card - (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PanMainPrefix N N A₁ A₂ d b c - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PanMainPrefix N ⌊ε * ↑N⌋₊ A₁ A₂ d b c)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.liuMainPanCoprimeIntervalSum_eq_prefixCount_sub_mainPrefix (N Y A₁ A₂ d l : ℕ) (b c : ℝ) : LiuWeight.liuMainPanCoprimeIntervalSum (LiuWeight.liuLogarithmicIntegral goldbachB10PanKappa0) Y A₁ A₂ d l (goldbachC10CoeffReal N b c) = goldbachB10PanAPPrefixCount N Y A₁ A₂ d l b c - goldbachB10PanMainPrefix N Y A₁ A₂ d b c

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PanPrefixRemainder_eq_panErrors_sub {N d A₁ A₂ : ℕ} {ε b c : ℝ} (hd : 1 ≤ d) (hdN : d.Coprime N) (hε0 : 0 < ε) (hε1 : ε < 1) (hsupp : ∀ ⦃m : ℕ⦄, m ∈ goldbachC10ProductSupport N b c → m ∈ Finset.Ioc A₁ A₂) : goldbachB10PanPrefixRemainder N d A₁ A₂ ε b c = LiuWeight.liuMainPanCoprimeIntervalSum (LiuWeight.liuLogarithmicIntegral goldbachB10PanKappa0) N A₁ A₂ d (N % d) (goldbachC10CoeffReal N b c) - LiuWeight.liuMainPanCoprimeIntervalSum (LiuWeight.liuLogarithmicIntegral goldbachB10PanKappa0) ⌊ε * ↑N⌋₊ A₁ A₂ d (N % d) (goldbachC10CoeffReal N b c)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.abs_goldbachB10PanPrefixRemainder_le {N d A₁ A₂ : ℕ} {ε b c : ℝ} (hd : 1 ≤ d) (hdN : d.Coprime N) (hε0 : 0 < ε) (hε1 : ε < 1) (hsupp : ∀ ⦃m : ℕ⦄, m ∈ goldbachC10ProductSupport N b c → m ∈ Finset.Ioc A₁ A₂) : |goldbachB10PanPrefixRemainder N d A₁ A₂ ε b c| ≤ |LiuWeight.liuMainPanCoprimeIntervalSum (LiuWeight.liuLogarithmicIntegral goldbachB10PanKappa0) N A₁ A₂ d (N % d) (goldbachC10CoeffReal N b c)| + |LiuWeight.liuMainPanCoprimeIntervalSum (LiuWeight.liuLogarithmicIntegral goldbachB10PanKappa0) ⌊ε * ↑N⌋₊ A₁ A₂ d (N % d) (goldbachC10CoeffReal N b c)|