StoppingCoefficientIdentity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The literal fixed-label stopping contribution as a sum over primary factor pairs. This is the arithmetic bridge to independent alpha/beta.

theorem OAI.CubicFirstMoment.stopping_primary_pair_sum line 15

Source documentation

Exact fixed-label coefficient identity, before any estimate or extension by vanishing nonsquarefree terms.

theorem stopping_primary_pair_sum {n : Eisenstein} (hn : primary n)
    (hs : Squarefree n) {B : ℝ} (hnB : norm n ≤ B)
    (bin : Eisenstein → ℕ) (ell : ℕ → ℝ) (j k l : ℕ) (Z : ℝ) (r : Eisenstein)
    (ψ : ℝ → ℝ) (w : ℝ) (K : Eisenstein → Eisenstein → ℂ) :
    (∑ t ∈ (primeBin (primaryPrimeFactors n) bin j).powersetCard k,
      if (primeBin (stoppingRemainder (primaryPrimeFactors n) bin j t) bin j).card = l ∧
          (norm r*primeSurrogate (stoppingSelected (primaryPrimeFactors n) bin j t) bin ell/
              ell j < Z ∧
            Z ≤ norm r*primeSurrogate
              (stoppingSelected (primaryPrimeFactors n) bin j t) bin ell) then
        cutoffMoebius ψ w (∏ p ∈ stoppingSelected (primaryPrimeFactors n) bin j t, p)*
          cutoffMoebius ψ w (∏ p ∈ stoppingRemainder (primaryPrimeFactors n) bin j t, p)*
…

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

theorem OAI.CubicFirstMoment.stopping_primary_cutoff_sum line 65

Source documentation

Summing the fixed-label identity over the original squarefree terms leaves the sharp product cutoff on the independent factor pair.

theorem stopping_primary_cutoff_sum (B : ℝ)
    (bin : Eisenstein → ℕ) (ell : ℕ → ℝ) (j k l : ℕ) (Z : ℝ) (r : Eisenstein)
    (ψ : ℝ → ℝ) (w : ℝ) (K : Eisenstein → Eisenstein → ℂ) :
    (∑ n ∈ (primaryElementBall B).filter Squarefree,
      ∑ t ∈ (primeBin (primaryPrimeFactors n) bin j).powersetCard k,
        if (primeBin (stoppingRemainder (primaryPrimeFactors n) bin j t) bin j).card = l ∧
            (norm r*primeSurrogate (stoppingSelected (primaryPrimeFactors n) bin j t) bin ell/
                ell j < Z ∧
              Z ≤ norm r*primeSurrogate
                (stoppingSelected (primaryPrimeFactors n) bin j t) bin ell) then
          cutoffMoebius ψ w (∏ p ∈ stoppingSelected (primaryPrimeFactors n) bin j t, p)*
            cutoffMoebius ψ w (∏ p ∈ stoppingRemainder (primaryPrimeFactors n) bin j t, p)*
…

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

theorem OAI.CubicFirstMoment.stopping_primary_cutoff_sum_vanishing line 102

Source documentation

A squarefree-supported kernel removes the coupled squarefree test, but does not remove the literal product cutoff.

theorem stopping_primary_cutoff_sum_vanishing (B : ℝ)
    (bin : Eisenstein → ℕ) (ell : ℕ → ℝ) (j k l : ℕ) (Z : ℝ) (r : Eisenstein)
    (ψ : ℝ → ℝ) (w : ℝ) (K : Eisenstein → Eisenstein → ℂ)
    (hK : ∀ d ∈ primaryElementBall B, ∀ e ∈ primaryElementBall B,
      ¬Squarefree (d*e) → K d e = 0) :
    (∑ n ∈ (primaryElementBall B).filter Squarefree,
      ∑ t ∈ (primeBin (primaryPrimeFactors n) bin j).powersetCard k,
        if (primeBin (stoppingRemainder (primaryPrimeFactors n) bin j t) bin j).card = l ∧
            (norm r*primeSurrogate (stoppingSelected (primaryPrimeFactors n) bin j t) bin ell/
                ell j < Z ∧
              Z ≤ norm r*primeSurrogate
                (stoppingSelected (primaryPrimeFactors n) bin j t) bin ell) then
…