@[instance_reducible]

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

Equations

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

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedLabels (N : ℕ) (T : ℝ) : Finset ((_ : ℕ) × ℕ)

The literal relaxed switched labels (r,q) for the actual S2 source.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedLabels N T = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2Primes N T).sigma fun (r : ℕ) => {q ∈ Finset.range (N + 1) | Nat.Prime q ∧ r * q < N}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachS2SwitchedLabels_iff {N : ℕ} {T : ℝ} {x : (_ : ℕ) × ℕ} : x ∈ goldbachS2SwitchedLabels N T ↔ x.fst ∈ goldbachS2Primes N T ∧ Nat.Prime x.snd ∧ x.fst * x.snd < N

@[reducible, inline]

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

The switched output is the literal partner b(r,q)=N-rq.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedOutput N x = N - x.fst * x.snd

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedOutput_eq_sub {N : ℕ} {x : (_ : ℕ) × ℕ} : goldbachS2SwitchedOutput N x = N - x.fst * x.snd

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedAtom_prod_lt {N : ℕ} {T : ℝ} {x : (_ : ℕ) × ℕ} (hx : x ∈ goldbachS2SwitchedLabels N T) : x.fst * x.snd < N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedAtom_prod_add_output {N : ℕ} {T : ℝ} {x : (_ : ℕ) × ℕ} (hx : x ∈ goldbachS2SwitchedLabels N T) : x.fst * x.snd + goldbachS2SwitchedOutput N x = N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedAtom_output_dvd_iff_modEq {N d : ℕ} {T : ℝ} {x : (_ : ℕ) × ℕ} (_hd : 1 ≤ d) (hx : x ∈ goldbachS2SwitchedLabels N T) : d ∣ goldbachS2SwitchedOutput N x ↔ x.fst * x.snd ≡ N [MOD d]

On a genuine switched label, divisibility of the output is exactly the congruence rq ≡ N (mod d).

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedDivisorResidueCondition (N d : ℕ) (x : (_ : ℕ) × ℕ) : Prop

Exact residue condition on a switched divisor fibre.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedDivisorResidueCondition N d x = (x.fst.Coprime d ∧ ↑x.snd = ↑N * (↑x.fst)⁻¹)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedAtom_left_coprime_of_coprime_modulus {N d : ℕ} {T : ℝ} {x : (_ : ℕ) × ℕ} (_hd : 1 ≤ d) (hx : x ∈ goldbachS2SwitchedLabels N T) (hdp : d ∣ goldbachS2SwitchedOutput N x) : x.fst.Coprime d

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedAtom_output_dvd_iff_residueCondition {N d : ℕ} {T : ℝ} {x : (_ : ℕ) × ℕ} (hd : 1 ≤ d) (hx : x ∈ goldbachS2SwitchedLabels N T) : d ∣ goldbachS2SwitchedOutput N x ↔ goldbachS2SwitchedDivisorResidueCondition N d x

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedDivisorLabels (N : ℕ) (T : ℝ) (d : ℕ) : Finset ((_ : ℕ) × ℕ)

The literal divisor fibre on the relaxed switched labels.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedDivisorLabels N T d = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedLabels N T | d ∣ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedOutput N x}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachS2SwitchedDivisorLabels_iff {N d : ℕ} {T : ℝ} {x : (_ : ℕ) × ℕ} : x ∈ goldbachS2SwitchedDivisorLabels N T d ↔ x ∈ goldbachS2SwitchedLabels N T ∧ d ∣ goldbachS2SwitchedOutput N x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedDivisorLabels_eq_residueFilter {N d : ℕ} {T : ℝ} (hd : 1 ≤ d) : goldbachS2SwitchedDivisorLabels N T d = Finset.filter (goldbachS2SwitchedDivisorResidueCondition N d) (goldbachS2SwitchedLabels N T)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedSupport (N : ℕ) (T : ℝ) : Finset ℕ

