@[instance_reducible]

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

Equations

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

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

The actual finite product support of the corrected C10 carrier.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10ProductSupport N b c = Finset.image MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Pairs N b c)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachC10ProductSupport_iff {N : ℕ} {b c : ℝ} {m : ℕ} : m ∈ goldbachC10ProductSupport N b c ↔ ∃ rs ∈ goldbachC10Pairs N b c, goldbachC10Prod rs = m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Coeff_eq_one_of_mem_productSupport {N : ℕ} {b c : ℝ} {m : ℕ} (hm : m ∈ goldbachC10ProductSupport N b c) : goldbachC10Coeff N b c m = 1

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10_sum_nat_eq_sum_productSupport (N : ℕ) (b c : ℝ) (f : ℕ → ℕ) : ∑ rs ∈ goldbachC10Pairs N b c, f (goldbachC10Prod rs) = ∑ m ∈ goldbachC10ProductSupport N b c, goldbachC10Coeff N b c m * f m

Exact finite reindexing of a sum over the corrected C10 carrier by the actual product support, with the genuine coefficient α(m).

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10_sum_int_eq_sum_productSupport (N : ℕ) (b c : ℝ) (f : ℕ → ℤ) : ∑ rs ∈ goldbachC10Pairs N b c, f (goldbachC10Prod rs) = ∑ m ∈ goldbachC10ProductSupport N b c, ↑(goldbachC10Coeff N b c m) * f m

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProductQFiber (N : ℕ) (ε : ℝ) (m : ℕ) : Finset ℕ

The literal q-carrier above a fixed product label m = rs, with the actual m-dependent interval εN/m < q < N/m.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProductQFiber N ε m = {q ∈ Finset.range (N + 1) | Nat.Prime q ∧ ε * ↑N / ↑m < ↑q ∧ ↑q < ↑N / ↑m}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachB10ProductQFiber_iff {N : ℕ} {ε : ℝ} {m q : ℕ} : q ∈ goldbachB10ProductQFiber N ε m ↔ q ∈ Finset.range (N + 1) ∧ Nat.Prime q ∧ ε * ↑N / ↑m < ↑q ∧ ↑q < ↑N / ↑m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Fiber_eq_productQFiber (N : ℕ) (ε : ℝ) (rs : ℕ × ℕ) : goldbachB10Fiber N ε rs = goldbachB10ProductQFiber N ε (goldbachC10Prod rs)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Atoms_card_eq_sum_productSupport (N : ℕ) (ε b c : ℝ) : (goldbachB10Atoms N ε b c).card = ∑ m ∈ goldbachC10ProductSupport N b c, goldbachC10Coeff N b c m * (goldbachB10ProductQFiber N ε m).card

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProductSiftedQFiber (N : ℕ) (ε Z : ℝ) (m : ℕ) : Finset ℕ

The literal sifted q-fibre above a fixed product label m = rs.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProductSiftedQFiber N ε Z m = {q ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProductQFiber N ε m | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalHPoint N 1 Z (N - m * q)}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftedFiber_eq_productSiftedQFiber (N : ℕ) (ε Z : ℝ) (rs : ℕ × ℕ) : goldbachB10SiftedFiber N ε Z rs = goldbachB10ProductSiftedQFiber N ε Z (goldbachC10Prod rs)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftedCount_eq_sum_productSupport (N : ℕ) (ε b c Z : ℝ) : goldbachB10SiftedCount N ε b c Z = ∑ m ∈ goldbachC10ProductSupport N b c, ↑(goldbachC10Coeff N b c m) * ↑{q ∈ goldbachB10ProductQFiber N ε m | literalHPoint N 1 Z (N - m * q)}.card

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProductResidueQFiber (N d : ℕ) (ε : ℝ) (m : ℕ) : Finset ℕ

The inverse-residue q-filter above a fixed product label m = rs.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProductResidueQFiber N d ε m = {q ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProductQFiber N ε m | ↑q = ↑N * (↑m)⁻¹}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProductResidueQFiber_eq_filter (N d : ℕ) (ε : ℝ) (m : ℕ) : goldbachB10ProductResidueQFiber N d ε m = {q ∈ goldbachB10ProductQFiber N ε m | ↑q = ↑N * (↑m)⁻¹}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachB10ProductResidueQFiber_iff {N d : ℕ} {ε : ℝ} {m q : ℕ} : q ∈ goldbachB10ProductResidueQFiber N d ε m ↔ q ∈ goldbachB10ProductQFiber N ε m ∧ ↑q = ↑N * (↑m)⁻¹

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10DivisorAtoms_card_eq_sum_productSupport {N d : ℕ} (ε b c : ℝ) (hd : 1 ≤ d) (hdN : d.Coprime N) : (goldbachB10DivisorAtoms N d ε b c).card = ∑ m ∈ goldbachC10ProductSupport N b c, goldbachC10Coeff N b c m * if m.Coprime d then (goldbachB10ProductResidueQFiber N d ε m).card else 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10ProductSupport_pos {N : ℕ} {b c : ℝ} {m : ℕ} (hm : m ∈ goldbachC10ProductSupport N b c) : 0 < m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10ProductSupport_le_rpow_half_and_lt_two_thirds {N : ℕ} {b γ : ℝ} {m : ℕ} (hN : 2 ≤ N) (hγ : γ < 1 / 3) (hm : m ∈ goldbachC10ProductSupport N b (↑N ^ γ)) : ↑m ≤ ↑N ^ ((1 + γ) / 2) ∧ ↑N ^ ((1 + γ) / 2) < ↑N ^ (2 / 3)