Logarithmic meshes and local prime-mass bounds

Atomic prime bounds and logarithmic partitions lead to fixed-depth Rosser meshes, Darboux estimates, and compact logarithmic coordinate boxes.

All declarations retain the MathlibNt.SieveTheory.SwitchingPrinciple namespace.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.nu_div_one_sub_le_of_dimensionOneLocalProductBound {S : BoundingSieve} {K : ℝ} {q : ℕ} (hlocal : HasDimensionOneLocalProductBound S K) (hq : q ∈ S.prodPrimes.primeFactors) : S.nu q / (1 - S.nu q) ≤ Real.log (↑q + 1) / Real.log ↑q * (1 + K / Real.log ↑q) - 1

The local-product hypothesis controls each normalized prime density by applying it to the unit interval containing that prime. This is the atomic estimate needed when the Rosser path expansion is summed prime by prime.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.nu_div_one_sub_le_atomic_log_error {S : BoundingSieve} {K : ℝ} {q : ℕ} (hlocal : HasDimensionOneLocalProductBound S K) (hK : 0 ≤ K) (hq : q ∈ S.prodPrimes.primeFactors) : S.nu q / (1 - S.nu q) ≤ 1 / (↑q * Real.log ↑q) + (1 + 1 / (↑q * Real.log ↑q)) * (K / Real.log ↑q)

Quantitative atomic form of the local-product estimate. The normalized density at one prime is bounded by the logarithmic unit-cell width plus its interaction with the dimension-one error. In particular, atoms vanish uniformly when the prime and its logarithm tend to infinity.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.prod_inv_one_sub_nu_le_of_subset_interval {S : BoundingSieve} {K z₁ z₂ : ℝ} {T : Finset ℕ} (hlocal : HasDimensionOneLocalProductBound S K) (hz₁ : 2 ≤ z₁) (hz₁₂ : z₁ ≤ z₂) (hT : T ⊆ S.prodPrimes.primeFactors) (hinterval : ∀ p ∈ T, z₁ ≤ ↑p ∧ ↑p < z₂) : ∏ p ∈ T, (1 - S.nu p)⁻¹ ≤ Real.log z₂ / Real.log z₁ * (1 + K / Real.log z₁)

The dimension-one bound also controls any subproduct lying in the same real prime interval. Positivity of the sieve density makes every omitted inverse Euler factor at least one.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.nu_div_one_sub_nonneg_of_mem {S : BoundingSieve} {p : ℕ} (hp : p ∈ S.prodPrimes.primeFactors) : 0 ≤ S.nu p / (1 - S.nu p)

Every normalized local density appearing in a Rosser chain is nonnegative.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.one_add_sum_le_prod_one_add {ι : Type u_1} [DecidableEq ι] (T : Finset ι) (f : ι → ℝ) (hf : ∀ i ∈ T, 0 ≤ f i) : 1 + ∑ i ∈ T, f i ≤ ∏ i ∈ T, (1 + f i)

The linear part of a finite product of nonnegative Euler increments is bounded by the full product.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.sum_nu_div_one_sub_le_of_subset_interval {S : BoundingSieve} {K z₁ z₂ : ℝ} {T : Finset ℕ} (hlocal : HasDimensionOneLocalProductBound S K) (hz₁ : 2 ≤ z₁) (hz₁₂ : z₁ ≤ z₂) (hT : T ⊆ S.prodPrimes.primeFactors) (hinterval : ∀ p ∈ T, z₁ ≤ ↑p ∧ ↑p < z₂) : ∑ p ∈ T, S.nu p / (1 - S.nu p) ≤ Real.log z₂ / Real.log z₁ * (1 + K / Real.log z₁) - 1

Stieltjes mass bound extracted from the dimension-one Euler-product hypothesis. This is the interval atom used by logarithmic partitions: no individual estimate for the primes in T is required.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.sum_nu_div_one_sub_le_of_log_mesh {S : BoundingSieve} {K z₁ z₂ η : ℝ} {T : Finset ℕ} (hlocal : HasDimensionOneLocalProductBound S K) (hz₁ : 2 ≤ z₁) (hz₁₂ : z₁ ≤ z₂) (hT : T ⊆ S.prodPrimes.primeFactors) (hinterval : ∀ p ∈ T, z₁ ≤ ↑p ∧ ↑p < z₂) (hK : 0 ≤ K) (hη : 0 ≤ η) (hmesh : Real.log z₂ / Real.log z₁ ≤ 1 + η) (herror : K / Real.log z₁ ≤ η) : ∑ p ∈ T, S.nu p / (1 - S.nu p) ≤ 2 * η + η ^ 2