The relaxed switched support after pushforward along b(r,q)=N-rq.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedSupport N T = Finset.image (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedOutput N) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedLabels N T)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachS2SwitchedSupport_iff {N n : ℕ} {T : ℝ} : n ∈ goldbachS2SwitchedSupport N T ↔ ∃ x ∈ goldbachS2SwitchedLabels N T, goldbachS2SwitchedOutput N x = n

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedWeight (N : ℕ) (T : ℝ) (n : ℕ) : ℝ

The fibre multiplicity of the output value b=N-rq.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedWeight N T n = ↑{x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedLabels N T | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedOutput N x = n}.card

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedSiftedLabels (N : ℕ) (T Z : ℝ) : Finset ((_ : ℕ) × ℕ)

The relaxed switched sifted labels at the literal sieve cutoff Z.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedSiftedLabels N T Z = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedLabels N T | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.SurvivesSieve N Z (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedOutput N x)}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachS2SwitchedSiftedLabels_iff {N : ℕ} {T Z : ℝ} {x : (_ : ℕ) × ℕ} : x ∈ goldbachS2SwitchedSiftedLabels N T Z ↔ x ∈ goldbachS2SwitchedLabels N T ∧ SurvivesSieve N Z (goldbachS2SwitchedOutput N x)

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

The literal sifted count on the relaxed switched labels.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedSiftedCount N T Z = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedSiftedLabels N T Z).card

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedDivCount (N : ℕ) (T : ℝ) (d : ℕ) : ℕ

Exact divisor count on the relaxed switched labels.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedDivCount N T d = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedDivisorLabels N T d).card

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedMainMass (N : ℕ) (T : ℝ) : ℝ

The actual one-endpoint switched mass X(N,T).

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedMainMass N T = ∑ r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2Primes N T, MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) (↑N / ↑r)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedMainMass_nonneg (N : ℕ) (T : ℝ) : 0 ≤ goldbachS2SwitchedMainMass N T

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedWeight_sum_eq_card_labels (N : ℕ) (T : ℝ) : ∑ n ∈ goldbachS2SwitchedSupport N T, goldbachS2SwitchedWeight N T n = ↑(goldbachS2SwitchedLabels N T).card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedWeight_nonneg (N : ℕ) (T : ℝ) (n : ℕ) : 0 ≤ goldbachS2SwitchedWeight N T n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2Switched_coprime_prodPrimes_iff_survivesSieve (N : ℕ) (Z : ℝ) (n : ℕ) : (goldbachS1ProdPrimes N Z).Coprime n ↔ SurvivesSieve N Z n

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedBoundingSieve (N : ℕ) (hEven : Even N) (T Z : ℝ) : BoundingSieve

The actual bounding sieve carried by the relaxed switched labels.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedBoundingSieve N hEven T Z = { support := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedSupport N T, prodPrimes := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1ProdPrimes N Z, prodPrimes_squarefree := ⋯, weights := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedWeight N T, weights_nonneg := ⋯, totalMass := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedMainMass N T, nu := AnalyticNumberTheory.Sieve.goldbachNu, nu_mult := AnalyticNumberTheory.Sieve.goldbachNu_isMultiplicative, nu_pos_of_prime := ⋯, nu_lt_one_of_prime := ⋯ }

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedBoundingSieve_multSum_eq_divCount (N : ℕ) (hEven : Even N) (T Z : ℝ) (d : ℕ) : BoundingSieve.multSum d = ↑(goldbachS2SwitchedDivCount N T d)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedBoundingSieve_siftedSum_eq (N : ℕ) (hEven : Even N) (T Z : ℝ) : BoundingSieve.siftedSum = ↑(goldbachS2SwitchedSiftedCount N T Z)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedBoundingSieve_nu_eq_inv_totient {N : ℕ} (hEven : Even N) {T Z : ℝ} {d : ℕ} (hd : d ∣ goldbachS1ProdPrimes N Z) : (goldbachS2SwitchedBoundingSieve N hEven T Z).nu d = 1 / ↑d.totient

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedBoundingSieve_rem_eq_divCount_sub {N : ℕ} (hEven : Even N) {T Z : ℝ} {d : ℕ} (hd : d ∣ goldbachS1ProdPrimes N Z) : BoundingSieve.rem d = ↑(goldbachS2SwitchedDivCount N T d) - goldbachS2SwitchedMainMass N T / ↑d.totient

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedSmallPartnerLoss (N : ℕ) (ε T Z : ℝ) : ℕ

