GeometricStoppingKernel.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact all-label stopping with the original product kernel attached. The product kernel may include a sharp norm cutoff.

lemma OAI.CubicFirstMoment.stoppingSelected_product_remainder line 12

theorem OAI.CubicFirstMoment.geometric_label_stopping_kernel line 21

Source documentation

The inverse-binomial stopping sum reconstructs the literal original kernel, without smoothing or changing the product support.

theorem geometric_label_stopping_kernel {n : Eisenstein} (hn : primary n)
    (hs : Squarefree n) {ρ X : ℝ} (hρ : 1 < ρ) (hρ₂ : ρ ≤ 2)
    (hX : 1 ≤ X) (hnorm : norm n ≤ X) {R Z : ℝ} (hR : 0 < R) (hstart : R < Z)
    (hend : Z ≤ R*primeSurrogate (primaryPrimeFactors n)
      (geometricPrimeBin ρ X) (geometricBinLower ρ X))
    (ψ : ℝ → ℝ) (w : ℝ) (K : Eisenstein → ℂ) :
    (∑ q ∈ stoppingLabelBox ρ X,
      ∑ t ∈ (primeBin (primaryPrimeFactors n) (geometricPrimeBin ρ X) q.1).powersetCard q.2.1,
        if (primeBin (stoppingRemainder (primaryPrimeFactors n) (geometricPrimeBin ρ X) q.1 t)
              (geometricPrimeBin ρ X) q.1).card = q.2.2 ∧
            (R*primeSurrogate (stoppingSelected (primaryPrimeFactors n)
                (geometricPrimeBin ρ X) q.1 t) (geometricPrimeBin ρ X) (geometricBinLower ρ X)/
…

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