Quantitative mesh form of the Stieltjes mass bound. If both the logarithmic width and the local-product error are at most η, the normalized density mass of the cell is at most 2η + η².

theorem MathlibNt.SieveTheory.SwitchingPrinciple.sum_nu_div_one_sub_le_of_rpow_interval {S : BoundingSieve} {K z a b : ℝ} {T : Finset ℕ} (hlocal : HasDimensionOneLocalProductBound S K) (hz : 1 < z) (ha : 0 < a) (hab : a ≤ b) (hza : 2 ≤ z ^ a) (hT : T ⊆ S.prodPrimes.primeFactors) (hinterval : ∀ p ∈ T, z ^ a ≤ ↑p ∧ ↑p < z ^ b) : ∑ p ∈ T, S.nu p / (1 - S.nu p) ≤ b / a * (1 + K / (a * Real.log z)) - 1

Logarithmic-coordinate form of the interval mass estimate. On the cell [z^a, z^b), the main local-product increment is exactly b / a; this is the form used in the Rosser-chain Riemann sums.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.weighted_sum_nu_div_one_sub_le_of_subset_interval {S : BoundingSieve} {K z₁ z₂ M : ℝ} {T : Finset ℕ} {w : ℕ → ℝ} (hlocal : HasDimensionOneLocalProductBound S K) (hz₁ : 2 ≤ z₁) (hz₁₂ : z₁ ≤ z₂) (hT : T ⊆ S.prodPrimes.primeFactors) (hinterval : ∀ p ∈ T, z₁ ≤ ↑p ∧ ↑p < z₂) (hM : 0 ≤ M) (hw : ∀ p ∈ T, 0 ≤ w p ∧ w p ≤ M) : ∑ p ∈ T, w p * (S.nu p / (1 - S.nu p)) ≤ M * (Real.log z₂ / Real.log z₁ * (1 + K / Real.log z₁) - 1)

Upper Darboux-sum form of the local-product estimate. A nonnegative weight bounded by M on one prime interval costs at most M times that interval's Stieltjes mass.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.weighted_sum_nu_div_one_sub_le_of_rpow_interval {S : BoundingSieve} {K z a b M : ℝ} {T : Finset ℕ} {w : ℕ → ℝ} (hlocal : HasDimensionOneLocalProductBound S K) (hz : 1 < z) (ha : 0 < a) (hab : a ≤ b) (hza : 2 ≤ z ^ a) (hT : T ⊆ S.prodPrimes.primeFactors) (hinterval : ∀ p ∈ T, z ^ a ≤ ↑p ∧ ↑p < z ^ b) (hM : 0 ≤ M) (hw : ∀ p ∈ T, 0 ≤ w p ∧ w p ≤ M) : ∑ p ∈ T, w p * (S.nu p / (1 - S.nu p)) ≤ M * (b / a * (1 + K / (a * Real.log z)) - 1)

Weighted logarithmic-coordinate cell estimate. This is the direct Darboux-sum input for a continuous Rosser-chain integrand on [z^a, z^b).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.weighted_sum_nu_div_one_sub_le_of_rpow_Icc_add_atom {S : BoundingSieve} {K z a b M η : ℝ} {T : Finset ℕ} {w : ℕ → ℝ} (hlocal : HasDimensionOneLocalProductBound S K) (hz : 1 < z) (ha : 0 < a) (hab : a ≤ b) (hza : 2 ≤ z ^ a) (hT : T ⊆ S.prodPrimes.primeFactors) (hinterval : ∀ p ∈ T, z ^ a ≤ ↑p ∧ ↑p ≤ z ^ b) (hM : 0 ≤ M) (hw : ∀ p ∈ T, 0 ≤ w p ∧ w p ≤ M) (hη : 0 ≤ η) (hatom : ∀ p ∈ T, w p * (S.nu p / (1 - S.nu p)) ≤ η) : ∑ p ∈ T, w p * (S.nu p / (1 - S.nu p)) ≤ M * (b / a * (1 + K / (a * Real.log z)) - 1) + η

