@[instance_reducible]

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

Equations

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

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1Endpoint (N : ℕ) (ε : ℝ) : ℕ

The literal integer endpoint attached to the strict carrier condition p < (1 - ε)N.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1Endpoint N ε = ⌈(1 - ε) * ↑N⌉₊ - 1

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1SiftingPrimes (N : ℕ) (z : ℝ) : Finset ℕ

The actual finite sifting-prime carrier for the literal strict cutoff ℓ < z, with the exceptional primes dividing N removed.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1SiftingPrimes N z = {p ∈ Finset.range ⌈z⌉₊ | Nat.Prime p ∧ ¬p ∣ N}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1ProdPrimes (N : ℕ) (z : ℝ) : ℕ

The corresponding finite product P_z.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1ProdPrimes N z = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1SiftingPrimes N z).prod id

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachS1SiftingPrimes_iff {N : ℕ} {z : ℝ} {p : ℕ} : p ∈ goldbachS1SiftingPrimes N z ↔ p < ⌈z⌉₊ ∧ Nat.Prime p ∧ ¬p ∣ N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1ProdPrimes_squarefree (N : ℕ) (z : ℝ) : Squarefree (goldbachS1ProdPrimes N z)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1ProdPrimes_ne_zero (N : ℕ) (z : ℝ) : goldbachS1ProdPrimes N z ≠ 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1ProdPrimes_primeFactors (N : ℕ) (z : ℝ) : (goldbachS1ProdPrimes N z).primeFactors = goldbachS1SiftingPrimes N z

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.prime_dvd_goldbachS1ProdPrimes_iff {N : ℕ} {z : ℝ} {p : ℕ} (hp : Nat.Prime p) : p ∣ goldbachS1ProdPrimes N z ↔ ↑p < z ∧ ¬p ∣ N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1ProdPrimes_coprime_N (N : ℕ) (z : ℝ) : (goldbachS1ProdPrimes N z).Coprime N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1_dvd_prodPrimes_coprime_N {N d : ℕ} {z : ℝ} (hd : d ∣ goldbachS1ProdPrimes N z) : d.Coprime N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1Endpoint_le (N : ℕ) {ε : ℝ} (hε : 0 ≤ ε) : goldbachS1Endpoint N ε ≤ N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1Endpoint_add_one {N : ℕ} {ε : ℝ} (hm : 2 ≤ goldbachS1Endpoint N ε) : goldbachS1Endpoint N ε + 1 = ⌈(1 - ε) * ↑N⌉₊

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachPrimeCarrier_iff_prime_le_goldbachS1Endpoint {N p : ℕ} {ε : ℝ} (hε : 0 ≤ ε) (hm : 2 ≤ goldbachS1Endpoint N ε) : p ∈ goldbachPrimeCarrier N ε ↔ Nat.Prime p ∧ p ≤ goldbachS1Endpoint N ε

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1_coprime_prodPrimes_iff_literalHPoint (N : ℕ) (z : ℝ) (n : ℕ) : (goldbachS1ProdPrimes N z).Coprime n ↔ literalHPoint N 1 z n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1_mod_mem_unitResidues {N d : ℕ} {z : ℝ} (hd : d ∣ goldbachS1ProdPrimes N z) : N % d ∈ AnalyticNumberTheory.Sieve.unitResidues d

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1BoundingSieve (N : ℕ) (hEven : Even N) (ε z : ℝ) : BoundingSieve

The actual finite S1 sieve on the genuine difference carrier, with unit weights, the genuine mass Li(m), and the true Goldbach local density.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1BoundingSieve N hEven ε z = { support := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachDifferenceCarrier N ε, prodPrimes := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1ProdPrimes N z, prodPrimes_squarefree := ⋯, weights := fun (x : ℕ) => 1, weights_nonneg := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1BoundingSieve._proof_1, totalMass := MathlibNt.SieveTheory.BombieriVinogradov.trueLogarithmicIntegral ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1Endpoint N ε), nu := AnalyticNumberTheory.Sieve.goldbachNu, nu_mult := AnalyticNumberTheory.Sieve.goldbachNu_isMultiplicative, nu_pos_of_prime := ⋯, nu_lt_one_of_prime := ⋯ }

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1BoundingSieve_multSum_eq_primesInAP {N : ℕ} (hEven : Even N) {ε z : ℝ} {d : ℕ} (hε : 0 ≤ ε) (hm : 2 ≤ goldbachS1Endpoint N ε) : BoundingSieve.multSum d = ↑(BombieriVinogradov.primesInAP (goldbachS1Endpoint N ε) d (N % d))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1BoundingSieve_siftedSum_eq {N : ℕ} (hEven : Even N) (ε z : ℝ) : BoundingSieve.siftedSum = ↑(goldbachS1 (goldbachDifferenceCarrier N ε) N z)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1BoundingSieve_nu_eq_inv_totient {N : ℕ} (hEven : Even N) {ε z : ℝ} {d : ℕ} (hd : d ∣ goldbachS1ProdPrimes N z) : (goldbachS1BoundingSieve N hEven ε z).nu d = 1 / ↑d.totient

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1BoundingSieve_mainSum_eq_totientSum {N : ℕ} (hEven : Even N) (ε z : ℝ) (μ : ℕ → ℝ) : BoundingSieve.mainSum μ = ∑ d ∈ (goldbachS1ProdPrimes N z).divisors, μ d / ↑d.totient

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1BoundingSieve_rem_eq_standardPrimeAPError {N : ℕ} (hEven : Even N) {ε z : ℝ} (hε : 0 ≤ ε) (hm : 2 ≤ goldbachS1Endpoint N ε) {d : ℕ} (hd : d ∣ goldbachS1ProdPrimes N z) : BoundingSieve.rem d = BombieriVinogradov.standardPrimeAPError (goldbachS1Endpoint N ε) d (N % d)