LargestPrimeReindex.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact unordered largest-prime reindexing of finite squarefree primary sums. The free-prime/complement representation has multiplicity one.

lemma OAI.CubicFirstMoment.largestPrime_product_unique line 14
theorem OAI.CubicFirstMoment.sum_largestPrime_reindex line 44
Source documentation
A finite nonsmooth sum has exactly one free-largest-prime term for each original integer. Membership of the original support is retained.
```
theorem sum_largestPrime_reindex (D : Finset Eisenstein) (B : ℝ)
    (hD : ∀ d ∈ D, primary d ∧ Squarefree d ∧ norm d ≤ B)
    (hne : ∀ d ∈ D, (primaryPrimeFactors d).Nonempty)
    (F : Eisenstein → ℂ) :
    (∑ d ∈ D, F d) =
      ∑ t ∈ ((primeCutoff B) ×ˢ (primaryElementBall B)).filter
        (fun t => t.1*t.2 ∈ D ∧ ¬t.1 ∣ t.2 ∧
          largestPrimePredicate primeTieCode (primaryPrimeFactors t.2) t.1), F (t.1*t.2) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primaryPrimeFactors, OAI.CubicFirstMoment.primeCutoff, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.largestPrimePredicate, OAI.CubicFirstMoment.primeTieCode