Weighted logarithmic-coordinate cell estimate with a closed right endpoint. The strict part is controlled by the local-product interval estimate, while the unique possible prime on the right face is charged to the atomic error η.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.weighted_sum_nu_div_one_sub_le_partition {ι : Type u_1} [Fintype ι] [DecidableEq ι] {S : BoundingSieve} {K : ℝ} {T : Finset ℕ} {cell : ℕ → ι} {lo hi M : ι → ℝ} {w : ℕ → ℝ} (hlocal : HasDimensionOneLocalProductBound S K) (hT : T ⊆ S.prodPrimes.primeFactors) (hlo : ∀ (i : ι), 2 ≤ lo i) (hlohi : ∀ (i : ι), lo i ≤ hi i) (hinterval : ∀ p ∈ T, lo (cell p) ≤ ↑p ∧ ↑p < hi (cell p)) (hM : ∀ (i : ι), 0 ≤ M i) (hw : ∀ p ∈ T, 0 ≤ w p ∧ w p ≤ M (cell p)) : ∑ p ∈ T, w p * (S.nu p / (1 - S.nu p)) ≤ ∑ i : ι, M i * (Real.log (hi i) / Real.log (lo i) * (1 + K / Real.log (lo i)) - 1)

Finite upper-sum principle for the normalized density measure. Assigning each prime to a real interval reduces a weighted prime sum to the corresponding sum of local-product increments. Geometric logarithmic meshes are obtained by taking lo i and hi i to be consecutive powers of the global cutoff.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.weighted_sum_nu_div_one_sub_le_rpow_partition {ι : Type u_1} [Fintype ι] [DecidableEq ι] {S : BoundingSieve} {K z : ℝ} {T : Finset ℕ} {cell : ℕ → ι} {a b M : ι → ℝ} {w : ℕ → ℝ} (hlocal : HasDimensionOneLocalProductBound S K) (hz : 1 < z) (ha : ∀ (i : ι), 0 < a i) (hab : ∀ (i : ι), a i ≤ b i) (hza : ∀ (i : ι), 2 ≤ z ^ a i) (hT : T ⊆ S.prodPrimes.primeFactors) (hinterval : ∀ p ∈ T, z ^ a (cell p) ≤ ↑p ∧ ↑p < z ^ b (cell p)) (hM : ∀ (i : ι), 0 ≤ M i) (hw : ∀ p ∈ T, 0 ≤ w p ∧ w p ≤ M (cell p)) : ∑ p ∈ T, w p * (S.nu p / (1 - S.nu p)) ≤ ∑ i : ι, M i * (b i / a i * (1 + K / (a i * Real.log z)) - 1)

Finite logarithmic-coordinate upper sum. Each cell is an interval [z^(a i), z^(b i)), so its local-product increment has the explicit Riemann-sum form b i / a i - 1, together with the vanishing K / log z correction.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.weighted_sum_nu_div_one_sub_le_rpow_partition_Icc_add_atoms {ι : Type u_1} [Fintype ι] [DecidableEq ι] {S : BoundingSieve} {K z : ℝ} {T : Finset ℕ} {cell : ℕ → ι} {a b M η : ι → ℝ} {w : ℕ → ℝ} (hlocal : HasDimensionOneLocalProductBound S K) (hz : 1 < z) (ha : ∀ (i : ι), 0 < a i) (hab : ∀ (i : ι), a i ≤ b i) (hza : ∀ (i : ι), 2 ≤ z ^ a i) (hT : T ⊆ S.prodPrimes.primeFactors) (hinterval : ∀ p ∈ T, z ^ a (cell p) ≤ ↑p ∧ ↑p ≤ z ^ b (cell p)) (hM : ∀ (i : ι), 0 ≤ M i) (hw : ∀ p ∈ T, 0 ≤ w p ∧ w p ≤ M (cell p)) (hη : ∀ (i : ι), 0 ≤ η i) (hatom : ∀ p ∈ T, w p * (S.nu p / (1 - S.nu p)) ≤ η (cell p)) : ∑ p ∈ T, w p * (S.nu p / (1 - S.nu p)) ≤ ∑ i : ι, (M i * (b i / a i * (1 + K / (a i * Real.log z)) - 1) + η i)

