Documentation

MathlibNt.Wu2004MeanValue.BalancedAPWeightCount

The source-wise +1 AP envelope would cost d * |S|, which is not payable above the square root. Instead, group the actual pairs by their product. A positive integer has at most one such pair per prime divisor.

theorem Wu2004MeanValue.balanced_scaledPrimeCount_sum_bound (x : ℝ) (S : Finset ℕ) (r : ℕ → ℝ) (d b : ℕ) (hx : 2 ≤ x) (hdx : ↑d ≤ x) (hS : ∀ m ∈ S, 0 < m) (hr : ∀ m ∈ S, 0 ≤ r m ∧ ↑m * r m ≤ x) :
↑d * ∑ m ∈ S, ↑(scaledPrimeCount (↑m * r m) d b m) ≤ 2 / Real.log 2 * x * Real.log x
Inspect dependencies

Wu2004MeanValue.balanced_scaledPrimeCount_sum_bound · compiled type and proof/definition references.