Exact source splitting. The split exponent need not equal the final modulus-level exponent subsequently chosen by the small-source theorem.

def Wu2004MeanValue.sourceMask (S : Finset ℕ) (f : ℕ → ℝ) (m : ℕ) : ℝ

Equations

• Wu2004MeanValue.sourceMask S f m = if m ∈ S then f m else 0

theorem Wu2004MeanValue.abs_sourceMask_le (S : Finset ℕ) (f : ℕ → ℝ) (F : ℝ) (hF : 0 ≤ F) (hf : ∀ m ∈ S, |f m| ≤ F) (m : ℕ) : |sourceMask S f m| ≤ F

theorem Wu2004MeanValue.actualAPSum_split_source (S : Finset ℕ) (f r : ℕ → ℝ) (L U d b : ℕ) (hS : S ⊆ Finset.Icc 1 U) : actualAPSum S f r d b = actualAPSum ({m ∈ S | m ≤ L}) f r d b + actualAPSum (Finset.Ioc L U) (sourceMask S f) r d b

theorem Wu2004MeanValue.sourceMask_endpoint_extension (S : Finset ℕ) (f r : ℕ → ℝ) (x : ℝ) (hS : ∀ m ∈ S, 0 ≤ r m ∧ ↑m * r m ≤ x) (hx : 0 ≤ x) : (∀ (m : ℕ), (0 ≤ if m ∈ S then r m else 0) ∧ (↑m * if m ∈ S then r m else 0) ≤ x) ∧ ∀ (T : Finset ℕ) (d b : ℕ), actualAPSum T (sourceMask S f) (fun (m : ℕ) => if m ∈ S then r m else 0) d b = actualAPSum T (sourceMask S f) r d b

theorem Wu2004MeanValue.ceil_log_source_cutoff (x b : ℝ) (hlog : 2 ≤ Real.log x) (hb : 0 ≤ b) : Real.log x ^ (2 * b) ≤ ↑⌈Real.log x ^ (2 * b)⌉₊ ∧ ↑⌈Real.log x ^ (2 * b)⌉₊ ≤ Real.log x ^ (2 * b + 1)

theorem Wu2004MeanValue.legal_source_endpoint_extension (S : Finset ℕ) (f r : ℕ → ℝ) (x : ℝ) (hS : ∀ m ∈ S, 2 ≤ r m ∧ ↑m * r m ≤ x) (hx : 4 ≤ x) : (∀ (m : ℕ), ↑m ≤ √x → (2 ≤ if m ∈ S then r m else 2) ∧ (↑m * if m ∈ S then r m else 2) ≤ x) ∧ ∀ (T : Finset ℕ) (d b : ℕ), actualAPSum T (sourceMask S f) (fun (m : ℕ) => if m ∈ S then r m else 2) d b = actualAPSum T (sourceMask S f) r d b