RoughPrimeTuples.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Bounded ordered prime-factor expansion of the rough remainder in the large-R branch. Every tuple has its literal primary product.

lemma OAI.CubicFirstMoment.ordered_primary_factor_product line 13
lemma OAI.CubicFirstMoment.roughProduct_ordered_primary_factors line 22
lemma OAI.CubicFirstMoment.roughProduct_nonzero_prime_bound line 31
theorem OAI.CubicFirstMoment.bounded_rough_primary_factors line 46
Source documentation
The rough remainder also has uniformly bounded prime-factor count; this is needed before replacing it by independent prime dyads.
```
theorem bounded_rough_primary_factors {ξ C : ℝ} (hξ : 0 < ξ) (hC : 0 < C)
    {ψ : ℝ → ℝ} (hψ : ∀ x : ℝ, 0 < x → x ≤ 1 → ψ x = 1) :
    ∃ k : ℕ, ∀ᶠ X : ℝ in atTop, ∀ n : Eisenstein,
      primary n → Squarefree n → norm n ≤ C*X → roughProduct ψ (X^ξ) n ≠ 0 →
        (primaryPrimeFactors n).card < k := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.roughProduct, OAI.CubicFirstMoment.primaryPrimeFactors