StoppedSelectedBeta.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Selected-side prime cancellation applies to the literal stoppedBeta coefficient, with its global-largest role selected exactly.

def OAI.CubicFirstMoment.stoppedSelectedTest line 12
lemma OAI.CubicFirstMoment.selected_largest_bin_nonempty line 17
lemma OAI.CubicFirstMoment.selectedStoppedDivisorSet_eq line 34

theorem OAI.CubicFirstMoment.stoppedBeta_selected_identity line 54

Source documentation

Exact coefficient collection; all analytic cancellation belongs to stopped_selected_original_saving, already proved from the raw input.

theorem stoppedBeta_selected_identity {B ρ a b w u : ℝ} {j j₀ k h : ℕ}
    (hj : j < geometricBinCount ρ B) (Z Q : ℝ) (early : Bool)
    (R : Finset Eisenstein) (hR : ∀ r ∈ R, primary r)
    (f : Eisenstein → ℂ) (v e : Eisenstein) :
    (∑ n ∈ primaryPairSupport R (primaryElementBall B),
      stoppedBeta R (primaryElementBall B) f primeDetectorCutoff w
        (stoppedSelectedTest B ρ j j₀ k h Z Q early) n *
      (if Squarefree n ∧ IsCoprime n e ∧ a < norm n ∧ norm n ≤ b
        then normTwist u n*cubicSymbol n v else 0)) =
      ∑ r ∈ R, f r*∑ d ∈ selectedStoppedDivisorSet B ρ a b j j₀ k h Z Q early r e,
        cutoffMoebius primeDetectorCutoff w d*normTwist u (r*d)*cubicSymbol (r*d) v := by
…

Mentions: OAI.CubicFirstMoment.geometricBinCount, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.primaryPairSupport, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.stoppedBeta, OAI.CubicFirstMoment.primeDetectorCutoff, OAI.CubicFirstMoment.stoppedSelectedTest, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.normTwist, OAI.CubicFirstMoment.cubicSymbol, OAI.CubicFirstMoment.selectedStoppedDivisorSet, OAI.CubicFirstMoment.cutoffMoebius