Prime reciprocal sums on fixed logarithmic rectangles

This module defines the reciprocal mass of the ordered prime pairs in

(N ^ a₀, N ^ a₁] × (N ^ b₀, N ^ b₁].

The strict lower and non-strict upper endpoints are retained literally. The mass factors exactly into the two one-dimensional interval sums, so the fixed rectangle limit follows from PrimeReciprocalLogScale. Finite weighted sums then give a reusable simple-function limit for fixed Darboux grids.

No moving boundary or kernel-weighted transfer is asserted here.

noncomputable def MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.primeReciprocalLogRectangle (N : ℕ) (a₀ a₁ b₀ b₁ : ℝ) : ℝ

The double reciprocal mass of ordered prime pairs in the fixed logarithmic rectangle (N ^ a₀, N ^ a₁] × (N ^ b₀, N ^ b₁].

Equations

• MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.primeReciprocalLogRectangle N a₀ a₁ b₀ b₁ = ∑ p₁ ∈ Finset.range (MathlibNt.SieveTheory.PrimeReciprocalLogScale.rpowFloor N a₁ + 1) with Nat.Prime p₁ ∧ ↑N ^ a₀ < ↑p₁ ∧ ↑p₁ ≤ ↑N ^ a₁, ∑ p₂ ∈ Finset.range (MathlibNt.SieveTheory.PrimeReciprocalLogScale.rpowFloor N b₁ + 1) with Nat.Prime p₂ ∧ ↑N ^ b₀ < ↑p₂ ∧ ↑p₂ ≤ ↑N ^ b₁, 1 / (↑p₁ * ↑p₂)

noncomputable def MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.logarithmicRectangleMass (a₀ a₁ b₀ b₁ : ℝ) : ℝ

The logarithmic mass of the rectangle (a₀, a₁] × (b₀, b₁].

Equations

• MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.logarithmicRectangleMass a₀ a₁ b₀ b₁ = Real.log (a₁ / a₀) * Real.log (b₁ / b₀)

theorem MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.primeReciprocalLogRectangle_eq_mul (N : ℕ) (a₀ a₁ b₀ b₁ : ℝ) : primeReciprocalLogRectangle N a₀ a₁ b₀ b₁ = PrimeReciprocalLogScale.primeReciprocalLogInterval N a₀ a₁ * PrimeReciprocalLogScale.primeReciprocalLogInterval N b₀ b₁

The ordered-pair reciprocal mass factors exactly into its two interval masses.

theorem MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.tendsto_primeReciprocalLogRectangle {a₀ a₁ b₀ b₁ : ℝ} (ha₀ : 0 < a₀) (ha : a₀ < a₁) (hb₀ : 0 < b₀) (hb : b₀ < b₁) : Filter.Tendsto (fun (N : ℕ) => primeReciprocalLogRectangle N a₀ a₁ b₀ b₁) Filter.atTop (nhds (logarithmicRectangleMass a₀ a₁ b₀ b₁))

For a fixed positive logarithmic rectangle, its ordered-prime-pair mass tends to its logarithmic area.

theorem MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.eventually_abs_primeReciprocalLogRectangle_sub_lt {a₀ a₁ b₀ b₁ ε : ℝ} (ha₀ : 0 < a₀) (ha : a₀ < a₁) (hb₀ : 0 < b₀) (hb : b₀ < b₁) (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, |primeReciprocalLogRectangle N a₀ a₁ b₀ b₁ - logarithmicRectangleMass a₀ a₁ b₀ b₁| < ε

Eventual epsilon form of the fixed logarithmic rectangle limit.

theorem MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.exists_abs_primeReciprocalLogRectangle_sub_lt {a₀ a₁ b₀ b₁ ε : ℝ} (ha₀ : 0 < a₀) (ha : a₀ < a₁) (hb₀ : 0 < b₀) (hb : b₀ < b₁) (hε : 0 < ε) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → |primeReciprocalLogRectangle N a₀ a₁ b₀ b₁ - logarithmicRectangleMass a₀ a₁ b₀ b₁| < ε

Threshold form of the fixed logarithmic rectangle limit.

theorem MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.tendsto_weighted_sum_primeReciprocalLogRectangle {ι : Type u_1} (s : Finset ι) (c a₀ a₁ b₀ b₁ : ι → ℝ) (ha₀ : ∀ i ∈ s, 0 < a₀ i) (ha : ∀ i ∈ s, a₀ i < a₁ i) (hb₀ : ∀ i ∈ s, 0 < b₀ i) (hb : ∀ i ∈ s, b₀ i < b₁ i) : Filter.Tendsto (fun (N : ℕ) => ∑ i ∈ s, c i * primeReciprocalLogRectangle N (a₀ i) (a₁ i) (b₀ i) (b₁ i)) Filter.atTop (nhds (∑ i ∈ s, c i * logarithmicRectangleMass (a₀ i) (a₁ i) (b₀ i) (b₁ i)))

A fixed finite weighted sum of logarithmic rectangle masses converges to the same weighted sum of logarithmic areas.

theorem MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.eventually_abs_weighted_sum_primeReciprocalLogRectangle_sub_lt {ι : Type u_1} (s : Finset ι) (c a₀ a₁ b₀ b₁ : ι → ℝ) (ha₀ : ∀ i ∈ s, 0 < a₀ i) (ha : ∀ i ∈ s, a₀ i < a₁ i) (hb₀ : ∀ i ∈ s, 0 < b₀ i) (hb : ∀ i ∈ s, b₀ i < b₁ i) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, |∑ i ∈ s, c i * primeReciprocalLogRectangle N (a₀ i) (a₁ i) (b₀ i) (b₁ i) - ∑ i ∈ s, c i * logarithmicRectangleMass (a₀ i) (a₁ i) (b₀ i) (b₁ i)| < ε

Eventual epsilon form of finite-grid convergence.

theorem MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.exists_abs_weighted_sum_primeReciprocalLogRectangle_sub_lt {ι : Type u_1} (s : Finset ι) (c a₀ a₁ b₀ b₁ : ι → ℝ) (ha₀ : ∀ i ∈ s, 0 < a₀ i) (ha : ∀ i ∈ s, a₀ i < a₁ i) (hb₀ : ∀ i ∈ s, 0 < b₀ i) (hb : ∀ i ∈ s, b₀ i < b₁ i) {ε : ℝ} (hε : 0 < ε) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → |∑ i ∈ s, c i * primeReciprocalLogRectangle N (a₀ i) (a₁ i) (b₀ i) (b₁ i) - ∑ i ∈ s, c i * logarithmicRectangleMass (a₀ i) (a₁ i) (b₀ i) (b₁ i)| < ε

Threshold form of fixed finite weighted-grid convergence.