Positive linear means give lower bounds in dyadic divisor windows

theorem NairTenenbaum.sum_shortInterval_half_eq_summatory_sub (a : ℕ → ℝ) {y : ℝ} (hy : 0 ≤ y) : ∑ n ∈ shortInterval (y / 2) (y / 2), a n = arithmeticSummatory a y - arithmeticSummatory a (y / 2)

theorem NairTenenbaum.tendsto_dyadic_mean {a : ℕ → ℝ} {L : ℝ} (h : Filter.Tendsto (fun (x : ℝ) => arithmeticSummatory a x / x) Filter.atTop (nhds L)) : Filter.Tendsto (fun (y : ℝ) => (∑ n ∈ shortInterval (y / 2) (y / 2), a n) / y) Filter.atTop (nhds (L / 2))

theorem NairTenenbaum.eventually_dyadic_weighted_sum_ge_of_mean {a : ℕ → ℝ} {L : ℝ} (ha : ∀ (n : ℕ), 0 ≤ a n) (hL : 0 < L) (h : Filter.Tendsto (fun (x : ℝ) => arithmeticSummatory a x / x) Filter.atTop (nhds L)) : ∀ᶠ (y : ℝ) in Filter.atTop, L / 4 ≤ ∑ n ∈ shortInterval (y / 2) (y / 2), a n / ↑n

theorem NairTenenbaum.eventually_dyadicRootDensity_ge_of_minorant_mean {Q : Polynomial ℤ} {a : ℕ → ℝ} {L : ℝ} (ha : ∀ (n : ℕ), 0 ≤ a n) (hroot : ∀ (n : ℕ), a n ≤ ↑(rootCount Q n)) (hL : 0 < L) (h : Filter.Tendsto (fun (x : ℝ) => arithmeticSummatory a x / x) Filter.atTop (nhds L)) : ∀ᶠ (y : ℝ) in Filter.atTop, L / 4 ≤ dyadicRootDensitySum Q y