Finite logarithmic-coordinate upper sum with closed right faces. Every cell has at most one prime on its right face, and η i pays for that atom instead of discarding the equality case.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.weighted_sum_nu_div_one_sub_le_rpow_partition_Icc_add_global_atoms {ι : Type u_1} [Fintype ι] [DecidableEq ι] {S : BoundingSieve} {K z η : ℝ} {T : Finset ℕ} {cell : ℕ → ι} {a b M : ι → ℝ} {w : ℕ → ℝ} (hlocal : HasDimensionOneLocalProductBound S K) (hz : 1 < z) (ha : ∀ (i : ι), 0 < a i) (hab : ∀ (i : ι), a i ≤ b i) (hza : ∀ (i : ι), 2 ≤ z ^ a i) (hT : T ⊆ S.prodPrimes.primeFactors) (hinterval : ∀ p ∈ T, z ^ a (cell p) ≤ ↑p ∧ ↑p ≤ z ^ b (cell p)) (hM : ∀ (i : ι), 0 ≤ M i) (hw : ∀ p ∈ T, 0 ≤ w p ∧ w p ≤ M (cell p)) (hatom : ∑ p ∈ T with ¬↑p < z ^ b (cell p), w p * (S.nu p / (1 - S.nu p)) ≤ η) : ∑ p ∈ T, w p * (S.nu p / (1 - S.nu p)) ≤ ∑ i : ι, M i * (b i / a i * (1 + K / (a i * Real.log z)) - 1) + η

Closed logarithmic cells with a single global budget for all right-face atoms. Splitting off the union of the closed faces before applying the half-open partition estimate prevents an error proportional to the number of mesh cells.

A fixed logarithmic mesh on the screened depth-two interval

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserDepthTwoMeshWidth (m : ℕ) : ℝ

The mesh width of the uniform m + 1-cell partition of [1 / 6, 1].

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserDepthTwoMeshWidth m = 5 / 6 / (↑m + 1)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserDepthTwoMeshLeft (m : ℕ) (i : Fin (m + 1)) : ℝ

The left endpoint of a cell in the uniform partition of [1 / 6, 1].

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserDepthTwoMeshLeft m i = 1 / 6 + ↑↑i * MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserDepthTwoMeshWidth m

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserDepthTwoMeshRight (m : ℕ) (i : Fin (m + 1)) : ℝ

The right endpoint of a cell in the uniform partition of [1 / 6, 1].

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserDepthTwoMeshRight m i = MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserDepthTwoMeshLeft m i + MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserDepthTwoMeshWidth m

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserDepthTwoMeshCell (m : ℕ) (x : ℝ) : Fin (m + 1)

The (clamped) cell containing a screened logarithmic coordinate.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserDepthTwoMeshCell m x = ⟨min ⌊(x - 1 / 6) / MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserDepthTwoMeshWidth m⌋₊ m, ⋯⟩

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserDepthTwoMeshWidth_pos (m : ℕ) : 0 < upperRosserDepthTwoMeshWidth m

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserDepthTwoMeshLeft_pos (m : ℕ) (i : Fin (m + 1)) : 0 < upperRosserDepthTwoMeshLeft m i

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserDepthTwoMeshLeft_le_right (m : ℕ) (i : Fin (m + 1)) : upperRosserDepthTwoMeshLeft m i ≤ upperRosserDepthTwoMeshRight m i

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserDepthTwoMeshRight_le_one (m : ℕ) (i : Fin (m + 1)) : upperRosserDepthTwoMeshRight m i ≤ 1

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserDepthTwoMeshRight_last (m : ℕ) : upperRosserDepthTwoMeshRight m (Fin.last m) = 1

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserDepthTwoMeshCell_bounds (m : ℕ) {x : ℝ} (hx : x ∈ Set.Icc (1 / 6) 1) : upperRosserDepthTwoMeshLeft m (upperRosserDepthTwoMeshCell m x) ≤ x ∧ x ≤ upperRosserDepthTwoMeshRight m (upperRosserDepthTwoMeshCell m x)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMeshWidth (c : ℝ) (m : ℕ) : ℝ

The uniform logarithmic mesh on an arbitrary fixed positive screen [c,1]. The depth-two mesh above is its specialization at c = 1 / 6; this version is used by the arbitrary fixed-depth Rosser recursion.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMeshWidth c m = (1 - c) / (↑m + 1)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMeshLeft (c : ℝ) (m : ℕ) (i : Fin (m + 1)) : ℝ

The left endpoint of a fixed-depth logarithmic mesh cell.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMeshLeft c m i = c + ↑↑i * MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMeshWidth c m

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMeshRight (c : ℝ) (m : ℕ) (i : Fin (m + 1)) : ℝ

