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.
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.
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.
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.
Every normalized local density appearing in a Rosser chain is nonnegative.
The linear part of a finite product of nonnegative Euler increments is bounded by the full product.
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.
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η + η².
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.
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.
Weighted logarithmic-coordinate cell estimate. This is the direct
Darboux-sum input for a continuous Rosser-chain integrand on [z^a, z^b).
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 η.
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.
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.
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.
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 #
The mesh width of the uniform m + 1-cell partition of [1 / 6, 1].
Equations
- MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserDepthTwoMeshWidth m = 5 / 6 / (↑m + 1)
Instances For
The left endpoint of a cell in the uniform partition of [1 / 6, 1].
Equations
Instances For
The right endpoint of a cell in the uniform partition of [1 / 6, 1].
Equations
Instances For
The (clamped) cell containing a screened logarithmic coordinate.
Equations
Instances For
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)
Instances For
The left endpoint of a fixed-depth logarithmic mesh cell.
Equations
Instances For
The right endpoint of a fixed-depth logarithmic mesh cell.
Equations
Instances For
The clamped fixed-depth mesh cell containing a screened logarithmic coordinate.
Equations
Instances For
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.
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.
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.
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.
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.
The canonical upper sum of a nonnegative Lipschitz weight on the screened
mesh is within O(meshWidth) of its logarithmic integral.
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.
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.
The innermost pair of every nonempty explicit boundary chain, normalized by
the distinguished-prime coordinate, lies in the initial r = 3 cell of
upperRosserAlternatingPairTransform.
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.
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.
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.
The logarithmic coordinates of a chain of prescribed even length, packaged as a fixed finite-dimensional vector.
Equations
Instances For
A compact box containing every logarithmic coordinate vector at fixed Rosser depth on the fundamental-lemma range.
Equations
Instances For
The vector form of fixed-depth support, suitable for integration against
the product Lebesgue measure on Fin (2k) → ℝ.
An explicit cutoff makes the local-product correction uniformly smaller
than a prescribed error on every logarithmic coordinate bounded below by c.