Documentation

MathlibNt.SieveTheory.LinearSieve.BoundaryRegularity

Regularity of upper Rosser boundary mass #

Fixed-depth bounds, integrability, continuity, uniform moduli, and cell majorants with moving levels and endpoints.

Every fixed-depth boundary mass is uniformly bounded once the recursive coordinates are bounded away from zero and the inherited upper endpoint is at most one. The deliberately coarse bound is stable under the two integrations in the Rosser recursion.

A common positive lower cutoff gives a uniform fixed-depth bound independent of all other parameters of the recursive boundary mass.

The same recursive bound for the boundary mass with global upper cutoff one.

On a fixed screened interval, the complete outer integrand has a constant majorant depending only on the depth and the lower endpoint.

The inner integrand in the Rosser pair recursion is integrable on every positive screened interval, at every finite depth.

The complete fixed-depth Rosser boundary integrand is integrable on every compact interval bounded away from zero.

On every screened compact parameter box, the full three-parameter residual mass is integrable. This supplies a common dominated-convergence envelope for fixed-depth Darboux approximations.

The complete outer integrand in one recursive Rosser step is integrable on every positive screened interval.

theorem MathlibNt.SieveTheory.LinearSieve.integral_inv_mul_upperRosserBoundaryMassAux_le (k : ) {s a x₀ : } (ha : 0 < a) (hx₀ : x₀ 1) :
(x₁ : ) in Set.Ioo a x₀, x₁⁻¹ * upperRosserBoundaryMassAux k (s - x₀ - x₁) a x₁ a⁻¹ * (a⁻¹ * a⁻¹) ^ k

The inner integral in one recursive Rosser pair is bounded uniformly in the residual level and in every outer coordinate at most 1.

theorem MathlibNt.SieveTheory.LinearSieve.continuousAt_integral_inv_mul_upperRosserBoundaryMassAux_level_of_ae (k : ) {s a x₀ : } (ha : 0 < a) (hx₀ : x₀ 1) (hcont : ∀ᵐ (x₁ : ) MeasureTheory.volume.restrict (Set.Ioo a x₀), ContinuousAt (fun (t : ) => upperRosserBoundaryMassAux k t a x₁) (s - x₀ - x₁)) :
ContinuousAt (fun (t : ) => (x₁ : ) in Set.Ioo a x₀, x₁⁻¹ * upperRosserBoundaryMassAux k (t - x₀ - x₁) a x₁) s

Dominated convergence for the inner integral in one Rosser pair. It is enough that the residual mass be continuous in its level almost everywhere in the peeled inner coordinate.

theorem MathlibNt.SieveTheory.LinearSieve.continuousAt_integral_inv_mul_upperRosserBoundaryMassAux_level_lower_of_ae (k : ) {s a x₀ : } (ha : 0 < a) (hx₀ : x₀ 1) (hcont : ∀ᵐ (x₁ : ) MeasureTheory.volume.restrict (Set.Iio 1), ContinuousAt (fun (p : × ) => upperRosserBoundaryMassAux k (p.1 - x₀ - x₁) p.2 x₁) (s, a)) :
ContinuousAt (fun (p : × ) => (x₁ : ) in Set.Ioo p.2 x₀, x₁⁻¹ * upperRosserBoundaryMassAux k (p.1 - x₀ - x₁) p.2 x₁) (s, a)

Dominated convergence for the inner Rosser integral when both the residual level and the positive lower cutoff vary. The moving lower face is negligible, and a fixed half-cutoff supplies an integrable envelope.

theorem MathlibNt.SieveTheory.LinearSieve.continuousAt_upperRosserBoundaryMassAux_succ_level_lower_of_ae (k : ) {s a b : } (ha : 0 < a) (hb : b 1) (hinner : ∀ᵐ (x₀ : ) MeasureTheory.volume.restrict (Set.Iio 1), ContinuousAt (fun (p : × ) => (x₁ : ) in Set.Ioo p.2 x₀, x₁⁻¹ * upperRosserBoundaryMassAux k (p.1 - x₀ - x₁) p.2 x₁) (s, a)) :
ContinuousAt (fun (p : × ) => upperRosserBoundaryMassAux (k + 1) p.1 p.2 b) (s, a)

Dominated convergence for one complete Rosser pair when the residual level and positive lower cutoff vary jointly. The three moving outer faces are null, while the preceding inner-integral lemma supplies pointwise continuity.

