@[instance_reducible]

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

Equations

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

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4ActualAtoms (N : ℕ) (eps : ℝ) : Finset ((_ : ℕ × ℕ) × ℕ)

The original integers are sifted with modulus N*r, before taking a quotient.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4ActualAtoms N eps = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Pairs N (↑N ^ (3 / 11))).sigma fun (rs : ℕ × ℕ) => Finset.filter (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalHPoint (N * rs.1) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Prod rs) ↑rs.2) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachDifferenceCarrier N eps)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachS4ActualAtoms_iff {N : ℕ} {eps : ℝ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachS4ActualAtoms N eps ↔ x.fst ∈ goldbachS4Pairs N (↑N ^ (3 / 11)) ∧ x.snd ∈ goldbachDifferenceCarrier N eps ∧ literalHPoint (N * x.fst.1) (goldbachC8Prod x.fst) (↑x.fst.2) x.snd

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4_eq_card_actualAtoms (N : ℕ) (eps : ℝ) : goldbachS4 (goldbachDifferenceCarrier N eps) N (↑N ^ (3 / 11)) = ↑(goldbachS4ActualAtoms N eps).card

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4BadAtoms (N : ℕ) (eps : ℝ) : Finset ((_ : ℕ × ℕ) × ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4BadAtoms N eps = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4ActualAtoms N eps | ¬x.snd.Coprime N}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4GoodAtoms (N : ℕ) (eps : ℝ) : Finset ((_ : ℕ × ℕ) × ℕ)

Nonbad means only coprimality of the original integer with N.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4GoodAtoms N eps = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4ActualAtoms N eps | x.snd.Coprime N}

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Cofactor (x : (_ : ℕ × ℕ) × ℕ) : ℕ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Cofactor x = x.snd / MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Prod x.fst

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4ActualAtom_factorization {N : ℕ} {eps : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hx : x ∈ goldbachS4ActualAtoms N eps) : x.snd = goldbachC8Prod x.fst * goldbachS4Cofactor x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Cofactor_two_le {N : ℕ} {eps : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hN : 2 ≤ N) (heps : 0 < eps) (hcut : ↑N ^ (2 / 3) ≤ eps * ↑N) (hx : x ∈ goldbachS4ActualAtoms N eps) : 2 ≤ goldbachS4Cofactor x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Cofactor_primeDivisor_ge {N ell : ℕ} {eps : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hx : x ∈ goldbachS4GoodAtoms N eps) (hell : Nat.Prime ell) (hd : ell ∣ goldbachS4Cofactor x) : ↑N ^ (3 / 11) ≤ ↑ell

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Cofactor_prime {N : ℕ} {eps : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hN : 2 ≤ N) (heps : 0 < eps) (hcut : ↑N ^ (2 / 3) ≤ eps * ↑N) (hx : x ∈ goldbachS4GoodAtoms N eps) : Nat.Prime (goldbachS4Cofactor x)

Four large factors cannot fit below N; repeated prime factors are retained.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusAtoms (N : ℕ) : Finset ((_ : ℕ × ℕ) × ℕ)

