@[instance_reducible]

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

Equations

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

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.largePrimeDivisors (n : ℕ) (z : ℝ) : Finset ℕ

The distinct prime divisors of n that lie at or above the real cutoff z.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.largePrimeDivisors n z = {p ∈ n.primeFactors | z ≤ ↑p}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.largePrimeDivisors_card_le_twenty {n N : ℕ} {κ : ℝ} (hn1 : 1 ≤ n) (hnN : n < N) (hk : 1 / 21 < κ) : (largePrimeDivisors n (↑N ^ κ)).card ≤ 20

The filtered set of distinct prime divisors above N^κ has cardinality at most 20 once 1 ≤ n < N and 1 / 21 < κ.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.card_filter_dvd_le_div (A : Finset ℕ) (N d : ℕ) (hA : ∀ n ∈ A, 1 ≤ n ∧ n ≤ N) (hd : 0 < d) : {n ∈ A | d ∣ n}.card ≤ N / d

Generic finite divisibility fibre bound on a bounded positive carrier.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.card_filter_dvd_le_div_real (A : Finset ℕ) (N d : ℕ) (hA : ∀ n ∈ A, 1 ≤ n ∧ n ≤ N) (hd : 0 < d) : ↑{n ∈ A | d ∣ n}.card ≤ ↑N / ↑d

Real-valued version of the divisibility fibre bound.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachSquarePrimes (N : ℕ) (z : ℝ) : Finset ℕ

Prime carrier for the actual square mass QA(A,N,z).

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachSquarePrimes N z = {q ∈ Finset.range (N + 1) | Nat.Prime q ∧ z ≤ ↑q ∧ q ^ 2 ≤ N}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachSquarePrimes_iff {N q : ℕ} {z : ℝ} : q ∈ goldbachSquarePrimes N z ↔ Nat.Prime q ∧ z ≤ ↑q ∧ q ^ 2 ≤ N

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

Actual square-divisibility mass QA(A,N,z).

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachQA A N z = ∑ q ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachSquarePrimes N z, ↑{n ∈ A | q ^ 2 ∣ n}.card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachQA_nonneg (A : Finset ℕ) (N : ℕ) (z : ℝ) : 0 ≤ goldbachQA A N z

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachQA_real_le_two_mul_div (A : Finset ℕ) (N : ℕ) (z : ℝ) (hA : ∀ n ∈ A, 1 ≤ n ∧ n < N) (hz : 2 ≤ z) : ↑(goldbachQA A N z) ≤ 2 * ↑N / z

Actual square mass QA(A,N,z) is bounded by 2N / z on any finite carrier of positive integers below N.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachQ_le_goldbachQA (A : Finset ℕ) (N : ℕ) (z y : ℝ) (hA : ∀ n ∈ A, 1 ≤ n ∧ n < N) : goldbachQ A N z y ≤ goldbachQA A N z

The actual diagonal square term Q is bounded by the square mass QA.