MellinBoundedFrequencyLimit.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The low-frequency consequence of ordinary marginal prefix means

theorem OAI.JointDickman.angularMellin_uniform_bounded_frequency line 13

Source documentation

Uniformity over a fixed bounded frequency range follows from marginal means alone. Multiplicativity is needed only for the remaining frequencies.

theorem angularMellin_uniform_bounded_frequency (f : ℝ → ℕ → ℂ) {C : ℝ}
    (hC : 0 ≤ C) (hf : ∀ x n, ‖f x n‖ ≤ C) (hf0 : ∀ x, f x 0 = 0)
    (hmean : ∀ A : ℝ, 0 < A → Tendsto
      (fun x : ℝ => (∑ n ∈ Ioc 0 ⌊A * x⌋₊, f x n) / (x : ℂ)) atTop (𝓝 0))
    {A T ε : ℝ} (hA : 0 < A) (hT : 0 ≤ T) (hε : 0 < ε) :
    ∀ᶠ x : ℝ in atTop, ∀ t : ℝ, |t| ≤ T →
      ‖angularMellinPolynomial (Ioc ⌊A * x⌋₊ ⌊4 * (A * x)⌋₊) (f x) t‖ ≤ ε := by
…

Mentions: OAI.JointDickman.angularMellinPolynomial