Every positive-depth recursive Rosser mass is jointly continuous in the residual level and positive lower cutoff. At the first positive depth, the two depth-zero affine jumps occur only on null inner slices; subsequent depths follow by induction and dominated convergence.

theorem MathlibNt.SieveTheory.LinearSieve.continuousOn_upperRosserBoundaryMassAux_level_lower_succ (k : ) {b r₀ r₁ c : } (hb : b 1) (hc : 0 < c) :
ContinuousOn (fun (p : × ) => upperRosserBoundaryMassAux (k + 1) p.1 p.2 b) (Set.Icc r₀ r₁ ×ˢ Set.Icc c 1)

Positive-depth recursive Rosser mass is jointly continuous in residual level and lower cutoff on every compact box screened away from zero.

theorem MathlibNt.SieveTheory.LinearSieve.exists_upperRosserBoundaryMassAux_level_lower_modulus_succ (k : ) {b r₀ r₁ c ε : } (hb : b 1) (hc : 0 < c) ( : 0 < ε) :
δ > 0, pSet.Icc r₀ r₁ ×ˢ Set.Icc c 1, qSet.Icc r₀ r₁ ×ˢ Set.Icc c 1, dist p q < δ|upperRosserBoundaryMassAux (k + 1) p.1 p.2 b - upperRosserBoundaryMassAux (k + 1) q.1 q.2 b| < ε

Joint residual-level/lower-cutoff continuity has a uniform modulus on each compact box screened away from zero.

theorem MathlibNt.SieveTheory.LinearSieve.continuousAt_upperRosserBoundaryMassAux_succ_level_of_ae (k : ) {s a b : } (ha : 0 < a) (hb : b 1) (hinner : ∀ᵐ (x₀ : ) MeasureTheory.volume.restrict (Set.Ioo a b), ContinuousAt (fun (t : ) => (x₁ : ) in Set.Ioo a x₀, x₁⁻¹ * upperRosserBoundaryMassAux k (t - x₀ - x₁) a x₁) s) :
ContinuousAt (fun (t : ) => upperRosserBoundaryMassAux (k + 1) t a b) s

The outer integral in one Rosser pair is continuous in the residual level provided its inner integral is almost everywhere continuous there. The moving face x₀ = s / 3 is a singleton and hence does not obstruct dominated convergence.

Every positive-depth recursive Rosser boundary mass is continuous in its residual level. At depth zero there are two affine jumps; after one peeled pair, both jumps lie on null one-dimensional slices and dominated convergence smooths them.

The inner integral in one Rosser pair is jointly continuous in the residual level and the peeled outer coordinate once the residual boundary mass has positive depth. Clipping the moving upper face at 1 gives a global dominated convergence argument whose restriction is the desired ordered integral.

theorem MathlibNt.SieveTheory.LinearSieve.exists_integral_inv_mul_upperRosserBoundaryMassAux_outer_modulus_succ (k : ) {s₀ s₁ a ε : } (ha : 0 < a) ( : 0 < ε) :
δ > 0, pSet.Icc s₀ s₁ ×ˢ Set.Icc a 1, qSet.Icc s₀ s₁ ×ˢ Set.Icc a 1, dist p q < δ|( (x₁ : ) in Set.Ioo a p.2, x₁⁻¹ * upperRosserBoundaryMassAux (k + 1) (p.1 - p.2 - x₁) a x₁) - (x₁ : ) in Set.Ioo a q.2, x₁⁻¹ * upperRosserBoundaryMassAux (k + 1) (q.1 - q.2 - x₁) a x₁| < ε

On compact level and outer-coordinate ranges, the positive-depth inner Rosser integral has a uniform modulus.

Positive-depth residual-level continuity is uniform on every compact level interval.

theorem MathlibNt.SieveTheory.LinearSieve.exists_upperRosserBoundaryMassAux_level_modulus_succ (k : ) {a b r₀ r₁ ε : } (ha : 0 < a) (hb : b 1) ( : 0 < ε) :
δ > 0, sSet.Icc r₀ r₁, tSet.Icc r₀ r₁, |s - t| < δ|upperRosserBoundaryMassAux (k + 1) s a b - upperRosserBoundaryMassAux (k + 1) t a b| < ε

Quantitative residual-level modulus on a compact interval.

