OAI/NumberTheory/JointDickman/Analysis/CenteredMellinEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Centered short-average energy for the real mean-comparison application

  1. theorem OAI.JointDickman.complexShortAverage_sub_sq_integrable line 9
  2. theorem OAI.JointDickman.centeredShort_energy_le line 22

    Source documentation

    Passing to centered coefficients has only an O(1/H^2) energy cost.

    theorem centeredShort_energy_le (f : ArithmeticFunction ℂ) (hf : ∀ n, ‖f n‖ ≤ 1)
    {c : ℂ} (hc : ‖c‖ ≤ 2) {X H : ℝ} (hX : 0 < X) (hH : 0 < H) :
    (1 / X) * (∫ x in X..2 * X, ‖complexShortAverage f H x - c‖ ^ 2) ≤
      18 * ((1 / X) * (∫ x in X..2 * X,
        ‖complexShortAverage (centeredShortCoefficients f c) H x‖ ^ 2)) + 8 / H ^ 2 := by
…

    Mentions: OAI.JointDickman.centeredShortCoefficients

  3. theorem OAI.JointDickman.centeredShortAverage_dyadic_energy line 55