WeightedAbel.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Smooth weighting of prime-character sums

Partial summation applies the published unweighted Hecke prime estimate to independently specified smooth prime weights. It also retains the derivative cost of a norm twist.

theorem OAI.CubicFirstMoment.weighted_abel_bound line 21

Source documentation

Complex partial summation with an explicit bound for the cumulative coefficients. The right side records endpoint values and total variation.

theorem weighted_abel_bound (c : ℕ → ℂ) (f : ℝ → ℂ)
    {a b H : ℝ} (ha : 0 ≤ a) (hab : a ≤ b)
    (hdiff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t)
    (hderiv : IntegrableOn (deriv f) (Set.Icc a b))
    (hc : ∀ t ∈ Set.Icc a b, ‖∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k‖ ≤ H) :
    ‖∑ k ∈ Finset.Ioc ⌊a⌋₊ ⌊b⌋₊, f k * c k‖ ≤
      H * (‖f a‖ + ‖f b‖ + ∫ t in Set.Ioc a b, ‖deriv f t‖) := by
…

theorem OAI.CubicFirstMoment.weighted_abel_bound_zero_endpoints line 67

Source documentation

For a compactly supported dyadic weight, both boundary values can be chosen to vanish; only its total variation remains.

theorem weighted_abel_bound_zero_endpoints (c : ℕ → ℂ) (f : ℝ → ℂ)
    {a b H : ℝ} (ha : 0 ≤ a) (hab : a ≤ b)
    (hdiff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t)
    (hderiv : IntegrableOn (deriv f) (Set.Icc a b))
    (hc : ∀ t ∈ Set.Icc a b, ‖∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k‖ ≤ H)
    (hfa : f a = 0) (hfb : f b = 0) :
    ‖∑ k ∈ Finset.Ioc ⌊a⌋₊ ⌊b⌋₊, f k * c k‖ ≤
      H * ∫ t in Set.Ioc a b, ‖deriv f t‖ := by
…