Wu's exact modulus weight, paid using the product-fiber envelope.

noncomputable def Wu2004MeanValue.balancedAPEnvelopeConstant (F : ℝ) : ℝ

Equations

• Wu2004MeanValue.balancedAPEnvelopeConstant F = F * (2 / Real.log 2 + MathlibNt.SieveTheory.LiuWeight.liuPanLiEnvelopeConstant 0) * MathlibNt.SieveTheory.Richert1969.richertReciprocalTotientConstant

theorem Wu2004MeanValue.balancedAPEnvelopeConstant_nonneg {F : ℝ} (hF : 0 ≤ F) : 0 ≤ balancedAPEnvelopeConstant F

theorem Wu2004MeanValue.balanced_modulus_mul_actualAPError_le (x F : ℝ) (S : Finset ℕ) (f r : ℕ → ℝ) (d b : ℕ) (hx : 2 ≤ x) (hF : 0 ≤ F) (hd : 0 < d) (hdx : ↑d ≤ x) (hS : ∀ m ∈ S, 0 < m) (hf : ∀ m ∈ S, |f m| ≤ F) (hr : ∀ m ∈ S, 2 ≤ r m ∧ ↑m * r m ≤ x) : ↑d * actualAPError S f r d b ≤ balancedAPEnvelopeConstant F * x * (1 + Real.log x) ^ 2

theorem Wu2004MeanValue.balanced_actualAP_weighted_log_saving_of_unweighted (A F U : ℝ) (hF : 0 ≤ F) (hU : 0 ≤ U) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : ℝ) (Q : ℕ) (S : Finset ℕ) (f r : ℕ → ℝ) (b : ℕ → ℕ), Real.exp 1 ≤ x → ↑Q ≤ x → (∀ m ∈ S, 0 < m) → (∀ m ∈ S, |f m| ≤ F) → (∀ m ∈ S, 2 ≤ r m ∧ ↑m * r m ≤ x) → ∑ d ∈ Finset.Icc 1 Q, |actualAPSum S f r d (b d)| ≤ U * x / Real.log x ^ (2 * A + 11) → ∑ d ∈ Finset.Icc 1 Q, wuModulusWeight d * |actualAPSum S f r d (b d)| ≤ C * x / Real.log x ^ A