The right endpoint of a fixed-depth logarithmic mesh cell.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMeshRight c m i = MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMeshLeft c m i + MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMeshWidth c m

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMeshCell (c : ℝ) (m : ℕ) (x : ℝ) : Fin (m + 1)

The clamped fixed-depth mesh cell containing a screened logarithmic coordinate.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMeshCell c m x = ⟨min ⌊(x - c) / MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMeshWidth c m⌋₊ m, ⋯⟩

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMeshWidth_pos {c : ℝ} (hc : c < 1) (m : ℕ) : 0 < upperRosserFixedDepthMeshWidth c m

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMeshLeft_mem {c : ℝ} (hc : c < 1) (m : ℕ) (i : Fin (m + 1)) : upperRosserFixedDepthMeshLeft c m i ∈ Set.Icc c 1

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMeshLeft_le_right {c : ℝ} (hc : c < 1) (m : ℕ) (i : Fin (m + 1)) : upperRosserFixedDepthMeshLeft c m i ≤ upperRosserFixedDepthMeshRight c m i

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMeshRight_le_one {c : ℝ} (hc : c < 1) (m : ℕ) (i : Fin (m + 1)) : upperRosserFixedDepthMeshRight c m i ≤ 1

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMeshRight_mem {c : ℝ} (hc : c < 1) (m : ℕ) (i : Fin (m + 1)) : upperRosserFixedDepthMeshRight c m i ∈ Set.Icc c 1

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMeshRight_last {c : ℝ} (_hc : c < 1) (m : ℕ) : upperRosserFixedDepthMeshRight c m (Fin.last m) = 1

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMeshCell_bounds {c : ℝ} (hc : c < 1) (m : ℕ) {x : ℝ} (hx : x ∈ Set.Icc c 1) : upperRosserFixedDepthMeshLeft c m (upperRosserFixedDepthMeshCell c m x) ≤ x ∧ x ≤ upperRosserFixedDepthMeshRight c m (upperRosserFixedDepthMeshCell c m x)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMesh_darbouxSum_le_integral_add (m : ℕ) {c ε B : ℝ} (hc : 0 < c) (hc1 : c < 1) {f : ℝ → ℝ} {M : Fin (m + 1) → ℝ} (hε : 0 ≤ ε) (hB : 0 ≤ B) (hfB : ∀ x ∈ Set.Icc c 1, f x ≤ B) (hmajorant : ∀ (i : Fin (m + 1)), ∀ x ∈ Set.Ioo (upperRosserFixedDepthMeshLeft c m i) (upperRosserFixedDepthMeshRight c m i), M i ≤ f x + ε) (hint : MeasureTheory.IntegrableOn (fun (x : ℝ) => x⁻¹ * f x) (Set.Ioo c 1) MeasureTheory.volume) : ∑ i : Fin (m + 1), M i * (upperRosserFixedDepthMeshRight c m i / upperRosserFixedDepthMeshLeft c m i - 1) ≤ (∫ (x : ℝ) in Set.Ioo c 1, x⁻¹ * f x) + ε / c + B * upperRosserFixedDepthMeshWidth c m / c ^ 2

A finite logarithmic Darboux sum on the fixed-depth mesh is bounded by the corresponding integral, with an explicit cell-majorant and reciprocal-coordinate error. This is the analytic bridge used twice in one Rosser-pair recursion: first for the inner coordinate and then for the peeled outer coordinate.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserFixedDepthMesh_mass_majorant_succ (k : ℕ) {s a ε : ℝ} (ha : 0 < a) (ha1 : a < 1) (hε : 0 < ε) : ∃ (m : ℕ), ∀ (i j : Fin (m + 1)) (x₀ x₁ : ℝ), x₀ ∈ Set.Icc (upperRosserFixedDepthMeshLeft a m j) (upperRosserFixedDepthMeshRight a m j) → x₁ ∈ Set.Icc (upperRosserFixedDepthMeshLeft a m i) (upperRosserFixedDepthMeshRight a m i) → LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - x₀ - x₁) a x₁ ≤ LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight a m j - upperRosserFixedDepthMeshRight a m i) a (upperRosserFixedDepthMeshLeft a m i) + ε

