Total variation bounds for Dirichlet Abel weights

The bounds here are obtained from the real-interval fundamental theorem of calculus and intervalIntegral.norm_integral_le_integral_norm. In particular, no monotonicity assertion is made about the complex-valued weights.

noncomputable def DirichletLAbelWeightVariation.cpowWeight (s : ℂ) (x : ℝ) : ℂ

The complex Dirichlet-series weight on a positive real variable.

Equations

• DirichletLAbelWeightVariation.cpowWeight s x = ↑x ^ (-s)

noncomputable def DirichletLAbelWeightVariation.cpowWeightDeriv (s : ℂ) (x : ℝ) : ℂ

Its real derivative, written in a form convenient for norm estimates.

Equations

• DirichletLAbelWeightVariation.cpowWeightDeriv s x = -s * ↑x ^ (-s - 1)

theorem DirichletLAbelWeightVariation.hasDerivAt_cpowWeight (s : ℂ) {x : ℝ} (hx : 0 < x) : HasDerivAt (cpowWeight s) (cpowWeightDeriv s x) x

theorem DirichletLAbelWeightVariation.norm_cpowWeightDeriv (s : ℂ) {x : ℝ} (hx : 0 < x) : ‖cpowWeightDeriv s x‖ = ‖s‖ * x ^ (-s.re - 1)

theorem DirichletLAbelWeightVariation.norm_cpowWeight_succ_sub_le_integral (s : ℂ) {k : ℕ} (hk : 1 ≤ k) : ‖cpowWeight s (↑k + 1) - cpowWeight s ↑k‖ ≤ ∫ (x : ℝ) in ↑k..↑k + 1, ‖s‖ * x ^ (-s.re - 1)

One discrete complex weight difference is bounded by the integral of the norm of its real derivative.

theorem DirichletLAbelWeightVariation.norm_cpowWeight_succ_sub_le (s : ℂ) (hs : 0 < s.re) {k : ℕ} (hk : 1 ≤ k) : ‖cpowWeight s (↑k + 1) - cpowWeight s ↑k‖ ≤ ‖s‖ / s.re * (↑k ^ (-s.re) - (↑k + 1) ^ (-s.re))

Explicit one-step majorant.

theorem DirichletLAbelWeightVariation.sum_norm_cpowWeight_sub_le_sub (s : ℂ) (hs : 0 < s.re) {m n : ℕ} (hm : 1 ≤ m) (hmn : m ≤ n) : ∑ k ∈ Finset.Ico m n, ‖cpowWeight s (↑k + 1) - cpowWeight s ↑k‖ ≤ ‖s‖ / s.re * (↑m ^ (-s.re) - ↑n ^ (-s.re))

Strong finite telescoping estimate for the total variation of k ↦ k⁻ˢ.

theorem DirichletLAbelWeightVariation.sum_norm_cpowWeight_sub_le (s : ℂ) (hs : 0 < s.re) {m n : ℕ} (hm : 1 ≤ m) (hmn : m ≤ n) : ∑ k ∈ Finset.Ico m n, ‖cpowWeight s (↑k + 1) - cpowWeight s ↑k‖ ≤ ‖s‖ / s.re * ↑m ^ (-s.re)

Finite total variation, in the simple endpoint form used by Abel summation.

theorem DirichletLAbelWeightVariation.summable_norm_cpowWeight_sub (s : ℂ) (hs : 0 < s.re) (m : ℕ) (hm : 1 ≤ m) : Summable fun (j : ℕ) => ‖cpowWeight s (↑m + ↑j + 1) - cpowWeight s (↑m + ↑j)‖

The shifted infinite total variation is summable.

theorem DirichletLAbelWeightVariation.tsum_norm_cpowWeight_sub_le (s : ℂ) (hs : 0 < s.re) (m : ℕ) (hm : 1 ≤ m) : ∑' (j : ℕ), ‖cpowWeight s (↑m + ↑j + 1) - cpowWeight s (↑m + ↑j)‖ ≤ ‖s‖ / s.re * ↑m ^ (-s.re)

