PrimeStoppingLabels.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact stopping reconstruction in the three labels occurring in the manuscript: final bin, selected occupancy, and remaining occupancy.

lemma OAI.CubicFirstMoment.stoppingSelected_of_separated_bins line 14
Source documentation
The independent side predicates recover the exact selected subset.
```
lemma stoppingSelected_of_separated_bins (d e : Finset Eisenstein)
    (bin : Eisenstein → ℕ) (j : ℕ)
    (hd : ∀ p ∈ d, bin p ≤ j) (he : ∀ p ∈ e, j ≤ bin p) :
    stoppingSelected (d ∪ e) bin j (primeBin d bin j) = d := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.stoppingSelected, OAI.CubicFirstMoment.primeBin
lemma OAI.CubicFirstMoment.stoppingRemainder_of_separated_bins line 34
lemma OAI.CubicFirstMoment.stopping_occupancies_add line 48

lemma OAI.CubicFirstMoment.stopping_insert_remaining_count line 60

Source documentation

Inserting the remaining occupancy changes neither the actual finite sum nor its inverse-binomial coefficient.

lemma stopping_insert_remaining_count (s : Finset Eisenstein)
    (bin : Eisenstein → ℕ) (ell : ℕ → ℝ) (j k M : ℕ)
    (hM : s.card ≤ M) (R Z : ℝ) (ψ : ℝ → ℝ) (w : ℝ) :
    (∑ l ∈ Finset.range (M+1), ∑ t ∈ (primeBin s bin j).powersetCard k,
      if (primeBin (stoppingRemainder s bin j t) bin j).card = l ∧
          (R*primeSurrogate (stoppingSelected s bin j t) bin ell/ell j < Z ∧
            Z ≤ R*primeSurrogate (stoppingSelected s bin j t) bin ell) then
        (Nat.choose (k+l) k:ℂ)⁻¹ *
          (cutoffMoebius ψ w (∏ p ∈ stoppingSelected s bin j t, p) *
           cutoffMoebius ψ w (∏ p ∈ stoppingRemainder s bin j t, p))
      else 0) =
    ∑ t ∈ (primeBin s bin j).powersetCard k,
…

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

theorem OAI.CubicFirstMoment.geometric_label_stopping_sum line 98

Source documentation

The complete three-label stopping sum, with no assumed reconstruction identity and no hidden choice of the first bin.

theorem geometric_label_stopping_sum (s : Finset Eisenstein)
    (hs : ∀ p ∈ s, primaryPrime p) {ρ X : ℝ} (hρ : 1 < ρ) (hρ₂ : ρ ≤ 2)
    (hX : 1 ≤ X) (hnorm : norm (∏ p ∈ s, p) ≤ X)
    (hpX : ∀ p ∈ s, norm p ≤ X) {R Z : ℝ} (hR : 0 < R) (hstart : R < Z)
    (hend : Z ≤ R*primeSurrogate s (geometricPrimeBin ρ X) (geometricBinLower ρ X))
    (ψ : ℝ → ℝ) (w : ℝ) :
    (∑ q ∈ stoppingLabelBox ρ X,
      ∑ t ∈ (primeBin s (geometricPrimeBin ρ X) q.1).powersetCard q.2.1,
        if (primeBin (stoppingRemainder s (geometricPrimeBin ρ X) q.1 t)
              (geometricPrimeBin ρ X) q.1).card = q.2.2 ∧
            (R*primeSurrogate (stoppingSelected s (geometricPrimeBin ρ X) q.1 t)
                (geometricPrimeBin ρ X) (geometricBinLower ρ X)/
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primeSurrogate, OAI.CubicFirstMoment.geometricPrimeBin, OAI.CubicFirstMoment.geometricBinLower, OAI.CubicFirstMoment.stoppingLabelBox, OAI.CubicFirstMoment.primeBin, OAI.CubicFirstMoment.stoppingRemainder, OAI.CubicFirstMoment.stoppingSelected