StoppingTwoStage.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact two-stage stopping, first above a bin boundary and then after failure of that high-prime stage. The original kernel and inverse binomial coefficients remain unchanged.

def OAI.CubicFirstMoment.geometricStoppingLabel line 14
lemma OAI.CubicFirstMoment.geometricStoppedElement_eq_labels line 34
def OAI.CubicFirstMoment.geometricHighStoppedElement line 39
lemma OAI.CubicFirstMoment.geometricStoppingLabel_zero_boundary line 44
theorem OAI.CubicFirstMoment.geometricHighStoppedElement_exact line 59

theorem OAI.CubicFirstMoment.two_stage_stopping_split line 97

Source documentation

Exact ordinary two-stage decomposition before any estimate. The late term carries the failed-prefix condition on the selected divisor.

theorem two_stage_stopping_split {n : Eisenstein} (hn : primary n)
    (hs : Squarefree n) {ρ X : ℝ} (hρ : 1 < ρ) (hρ₂ : ρ ≤ 2)
    (hX : 1 ≤ X) (hnorm : norm n ≤ X) {R Q Z : ℝ} (hR : 0 < R)
    (hstart : R < Q) (hQZ : Q ≤ Z) (h : ℕ)
    (ψ : ℝ → ℝ) (w : ℝ) (K : Eisenstein → ℂ) :
    cutoffMoebius ψ w n*K n =
      (if R*primeSurrogate
          (primeBinPrefix (primaryPrimeFactors n) (geometricPrimeBin ρ X) h)
          (geometricPrimeBin ρ X) (geometricBinLower ρ X) < Q ∧
        R*primeSurrogate (primaryPrimeFactors n)
          (geometricPrimeBin ρ X) (geometricBinLower ρ X) < Z then
        cutoffMoebius ψ w n*K n else 0) +
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.cutoffMoebius, OAI.CubicFirstMoment.primeSurrogate, OAI.CubicFirstMoment.primeBinPrefix, OAI.CubicFirstMoment.primaryPrimeFactors, OAI.CubicFirstMoment.geometricPrimeBin, OAI.CubicFirstMoment.geometricBinLower

theorem OAI.CubicFirstMoment.finite_two_stage_stopping_split line 131

Source documentation

The literal finite rough-Moebius sum has the same two-stage split, with the product kernel unchanged in all three terms.

theorem finite_two_stage_stopping_split (S : Finset Eisenstein)
    {ρ X : ℝ} (hρ : 1 < ρ) (hρ₂ : ρ ≤ 2) (hX : 1 ≤ X)
    (hS : ∀ n ∈ S, primary n ∧ Squarefree n ∧ norm n ≤ X)
    {R Q Z : ℝ} (hR : 0 < R) (hstart : R < Q) (hQZ : Q ≤ Z)
    (h : ℕ) (ψ : ℝ → ℝ) (w : ℝ) (K : Eisenstein → ℂ) :
    (∑ n ∈ S, cutoffMoebius ψ w n*K n) =
      (∑ n ∈ S with R*primeSurrogate
          (primeBinPrefix (primaryPrimeFactors n) (geometricPrimeBin ρ X) h)
          (geometricPrimeBin ρ X) (geometricBinLower ρ X) < Q ∧
        R*primeSurrogate (primaryPrimeFactors n)
          (geometricPrimeBin ρ X) (geometricBinLower ρ X) < Z,
        cutoffMoebius ψ w n*K n) +
…