Transfer of a linear mean through an absolutely convergent convolution

The summatory function of a Dirichlet convolution has the form ∑ d, g d * A (x / d). Absolute convergence of ∑ |g d| / d allows its linear mean to be computed by dominated convergence.

theorem NairTenenbaum.tendsto_scaled_convolution_mean {A : ℝ → ℝ} {g : ℕ → ℝ} {C L : ℝ} (hA0 : A 0 = 0) (hbound : ∀ (t : ℝ), 0 ≤ t → |A t| ≤ C * t) (hmean : Filter.Tendsto (fun (t : ℝ) => A t / t) Filter.atTop (nhds L)) (hsum : Summable fun (d : ℕ) => |g d| / ↑d) : Filter.Tendsto (fun (x : ℝ) => (∑' (d : ℕ), g d * A (x / ↑d)) / x) Filter.atTop (nhds (L * ∑' (d : ℕ), g d / ↑d))

noncomputable def NairTenenbaum.arithmeticSummatory (a : ℕ → ℝ) (x : ℝ) : ℝ

The real summatory function, including only positive indices.

Equations

• NairTenenbaum.arithmeticSummatory a x = ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, a n

@[simp]

theorem NairTenenbaum.arithmeticSummatory_zero (a : ℕ → ℝ) : arithmeticSummatory a 0 = 0

theorem NairTenenbaum.arithmeticSummatory_limit_of_nat_limit {a : ℕ → ℝ} {L : ℝ} (h : Filter.Tendsto (fun (n : ℕ) => (∑ k ∈ Finset.Icc 1 n, a k) / ↑n) Filter.atTop (nhds L)) : Filter.Tendsto (fun (x : ℝ) => arithmeticSummatory a x / x) Filter.atTop (nhds L)

theorem NairTenenbaum.arithmeticSummatory_linear_bound_of_nat_limit {a : ℕ → ℝ} {L : ℝ} (h : Filter.Tendsto (fun (n : ℕ) => (∑ k ∈ Finset.Icc 1 n, a k) / ↑n) Filter.atTop (nhds L)) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : ℝ), 0 ≤ x → |arithmeticSummatory a x| ≤ C * x

theorem NairTenenbaum.tendsto_arithmeticSummatory_convolution_mean {a g : ℕ → ℝ} {L : ℝ} (h : Filter.Tendsto (fun (n : ℕ) => (∑ k ∈ Finset.Icc 1 n, a k) / ↑n) Filter.atTop (nhds L)) (hg : Summable fun (d : ℕ) => |g d| / ↑d) : Filter.Tendsto (fun (x : ℝ) => (∑' (d : ℕ), g d * arithmeticSummatory a (x / ↑d)) / x) Filter.atTop (nhds (L * ∑' (d : ℕ), g d / ↑d))

theorem NairTenenbaum.sum_divisorsAntidiagonal_eq_hyperbola (F : ℕ → ℕ → ℝ) (N : ℕ) : ∑ n ∈ Finset.Icc 1 N, ∑ de ∈ n.divisorsAntidiagonal, F de.1 de.2 = ∑ d ∈ Finset.Icc 1 N, ∑ e ∈ Finset.Icc 1 (N / d), F d e

theorem NairTenenbaum.arithmeticSummatory_mul (a g : ArithmeticFunction ℝ) (x : ℝ) : arithmeticSummatory (⇑(g * a)) x = ∑' (d : ℕ), g d * arithmeticSummatory (⇑a) (x / ↑d)

theorem NairTenenbaum.arithmeticFunction_convolution_mean {a g : ArithmeticFunction ℝ} {L : ℝ} (h : Filter.Tendsto (fun (n : ℕ) => (∑ k ∈ Finset.Icc 1 n, a k) / ↑n) Filter.atTop (nhds L)) (hg : Summable fun (d : ℕ) => |g d| / ↑d) : Filter.Tendsto (fun (x : ℝ) => arithmeticSummatory (⇑(g * a)) x / x) Filter.atTop (nhds (L * ∑' (d : ℕ), g d / ↑d))