The actual rough boundary mass

A failed full-product or parity-qualified cubic-prefix test supplies one distinguished prime. Its complementary prefix and suffix are kept disjoint until their weight factors exactly. Only then are both subsets summed freely.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.product_crossing_window {D a : ℝ} {b : ℕ → ℝ} {A : Finset ℕ} {p n : ℕ} (hD : 0 < D) (ha : 0 < a) (hb : ∀ q ∈ A, 0 < b q) (hp : p ∈ A) (hlo : (∏ q ∈ A, b q) * b p ^ n < D) (hhi : D ≤ (∏ q ∈ A, b q ^ a) * (b p ^ a) ^ n) : Window D a (∑ q ∈ A.erase p, Real.log (b q)) (↑n + 1) b p

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.crossing_witness {upper : Bool} {D a : ℝ} {b : ℕ → ℝ} {s : Finset ℕ} (hD : 1 < D) (ha : 0 < a) (hb : ∀ p ∈ s, 0 < b p) (hc : RoughBoundaryCrossing upper b (fun (p : ℕ) => b p ^ a) D s) : ∃ k ∈ {1, 3}, ∃ A ⊆ s, ∃ p ∈ A, Window D a (∑ q ∈ A.erase p, Real.log (b q)) (↑k) b p

This extraction uses the exact strict crossing theorem. Parity is discarded only after an actual failed cubic test has supplied its prime.

@[reducible, inline]

abbrev MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.Index : Type

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.Index = (ℕ × Finset ℕ × Finset ℕ × ℕ)

def MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.reconstruct (i : Index) : Finset ℕ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.reconstruct i = insert i.2.2.2 (i.2.1 ∪ i.2.2.1)

def MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.indices (R : Finset ℕ) : Finset Index

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.indices R = {1, 3} ×ˢ R.powerset ×ˢ R.powerset ×ˢ R

def MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.Valid (D a : ℝ) (b : ℕ → ℝ) (i : Index) : Prop

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.Valid D a b i = (Disjoint i.2.1 i.2.2.1 ∧ i.2.2.2 ∉ i.2.1 ∪ i.2.2.1 ∧ MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.Window D a (∑ q ∈ i.2.1, Real.log (b q)) (↑i.1) b i.2.2.2)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.boundary_subset_image (R : Finset ℕ) {upper : Bool} {D a : ℝ} {b : ℕ → ℝ} (hD : 1 < D) (ha : 0 < a) (hb : ∀ p ∈ R, 0 < b p) : roughBoundarySets upper b (fun (p : ℕ) => b p ^ a) D R ⊆ Finset.image reconstruct (Finset.filter (Valid D a b) (indices R))

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.reconstruct_subset {R : Finset ℕ} {i : Index} (hi : i ∈ indices R) : reconstruct i ⊆ R

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.mass_le_window_sums (upper : Bool) (R : Finset ℕ) {D a : ℝ} {b g : ℕ → ℝ} (hD : 1 < D) (ha : 0 < a) (hb : ∀ p ∈ R, 0 < b p) (hg : ∀ p ∈ R, 0 ≤ g p) : roughBoundaryMass upper b (fun (p : ℕ) => b p ^ a) D R g ≤ ∑ k ∈ {1, 3}, ∑ S ∈ R.powerset, ∑ T ∈ R.powerset, ((∏ q ∈ S, g q) * ∏ q ∈ T, g q) * ∑ p ∈ R with (Window D a (∑ q ∈ S, Real.log (b q)) (↑k) b) p, g p

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.mass_le_dimensionOne (upper : Bool) (P R : Finset ℕ) {D ε 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) (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) : roughBoundaryMass upper b (fun (p : ℕ) => b p ^ (1 + ε ^ 9)) D R g ≤ 2 * (∏ p ∈ R, (1 + g p)) ^ 2 * (3 * ε ^ 7 + 2 * K / (ε ^ 2 * Real.log D))

An Euler-weighted estimate of the actual boundary mass. There is no slot count, powerset cardinality, or replacement by a different family.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.BoundaryAnalytic.roughBoundaryMass_le_dimensionOne (upper : Bool) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε K : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hlarge : 1 ≤ ε ^ 2 * Real.log D) (hK : 0 ≤ K) {g : ℕ → ℝ} (hg : ∀ p ∈ P, 0 ≤ g p ∧ g p < 1) (hdim : SmallRosser.DimensionOneProductBound P g K) : have R := P \ geometricSmallPrimes P D ε; have b := fun (p : ℕ) => geometricLower D ε (ε ^ 9) (geometricSieveLabel D ε p); roughBoundaryMass upper b (fun (p : ℕ) => b p ^ (1 + ε ^ 9)) D R g ≤ 2 * (∏ p ∈ R, (1 + g p)) ^ 2 * (3 * ε ^ 7 + 2 * K / (ε ^ 2 * Real.log D))

Canonical geometric boxes on the original prime carrier and the same dimension-one constant K. Both Rosser parities are covered.