A sufficiently fine explicit logarithmic mesh simultaneously majorizes the positive-depth residual mass in both peeled prime coordinates. The corner uses the right endpoints for the residual level and the left endpoint for the inherited upper cutoff, exactly as required by the two-partition comparison.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserFixedDepthMesh_mass_majorant_succ_uniform (k : ℕ) {s₀ s₁ a ε : ℝ} (ha : 0 < a) (ha1 : a < 1) (hε : 0 < ε) : ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ s ∈ Set.Icc s₀ s₁, ∀ (i j : Fin (m + 1)) (x₀ x₁ : ℝ), x₀ ∈ Set.Icc (upperRosserFixedDepthMeshLeft a m j) (upperRosserFixedDepthMeshRight a m j) → x₁ ∈ Set.Icc (upperRosserFixedDepthMeshLeft a m i) (upperRosserFixedDepthMeshRight a m i) → LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - x₀ - x₁) a x₁ ≤ LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight a m j - upperRosserFixedDepthMeshRight a m i) a (upperRosserFixedDepthMeshLeft a m i) + ε

One sufficiently fine logarithmic mesh majorizes the positive-depth residual mass simultaneously for every level in a fixed compact interval. This removes the dependence of the mesh on the individual sieve ratio in the fixed-depth successor induction.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserFixedDepthMesh_mass_majorant_succ_uniform_finite {ι : Type u_1} [Fintype ι] (k : ℕ) (a : ι → ℝ) {s₀ s₁ ε : ℝ} (ha : ∀ (t : ι), 0 < a t) (ha1 : ∀ (t : ι), a t < 1) (hε : 0 < ε) : ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ (t : ι), ∀ s ∈ Set.Icc s₀ s₁, ∀ (i j : Fin (m + 1)) (x₀ x₁ : ℝ), x₀ ∈ Set.Icc (upperRosserFixedDepthMeshLeft (a t) m j) (upperRosserFixedDepthMeshRight (a t) m j) → x₁ ∈ Set.Icc (upperRosserFixedDepthMeshLeft (a t) m i) (upperRosserFixedDepthMeshRight (a t) m i) → LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - x₀ - x₁) (a t) x₁ ≤ LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight (a t) m j - upperRosserFixedDepthMeshRight (a t) m i) (a t) (upperRosserFixedDepthMeshLeft (a t) m i) + ε

A finite family of positive lower cutoffs admits one common refinement threshold. Hence any finer mesh simultaneously supplies all residual majorants, uniformly over the prescribed level interval.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserFixedDepthMesh_mass_majorant_succ_uniform_cutoffs (k : ℕ) {s₀ s₁ c ε : ℝ} (hc : 0 < c) (hc1 : c < 1) (hε : 0 < ε) : ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ s ∈ Set.Icc s₀ s₁, ∀ (h i j : Fin (m + 1)) (a x₀ x₁ : ℝ), a ∈ Set.Icc (upperRosserFixedDepthMeshLeft c m h) (upperRosserFixedDepthMeshRight c m h) → x₀ ∈ Set.Icc (upperRosserFixedDepthMeshLeft c m j) (upperRosserFixedDepthMeshRight c m j) → x₁ ∈ Set.Icc (upperRosserFixedDepthMeshLeft c m i) (upperRosserFixedDepthMeshRight c m i) → LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - x₀ - x₁) a x₁ ≤ LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight c m j - upperRosserFixedDepthMeshRight c m i) (upperRosserFixedDepthMeshLeft c m h) (upperRosserFixedDepthMeshRight c m i) + ε

One sufficiently fine logarithmic mesh simultaneously controls the residual level, the distinguished-prime cutoff, and the inherited upper face. Thus the majorizing corner is indexed only by the three mesh cells and is uniform in the sieve ratio on a compact interval.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserDepthTwoMesh_darbouxSum_le_integral_add (m : ℕ) {f : ℝ → ℝ} {B L : ℝ} (hB : 0 ≤ B) (hL : 0 ≤ L) (_hf : ∀ x ∈ Set.Icc (1 / 6) 1, 0 ≤ f x) (hfB : ∀ x ∈ Set.Icc (1 / 6) 1, f x ≤ B) (hfLip : ∀ x ∈ Set.Icc (1 / 6) 1, ∀ y ∈ Set.Icc (1 / 6) 1, |f x - f y| ≤ L * |x - y|) (hint : MeasureTheory.IntegrableOn (fun (x : ℝ) => x⁻¹ * f x) (Set.Ioo (1 / 6) 1) MeasureTheory.volume) : ∑ i : Fin (m + 1), (f (upperRosserDepthTwoMeshLeft m i) + L * upperRosserDepthTwoMeshWidth m) * (upperRosserDepthTwoMeshRight m i / upperRosserDepthTwoMeshLeft m i - 1) ≤ (∫ (x : ℝ) in Set.Ioo (1 / 6) 1, x⁻¹ * f x) + (12 * L + 36 * B) * upperRosserDepthTwoMeshWidth m