Explicit tsum bound for the infinite total variation.

noncomputable def DirichletLAbelWeightVariation.logCpowWeight (s : ℂ) (x : ℝ) : ℂ

The derivative weight -log(x) x⁻ˢ, with the logarithm kept real on the positive axis.

Equations

• DirichletLAbelWeightVariation.logCpowWeight s x = -↑(Real.log x) * DirichletLAbelWeightVariation.cpowWeight s x

noncomputable def DirichletLAbelWeightVariation.logCpowWeightDeriv (s : ℂ) (x : ℝ) : ℂ

Equations

• DirichletLAbelWeightVariation.logCpowWeightDeriv s x = (s * ↑(Real.log x) - 1) * ↑x ^ (-s - 1)

theorem DirichletLAbelWeightVariation.hasDerivAt_logCpowWeight (s : ℂ) {x : ℝ} (hx : 0 < x) : HasDerivAt (logCpowWeight s) (logCpowWeightDeriv s x) x

theorem DirichletLAbelWeightVariation.norm_logCpowWeightDeriv_le (s : ℂ) {x : ℝ} (hx : 1 ≤ x) : ‖logCpowWeightDeriv s x‖ ≤ (1 + ‖s‖ * Real.log x) * x ^ (-s.re - 1)

noncomputable def DirichletLAbelWeightVariation.logVariationBudget (s : ℂ) (x : ℝ) : ℝ

Explicit primitive budget for the derivative-weight variation.

Equations

• DirichletLAbelWeightVariation.logVariationBudget s x = x ^ (-s.re) * (1 / s.re + ‖s‖ * (Real.log x / s.re + 1 / s.re ^ 2))

theorem DirichletLAbelWeightVariation.hasDerivAt_logVariationBudget (s : ℂ) (hs : 0 < s.re) {x : ℝ} (hx : 0 < x) : HasDerivAt (logVariationBudget s) (-(1 + ‖s‖ * Real.log x) * x ^ (-s.re - 1)) x

theorem DirichletLAbelWeightVariation.norm_logCpowWeight_succ_sub_le (s : ℂ) (hs : 0 < s.re) {k : ℕ} (hk : 1 ≤ k) : ‖logCpowWeight s (↑k + 1) - logCpowWeight s ↑k‖ ≤ logVariationBudget s ↑k - logVariationBudget s (↑k + 1)

theorem DirichletLAbelWeightVariation.sum_norm_logCpowWeight_sub_le_sub (s : ℂ) (hs : 0 < s.re) {m n : ℕ} (hm : 1 ≤ m) (hmn : m ≤ n) : ∑ k ∈ Finset.Ico m n, ‖logCpowWeight s (↑k + 1) - logCpowWeight s ↑k‖ ≤ logVariationBudget s ↑m - logVariationBudget s ↑n

theorem DirichletLAbelWeightVariation.sum_norm_logCpowWeight_sub_le (s : ℂ) (hs : 0 < s.re) {m n : ℕ} (hm : 1 ≤ m) (hmn : m ≤ n) : ∑ k ∈ Finset.Ico m n, ‖logCpowWeight s (↑k + 1) - logCpowWeight s ↑k‖ ≤ logVariationBudget s ↑m

theorem DirichletLAbelWeightVariation.summable_norm_logCpowWeight_sub (s : ℂ) (hs : 0 < s.re) (m : ℕ) (hm : 1 ≤ m) : Summable fun (j : ℕ) => ‖logCpowWeight s (↑m + ↑j + 1) - logCpowWeight s (↑m + ↑j)‖

theorem DirichletLAbelWeightVariation.tsum_norm_logCpowWeight_sub_le (s : ℂ) (hs : 0 < s.re) (m : ℕ) (hm : 1 ≤ m) : ∑' (j : ℕ), ‖logCpowWeight s (↑m + ↑j + 1) - logCpowWeight s (↑m + ↑j)‖ ≤ ↑m ^ (-s.re) * (1 / s.re + ‖s‖ * (Real.log ↑m / s.re + 1 / s.re ^ 2))