Actual coprime half-open boxes and finite signed weighted limits, retaining the diagonal.

noncomputable def MathlibNt.SieveTheory.LiuWeight.coprimePrimeLogRectanglePairs (N : ℕ) (a b c d : ℝ) : Finset (ℕ × ℕ)

Equations

• MathlibNt.SieveTheory.LiuWeight.coprimePrimeLogRectanglePairs N a b c d = {p ∈ MathlibNt.SieveTheory.LiuWeight.primeLogRectanglePairs N a b c d | (p.1 * p.2).Coprime N}

theorem MathlibNt.SieveTheory.LiuWeight.coprimePrimeLogRectanglePairs_eq_product (N : ℕ) (a b c d : ℝ) : coprimePrimeLogRectanglePairs N a b c d = coprimePrimeLogIntervalPrimes N a b ×ˢ coprimePrimeLogIntervalPrimes N c d

noncomputable def MathlibNt.SieveTheory.LiuWeight.coprimePrimeReciprocalLogRectangle (N : ℕ) (a b c d : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiuWeight.coprimePrimeReciprocalLogRectangle N a b c d = ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.coprimePrimeLogRectanglePairs N a b c d, 1 / (↑p.1 * ↑p.2)

theorem MathlibNt.SieveTheory.LiuWeight.coprimePrimeReciprocalLogRectangle_eq_mul (N : ℕ) (a b c d : ℝ) : coprimePrimeReciprocalLogRectangle N a b c d = coprimePrimeReciprocalLogInterval N a b * coprimePrimeReciprocalLogInterval N c d

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_coprimePrimeReciprocalLogRectangle {a b c d : ℝ} (ha : 0 < a) (hab : a < b) (hc : 0 < c) (hcd : c < d) : Filter.Tendsto (fun (N : ℕ) => coprimePrimeReciprocalLogRectangle N a b c d) Filter.atTop (nhds (PrimeReciprocalLogRectangle.logarithmicRectangleMass a b c d))

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_sum_filter_coprime_primeLogRectanglePairs {a b c d : ℝ} (ha : 0 < a) (hab : a < b) (hc : 0 < c) (hcd : c < d) : Filter.Tendsto (fun (N : ℕ) => ∑ p ∈ primeLogRectanglePairs N a b c d with (p.1 * p.2).Coprime N, 1 / (↑p.1 * ↑p.2)) Filter.atTop (nhds (PrimeReciprocalLogRectangle.logarithmicRectangleMass a b c d))

The literal filtered original carrier, without a carrier-identification premise.

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_weighted_sum_coprimePrimeReciprocalLogRectangle {ι : Type u_1} (s : Finset ι) (w a b c d : ι → ℝ) (ha : ∀ i ∈ s, 0 < a i) (hab : ∀ i ∈ s, a i < b i) (hc : ∀ i ∈ s, 0 < c i) (hcd : ∀ i ∈ s, c i < d i) : Filter.Tendsto (fun (N : ℕ) => ∑ i ∈ s, w i * coprimePrimeReciprocalLogRectangle N (a i) (b i) (c i) (d i)) Filter.atTop (nhds (∑ i ∈ s, w i * PrimeReciprocalLogRectangle.logarithmicRectangleMass (a i) (b i) (c i) (d i)))

Fixed finite signed weights: an exact sum limit, not multiplication of inequalities.

theorem MathlibNt.SieveTheory.LiuWeight.exists_abs_weighted_sum_coprimePrimeReciprocalLogRectangle_sub_lt {ι : Type u_1} (s : Finset ι) (w a b c d : ι → ℝ) (ha : ∀ i ∈ s, 0 < a i) (hab : ∀ i ∈ s, a i < b i) (hc : ∀ i ∈ s, 0 < c i) (hcd : ∀ i ∈ s, c i < d i) (Nmin : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (N₀ : ℕ), Nmin ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → |∑ i ∈ s, w i * coprimePrimeReciprocalLogRectangle N (a i) (b i) (c i) (d i) - ∑ i ∈ s, w i * PrimeReciprocalLogRectangle.logarithmicRectangleMass (a i) (b i) (c i) (d i)| < ε

The finite box family and weights precede a common threshold above Nmin.