@[reducible, inline]

abbrev MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11Label : Type

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11Label = ((_ : ℕ) × (_ : ℕ) × (_ : ℕ) × ℕ)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Labels (N : ℕ) (z b : ℝ) : Finset GoldbachG11Label

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Labels N z b = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N z b).sigma fun (t : ℕ) => (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N z ↑t).sigma fun (s : ℕ) => (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N z ↑s).sigma fun (r : ℕ) => MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N ↑r ↑s

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd (v : GoldbachG11Label) : ℕ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v = v.snd.snd.fst * v.snd.snd.snd * v.snd.fst * v.fst

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Labels_sum (N : ℕ) (z b : ℝ) (f : GoldbachG11Label → ℤ) : ∑ v ∈ goldbachG11Labels N z b, f v = ∑ t ∈ goldbachClosedPrimes N z b, ∑ s ∈ goldbachClosedPrimes N z ↑t, ∑ r ∈ goldbachClosedPrimes N z ↑s, ∑ q ∈ goldbachClosedPrimes N ↑r ↑s, f ⟨t, ⟨s, ⟨r, q⟩⟩⟩

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11_eq_label_sum (A : Finset ℕ) (N : ℕ) (z b : ℝ) : goldbachWeightG11 A N z b = ∑ v ∈ goldbachG11Labels N z b, literalH A (N * v.snd.snd.fst) (goldbachG11LabelProd v) ↑v.snd.snd.snd

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG11Labels_iff {N r q s t : ℕ} {z b : ℝ} : ⟨t, ⟨s, ⟨r, q⟩⟩⟩ ∈ goldbachG11Labels N z b ↔ Nat.Prime r ∧ Nat.Prime q ∧ Nat.Prime s ∧ Nat.Prime t ∧ (r * q * s * t).Coprime N ∧ z ≤ ↑r ∧ r ≤ q ∧ q ≤ s ∧ s ≤ t ∧ ↑t ≤ b

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd_pos {N : ℕ} {z b : ℝ} {v : GoldbachG11Label} (hv : v ∈ goldbachG11Labels N z b) : 0 < goldbachG11LabelProd v

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_survives_one_iff (x : ℝ) (m : ℕ) : SurvivesSieve 1 x m ↔ ∀ (ell : ℕ), Nat.Prime ell → ell ∣ m → x ≤ ↑ell

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_survives_one (x : ℝ) : SurvivesSieve 1 x 1

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11QuotientPairs N ε d = {pm ∈ (Finset.range (N + 1)).product (Finset.Icc 1 N) | Nat.Prime pm.1 ∧ ↑pm.1 < (1 - ε) * ↑N ∧ pm.1 + d * pm.2 = N}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughPairs (N : ℕ) (ε : ℝ) (v : GoldbachG11Label) : Finset (ℕ × ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughPairs N ε v = {pm ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11QuotientPairs N ε (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v) | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.SurvivesSieve 1 (↑v.snd.snd.snd) pm.2}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughCount (N : ℕ) (ε : ℝ) (v : GoldbachG11Label) : ℤ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughCount N ε v = ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughPairs N ε v).card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG11QuotientPairs_iff {N d p m : ℕ} {ε : ℝ} : (p, m) ∈ goldbachG11QuotientPairs N ε d ↔ p ≤ N ∧ 1 ≤ m ∧ m ≤ N ∧ Nat.Prime p ∧ ↑p < (1 - ε) * ↑N ∧ p + d * m = N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG11RoughPairs_iff {N p m : ℕ} {ε : ℝ} {v : GoldbachG11Label} : (p, m) ∈ goldbachG11RoughPairs N ε v ↔ p ≤ N ∧ 1 ≤ m ∧ m ≤ N ∧ Nat.Prime p ∧ ↑p < (1 - ε) * ↑N ∧ p + goldbachG11LabelProd v * m = N ∧ ∀ (ell : ℕ), Nat.Prime ell → ell ∣ m → ↑v.snd.snd.snd ≤ ↑ell

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_quotient_forward {N n d : ℕ} {ε : ℝ} (hε : 0 ≤ ε) (hd : 0 < d) (hn : n ∈ goldbachDifferenceCarrier N ε) (hdn : d ∣ n) : (N - n, n / d) ∈ goldbachG11QuotientPairs N ε d

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_quotient_backward {N d p m : ℕ} {ε : ℝ} (hε : 0 ≤ ε) (hpm : (p, m) ∈ goldbachG11QuotientPairs N ε d) : d * m ∈ goldbachDifferenceCarrier N ε ∧ d ∣ d * m ∧ N - d * m = p

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_quotient_cast {N n d : ℕ} {ε : ℝ} (hε : 0 ≤ ε) (hd : 0 < d) (hn : n ∈ goldbachDifferenceCarrier N ε) (hdn : d ∣ n) : ↑(n / d) = ↑n / ↑d ∧ ↑(N - n) + ↑d * ↑(n / d) = ↑N

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11QuotientEquiv (N : ℕ) (ε : ℝ) (d : ℕ) (hε : 0 ≤ ε) (hd : 0 < d) : { n : ℕ // n ∈ goldbachDifferenceCarrier N ε ∧ d ∣ n } ≃ ↥(goldbachG11QuotientPairs N ε d)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11QuotientEquiv N ε d hε hd = { toFun := fun (n : { n : ℕ // n ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachDifferenceCarrier N ε ∧ d ∣ n }) => ⟨(N - ↑n, ↑n / d), ⋯⟩, invFun := fun (pm : ↥(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11QuotientPairs N ε d)) => ⟨d * (↑pm).2, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughCount_eq_filter (N : ℕ) (ε : ℝ) (v : GoldbachG11Label) (hε : 0 ≤ ε) (hv : 0 < goldbachG11LabelProd v) : goldbachG11RoughCount N ε v = ↑{n ∈ goldbachDifferenceCarrier N ε | goldbachG11LabelProd v ∣ n ∧ SurvivesSieve 1 (↑v.snd.snd.snd) (n / goldbachG11LabelProd v)}.card