ActiveRoughStopping.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

One-stage stopping needs an initial bound only on nonzero rows. This exact form applies to the upper-height distinguished-scale cutoff.

lemma OAI.CubicFirstMoment.active_sum_four_reorder line 12

theorem OAI.CubicFirstMoment.roughProduct_matrix_stopping_active line 36

Source documentation

Every distinguished row of the original rough-product expansion equals its literal no-stop term plus the independent stopped matrix. The inverse binomial is unchanged; total support is carried inside K.

theorem roughProduct_matrix_stopping_active (S R : Finset Eisenstein)
    {ρ X : ℝ} (hρ : 1 < ρ) (hρ₂ : ρ ≤ 2) (hX : 1 ≤ X)
    (hS : ∀ n ∈ S, primary n ∧ Squarefree n ∧ norm n ≤ X)
    (hR : ∀ r ∈ R, primary r) {Z : ℝ} (v : Eisenstein → ℂ) (hstart : ∀ r ∈ R, v r ≠ 0 → norm r < Z)
    (h : ℕ) (Q : ℝ)
    (ψ : ℝ → ℝ) (w : ℝ) (K : Eisenstein → ℂ) :
    (∑ r ∈ R, v r *
      ∑ n ∈ primaryProductSlice S X r, (roughProduct ψ w n:ℂ)*K (r*n)) =
      (∑ r ∈ R, v r *
        ∑ u ∈ primaryElementBall X,
          ∑ m ∈ primaryProductSlice S X (r*u) with
            norm r*primeSurrogate (primaryPrimeFactors m)
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primaryProductSlice, OAI.CubicFirstMoment.roughProduct, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.primeSurrogate, OAI.CubicFirstMoment.primaryPrimeFactors