Regularity of upper Rosser boundary mass

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

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux_le_inv_sq_pow (k : ℕ) {s a b : ℝ} (ha : 0 < a) (hb : b ≤ 1) : upperRosserBoundaryMassAux k s a b ≤ (a⁻¹ * a⁻¹) ^ k

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.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux_le_of_lower_bound (k : ℕ) {s c a b : ℝ} (hc : 0 < c) (hca : c ≤ a) (hb : b ≤ 1) : upperRosserBoundaryMassAux k s a b ≤ (c⁻¹ * c⁻¹) ^ k

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

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMass_le_inv_sq_pow (k : ℕ) {s a : ℝ} (ha : 0 < a) : upperRosserBoundaryMass k s a ≤ (a⁻¹ * a⁻¹) ^ k

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

theorem MathlibNt.SieveTheory.LinearSieve.inv_sq_mul_upperRosserBoundaryMass_le_of_lower_bound (k : ℕ) {s a c : ℝ} (hc : 0 < c) (hca : c ≤ a) : a⁻¹ * a⁻¹ * upperRosserBoundaryMass k s a ≤ (c⁻¹ * c⁻¹) ^ (k + 1)

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

theorem MathlibNt.SieveTheory.LinearSieve.integrableOn_inv_mul_upperRosserBoundaryMassAux (k : ℕ) {s a b : ℝ} (ha : 0 < a) (hb : b ≤ 1) : MeasureTheory.IntegrableOn (fun (x : ℝ) => x⁻¹ * upperRosserBoundaryMassAux k (s - x) a x) (Set.Ioo a b) MeasureTheory.volume

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

theorem MathlibNt.SieveTheory.LinearSieve.integrableOn_inv_sq_mul_upperRosserBoundaryMass (k : ℕ) (s : ℝ) {c : ℝ} (hc : 0 < c) : MeasureTheory.IntegrableOn (fun (a : ℝ) => a⁻¹ * a⁻¹ * upperRosserBoundaryMass k s a) (Set.Ioo c 1) MeasureTheory.volume

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

theorem MathlibNt.SieveTheory.LinearSieve.integrableOn_upperRosserBoundaryMassAux_compactBox (k : ℕ) (s₀ s₁ : ℝ) {c : ℝ} (hc : 0 < c) : MeasureTheory.IntegrableOn (fun (p : (ℝ × ℝ) × ℝ) => upperRosserBoundaryMassAux k p.1.1 p.1.2 p.2) ((Set.Icc s₀ s₁ ×ˢ Set.Icc c 1) ×ˢ Set.Icc c 1) MeasureTheory.volume

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.

theorem MathlibNt.SieveTheory.LinearSieve.integrableOn_outer_integrand_upperRosserBoundaryMassAux (k : ℕ) {s a b : ℝ} (ha : 0 < a) (hb : b ≤ 1) : MeasureTheory.IntegrableOn (fun (x₀ : ℝ) => x₀⁻¹ * ∫ (x₁ : ℝ) in Set.Ioo a x₀, x₁⁻¹ * upperRosserBoundaryMassAux k (s - x₀ - x₁) a x₁) (Set.Ioo a b) MeasureTheory.volume

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.

theorem MathlibNt.SieveTheory.LinearSieve.continuousAt_upperRosserBoundaryMassAux_level_lower_succ (k : ℕ) {s a b : ℝ} (ha : 0 < a) (hb : b ≤ 1) : ContinuousAt (fun (p : ℝ × ℝ) => upperRosserBoundaryMassAux (k + 1) p.1 p.2 b) (s, a)

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) (hε : 0 < ε) : ∃ δ > 0, ∀ p ∈ Set.Icc r₀ r₁ ×ˢ Set.Icc c 1, ∀ q ∈ Set.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.

theorem MathlibNt.SieveTheory.LinearSieve.continuous_upperRosserBoundaryMassAux_level_succ (k : ℕ) {a b : ℝ} (ha : 0 < a) (hb : b ≤ 1) : Continuous fun (s : ℝ) => upperRosserBoundaryMassAux (k + 1) s a b

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.

theorem MathlibNt.SieveTheory.LinearSieve.continuousOn_integral_inv_mul_upperRosserBoundaryMassAux_outer_succ (k : ℕ) {a : ℝ} (ha : 0 < a) : ContinuousOn (fun (p : ℝ × ℝ) => ∫ (x₁ : ℝ) in Set.Ioo a p.2, x₁⁻¹ * upperRosserBoundaryMassAux (k + 1) (p.1 - p.2 - x₁) a x₁) (Set.univ ×ˢ Set.Icc a 1)

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) (hε : 0 < ε) : ∃ δ > 0, ∀ p ∈ Set.Icc s₀ s₁ ×ˢ Set.Icc a 1, ∀ q ∈ Set.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.