theorem MathlibNt.SieveTheory.LinearSieve.exists_upperRosserBoundaryMassAux_level_cell_majorant_succ (k : ) {a b r₀ r₁ ε : } (ha : 0 < a) (hb : b 1) ( : 0 < ε) :
δ > 0, ∀ {l r s : }, l Set.Icc r₀ r₁r Set.Icc r₀ r₁l ss rr - l < δupperRosserBoundaryMassAux (k + 1) s a b upperRosserBoundaryMassAux (k + 1) l a b + ε

On a sufficiently short residual-level cell, the left-endpoint value plus an arbitrarily small error majorizes every positive-depth value in that cell.

At fixed level and positive lower cutoff, enlarging an inherited upper face up to the global cutoff can only increase the recursive boundary mass.

At fixed level and positive lower cutoff, every finite-depth boundary mass is continuous in its inherited upper face on the global screened interval.

On a positive screen, the cutoff dependence of every finite-depth boundary mass has a modulus uniform across the whole inherited-cutoff interval.

theorem MathlibNt.SieveTheory.LinearSieve.exists_upperRosserBoundaryMassAux_upper_modulus (k : ) {s a ε : } (ha : 0 < a) ( : 0 < ε) :
δ > 0, bSet.Icc a 1, dSet.Icc a 1, |b - d| < δ|upperRosserBoundaryMassAux k s a b - upperRosserBoundaryMassAux k s a d| < ε

Quantitative form of uniform cutoff continuity, suitable for controlling right-endpoint majorants on a sufficiently fine finite partition.

theorem MathlibNt.SieveTheory.LinearSieve.exists_upperRosserBoundaryMassAux_cell_majorant (k : ) {s a ε : } (ha : 0 < a) ( : 0 < ε) :
δ > 0, ∀ {l r b : }, l Set.Icc a 1r Set.Icc a 1l bb rr - l < δupperRosserBoundaryMassAux k s a b upperRosserBoundaryMassAux k s a l + ε

On every sufficiently short cutoff cell, its right-endpoint boundary mass majorizes all values in the cell and exceeds its left-endpoint value by less than the prescribed error.

theorem MathlibNt.SieveTheory.LinearSieve.exists_upperRosserBoundaryMassAux_level_upper_cell_majorant_succ (k : ) {a d r₀ r₁ l ε : } (ha : 0 < a) (hd : d Set.Icc a 1) (hl : l Set.Icc r₀ r₁) ( : 0 < ε) :
δ > 0, ∀ {s c b : }, s Set.Icc r₀ r₁c Set.Icc a 1l ss - l < δc bb dd - c < δupperRosserBoundaryMassAux (k + 1) s a b upperRosserBoundaryMassAux (k + 1) l a c + ε

A local rectangular-cell majorant combining residual-level continuity with cutoff continuity. The residual lower endpoint l and cutoff upper endpoint d are fixed cell corners; taking the minimum of these finitely many local moduli gives the mesh datum required by a finite two-stage Darboux partition.

theorem MathlibNt.SieveTheory.LinearSieve.exists_upperRosserBoundaryMassAux_inner_cell_majorant_succ (k : ) {s x₀ a l r r₀ r₁ ε : } (ha : 0 < a) (hl : l Set.Icc a 1) (hr : r Set.Icc a 1) (hresL : s - x₀ - r Set.Icc r₀ r₁) (hresR : s - x₀ - l Set.Icc r₀ r₁) ( : 0 < ε) :
δ > 0, r - l < δxSet.Icc l r, upperRosserBoundaryMassAux (k + 1) (s - x₀ - x) a x upperRosserBoundaryMassAux (k + 1) (s - x₀ - r) a l + ε

Specialization of the two-parameter cell estimate to the affine residual s - x₀ - x. On a short inner-coordinate cell, its lower residual corner and lower cutoff jointly majorize every positive-depth residual, up to ε.

At positive residual depth, the residual level and inherited upper cutoff vary jointly continuously on every compact screened rectangle. Monotonicity in the upper cutoff lets the two separate continuity estimates be combined without requiring any regularity of the depth-zero integrand.

