StoppedCoefficientBounds.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Pointwise bounds for the actual stopped coefficients, before any analytic sequence estimate. The divisor count is literal and introduces no dependence on the number or width of prime bins.

lemma OAI.CubicFirstMoment.cutoffMoebius_norm_le_one line 14
lemma OAI.CubicFirstMoment.primeDetectorCutoff_moebius_norm line 25
theorem OAI.CubicFirstMoment.stoppedAlpha_divisor_bound line 30
theorem OAI.CubicFirstMoment.stoppedBeta_divisor_bound line 41

theorem OAI.CubicFirstMoment.stopped_coefficients_squarefree_sides line 58

Source documentation

An independently supported side can be restricted to squarefree elements without adding any cross-side coprimality predicate.

theorem stopped_coefficients_squarefree_sides (R D E U : Finset Eisenstein)
    (v : Eisenstein → ℂ) (ψ : ℝ → ℝ) (w : ℝ)
    (selected : Eisenstein → Eisenstein → Prop) (remaining : Eisenstein → Prop)
    (K : Eisenstein → ℂ) (hK : ∀ n, ¬Squarefree n → K n = 0) :
    (∑ a ∈ (primaryPairSupport E U).filter Squarefree,
      ∑ b ∈ (primaryPairSupport R D).filter Squarefree,
        stoppedAlpha E U ψ w remaining a*stoppedBeta R D v ψ w selected b*K (a*b)) =
    ∑ a ∈ primaryPairSupport E U, ∑ b ∈ primaryPairSupport R D,
      stoppedAlpha E U ψ w remaining a*stoppedBeta R D v ψ w selected b*K (a*b) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPairSupport, OAI.CubicFirstMoment.stoppedAlpha, OAI.CubicFirstMoment.stoppedBeta