StoppingCount.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual first-crossing count in one prime bin. All subsets with that count obey the same predicate, so inverse-binomial weighting is exact.

lemma OAI.CubicFirstMoment.first_bin_crossing line 12

theorem OAI.CubicFirstMoment.first_bin_crossing_coefficient line 38

Source documentation

This is the source crossing predicate on the selected side, with actual primary prime products and their actual cutoff-Möbius weights.

theorem first_bin_crossing_coefficient (ψ : ℝ → ℝ) (w : ℝ)
    (s : Finset Eisenstein) (hs : ∀ p ∈ s, primaryPrime p)
    {R ell Z : ℝ} (hR : 0 < R) (hell : 1 < ell) (hstart : R < Z)
    (hend : Z ≤ R*ell^s.card) :
    ∃ k : ℕ, 1 ≤ k ∧ k ≤ s.card ∧
      (∑ t ∈ s.powersetCard k,
        if R*ell^t.card/ell < Z ∧ Z ≤ R*ell^t.card then
          (s.card.choose k:ℂ)⁻¹*
            (cutoffMoebius ψ w (∏ p ∈ t, p)*cutoffMoebius ψ w (∏ p ∈ s\t, p))
        else 0) = cutoffMoebius ψ w (∏ p ∈ s, p) := by
…

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