theorem MathlibNt.SieveTheory.LinearSieve.exists_upperRosserBoundaryMassAux_level_upper_modulus_succ (k : ) {a r₀ r₁ ε : } (ha : 0 < a) ( : 0 < ε) :
δ > 0, pSet.Icc r₀ r₁ ×ˢ Set.Icc a 1, qSet.Icc r₀ r₁ ×ˢ Set.Icc a 1, dist p q < δ|upperRosserBoundaryMassAux (k + 1) p.1 a p.2 - upperRosserBoundaryMassAux (k + 1) q.1 a q.2| < ε

Quantitative joint modulus for positive-depth residual mass on a compact level/cutoff rectangle.

At fixed residual level and positive lower cutoff, the inherited upper face varies continuously on any compact interval below the global cutoff, including the part where that face lies below the lower cutoff and the mass vanishes.

theorem MathlibNt.SieveTheory.LinearSieve.exists_upperRosserBoundaryMassAux_level_lower_upper_modulus_succ (k : ) {r₀ r₁ c ε : } (hc : 0 < c) ( : 0 < ε) :
δ > 0, p ∈ (Set.Icc r₀ r₁ ×ˢ Set.Icc c 1) ×ˢ Set.Icc c 1, q ∈ (Set.Icc r₀ r₁ ×ˢ Set.Icc c 1) ×ˢ Set.Icc c 1, dist p q < δ|upperRosserBoundaryMassAux (k + 1) p.1.1 p.1.2 p.2 - upperRosserBoundaryMassAux (k + 1) q.1.1 q.1.2 q.2| < ε

Positive-depth residual mass has one uniform modulus in the residual level, lower cutoff, and inherited upper face on every screened compact box.

theorem MathlibNt.SieveTheory.LinearSieve.exists_integral_inv_mul_upperRosserBoundaryMassAux_lower_modulus_succ (k : ) {s₀ s₁ c ε : } (hc : 0 < c) ( : 0 < ε) :
δ > 0, ∀ {s x₀ l a : }, s Set.Icc s₀ s₁x₀ Set.Icc c 1l Set.Icc c 1a Set.Icc c 1l aa - l < δ (x : ) in Set.Ioo l x₀, x⁻¹ * upperRosserBoundaryMassAux (k + 1) (s - x₀ - x) l x ( (x : ) in Set.Ioo a x₀, x⁻¹ * upperRosserBoundaryMassAux (k + 1) (s - x₀ - x) a x) + ε

Moving the positive lower cutoff of a positive-depth inner Rosser integral through a sufficiently short interval changes the integral by an arbitrarily small amount, uniformly in the residual level and outer coordinate on a compact screened box.

theorem MathlibNt.SieveTheory.LinearSieve.exists_integral_inv_mul_upperRosserBoundaryMassAux_outer_endpoint_modulus_succ (k : ) {s₀ s₁ c ε : } (hc : 0 < c) ( : 0 < ε) :
δ > 0, ∀ {s a x₀ y₀ : }, s Set.Icc s₀ s₁a Set.Icc c 1x₀ Set.Icc c 1y₀ Set.Icc c 1a x₀x₀ y₀y₀ - x₀ < δ (x : ) in Set.Ioo a y₀, x⁻¹ * upperRosserBoundaryMassAux (k + 1) (s - y₀ - x) a x ( (x : ) in Set.Ioo a x₀, x⁻¹ * upperRosserBoundaryMassAux (k + 1) (s - x₀ - x) a x) + ε

Increasing the outer endpoint of a positive-depth inner Rosser integral by a short amount has uniformly small cost, simultaneously for every lower cutoff in a compact positive screen.

theorem MathlibNt.SieveTheory.LinearSieve.exists_integral_inv_mul_upperRosserBoundaryMassAux_outer_endpoint_modulus_succ_global (k : ) {s₀ s₁ c ε : } (hc : 0 < c) ( : 0 < ε) :
δ > 0, ∀ {s a x₀ y₀ : }, s Set.Icc s₀ s₁a Set.Icc c 1x₀ Set.Icc c 1y₀ Set.Icc c 1x₀ y₀y₀ - x₀ < δ (x : ) in Set.Ioo a y₀, x⁻¹ * upperRosserBoundaryMassAux (k + 1) (s - y₀ - x) a x ( (x : ) in Set.Ioo a x₀, x⁻¹ * upperRosserBoundaryMassAux (k + 1) (s - x₀ - x) a x) + ε

The outer-endpoint modulus also covers the unique mesh cell crossing the moving lower cutoff: below the cutoff the integral vanishes, while the remaining strip has uniformly bounded length.