DistinguishedStoppingMatrix.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The small distinguished-product branch in the original ordered prime expansion. The factorial, independent weights, no-stop term and sharp total-product support are all retained.

def OAI.CubicFirstMoment.distinguishedSmallSupport line 15
lemma OAI.CubicFirstMoment.distinguishedTupleCoefficient_filtered_sum line 18

theorem OAI.CubicFirstMoment.distinguished_roughProduct_matrix line 51

Source documentation

The original ordered distinguished tuples with small product are exactly the no-stop sum plus the independent stopped-coefficient matrix. No analytic estimate or replacement of the product cutoff is used.

theorem distinguished_roughProduct_matrix (S : Finset Eisenstein)
    {ρ X : ℝ} (hρ : 1 < ρ) (hρ₂ : ρ ≤ 2) (hX : 1 ≤ X)
    (hS : ∀ n ∈ S, primary n ∧ Squarefree n ∧ norm n ≤ X)
    (P : ι → Finset Eisenstein) (hP : ∀ i, ∀ p ∈ P i, primaryPrime p)
    (W : ι → Eisenstein → ℂ) (Z Q : ℝ) (h : ℕ)
    (ψ : ℝ → ℝ) (w z : ℝ) (K : Eisenstein → ℂ) :
    (((Fintype.card ι).factorial:ℂ)⁻¹ *
      ∑ f ∈ (Fintype.piFinset P).filter (fun f => norm (∏ i, f i) < Z),
        (∏ i, W i (f i)*distinguishedPrimeWeight ψ w z (f i))*
          ∑ n ∈ primaryProductSlice S X (∏ i, f i),
            (roughProduct ψ w n:ℂ)*K ((∏ i, f i)*n)) =
      (∑ r ∈ distinguishedSmallSupport P Z,
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.distinguishedPrimeWeight, OAI.CubicFirstMoment.primaryProductSlice, OAI.CubicFirstMoment.roughProduct, OAI.CubicFirstMoment.distinguishedSmallSupport