@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachB9LowPositivePrefix (p : Prop) : Decidable p

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachB9LowPositivePrefix p = Classical.propDecidable p

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5LowFirstActualAtoms N eps = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5ActualAtoms N eps | ↑x.fst.1 < ↑N ^ (1 / 10)}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5ClosedBelow_eq_card_lowActualAtoms (N : ℕ) (eps : ℝ) : goldbachS5ClosedBelow (goldbachDifferenceCarrier N eps) N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) (↑N ^ (1 / 10)) = ↑(goldbachS5LowFirstActualAtoms N eps).card

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

The original positive-epsilon B10 mother, restricted only at the first label.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixAtoms N eps = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Atoms N eps (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) | ↑x.fst.1 < ↑N ^ (1 / 10)}

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixSiftedAtoms N eps Z = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftedAtoms N eps (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) Z | ↑x.fst.1 < ↑N ^ (1 / 10)}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixSiftedCount (N : ℕ) (eps Z : ℝ) : ℤ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixSiftedCount N eps Z = ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixSiftedAtoms N eps Z).card

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixPrimeAtoms N eps = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixAtoms N eps | Nat.Prime (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPi10Output N x)}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachB9LowPositivePrefixAtoms_iff {N : ℕ} {eps : ℝ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachB9LowPositivePrefixAtoms N eps ↔ x ∈ goldbachB10Atoms N eps (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) ∧ ↑x.fst.1 < ↑N ^ (1 / 10)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachB9LowPositivePrefixSiftedAtoms_iff {N : ℕ} {eps Z : ℝ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachB9LowPositivePrefixSiftedAtoms N eps Z ↔ x ∈ goldbachB10SiftedAtoms N eps (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) Z ∧ ↑x.fst.1 < ↑N ^ (1 / 10)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixSiftedAtoms_eq_filter (N : ℕ) (eps Z : ℝ) : goldbachB9LowPositivePrefixSiftedAtoms N eps Z = {x ∈ goldbachB9LowPositivePrefixAtoms N eps | literalHPoint N 1 Z (goldbachPi10Output N x)}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixPrimeAtoms_eq_Pi10_filter (N : ℕ) (eps : ℝ) : goldbachB9LowPositivePrefixPrimeAtoms N eps = {x ∈ goldbachPi10Atoms N eps (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) | ↑x.fst.1 < ↑N ^ (1 / 10)}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixAtoms_product_window {N : ℕ} {eps : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hx : x ∈ goldbachB9LowPositivePrefixAtoms N eps) : Nat.Prime x.snd ∧ eps * ↑N < ↑(x.fst.1 * x.fst.2 * x.snd) ∧ ↑(x.fst.1 * x.fst.2 * x.snd) < ↑N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixSiftedAtoms_product_window {N : ℕ} {eps Z : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hx : x ∈ goldbachB9LowPositivePrefixSiftedAtoms N eps Z) : Nat.Prime x.snd ∧ eps * ↑N < ↑(x.fst.1 * x.fst.2 * x.snd) ∧ ↑(x.fst.1 * x.fst.2 * x.snd) < ↑N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixAtoms_subset_B9Plus (N : ℕ) (eps : ℝ) : goldbachB9LowPositivePrefixAtoms N eps ⊆ goldbachB9PlusAtoms N

This inclusion is used only for the already-paid low-output error.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5ActualAtom_retained_epsilon {N : ℕ} {eps : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (heps : 0 < eps) (hx : x ∈ goldbachS5ActualAtoms N eps) : eps * ↑N < ↑(goldbachC9Prod x.fst * goldbachS5Cofactor x) ∧ eps * ↑N / ↑(goldbachC10Prod x.fst) < ↑(goldbachS5Cofactor x)

Retain the strict epsilon bound from the original integer, before any switch.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5LowFirstSwitch_preserves_pair (x : (_ : ℕ × ℕ) × ℕ) : (goldbachS5Switch x).fst = x.fst

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5LowFirstSwitch_mem_positivePrimeAtoms {N : ℕ} {eps : ℝ} (hN : 2 ≤ N) (heps : 0 < eps) (hcut : ↑N ^ (2 / 3) ≤ eps * ↑N) {x : (_ : ℕ × ℕ) × ℕ} (hx : x ∈ goldbachS5GoodNonsquareAtoms N eps) (hfirst : ↑x.fst.1 < ↑N ^ (1 / 10)) : goldbachS5Switch x ∈ goldbachB9LowPositivePrefixPrimeAtoms N eps

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5ClosedBelow_le_positivePrefix_sifted {N : ℕ} {eps Z : ℝ} (hN : 2 ≤ N) (heps : 0 < eps) (hcut : ↑N ^ (2 / 3) ≤ eps * ↑N) (hZ : 1 ≤ Z) : goldbachS5ClosedBelow (goldbachDifferenceCarrier N eps) N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) (↑N ^ (1 / 10)) ≤ goldbachB9LowPositivePrefixSiftedCount N eps Z + 400 * goldbachBadCount (goldbachDifferenceCarrier N eps) N + 400 * goldbachS5SquareCount N + 400 * ↑⌊Z⌋₊