The actual small-partner loss keeps the original ordered prime pairs whose prime partner lies below the switched sieve cutoff.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedSmallPartnerLoss N ε T Z = {rq ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2PrimePairs N ε T | ↑(N - rq.1 * rq.2) < Z}.card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2PrimePairs_card_le_switchedSiftedCount_add_smallPartnerLoss (N : ℕ) (ε T Z : ℝ) : (goldbachS2PrimePairs N ε T).card ≤ goldbachS2SwitchedSiftedCount N T Z + goldbachS2SwitchedSmallPartnerLoss N ε T Z

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedSmallPartnerLoss_le_ceil (N : ℕ) (ε T Z : ℝ) : goldbachS2SwitchedSmallPartnerLoss N ε T Z ≤ ⌈Z⌉₊

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2PrimePairs_card_le_switchedSiftedCount_add_ceil (N : ℕ) (ε T Z : ℝ) : (goldbachS2PrimePairs N ε T).card ≤ goldbachS2SwitchedSiftedCount N T Z + ⌈Z⌉₊

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2_le_switchedSiftedCount_add_smallPartnerLoss_add_primeFactors (N : ℕ) (ε T Z : ℝ) (hN : 2 ≤ N) (hε : 0 < ε) (hε1 : ε < 1) (hT : 0 < T) (hcube : ↑N < T ^ 3) (hsqrt : √↑N ≤ ε * ↑N) : goldbachS2 (goldbachDifferenceCarrier N ε) N T ≤ ↑(goldbachS2SwitchedSiftedCount N T Z) + ↑(goldbachS2SwitchedSmallPartnerLoss N ε T Z) + ↑N.primeFactors.card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2_le_switchedSiftedCount_add_ceil_add_primeFactors (N : ℕ) (ε T Z : ℝ) (hN : 2 ≤ N) (hε : 0 < ε) (hε1 : ε < 1) (hT : 0 < T) (hcube : ↑N < T ^ 3) (hsqrt : √↑N ≤ ε * ↑N) : goldbachS2 (goldbachDifferenceCarrier N ε) N T ≤ ↑(goldbachS2SwitchedSiftedCount N T Z) + ↑⌈Z⌉₊ + ↑N.primeFactors.card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2_le_switchedSiftedCount_add_smallPartnerLoss_add_primeFactors_eventually (ε : ℝ) (hε : 0 < ε) (hε15 : ε < 2 / 15) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → ∀ (Z : ℝ), have T := ↑N ^ (9 / 19 - ε); goldbachS2 (goldbachDifferenceCarrier N ε) N T ≤ ↑(goldbachS2SwitchedSiftedCount N T Z) + ↑(goldbachS2SwitchedSmallPartnerLoss N ε T Z) + ↑N.primeFactors.card

The threshold is uniform in the later sieve cutoff, including moving cutoffs.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2_le_switchedSiftedCount_add_ceil_add_primeFactors_eventually (ε : ℝ) (hε : 0 < ε) (hε15 : ε < 2 / 15) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → ∀ (Z : ℝ), have T := ↑N ^ (9 / 19 - ε); goldbachS2 (goldbachDifferenceCarrier N ε) N T ≤ ↑(goldbachS2SwitchedSiftedCount N T Z) + ↑⌈Z⌉₊ + ↑N.primeFactors.card

Uniform-cutoff form with the actual small-partner cardinality paid by ceil Z.