@[instance_reducible]

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

Equations

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

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

The corrected closed pair carrier for the finite G10 switch.

Equations

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachC10Pairs_iff {N : ℕ} {b c : ℝ} {rs : ℕ × ℕ} : rs ∈ goldbachC10Pairs N b c ↔ Nat.Prime rs.1 ∧ Nat.Prime rs.2 ∧ (rs.1 * rs.2).Coprime N ∧ b ≤ ↑rs.1 ∧ ↑rs.1 ≤ c ∧ c ≤ ↑rs.2 ∧ rs.1 * rs.2 ^ 2 ≤ N

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod (rs : ℕ × ℕ) : ℕ

The product label attached to a corrected G10 pair.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod rs = rs.1 * rs.2

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Cutoff (N : ℕ) (rs : ℕ × ℕ) : ℝ

The literal square-root cutoff attached to a corrected G10 pair.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Cutoff N rs = √(↑N / ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod rs))

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10Corrected (A : Finset ℕ) (N : ℕ) (b c : ℝ) : ℤ

The corrected literal finite G10 sum, keeping the modulus N*r*s.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10Corrected A N b c = ∑ rs ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Pairs N b c, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH A (N * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod rs) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod rs) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Cutoff N rs)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10CorrectedFiber (A : Finset ℕ) (N : ℕ) (rs : ℕ × ℕ) : Finset ℕ

The corrected G10 fibre above a fixed pair label.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10CorrectedFiber A N rs = Finset.filter (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalHPoint (N * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod rs) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod rs) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Cutoff N rs)) A

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

Pair-labelled corrected G10 atoms.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10CorrectedAtoms A N b c = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Pairs N b c).sigma (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10CorrectedFiber A N)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10Corrected_eq_card_atoms (A : Finset ℕ) (N : ℕ) (b c : ℝ) : goldbachG10Corrected A N b c = ↑(goldbachG10CorrectedAtoms A N b c).card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG10CorrectedAtoms_iff {A : Finset ℕ} {N : ℕ} {b c : ℝ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachG10CorrectedAtoms A N b c ↔ x.fst ∈ goldbachC10Pairs N b c ∧ x.snd ∈ A ∧ literalHPoint (N * goldbachC10Prod x.fst) (goldbachC10Prod x.fst) (goldbachC10Cutoff N x.fst) x.snd

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

The pair-labelled actual corrected G10 atoms, with the literal difference carrier.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10ActualAtoms N ε b c = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10CorrectedAtoms (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachDifferenceCarrier N ε) N b c

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG10ActualAtoms_iff {N : ℕ} {ε b c : ℝ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachG10ActualAtoms N ε b c ↔ x.fst ∈ goldbachC10Pairs N b c ∧ x.snd ∈ goldbachDifferenceCarrier N ε ∧ literalHPoint (N * goldbachC10Prod x.fst) (goldbachC10Prod x.fst) (goldbachC10Cutoff N x.fst) x.snd

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachDifferenceCarrier_iff_exists {N : ℕ} {ε : ℝ} {n : ℕ} : n ∈ goldbachDifferenceCarrier N ε ↔ ∃ p ∈ goldbachPrimeCarrier N ε, n = N - p

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachDifferenceCarrier_prime_data {N n : ℕ} {ε : ℝ} (hε : 0 < ε) (hn : n ∈ goldbachDifferenceCarrier N ε) : ∃ (p : ℕ), Nat.Prime p ∧ ↑p < (1 - ε) * ↑N ∧ n = N - p

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10DifferenceCarrier_bounds {N n : ℕ} {ε : ℝ} (hε : 0 < ε) (hn : n ∈ goldbachDifferenceCarrier N ε) : 1 ≤ n ∧ n < N ∧ ε * ↑N < ↑n

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

The strict actual bad atoms in the corrected G10 carrier.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10BadActualAtoms N ε b c = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10ActualAtoms N ε b c | ¬x.snd.Coprime N}

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

The actual non-bad corrected G10 atoms.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10NonbadActualAtoms N ε b c = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10ActualAtoms N ε b c | x.snd.Coprime N}

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

The corrected G10 atoms with an r²-exception removed from the actual carrier.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10RSquareActualAtoms N ε b c = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10NonbadActualAtoms N ε b c | x.fst.1 ^ 2 ∣ x.snd}

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

The actual corrected G10 atoms remaining after the r² split.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10NoRSquareActualAtoms N ε b c = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10NonbadActualAtoms N ε b c | ¬x.fst.1 ^ 2 ∣ x.snd}

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

The corrected G10 atoms with an s²-exception removed from the actual carrier.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10SSquareActualAtoms N ε b c = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10NoRSquareActualAtoms N ε b c | x.fst.2 ^ 2 ∣ x.snd}

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