The canonical upper sum of a nonnegative Lipschitz weight on the screened mesh is within O(meshWidth) of its logarithmic integral.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryChains_logarithmicCoordinates_mem {S : BoundingSieve} {z Δ s : ℝ} {q : ℕ} {l : List ℕ} (hz : 2 ≤ z) (hΔ : 0 < Δ) (hs : s = Real.log Δ / Real.log z) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hq : q ∈ S.prodPrimes.primeFactors) (hl : l ∈ LinearSieve.upperRosserBoundaryChains (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p})) : LinearSieve.UpperRosserLogRegion s (Real.log ↑q / Real.log z) (LinearSieve.logarithmicCoordinates z l) ∧ ∀ x ∈ LinearSieve.logarithmicCoordinates z l, Real.log ↑q / Real.log z < x ∧ x ≤ 1

Every canonical boundary chain in the normalized density expansion lands in the real Rosser region, with all coordinates in the compact interval between the distinguished-prime coordinate and 1.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryChains_logarithmicCoordinates_even_lt_suffix {S : BoundingSieve} {z Δ s : ℝ} {q : ℕ} {l : List ℕ} (hz : 2 ≤ z) (hΔ : 0 < Δ) (hs : s = Real.log Δ / Real.log z) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hq : q ∈ S.prodPrimes.primeFactors) (hl : l ∈ LinearSieve.upperRosserBoundaryChains (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p})) {i : ℕ} (hi : i < (LinearSieve.logarithmicCoordinates z l).length) (heven : Even i) : 2 * (LinearSieve.logarithmicCoordinates z l)[i] < (List.drop (i + 1) (LinearSieve.logarithmicCoordinates z l)).sum + 3 * (Real.log ↑q / Real.log z)

Every even prefix of an explicit boundary chain satisfies the reverse suffix inequality used by the geometric tail operator. This keeps the alternating Rosser restrictions in the exact mainSum expansion rather than discarding them in an unrestricted factorial bound.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryChains_last_pair_log_ratios_mem {S : BoundingSieve} {z Δ s : ℝ} {q k : ℕ} {l : List ℕ} (hz : 2 ≤ z) (hΔ : 0 < Δ) (hs : s = Real.log Δ / Real.log z) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hq : q ∈ S.prodPrimes.primeFactors) (hl : l ∈ LinearSieve.upperRosserBoundaryChains (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p})) (hlen : (LinearSieve.logarithmicCoordinates z l).length = 2 * (k + 1)) : (LinearSieve.logarithmicCoordinates z l)[2 * k + 1] / (Real.log ↑q / Real.log z) ∈ Set.Ioo 1 3 ∧ (LinearSieve.logarithmicCoordinates z l)[2 * k] / (Real.log ↑q / Real.log z) ∈ Set.Ioo ((LinearSieve.logarithmicCoordinates z l)[2 * k + 1] / (Real.log ↑q / Real.log z)) (((LinearSieve.logarithmicCoordinates z l)[2 * k + 1] / (Real.log ↑q / Real.log z) + 3) / 2)

The innermost pair of every nonempty explicit boundary chain, normalized by the distinguished-prime coordinate, lies in the initial r = 3 cell of upperRosserAlternatingPairTransform.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryChains_logarithmicCoordinates_mem_below {S : BoundingSieve} {z Δ s ε : ℝ} {q : ℕ} {l : List ℕ} (hz : 2 ≤ z) (hΔ : 0 < Δ) (hs : s = Real.log Δ / Real.log z) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hq : q ∈ S.prodPrimes.primeFactors) (hl : l ∈ LinearSieve.upperRosserBoundaryChains (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p})) (hε : 0 < ε) : LinearSieve.UpperRosserLogRegionBelow s (Real.log ↑q / Real.log z) (1 + ε) (LinearSieve.logarithmicCoordinates z l)

