@[instance_reducible]

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

Equations

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

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Point (N : ℕ) (ε : ℝ) (rs : ℕ × ℕ) (q : ℕ) : Prop

The labelled B10 point keeps the genuine Pi10 prime q and interval constraints, and drops only the primality of N - rsq.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Point N ε rs q = (Nat.Prime q ∧ ε * ↑N / ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod rs) < ↑q ∧ ↑q < ↑N / ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod rs))

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Fiber (N : ℕ) (ε : ℝ) (rs : ℕ × ℕ) : Finset ℕ

The pair-labelled B10 fibre above a fixed corrected C10 pair.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Fiber N ε rs = Finset.filter (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Point N ε rs) (Finset.range (N + 1))

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Atoms (N : ℕ) (ε b c : ℝ) : Finset ((_ : ℕ × ℕ) × ℕ)

Pair-labelled B10 atoms.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Atoms N ε b c = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Pairs N b c).sigma (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Fiber N ε)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachB10Atoms_iff {N : ℕ} {ε b c : ℝ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachB10Atoms N ε b c ↔ x.fst ∈ goldbachC10Pairs N b c ∧ x.snd ∈ Finset.range (N + 1) ∧ goldbachB10Point N ε x.fst x.snd

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

The literal output prime candidate attached to a labelled Pi10/B10 atom.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPi10Output N x = N - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod x.fst * x.snd

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftedFiber (N : ℕ) (ε Z : ℝ) (rs : ℕ × ℕ) : Finset ℕ

The sifted B10 fibre keeps the same labels and additionally requires the literal sieve condition on the output N - rsq.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftedFiber N ε Z rs = {q ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Fiber N ε rs | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalHPoint N 1 Z (N - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod rs * q)}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftedAtoms (N : ℕ) (ε b c Z : ℝ) : Finset ((_ : ℕ × ℕ) × ℕ)

Pair-labelled sifted B10 atoms.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftedAtoms N ε b c Z = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Pairs N b c).sigma (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftedFiber N ε Z)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftedCount (N : ℕ) (ε b c Z : ℝ) : ℤ

The sifted labelled B10 count.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftedCount N ε b c Z = ∑ rs ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Pairs N b c, ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftedFiber N ε Z rs).card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftedCount_eq_card_atoms (N : ℕ) (ε b c Z : ℝ) : goldbachB10SiftedCount N ε b c Z = ↑(goldbachB10SiftedAtoms N ε b c Z).card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachB10SiftedAtoms_iff {N : ℕ} {ε b c Z : ℝ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachB10SiftedAtoms N ε b c Z ↔ x.fst ∈ goldbachC10Pairs N b c ∧ x.snd ∈ Finset.range (N + 1) ∧ goldbachB10Point N ε x.fst x.snd ∧ literalHPoint N 1 Z (goldbachPi10Output N x)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPi10OutputFiber (N : ℕ) (ε b c : ℝ) (p : ℕ) : Finset ((_ : ℕ × ℕ) × ℕ)

The labelled Pi10 fibre over a fixed output value p = N - rsq.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPi10OutputFiber N ε b c p = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPi10Atoms N ε b c | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPi10Output N x = p}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachPi10OutputFiber_iff {N : ℕ} {ε b c : ℝ} {p : ℕ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachPi10OutputFiber N ε b c p ↔ x ∈ goldbachPi10Atoms N ε b c ∧ goldbachPi10Output N x = p

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPi10OutputFiber_card_le_fourHundred {N : ℕ} {ε β c : ℝ} (hβ : 1 / 18 < β) (p : ℕ) : ↑(goldbachPi10OutputFiber N ε (↑N ^ β) c p).card ≤ 400

Each fixed labelled Pi10 output fibre is bounded by 400.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPi10_le_goldbachB10SiftedCount_add_fourHundred_floor {N : ℕ} {ε β c Z : ℝ} (_hN : 2 ≤ N) (_hε : 0 < ε) (hβ : 1 / 18 < β) (hZ : 1 ≤ Z) : goldbachPi10 N ε (↑N ^ β) c ≤ goldbachB10SiftedCount N ε (↑N ^ β) c Z + 400 * ↑⌊Z⌋₊

Pi10 is bounded by the sifted labelled B10 source plus the 400 * floor(Z) low-output error.