RoughProductMatrix.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual rough-product divisor expansion collected into the independent stopping coefficients. Original finite support and kernel are retained, and the no-stop summand is not discarded.

lemma OAI.CubicFirstMoment.sum_four_reorder line 14

theorem OAI.CubicFirstMoment.roughProduct_matrix_stopping line 38

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 (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 : ℝ} (hstart : ∀ r ∈ R, norm r < Z)
    (h : ℕ) (Q : ℝ) (v : Eisenstein → ℂ)
    (ψ : ℝ → ℝ) (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