Uniform logarithmic cost of the actual frequency shells

The count bound depends only on the ambient scale and the fixed cutoff exponent, not the residue, nu, coefficient family, or surviving masks.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.log_two_ceil_rpow_bound {x C : ℝ} (hx : 1 ≤ x) (hC : 0 ≤ C) : ↑(Nat.log 2 ⌈x ^ C⌉₊ + 1) ≤ 2 + C * Real.log x / Real.log 2

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fullLevel_frequency_count_bound {x L M η : ℝ} (hx : 1 ≤ x) (hL0 : 0 ≤ L) (hL : L ≤ x) (hM : 1 ≤ M) (hη : 0 ≤ η) : ↑(Nat.log 2 ⌈L ^ 2 / M * x ^ η⌉₊ + 1) ≤ 2 + (η + 2) * Real.log x / Real.log 2

The full-level cutoff is at most a fixed power of x. This merely bounds the number of shells; individual cutoff tests stay unchanged.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2_frequency_count_bound {x M η ν ε : ℝ} (hx : 1 ≤ x) (hM : 1 ≤ M) (hη : 0 ≤ η) (hν : 0 ≤ ν) (hε : 0 ≤ ε) : ↑(Nat.log 2 ⌈(x ^ ((5 - 5 * ν) / 9 - ε)) ^ 2 / M * x ^ η⌉₊ + 1) ≤ 2 + (η + 2) * Real.log x / Real.log 2

The C.2 level gives the required ambient-scale bound with no constant depending on the varying short-variable exponent nu.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.eventually_fullLevel_frequency_count_le_rpow {η δ : ℝ} (hη : 0 ≤ η) (hδ : 0 < δ) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (L M : ℝ), 0 ≤ L → L ≤ x → 1 ≤ M → ↑(Nat.log 2 ⌈L ^ 2 / M * x ^ η⌉₊ + 1) ≤ x ^ δ

A fixed power margin absorbs the shell count uniformly over both varying scales. The threshold is chosen before L and M.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.eventually_fullLevel_exponential_rpow_bound {η δ : ℝ} (hη : 0 ≤ η) (hδ : 0 < δ) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (L M : ℝ), 0 ≤ L → L ≤ x → 1 ≤ M → ∀ (N : Finset ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ), ∃ b ≤ Nat.log 2 ⌈L ^ 2 / M * x ^ η⌉₊, ∃ y ∈ Set.Icc (1 / 2) 3, |wMaskedFactorExtractedTruncated M (wUniformCutoff M (x ^ η)) N (Finset.Ioc 0 ⌊L⌋₊) β c₁ γ ζ a P R S ξ| ≤ 3 * M * x ^ δ * ‖wExtractedBlockExponential (wUniformCutoff M (x ^ η)) N (Finset.Ioc 0 ⌊L⌋₊) β c₁ γ ζ a P R S ξ b (M * y)‖

Absorb the shell count in the actual integral-to-maximum W estimate. There is still no hypothesis asserting cancellation in a weighted sum.