ScaleFirstTailAggregation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact summation of retained-envelope height tails over the original labels, sharp side dyads and low distinguished-scale pieces.

def OAI.CubicFirstMoment.scaleFirstStoppedEnvelopeTail line 15
lemma OAI.CubicFirstMoment.scaleFirstTailStoppedRow_height_dyads line 22
theorem OAI.CubicFirstMoment.scaleFirstStoppedEnvelopeTail_aggregate line 45
theorem OAI.CubicFirstMoment.scaleFirstStoppedEnvelopeTail_bound line 107

theorem OAI.CubicFirstMoment.scaleFirstStoppedEnvelopeTail_isLittleO line 140

Source documentation

A common logarithmic height cutoff works for every arity in a fixed finite collection, without restrictions on the chosen boundary label.

theorem scaleFirstStoppedEnvelopeTail_isLittleO (m : ℕ)
    (hpnt : PrimaryPrimePNT) {C ξ ρ ε : ℝ}
    (hMV : MontgomeryVaughanBound C) (hC : 0 ≤ C)
    (hHuxley : HuxleyAdditiveLargeSieve)
    (hξ : 0 < ξ) (hξz : ξ ≤ 2/5) (hρ : 1 < ρ) (hρ₂ : ρ ≤ 2)
    (hε : 0 ≤ ε) (hsmall : ρ ≤ (2:ℝ)^ε) (hgap : ξ+ε < 1/100) :
    ∃ Ct : ℕ, ∀ (H T : ℝ → ℝ) (h : ℝ → ℕ) (early : ℝ → Bool),
      (∀ᶠ X : ℝ in atTop, (1+Real.log X)^Ct ≤ T X) →
      (∀ᶠ X : ℝ in atTop, 1 ≤ H X) →
      (∀ᶠ X : ℝ in atTop, H X ≤ X) →
      (fun X => ∑ i ∈ Finset.range m,
        scaleFirstStoppedEnvelopeTail i ρ ξ (H X) (T X) X (h X) (early X))
…

Mentions: OAI.CubicFirstMoment.PrimaryPrimePNT, OAI.CubicFirstMoment.MontgomeryVaughanBound, OAI.CubicFirstMoment.HuxleyAdditiveLargeSieve, OAI.CubicFirstMoment.scaleFirstStoppedEnvelopeTail