RoughMoebius.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The literal primary-divisor Möbius expansion used in the small-R branch, and its exact splitting at a prime bin.

def OAI.CubicFirstMoment.cutoffMoebius line 13
lemma OAI.CubicFirstMoment.cutoffMoebius_prime_product line 16
lemma OAI.CubicFirstMoment.primary_divisors_of_squarefree_eq line 24
theorem OAI.CubicFirstMoment.roughProduct_primary_divisor_sum line 43
Source documentation
The small-R expansion is a sum over genuine primary divisors, with no ordered-factor or unit multiplicity hidden in the coefficient.
```
theorem roughProduct_primary_divisor_sum {n : Eisenstein} (hn : primary n) (hs : Squarefree n)
    (ψ : ℝ → ℝ) (w : ℝ) :
    (roughProduct ψ w n:ℂ) = ∑ d ∈ metaplecticPrimaryDivisors n, cutoffMoebius ψ w d := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.roughProduct, OAI.CubicFirstMoment.metaplecticPrimaryDivisors, OAI.CubicFirstMoment.cutoffMoebius

theorem OAI.CubicFirstMoment.cutoffMoebius_stopping_bin line 58

Source documentation

Selecting k factors in the last bin and averaging over all choices restores the exact Möbius-cutoff coefficient.

theorem cutoffMoebius_stopping_bin (ψ : ℝ → ℝ) (w : ℝ)
    (s : Finset Eisenstein) (hs : ∀ p ∈ s, primaryPrime p)
    (k : ℕ) (hk : k ≤ s.card) :
    (∑ t ∈ s.powersetCard k, (s.card.choose k:ℂ)⁻¹*
      (cutoffMoebius ψ w (∏ p ∈ t, p)*cutoffMoebius ψ w (∏ p ∈ s\t, p))) =
        cutoffMoebius ψ w (∏ p ∈ s, p) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.cutoffMoebius