UniformPrefixLimit.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform scaled-prefix consequence of marginal mean convergence

theorem OAI.JointDickman.uniform_prefix_of_marginal_means line 12

Source documentation

Pointwise convergence at every fixed positive counting multiple becomes uniform on a bounded interval because each summand is bounded.

theorem uniform_prefix_of_marginal_means (f : ℝ → ℕ → ℂ) {C : ℝ}
    (hC : 0 ≤ C) (hf : ∀ x n, ‖f x n‖ ≤ C)
    (hmean : ∀ A : ℝ, 0 < A → Tendsto
      (fun x : ℝ => (∑ n ∈ Ioc 0 ⌊A * x⌋₊, f x n) / (x : ℂ)) atTop (𝓝 0))
    (R : ℝ) (_hR : 0 ≤ R) {ε : ℝ} (hε : 0 < ε) :
    ∀ᶠ x : ℝ in atTop, ∀ u ∈ Set.Icc (0 : ℝ) (R * x),
      ‖∑ n ∈ Ioc 0 ⌊u⌋₊, f x n‖ ≤ ε * x := by
…