PrimeTupleDecomposition.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Actual primary factor tuples in the distinguished-prime expansion. Ordering a subset contributes its factorial; the remaining primary factor is the literal complementary product, not an abstract coefficient.

def OAI.CubicFirstMoment.distinguishedPrimeWeight line 16
def OAI.CubicFirstMoment.primaryFactorRemainder line 19
lemma OAI.CubicFirstMoment.primaryFactorRemainder_spec line 22
lemma OAI.CubicFirstMoment.roughProduct_primaryFactorRemainder line 32
lemma OAI.CubicFirstMoment.ordered_subset_product line 40
theorem OAI.CubicFirstMoment.roughProduct_ordered_primary_tuples line 55
Source documentation
The exact distinguished expansion with ordered distinct primary prime tuples and the manuscript's factor 1/i!.
```
theorem roughProduct_ordered_primary_tuples {n : Eisenstein} (hn : primary n)
    (ψ : ℝ → ℝ) (w z : ℝ) :
    (roughProduct ψ z n:ℂ) =
      ∑ s ∈ (primaryPrimeFactors n).powerset,
        ((s.card.factorial:ℂ)⁻¹)*
          (∑ e : Fin s.card ≃ s,
            (∏ i : Fin s.card, distinguishedPrimeWeight ψ w z (e i)))*
          (roughProduct ψ w (primaryFactorRemainder n s):ℂ) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.roughProduct, OAI.CubicFirstMoment.primaryPrimeFactors, OAI.CubicFirstMoment.distinguishedPrimeWeight, OAI.CubicFirstMoment.primaryFactorRemainder
lemma OAI.CubicFirstMoment.distinguishedPrimeWeight_support line 73
lemma OAI.CubicFirstMoment.primary_factor_subset_card_lt line 96
Source documentation
Every chosen prime is large; the product bound therefore bounds the number of chosen factors, uniformly in the original squarefree element.
```
lemma primary_factor_subset_card_lt {n : Eisenstein} (hn : primary n) (hs : Squarefree n)
    {s : Finset Eisenstein} (hsub : s ⊆ primaryPrimeFactors n)
    {w : ℝ} (hw : 1 ≤ w) (hlarge : ∀ p ∈ s, w ≤ norm p)
    {k : ℕ} (hsize : norm n < w^k) : s.card < k := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.primaryPrimeFactors, OAI.CubicFirstMoment.norm