Analytic boundary windows

Closed lower and strict upper logarithmic windows are estimated directly from the original dimension-one product hypothesis.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.log_interval_sum_le (P S : Finset ℕ) {g : ℕ → ℝ} {K t l r δ : ℝ} (hg : ∀ p ∈ P, 0 ≤ g p ∧ g p < 1) (hdim : SmallRosser.DimensionOneProductBound P g K) (hK : 0 ≤ K) (ht : 1 ≤ t) (hl : t ≤ l) (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1) (hwidth : r - l ≤ δ * t) (hS : ∀ p ∈ S, p ∈ P ∧ Nat.Prime p ∧ l ≤ Real.log ↑p ∧ Real.log ↑p < r) : ∑ p ∈ S, g p ≤ δ + 2 * K / t

A narrow interval in logarithmic coordinates, with its lower endpoint closed, pays its width rather than a whole dimension-one product.

def MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.Window (D a x k : ℝ) (b : ℕ → ℝ) (p : ℕ) : Prop

The exponent is 1 for a full product and 3 for a cubic prefix. The remaining prefix is recorded by its logarithmic product x.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.Window D a x k b p = (Real.log D / a ≤ x + k * Real.log (b p) ∧ x + k * Real.log (b p) < Real.log D)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.window_sum_le (P R : Finset ℕ) {D ε K x k : ℝ} {b : ℕ → ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hlarge : 1 ≤ ε ^ 2 * Real.log D) (hK : 0 ≤ K) (hR : R ⊆ P) (hP : ∀ p ∈ P, Nat.Prime p) (hx : 0 ≤ x) (hk : 1 ≤ k) (hb : ∀ p ∈ R, 1 ≤ b p ∧ b p ≤ ↑p ∧ ↑p < b p ^ (1 + ε ^ 9)) (hrough : ∀ p ∈ R, D ^ ε ^ 2 ≤ ↑p) {g : ℕ → ℝ} (hg : ∀ p ∈ P, 0 ≤ g p ∧ g p < 1) (hdim : SmallRosser.DimensionOneProductBound P g K) : ∑ p ∈ R with (Window D (1 + ε ^ 9) x k b) p, g p ≤ 3 * ε ^ 7 + 2 * K / (ε ^ 2 * Real.log D)