GeometricStoppingCollection.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Exact independent-factor reconstruction of all stopped squarefree terms. The original finite support remains a product test.

theorem OAI.CubicFirstMoment.geometric_stopping_collection line 14

Source documentation

The full stopping-label sum reconstructs the original finite sum. The kernel and support are unchanged, including any sharp product cutoff.

theorem geometric_stopping_collection (S : Finset Eisenstein)
    {ρ X : ℝ} (hρ : 1 < ρ) (hρ₂ : ρ ≤ 2) (hX : 1 ≤ X)
    (hS : ∀ n ∈ S, primary n ∧ Squarefree n ∧ norm n ≤ X)
    {r : Eisenstein} (hr : primary r) {Z : ℝ} (hstart : norm r < Z)
    (hend : ∀ n ∈ S, Z ≤ norm r*primeSurrogate (primaryPrimeFactors n)
      (geometricPrimeBin ρ X) (geometricBinLower ρ X))
    (ψ : ℝ → ℝ) (w : ℝ) (K : Eisenstein → ℂ) :
    (∑ n ∈ S, cutoffMoebius ψ w n*K n) =
    ∑ q ∈ stoppingLabelBox ρ X, (Nat.choose (q.2.1+q.2.2) q.2.1:ℂ)⁻¹ *
      ∑ d ∈ primaryElementBall X, ∑ e ∈ primaryElementBall X,
        if d*e ∈ S then
          (if stoppingSideTest (geometricPrimeBin ρ X) (geometricBinLower ρ X)
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primeSurrogate, OAI.CubicFirstMoment.primaryPrimeFactors, OAI.CubicFirstMoment.geometricPrimeBin, OAI.CubicFirstMoment.geometricBinLower, OAI.CubicFirstMoment.cutoffMoebius, OAI.CubicFirstMoment.stoppingLabelBox, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.stoppingSideTest