noncomputable def MathlibNt.SieveTheory.LiuWeight.pairLogCoordinate (N : ℕ) (p : ℕ × ℕ) : ℝ × ℝ

Equations

• MathlibNt.SieveTheory.LiuWeight.pairLogCoordinate N p = (MathlibNt.SieveTheory.LiuWeight.primeLogExponent N p.1, MathlibNt.SieveTheory.LiuWeight.primeLogExponent N p.2)

theorem MathlibNt.SieveTheory.LiuWeight.mem_coprimePrimeLogRectanglePairs_iff_coordinate {N : ℕ} (hN : 1 < N) {p : ℕ × ℕ} {a b c d : ℝ} : p ∈ coprimePrimeLogRectanglePairs N a b c d ↔ Nat.Prime p.1 ∧ Nat.Prime p.2 ∧ (p.1 * p.2).Coprime N ∧ pairLogCoordinate N p ∈ Set.Ioc a b ×ˢ Set.Ioc c d

noncomputable def MathlibNt.SieveTheory.LiuWeight.coprimePrimeKernelRectangle (N : ℕ) (a b c d : ℝ) (K : ℝ × ℝ → ℝ) : ℝ

Equations

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

theorem MathlibNt.SieveTheory.LiuWeight.weighted_coprime_grid_le_kernel {N n : ℕ} (hN : 1 < N) (hn : 0 < n) {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) (K : ℝ × ℝ → ℝ) (coeff : Fin n × Fin n → ℝ) (hpos : ∀ x ∈ Set.Ioc a b ×ˢ Set.Ioc c d, 0 ≤ K x) (hcoeff : ∀ (q : Fin n × Fin n), ∀ x ∈ LiLiuGoldbachLogDarboux.cell a b c d n q, coeff q ≤ K x) : ∑ q : Fin n × Fin n, coeff q * coprimePrimeReciprocalLogRectangle N (LiLiuGoldbachLogDarboux.grid a b n ↑q.1) (LiLiuGoldbachLogDarboux.grid a b n (↑q.1 + 1)) (LiLiuGoldbachLogDarboux.grid c d n ↑q.2) (LiLiuGoldbachLogDarboux.grid c d n (↑q.2 + 1)) ≤ coprimePrimeKernelRectangle N a b c d K

A lower grid is transported using disjoint boxes, not a cover with free overlap.

theorem MathlibNt.SieveTheory.LiuWeight.exists_coprimePrimeKernelRectangle_lower {a b c d : ℝ} (ha : 0 < a) (hab : a < b) (hc : 0 < c) (hcd : c < d) {K : ℝ × ℝ → ℝ} {L : NNReal} (hK : LipschitzWith L K) (hpos : ∀ x ∈ Set.Ioc a b ×ˢ Set.Ioc c d, 0 ≤ K x) {η : ℝ} (hη : 0 < η) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → (∫ (u : ℝ) in a..b, ∫ (v : ℝ) in c..d, K (u, v) / (u * v)) - η ≤ coprimePrimeKernelRectangle N a b c d K

Fixed positive rectangles: actual copN prime sums dominate the kernel integral asymptotically. The finite grid is chosen before the common prime-count threshold.