The good actual corrected G10 atoms.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10GoodActualAtoms N ε b c = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10NoRSquareActualAtoms N ε b c | ¬x.fst.2 ^ 2 ∣ x.snd}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG10BadActualAtoms_iff {N : ℕ} {ε b c : ℝ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachG10BadActualAtoms N ε b c ↔ x ∈ goldbachG10ActualAtoms N ε b c ∧ ¬x.snd.Coprime N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG10NonbadActualAtoms_iff {N : ℕ} {ε b c : ℝ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachG10NonbadActualAtoms N ε b c ↔ x ∈ goldbachG10ActualAtoms N ε b c ∧ x.snd.Coprime N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG10RSquareActualAtoms_iff {N : ℕ} {ε b c : ℝ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachG10RSquareActualAtoms N ε b c ↔ x ∈ goldbachG10ActualAtoms N ε b c ∧ x.snd.Coprime N ∧ x.fst.1 ^ 2 ∣ x.snd

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG10NoRSquareActualAtoms_iff {N : ℕ} {ε b c : ℝ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachG10NoRSquareActualAtoms N ε b c ↔ x ∈ goldbachG10ActualAtoms N ε b c ∧ x.snd.Coprime N ∧ ¬x.fst.1 ^ 2 ∣ x.snd

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG10SSquareActualAtoms_iff {N : ℕ} {ε b c : ℝ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachG10SSquareActualAtoms N ε b c ↔ x ∈ goldbachG10ActualAtoms N ε b c ∧ x.snd.Coprime N ∧ ¬x.fst.1 ^ 2 ∣ x.snd ∧ x.fst.2 ^ 2 ∣ x.snd

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG10GoodActualAtoms_iff {N : ℕ} {ε b c : ℝ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachG10GoodActualAtoms N ε b c ↔ x ∈ goldbachG10ActualAtoms N ε b c ∧ x.snd.Coprime N ∧ ¬x.fst.1 ^ 2 ∣ x.snd ∧ ¬x.fst.2 ^ 2 ∣ x.snd

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

The actual cofactor attached to a corrected G10 atom.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10Cofactor x = x.snd / MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod x.fst

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10ActualAtom_eq_prod_mul_cofactor {N : ℕ} {ε b c : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hx : x ∈ goldbachG10ActualAtoms N ε b c) : x.snd = goldbachC10Prod x.fst * goldbachG10Cofactor x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10ActualAtom_fst_mem_largePrimeDivisors {N n : ℕ} {ε β γ : ℝ} (hε : 0 < ε) {rs : ℕ × ℕ} (hx : ⟨rs, n⟩ ∈ goldbachG10ActualAtoms N ε (↑N ^ β) (↑N ^ γ)) : rs.1 ∈ largePrimeDivisors n (↑N ^ β)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10ActualAtom_snd_mem_largePrimeDivisors {N n : ℕ} {ε β γ : ℝ} (hε : 0 < ε) {rs : ℕ × ℕ} (hx : ⟨rs, n⟩ ∈ goldbachG10ActualAtoms N ε (↑N ^ β) (↑N ^ γ)) : rs.2 ∈ largePrimeDivisors n (↑N ^ β)

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

The strictly labelled prime source counted fibrewise over the corrected pair carrier.

Equations

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

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

The corrected Pi10 fibre above a fixed pair label.

Equations

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

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

Pair-labelled corrected Pi10 atoms.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPi10Atoms N ε b c = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Pairs N b c).sigma (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPi10Fiber N ε)

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

The actual labelled prime source attached to the corrected pair carrier.

Equations

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPi10_eq_card_atoms (N : ℕ) (ε b c : ℝ) : goldbachPi10 N ε b c = ↑(goldbachPi10Atoms N ε b c).card

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10GoodActualAtom_pair_ne {N : ℕ} {ε b c : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hx : x ∈ goldbachG10GoodActualAtoms N ε b c) : x.fst.1 ≠ x.fst.2

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10Cofactor_coprime {N : ℕ} {ε b c : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hx : x ∈ goldbachG10GoodActualAtoms N ε b c) : (goldbachG10Cofactor x).Coprime (N * goldbachC10Prod x.fst)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10Cofactor_primeDivisor_ge_cutoff {N : ℕ} {ε b c : ℝ} {x : (_ : ℕ × ℕ) × ℕ} {p : ℕ} (hx : x ∈ goldbachG10GoodActualAtoms N ε b c) (hpPrime : Nat.Prime p) (hpdvd : p ∣ goldbachG10Cofactor x) : goldbachC10Cutoff N x.fst ≤ ↑p

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10Cofactor_prime_of_lt_sq {N : ℕ} {ε b c : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hx : x ∈ goldbachG10GoodActualAtoms N ε b c) (hq2 : 2 ≤ goldbachG10Cofactor x) (hSq : ↑(goldbachG10Cofactor x) < goldbachC10Cutoff N x.fst ^ 2) : Nat.Prime (goldbachG10Cofactor x)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10Cofactor_prime {N : ℕ} {ε β γ : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hε : 0 < ε) (hβ : 1 / 18 < β) (hβγ : β < (1 - 3 * β) / 3) (hγ : (1 - 3 * β) / 3 < γ) (hcut : 1 < ε * ↑N ^ (1 / 6)) (hx : x ∈ goldbachG10GoodActualAtoms N ε (↑N ^ β) (↑N ^ γ)) : Nat.Prime (goldbachG10Cofactor x)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10GoodActualAtoms_card_le_goldbachPi10 {N : ℕ} {ε β γ : ℝ} (hε : 0 < ε) (hβ : 1 / 18 < β) (hβγ : β < (1 - 3 * β) / 3) (hγ : (1 - 3 * β) / 3 < γ) (hcut : 1 < ε * ↑N ^ (1 / 6)) : ↑(goldbachG10GoodActualAtoms N ε (↑N ^ β) (↑N ^ γ)).card ≤ goldbachPi10 N ε (↑N ^ β) (↑N ^ γ)

The actual good corrected G10 atoms inject into the pair-labelled Pi10 source.