The same ordinary rough density, with the genuine global F/f factors

The real level is transported exactly to its natural ceiling; the coordinate is correspondingly log (ceil D) / log z. Monotonicity of the genuine JR functions then returns to log D / log z in the favorable directions. The moving-range power budget is retained explicitly in this module.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoarseDensity.roughOrdinaryDensity_lower (D : ℝ) (B : Finset ℕ) (g : ℕ → ℝ) : roughOrdinaryDensity false D B g = SmallRosser.lowerSetDensity D g B

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoarseDensity.roughOrdinaryDensity_upper (D : ℝ) (B : Finset ℕ) (g : ℕ → ℝ) : roughOrdinaryDensity true D B g = SmallRosser.upperSetDensity D g B

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoarseDensity.exp_sqrt_max_two_le_target {K : ℝ} (hK : 0 ≤ K) : Real.exp √(max K 2) ≤ Real.exp (6 * K + 2)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoarseDensity.dimensionOneProductBound_subset {P B : Finset ℕ} {g : ℕ → ℝ} {K : ℝ} (hBP : B ⊆ P) (hg : ∀ p ∈ P, 0 ≤ g p ∧ g p < 1) (hdim : SmallRosser.DimensionOneProductBound P g K) : SmallRosser.DimensionOneProductBound B g K

The local product hypothesis descends to a subcarrier with the SAME K. Zero deletion is handled separately by the existing actual density sieve.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoarseDensity.exists_roughOrdinaryDensity_ff_of_powerBudget : ∃ (C : ℝ), 0 < C ∧ ∀ (B : Finset ℕ), (∀ p ∈ B, Nat.Prime p) → ∀ (g : ArithmeticFunction ℝ), g.IsMultiplicative → (∀ p ∈ B, 0 ≤ g p ∧ g p < 1) → ∀ (D z K : ℝ), 1 < D → 1 < z → z ≤ D → (∀ p ∈ B, ↑p < z) → 0 ≤ K → SmallRosser.DimensionOneProductBound B (⇑g) K → 2 ≤ Real.log D / Real.log z → SmallRosser.roundedSieveCoordinate D z ^ 13 ≤ Real.log ↑⌈D⌉₊ → Real.exp 1 ≤ Real.log ↑⌈D⌉₊ → have V := ∏ p ∈ B, (1 - g p); have E := C * Real.exp (6 * K + 2) * Real.log D ^ (-(1 / 3)); V * (JurkatRichert1965ChenGammaOneQOne.jr1965f (Real.log D / Real.log z) - E) ≤ roughOrdinaryDensity false D B ⇑g ∧ roughOrdinaryDensity true D B ⇑g ≤ V * (JurkatRichert1965ChenGammaOneQOne.jr1965F (Real.log D / Real.log z) + E)

Uniform in the entire finite carrier, including its adaptive exhaustive depth. Only the error envelope is exponentially bounded, never the main continuous source mass.