CenteredShortCoefficients.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Centering the short average before the Mellin transfer

def OAI.JointDickman.centeredShortCoefficients line 10
Source documentation
The factor three accommodates a long average of norm at most two.
```
noncomputable def centeredShortCoefficients (f : ArithmeticFunction ℂ) (c : ℂ) :
    ArithmeticFunction ℂ :=
…
```
theorem OAI.JointDickman.centeredShortCoefficients_norm_le line 14
lemma OAI.JointDickman.short_interval_card_error line 25

theorem OAI.JointDickman.centeredShortCoefficients_short_identity line 35

Source documentation

Centering commutes with short averaging up to the exact integer count.

theorem centeredShortCoefficients_short_identity (f : ArithmeticFunction ℂ) (c : ℂ)
    (x H : ℝ) :
    complexShortAverage f H x - c =
      3 * complexShortAverage (centeredShortCoefficients f c) H x +
        (((Ioc ⌊x⌋₊ ⌊x + H⌋₊).card : ℂ) / (H : ℂ) - 1) * c := by
…

Mentions: OAI.JointDickman.centeredShortCoefficients

theorem OAI.JointDickman.centeredShortCoefficients_short_error line 57

Source documentation

The integer count costs at most 2/H; no regularity of the coefficients is used in this centering step.

theorem centeredShortCoefficients_short_error (f : ArithmeticFunction ℂ)
    {c : ℂ} (hc : ‖c‖ ≤ 2) {x H : ℝ} (hx : 0 ≤ x) (hH : 0 < H) :
    ‖complexShortAverage f H x - c‖ ≤
      3 * ‖complexShortAverage (centeredShortCoefficients f c) H x‖ + 2 / H := by
…

Mentions: OAI.JointDickman.centeredShortCoefficients