PrimeStoppingUnique.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Uniqueness of the actual first crossing bin and the selected count. This supplies the missing uniqueness direction for the finite stop sum.

lemma OAI.CubicFirstMoment.crossing_index_unique line 14
lemma OAI.CubicFirstMoment.bin_count_predecessor line 24
lemma OAI.CubicFirstMoment.first_bin_count_unique line 30
lemma OAI.CubicFirstMoment.partial_count_bin_crossing line 47
lemma OAI.CubicFirstMoment.prime_prefix_monotone line 58
lemma OAI.CubicFirstMoment.selected_crossing_implies_bin_crossing line 72
lemma OAI.CubicFirstMoment.selected_crossing_bin_unique line 95
lemma OAI.CubicFirstMoment.selected_crossing_indices_unique line 108

theorem OAI.CubicFirstMoment.prime_bin_stopping_sum line 136

Source documentation

Every original term is restored by summing the actual possible last bin and selected count. Uniqueness makes all other labels vanish.

theorem prime_bin_stopping_sum (s : Finset Eisenstein)
    (hs : ∀ p ∈ s, primaryPrime p) (bin : Eisenstein → ℕ) (ell : ℕ → ℝ)
    {m : ℕ} (hbin : ∀ p ∈ s, bin p < m) (hell : ∀ j, 1 ≤ ell j)
    (hell' : ∀ j < m, 1 < ell j) {R Z : ℝ} (hR : 0 < R) (hstart : R < Z)
    (hend : Z ≤ R*primeSurrogate s bin ell) (ψ : ℝ → ℝ) (w : ℝ) :
    (∑ j ∈ Finset.range m, ∑ k ∈ Finset.Icc 1 s.card,
      ∑ t ∈ (primeBin s bin j).powersetCard k,
        if R*primeSurrogate (stoppingSelected s bin j t) bin ell/ell j < Z ∧
            Z ≤ R*primeSurrogate (stoppingSelected s bin j t) bin ell then
          ((primeBin s bin j).card.choose k:ℂ)⁻¹ *
            (cutoffMoebius ψ w (∏ p ∈ stoppingSelected s bin j t, p) *
             cutoffMoebius ψ w (∏ p ∈ stoppingRemainder s bin j t, p))
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.primeSurrogate, OAI.CubicFirstMoment.primeBin, OAI.CubicFirstMoment.stoppingSelected, OAI.CubicFirstMoment.cutoffMoebius, OAI.CubicFirstMoment.stoppingRemainder

theorem OAI.CubicFirstMoment.geometric_bin_stopping_sum line 208