One full prefix, without an epsilon lower endpoint or restrictions on q relative to r,s.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusAtoms N = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Pairs N (↑N ^ (3 / 11))).sigma fun (rs : ℕ × ℕ) => {q ∈ Finset.range (N + 1) | Nat.Prime q ∧ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Prod rs * q < N}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachB8PlusAtoms_iff {N : ℕ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachB8PlusAtoms N ↔ x.fst ∈ goldbachS4Pairs N (↑N ^ (3 / 11)) ∧ Nat.Prime x.snd ∧ goldbachC8Prod x.fst * x.snd < N

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusOutput (N : ℕ) (x : (_ : ℕ × ℕ) × ℕ) : ℕ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusOutput N x = N - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Prod x.fst * x.snd

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusSiftedAtoms (N : ℕ) (Z : ℝ) : Finset ((_ : ℕ × ℕ) × ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusSiftedAtoms N Z = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusAtoms N | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalHPoint N 1 Z (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusOutput N x)}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachB8PlusSiftedAtoms_iff {N : ℕ} {Z : ℝ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachB8PlusSiftedAtoms N Z ↔ x ∈ goldbachB8PlusAtoms N ∧ SurvivesSieve N Z (goldbachB8PlusOutput N x)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusSiftedAtoms_eq_coprime_filter (N : ℕ) (Z : ℝ) : goldbachB8PlusSiftedAtoms N Z = {x ∈ goldbachB8PlusAtoms N | (goldbachB10ProdPrimes N Z).Coprime (goldbachB8PlusOutput N x)}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusPrimeAtoms (N : ℕ) : Finset ((_ : ℕ × ℕ) × ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusPrimeAtoms N = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusAtoms N | Nat.Prime (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusOutput N x)}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusOutputFiber (N p : ℕ) : Finset ((_ : ℕ × ℕ) × ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusOutputFiber N p = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusAtoms N | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusOutput N x = p}

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Switch (x : (_ : ℕ × ℕ) × ℕ) : (_ : ℕ × ℕ) × ℕ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Switch x = ⟨x.fst, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Cofactor x⟩

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Switch_output {N : ℕ} {eps : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hx : x ∈ goldbachS4ActualAtoms N eps) : goldbachB8PlusOutput N (goldbachS4Switch x) = N - x.snd

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Switch_injOn {N : ℕ} {eps : ℝ} : Set.InjOn goldbachS4Switch ↑(goldbachS4ActualAtoms N eps)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Switch_mem_primeAtoms {N : ℕ} {eps : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hN : 2 ≤ N) (heps : 0 < eps) (hcut : ↑N ^ (2 / 3) ≤ eps * ↑N) (hx : x ∈ goldbachS4GoodAtoms N eps) : goldbachS4Switch x ∈ goldbachB8PlusPrimeAtoms N ∧ eps * ↑N < ↑(goldbachC8Prod x.fst * goldbachS4Cofactor x)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4ActualAtoms_fiber_card_le_fourHundred {N n : ℕ} {eps : ℝ} (hn1 : 1 ≤ n) (hnN : n < N) : {x ∈ goldbachS4ActualAtoms N eps | x.snd = n}.card ≤ 400

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4BadAtoms_card_le {N : ℕ} {eps : ℝ} (heps : 0 < eps) : ↑(goldbachS4BadAtoms N eps).card ≤ 400 * goldbachBadCount (goldbachDifferenceCarrier N eps) N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusOutputFiber_card_le_fourHundred (N p : ℕ) : (goldbachB8PlusOutputFiber N p).card ≤ 400

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8Plus_low_card_le (N : ℕ) {Z : ℝ} (hZ : 1 ≤ Z) : ↑{x ∈ goldbachB8PlusAtoms N | ↑(goldbachB8PlusOutput N x) < Z}.card ≤ 400 * ↑⌊Z⌋₊

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8Plus_highPrime_subset_sifted (N : ℕ) (Z : ℝ) : {x ∈ goldbachB8PlusPrimeAtoms N | Z ≤ ↑(goldbachB8PlusOutput N x)} ⊆ goldbachB8PlusSiftedAtoms N Z

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusPrimeAtoms_card_le_sifted (N : ℕ) {Z : ℝ} (hZ : 1 ≤ Z) : ↑(goldbachB8PlusPrimeAtoms N).card ≤ ↑(goldbachB8PlusSiftedAtoms N Z).card + 400 * ↑⌊Z⌋₊

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4_le_sifted_B8Plus {N : ℕ} {eps Z : ℝ} (hN : 2 ≤ N) (heps : 0 < eps) (hcut : ↑N ^ (2 / 3) ≤ eps * ↑N) (hZ : 1 ≤ Z) : goldbachS4 (goldbachDifferenceCarrier N eps) N (↑N ^ (3 / 11)) ≤ ↑(goldbachB8PlusSiftedAtoms N Z).card + 400 * goldbachBadCount (goldbachDifferenceCarrier N eps) N + 400 * ↑⌊Z⌋₊

The finite switch for the actual S4, with both labelled losses paid explicitly.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.exists_goldbachS4_switch_threshold (eps : ℝ) (heps : 0 < eps) : ∃ (N0 : ℕ), 2 ≤ N0 ∧ ∀ (N : ℕ), N0 ≤ N → ↑N ^ (2 / 3) ≤ eps * ↑N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4_eventually_le_sifted_B8Plus (eps : ℝ) : 0 < eps → eps < 2 / 15 → ∃ (N0 : ℕ), 2 ≤ N0 ∧ ∀ (N : ℕ), N0 ≤ N → ∀ (Z : ℝ), 1 ≤ Z → goldbachS4 (goldbachDifferenceCarrier N eps) N (↑N ^ (3 / 11)) ≤ ↑(goldbachB8PlusSiftedAtoms N Z).card + 400 * goldbachBadCount (goldbachDifferenceCarrier N eps) N + 400 * ↑⌊Z⌋₊