@[instance_reducible]

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

Equations

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

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.SurvivesSieve (M : ℕ) (x : ℝ) (n : ℕ) : Prop

The literal sieve condition used in Li--Liu: every prime divisor of n which is not excluded by the modulus M lies at or above the real cutoff x. The integer n is not divided by d; the original n is filtered directly.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.SurvivesSieve M x n = ∀ (ℓ : ℕ), Nat.Prime ℓ → ℓ ∣ n → ¬ℓ ∣ M → x ≤ ↑ℓ

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalHPoint (M d : ℕ) (x : ℝ) (n : ℕ) : Prop

Pointwise membership in the literal Li--Liu fibre H(A,M,d;x).

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalHPoint M d x n = (d ∣ n ∧ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.SurvivesSieve M x n)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH (A : Finset ℕ) (M d : ℕ) (x : ℝ) : ℤ

Literal finite count H(A,M,d;x) on the original integers n ∈ A.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH A M d x = ↑(Finset.filter (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalHPoint M d x) A).card

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachBadCount (A : Finset ℕ) (N : ℕ) : ℤ

The actual bad set X(A,N) = #{n ∈ A : ¬Coprime n N}.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachBadCount A N = ↑{n ∈ A | ¬n.Coprime N}.card

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachBadPoint (N n : ℕ) : ℤ

Pointwise indicator of the bad set.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachBadPoint N n = if n.Coprime N then 0 else 1

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1 (A : Finset ℕ) (N : ℕ) (u : ℝ) : ℤ

Literal S1(A,N;u) = H(A,N,1;u).

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1 A N u = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH A N 1 u

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2Primes (N : ℕ) (T : ℝ) : Finset ℕ

The prime carrier of S2(A,N;T).

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2Primes N T = {r ∈ Finset.range (N + 1) | Nat.Prime r ∧ r.Coprime N ∧ T ≤ ↑r ∧ r ^ 2 ≤ N}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2 (A : Finset ℕ) (N : ℕ) (T : ℝ) : ℤ

Literal S2(A,N;T).

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2 A N T = ∑ r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2Primes N T, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH A N r ↑r

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Pairs (N : ℕ) (u : ℝ) : Finset (ℕ × ℕ)

The pair carrier of S4(A,N;u).

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Pairs N u = {rs ∈ (Finset.range (N + 1)).product (Finset.range (N + 1)) | Nat.Prime rs.1 ∧ Nat.Prime rs.2 ∧ (rs.1 * rs.2).Coprime N ∧ u ≤ ↑rs.1 ∧ rs.1 ≤ rs.2 ∧ rs.1 * rs.2 ^ 2 ≤ N}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4 (A : Finset ℕ) (N : ℕ) (u : ℝ) : ℤ

Literal S4(A,N;u).

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4 A N u = ∑ rs ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Pairs N u, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH A (N * rs.1) (rs.1 * rs.2) ↑rs.2

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1Point (N : ℕ) (u : ℝ) (n : ℕ) : ℤ

Pointwise S1 multiplicity at n.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1Point N u n = if MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalHPoint N 1 u n then 1 else 0

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2Point (N : ℕ) (T : ℝ) (n : ℕ) : ℤ

Pointwise S2 multiplicity at n.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2Point N T n = ↑{r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2Primes N T | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalHPoint N r (↑r) n}.card

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Point (N : ℕ) (u : ℝ) (n : ℕ) : ℤ

Pointwise S4 multiplicity at n.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Point N u n = ↑{rs ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Pairs N u | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalHPoint (N * rs.1) (rs.1 * rs.2) (↑rs.2) n}.card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH_eq_sum_indicator (A : Finset ℕ) (M d : ℕ) (x : ℝ) : literalH A M d x = ∑ n ∈ A, if literalHPoint M d x n then 1 else 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachBadCount_eq_sum_indicator (A : Finset ℕ) (N : ℕ) : goldbachBadCount A N = ∑ n ∈ A, goldbachBadPoint N n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1_eq_sum_point (A : Finset ℕ) (N : ℕ) (u : ℝ) : goldbachS1 A N u = ∑ n ∈ A, goldbachS1Point N u n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.survivesSieve_mono {M n : ℕ} {x y : ℝ} (hxy : x ≤ y) : SurvivesSieve M y n → SurvivesSieve M x n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.leastPrimeFactorAtLeast_mono {m n k : ℕ} (hmn : m ≤ n) : LeastPrimeFactorAtLeast n k → LeastPrimeFactorAtLeast m k

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachBasicWeight_nonneg_of_le {zAlpha zTau n : ℕ} (hz : zAlpha ≤ zTau) : 0 ≤ goldbachBasicWeight zAlpha zTau n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.prime_not_dvd_of_coprime {n M ℓ : ℕ} (hcop : n.Coprime M) (hℓPrime : Nat.Prime ℓ) (hℓn : ℓ ∣ n) : ¬ℓ ∣ M

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.survivesSieve_iff_leastPrimeFactorAtLeast_of_coprime {M n : ℕ} {u : ℝ} (hcop : n.Coprime M) : SurvivesSieve M u n ↔ LeastPrimeFactorAtLeast ⌈u⌉₊ n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalHPoint_one_iff_survivesSieve {M n : ℕ} {u : ℝ} : literalHPoint M 1 u n ↔ SurvivesSieve M u n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1Point_eq_indicator_of_coprime {N n : ℕ} {u : ℝ} (hcop : n.Coprime N) : goldbachS1Point N u n = if LeastPrimeFactorAtLeast ⌈u⌉₊ n then 1 else 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1Point_le_one (N n : ℕ) (u : ℝ) : goldbachS1Point N u n ≤ 1

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2Point_nonneg (N n : ℕ) (T : ℝ) : 0 ≤ goldbachS2Point N T n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Point_nonneg (N n : ℕ) (u : ℝ) : 0 ≤ goldbachS4Point N u n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachBadPoint_nonneg (N n : ℕ) : 0 ≤ goldbachBadPoint N n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachBasicWeight_ge_s1_sub_s2_sub_s4_sub_bad {N n : ℕ} {u T : ℝ} (_hEven : Even N) (hn2 : 2 ≤ n) (hnN : n < N) (_hu : 2 ≤ u) (huT : u ≤ T) : goldbachBasicWeight ⌈u⌉₊ ⌈T⌉₊ n ≥ goldbachS1Point N u n - goldbachS2Point N T n - goldbachS4Point N u n - goldbachBadPoint N n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2_eq_sum_point (A : Finset ℕ) (N : ℕ) (T : ℝ) : goldbachS2 A N T = ∑ n ∈ A, goldbachS2Point N T n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4_eq_sum_point (A : Finset ℕ) (N : ℕ) (u : ℝ) : goldbachS4 A N u = ∑ n ∈ A, goldbachS4Point N u n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachBasicFiniteRHS_ge_S1_sub_S2_sub_S4_sub_X (A : Finset ℕ) {N : ℕ} {u T : ℝ} (hEven : Even N) (hA : ∀ ⦃n : ℕ⦄, n ∈ A → 2 ≤ n ∧ n < N) (hu : 2 ≤ u) (huT : u ≤ T) : goldbachBasicFiniteRHS A ⌈u⌉₊ ⌈T⌉₊ ≥ goldbachS1 A N u - goldbachS2 A N T - goldbachS4 A N u - goldbachBadCount A N