theorem MathlibNt.SieveTheory.LinearSieve.uniformContinuousOn_upperRosserBoundaryMassAux_level_succ (k : ℕ) {a b r₀ r₁ : ℝ} (ha : 0 < a) (hb : b ≤ 1) : UniformContinuousOn (fun (s : ℝ) => upperRosserBoundaryMassAux (k + 1) s a b) (Set.Icc r₀ r₁)

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) (hε : 0 < ε) : ∃ δ > 0, ∀ s ∈ Set.Icc r₀ r₁, ∀ t ∈ Set.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) (hε : 0 < ε) : ∃ δ > 0, ∀ {l r s : ℝ}, l ∈ Set.Icc r₀ r₁ → r ∈ Set.Icc r₀ r₁ → l ≤ s → s ≤ r → r - 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.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux_mono_upper (k : ℕ) {s a b d : ℝ} (ha : 0 < a) (hbd : b ≤ d) (hd : d ≤ 1) : upperRosserBoundaryMassAux k s a b ≤ upperRosserBoundaryMassAux k s a d

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

theorem MathlibNt.SieveTheory.LinearSieve.continuousOn_upperRosserBoundaryMassAux_upper (k : ℕ) {s a : ℝ} (ha : 0 < a) : ContinuousOn (fun (b : ℝ) => upperRosserBoundaryMassAux k s a b) (Set.Icc a 1)

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

theorem MathlibNt.SieveTheory.LinearSieve.uniformContinuousOn_upperRosserBoundaryMassAux_upper (k : ℕ) {s a : ℝ} (ha : 0 < a) : UniformContinuousOn (fun (b : ℝ) => upperRosserBoundaryMassAux k s a b) (Set.Icc a 1)

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) (hε : 0 < ε) : ∃ δ > 0, ∀ b ∈ Set.Icc a 1, ∀ d ∈ Set.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) (hε : 0 < ε) : ∃ δ > 0, ∀ {l r b : ℝ}, l ∈ Set.Icc a 1 → r ∈ Set.Icc a 1 → l ≤ b → b ≤ r → r - 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₁) (hε : 0 < ε) : ∃ δ > 0, ∀ {s c b : ℝ}, s ∈ Set.Icc r₀ r₁ → c ∈ Set.Icc a 1 → l ≤ s → s - l < δ → c ≤ b → b ≤ d → d - 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₁) (hε : 0 < ε) : ∃ δ > 0, r - l < δ → ∀ x ∈ Set.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 ε.

theorem MathlibNt.SieveTheory.LinearSieve.continuousOn_upperRosserBoundaryMassAux_level_upper_succ (k : ℕ) {a r₀ r₁ : ℝ} (ha : 0 < a) : ContinuousOn (fun (p : ℝ × ℝ) => upperRosserBoundaryMassAux (k + 1) p.1 a p.2) (Set.Icc r₀ r₁ ×ˢ Set.Icc a 1)

At positive residual depth, the residual level and inherited upper cutoff vary jointly continuously on every compact screened rectangle. This is a restriction of joint dominated-integral continuity; the depth-zero jumps have already been handled on null slices in the foundational induction.

theorem MathlibNt.SieveTheory.LinearSieve.exists_upperRosserBoundaryMassAux_level_upper_modulus_succ (k : ℕ) {a r₀ r₁ ε : ℝ} (ha : 0 < a) (hε : 0 < ε) : ∃ δ > 0, ∀ p ∈ Set.Icc r₀ r₁ ×ˢ Set.Icc a 1, ∀ q ∈ Set.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.

theorem MathlibNt.SieveTheory.LinearSieve.continuousOn_upperRosserBoundaryMassAux_upper_global (k : ℕ) {s a c : ℝ} (ha : 0 < a) : ContinuousOn (fun (b : ℝ) => upperRosserBoundaryMassAux k s a b) (Set.Icc c 1)

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. At positive depth the mass vanishes there; at depth zero it is independent of the inherited upper face.

theorem MathlibNt.SieveTheory.LinearSieve.exists_upperRosserBoundaryMassAux_level_lower_upper_modulus_succ (k : ℕ) {r₀ r₁ c ε : ℝ} (hc : 0 < c) (hε : 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) (hε : 0 < ε) : ∃ δ > 0, ∀ {s x₀ l a : ℝ}, s ∈ Set.Icc s₀ s₁ → x₀ ∈ Set.Icc c 1 → l ∈ Set.Icc c 1 → a ∈ Set.Icc c 1 → l ≤ a → a - 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) (hε : 0 < ε) : ∃ δ > 0, ∀ {s a x₀ y₀ : ℝ}, s ∈ Set.Icc s₀ s₁ → a ∈ Set.Icc c 1 → x₀ ∈ Set.Icc c 1 → y₀ ∈ Set.Icc c 1 → a ≤ 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) (hε : 0 < ε) : ∃ δ > 0, ∀ {s a x₀ y₀ : ℝ}, s ∈ Set.Icc s₀ s₁ → a ∈ Set.Icc c 1 → x₀ ∈ Set.Icc c 1 → y₀ ∈ Set.Icc c 1 → 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) + ε

The joint inner-integral modulus also covers a mesh cell crossing the moving lower cutoff. Empty and coincident intervals need no separate strip estimate because the moving-interval continuity theorem includes them.