ShortMellinEnergy.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Short-average energy from the actual Dirichlet polynomial on a block

theorem OAI.JointDickman.shortAverage_block_energy_of_support line 13

Source documentation

A linear spectral bound yields a uniform bound for the original short averages. The coefficient range is explicit and the smoothing error tends to zero with the block width, profile transition width, and endpoint scales.

theorem shortAverage_block_energy_of_support (η : ℝ) (hη : 0 < η) (hηhalf : η < 1/2) :
    ∃ C : ℝ, 0 < C ∧ ∀ (f : ArithmeticFunction ℂ), (∀ n, ‖f n‖ ≤ 1) →
      ∀ (K N : ℕ) (X H ε : ℝ), 0 < X → 1 ≤ H → H ≤ X → 0 ≤ ε → ε ≤ 1 →
      K ≤ ⌊X⌋₊ → ⌊(1 + ε) * (X + H)⌋₊ ≤ N →
      ∀ A B : ℝ, 0 ≤ A → 0 ≤ B →
      (∀ T : ℝ, 1 ≤ T →
        (∫ t in -T..T, ‖mellinPolynomial
          (Ioc K N) f t‖ ^ 2) ≤ A + B * T) →
      (1 / X) * (∫ x in X..(1 + ε) * X, ‖complexShortAverage f H x‖ ^ 2) ≤
        C * (A + B * X / H) +
          2 * ε * (3 * ε + 11 / H + H / X + 1 / X + 16 * η) ^ 2 := by
…

Mentions: OAI.JointDickman.mellinPolynomial

theorem OAI.JointDickman.shortAverage_block_energy line 98