@[instance_reducible]

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

Equations

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

@[reducible, inline]

abbrev MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Output (N : ℕ) : (_ : ℕ × ℕ) × ℕ → ℕ

The literal output value attached to a labelled B10 atom.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Output N = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPi10Output N

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

The finite support of the genuine B10 pushforward sieve.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Support N ε b c = Finset.image (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Output N) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Atoms N ε b c)

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

The multiplicity weight of an output value p = N - rsq. Repeated outputs from different labelled atoms are accumulated rather than collapsed.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Weight N ε b c p = ↑{x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Atoms N ε b c | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Output N x = p}.card

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes (N : ℕ) (Z : ℝ) : Finset ℕ

The exact finite prime carrier for the literal strict sieve cutoff p < Z with the exceptional primes dividing N removed.

Equations

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

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes (N : ℕ) (Z : ℝ) : ℕ

The corresponding finite product of the actual sieved primes.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes N Z = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z).prod id

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes_squarefree (N : ℕ) (Z : ℝ) : Squarefree (goldbachB10ProdPrimes N Z)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes_ne_zero (N : ℕ) (Z : ℝ) : goldbachB10ProdPrimes N Z ≠ 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes_primeFactors (N : ℕ) (Z : ℝ) : (goldbachB10ProdPrimes N Z).primeFactors = goldbachB10SiftingPrimes N Z

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes_coprime_N (N : ℕ) (Z : ℝ) : (goldbachB10ProdPrimes N Z).Coprime N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10_dvd_prodPrimes_coprime_N {N d : ℕ} {Z : ℝ} (hd : d ∣ goldbachB10ProdPrimes N Z) : d.Coprime N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.prime_dvd_goldbachB10ProdPrimes_lt {N : ℕ} {Z : ℝ} {p : ℕ} (hp : Nat.Prime p) (hpP : p ∣ goldbachB10ProdPrimes N Z) : ↑p < Z

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10_coprime_prodPrimes_iff_literalHPoint (N : ℕ) (Z : ℝ) (n : ℕ) : (goldbachB10ProdPrimes N Z).Coprime n ↔ literalHPoint N 1 Z n

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BoundingSieve (N : ℕ) (hEven : Even N) (ε b c Z X : ℝ) : BoundingSieve

The actual finite pushforward sieve on labelled B10 atoms. The total mass is the supplied parameter X; no analytic identification is built into this finite adapter.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BoundingSieve N hEven ε b c Z X = { support := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Support N ε b c, prodPrimes := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes N Z, prodPrimes_squarefree := ⋯, weights := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Weight N ε b c, weights_nonneg := ⋯, totalMass := X, nu := AnalyticNumberTheory.Sieve.goldbachNu, nu_mult := AnalyticNumberTheory.Sieve.goldbachNu_isMultiplicative, nu_pos_of_prime := ⋯, nu_lt_one_of_prime := ⋯ }

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BoundingSieve_multSum_eq_card_divisorAtoms (N : ℕ) (hEven : Even N) (ε b c Z X : ℝ) (d : ℕ) : BoundingSieve.multSum d = ↑(goldbachB10DivisorAtoms N d ε b c).card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BoundingSieve_siftedSum_eq (N : ℕ) (hEven : Even N) (ε b c Z X : ℝ) : BoundingSieve.siftedSum = ↑(goldbachB10SiftedCount N ε b c Z)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BoundingSieve_nu_eq_inv_totient {N : ℕ} (hEven : Even N) {ε b c Z X : ℝ} {d : ℕ} (hd : d ∣ goldbachB10ProdPrimes N Z) : (goldbachB10BoundingSieve N hEven ε b c Z X).nu d = 1 / ↑d.totient

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BoundingSieve_rem_eq_card_sub {N : ℕ} (hEven : Even N) {ε b c Z X : ℝ} {d : ℕ} (hd : d ∣ goldbachB10ProdPrimes N Z) : BoundingSieve.rem d = ↑(goldbachB10DivisorAtoms N d ε b c).card - X / ↑d.totient