noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductFirstPrimeFiber (N : ℕ) (eps z : ℝ) (m : ℕ) : Finset ℕ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductFirstPrimeFiber N eps z m = {r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N z ↑m.minFac | eps * ↑N < ↑(r * m) ∧ r * m < N ∧ Nat.Prime (N - r * m)}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG11ProductFirstPrimeFiber_iff {N m r : ℕ} {eps z : ℝ} : r ∈ goldbachG11ProductFirstPrimeFiber N eps z m ↔ Nat.Prime r ∧ ¬r ∣ N ∧ z ≤ ↑r ∧ r ≤ m.minFac ∧ eps * ↑N < ↑(r * m) ∧ r * m < N ∧ Nat.Prime (N - r * m)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FirstPrimeFiber_eq_product {N : ℕ} {eps z b : ℝ} {u : GoldbachG11SwitchedBody} (hu : u ∈ goldbachG11SwitchedBodies N z b) : goldbachG11FirstPrimeFiber N eps z u = goldbachG11ProductFirstPrimeFiber N eps z (goldbachG11SwitchedBodyProd u)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FirstPrimeFiber_eq_product_of_mem {N m : ℕ} {eps z b : ℝ} {u : GoldbachG11SwitchedBody} (hu : u ∈ goldbachG11ProductFiber N z b m) : goldbachG11FirstPrimeFiber N eps z u = goldbachG11ProductFirstPrimeFiber N eps z m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedBodies_sum_product (N : ℕ) (z b : ℝ) (f : ℕ → ℤ) : ∑ u ∈ goldbachG11GoodSwitchedBodies N z b, f (goldbachG11SwitchedBodyProd u) = ∑ m ∈ goldbachG11ProductSupport N z b, ↑(goldbachG11ProductCoefficient N z b m) * f m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedTotal_eq_product_sum (N : ℕ) (eps z b : ℝ) : goldbachG11GoodSwitchedTotal N eps z b = ∑ m ∈ goldbachG11ProductSupport N z b, ↑(goldbachG11ProductCoefficient N z b m) * ↑(goldbachG11ProductFirstPrimeFiber N eps z m).card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedTotal_eq_canonical_product_sum (N : ℕ) (eps : ℝ) : goldbachG11GoodSwitchedTotal N eps (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) = ∑ m ∈ goldbachG11ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), ↑(goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m) * ↑(goldbachG11ProductFirstPrimeFiber N eps (↑N ^ (4 / 53)) m).card