Subpolynomial cost at the F87 prime-factor cutoff

The partition count is at most x^ε, uniformly for 2 ≤ T ≤ x and ω ≤ C*(log x)^(1/5), for any fixed positive C. In particular C = 2 includes the product-variable cutoff used in F87, Section III.7, p. 628.

theorem LiLiuPrereqFouvry.CoprimePartition.partition_cost_isLittleO : (fun (u : ℝ) => u ^ (2 / 5) * Real.log (partitionConstant * u)) =o[Filter.atTop] fun (u : ℝ) => u

theorem LiLiuPrereqFouvry.CoprimePartition.eventually_partition_log_cost {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, Real.log x ^ (2 / 5) * Real.log (partitionConstant * Real.log x) ≤ ε * Real.log x

theorem LiLiuPrereqFouvry.CoprimePartition.eventually_card_realPartition_le_rpow_of_factor {C ε : ℝ} (hC : 0 < C) (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (T : ℝ), 2 ≤ T → T ≤ x → ∀ (ω : ℕ), ↑ω ≤ C * Real.log x ^ (1 / 5) → ↑(realPartition T ω).card ≤ x ^ ε

The asymptotic cost is uniform both in the real cutoff and in the growing number of distinct prime factors. No fixed-ω assumption is used.

theorem LiLiuPrereqFouvry.CoprimePartition.eventually_card_realPartition_le_rpow {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (T : ℝ), 2 ≤ T → T ≤ x → ∀ (ω : ℕ), ↑ω ≤ Real.log x ^ (1 / 5) → ↑(realPartition T ω).card ≤ x ^ ε