RescaledPrefixSums.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite weighted assembly at the actual divisor scale Y = X/u. The factor 1/u is retained exactly, including floor cutoffs.

lemma OAI.TwoPointCorrelations.tendsto_nat_div_atTop line 17
lemma OAI.TwoPointCorrelations.prefix_norm_of_average_bound line 24

theorem OAI.TwoPointCorrelations.finite_rescaled_prefix_bound line 36

Source documentation

Each profile may have its own parameter. The resulting long-average threshold is common to the finite divisor family and all parameter choices.

theorem finite_rescaled_prefix_bound {ι : Type*} (U : Finset ℕ)
    (a : ℕ → ℂ) (F : ℕ → ι → ℕ → ℂ) (Valid : ℕ → ι → Prop) (E : ℝ) (hE : 0 ≤ E)
    (hU : ∀ u ∈ U, 0 < u)
    (hF : ∀ u ∈ U, ∀ᶠ Y : ℕ in atTop,
      ∀ t : ι, Valid u t → ‖positivePrefix (F u t) Y / (Y : ℂ)‖ ≤ E) :
    ∀ᶠ X : ℕ in atTop, ∀ t : ℕ → ι, (∀ u ∈ U, Valid u (t u)) →
      ‖(∑ u ∈ U, a u * positivePrefix (F u (t u)) (X / u)) / (X : ℂ)‖ ≤
        E * ∑ u ∈ U, ‖a u‖ / (u : ℝ) := by
…

Mentions: OAI.TwoPointCorrelations.positivePrefix