Enlarging the global upper face by any positive amount places every discrete boundary chain in the strict bounded region used by the recursive continuous mass.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryChains_fixed_length_logarithmic_support {S : BoundingSieve} {z Δ s : ℝ} {q k : ℕ} {l : List ℕ} (hz : 2 ≤ z) (hΔ : 0 < Δ) (hs : s = Real.log Δ / Real.log z) (hslo : 3 / 2 ≤ s) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hq : q ∈ S.prodPrimes.primeFactors) (hl : l ∈ LinearSieve.upperRosserBoundaryChains (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p})) (hlen : l.length = 2 * k) : 1 / (2 * 3 ^ k) < Real.log ↑q / Real.log z ∧ ∀ x ∈ LinearSieve.logarithmicCoordinates z l, 1 / (2 * 3 ^ k) < x ∧ x ≤ 1

At each fixed even depth, both the distinguished prime and every selected prime coordinate stay in a compact interval bounded away from zero. This is the uniform support needed for the fixed-depth Darboux approximation.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.sum_mul_upperRosserBoundaryChainsFixedDepthDensity_eq_screened (nu w : ℕ → ℝ) {S : BoundingSieve} {z Δ s : ℝ} (k : ℕ) (hz : 2 ≤ z) (hΔ : 0 < Δ) (hs : s = Real.log Δ / Real.log z) (hslo : 3 / 2 ≤ s) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) : ∑ q ∈ S.prodPrimes.primeFactors, w q * LinearSieve.upperRosserBoundaryChainsFixedDepthDensity nu (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) k = ∑ q ∈ S.prodPrimes.primeFactors with 1 / (2 * 3 ^ k) < Real.log ↑q / Real.log z, w q * LinearSieve.upperRosserBoundaryChainsFixedDepthDensity nu (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) k

At a fixed pair depth, the complete outer boundary sum is exactly supported above the depth-dependent logarithmic cutoff. This equality is uniform in the outer weight and is the screening step used before recursive Stieltjes comparisons.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserLogCoordinateVector (z : ℝ) (l : List ℕ) (k : ℕ) (hlen : l.length = 2 * k) : List.Vector ℝ (2 * k)

The logarithmic coordinates of a chain of prescribed even length, packaged as a fixed finite-dimensional vector.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserLogCoordinateVector z l k hlen = ⟨MathlibNt.SieveTheory.LinearSieve.logarithmicCoordinates z l, ⋯⟩

def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthAmbientBox (k : ℕ) : Set (Fin (2 * k) → ℝ)

A compact box containing every logarithmic coordinate vector at fixed Rosser depth on the fundamental-lemma range.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthAmbientBox k = Set.Icc (fun (x : Fin (2 * k)) => 1 / (2 * 3 ^ k)) fun (x : Fin (2 * k)) => 1

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthAmbientBox_isCompact (k : ℕ) : IsCompact (upperRosserFixedDepthAmbientBox k)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthAmbientBox_measurableSet (k : ℕ) : MeasurableSet (upperRosserFixedDepthAmbientBox k)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserLogCoordinateVector_mem_fixedDepthAmbientBox {S : BoundingSieve} {z Δ s : ℝ} {q k : ℕ} {l : List ℕ} (hz : 2 ≤ z) (hΔ : 0 < Δ) (hs : s = Real.log Δ / Real.log z) (hslo : 3 / 2 ≤ s) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hq : q ∈ S.prodPrimes.primeFactors) (hl : l ∈ LinearSieve.upperRosserBoundaryChains (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p})) (hlen : l.length = 2 * k) : (fun (i : Fin (2 * k)) => (upperRosserLogCoordinateVector z l k hlen).get i) ∈ upperRosserFixedDepthAmbientBox k

The vector form of fixed-depth support, suitable for integration against the product Lebesgue measure on Fin (2k) → ℝ.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.localProduct_error_le_of_log_coordinate_lower {K z a c : ℝ} (hK : 0 ≤ K) (hz : 1 < z) (hc : 0 < c) (hca : c ≤ a) : K / (a * Real.log z) ≤ K / (c * Real.log z)

A lower bound for a logarithmic coordinate gives a uniform bound for the local-product correction occurring in every logarithmic cell.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_localProduct_error_cutoff {K η c : ℝ} (hη : 0 < η) (hc : 0 < c) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (z : ℝ), z₀ ≤ z → K / (c * Real.log z) ≤ η

An explicit cutoff makes the local-product correction uniformly smaller than a prescribed error on every logarithmic coordinate bounded below by c.