AngularStoppedAggregation.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.angular_scaleFirstStoppedEnvelopeTail line 16
lemma OAI.CubicFirstMoment.angular_scaleFirstTailStoppedRow_height_dyads line 23
theorem OAI.CubicFirstMoment.angular_scaleFirstStoppedEnvelopeTail_aggregate line 46
theorem OAI.CubicFirstMoment.angular_scaleFirstStoppedEnvelopeTail_bound line 108

theorem OAI.CubicFirstMoment.angular_scaleFirstStoppedEnvelopeTail_isLittleO line 141

Source documentation

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

theorem angular_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,
        angular_scaleFirstStoppedEnvelopeTail ℓ i ρ ξ (H X) (T X) X (h X) (early X))
…

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