PrimeDetectorStopping.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual primary-divisor rough weight split into un-stopped and stopped pieces. Every divisor support fact follows from divisibility.

lemma OAI.CubicFirstMoment.primary_divisor_stopping_support line 12
theorem OAI.CubicFirstMoment.roughProduct_primary_stopping_split line 24
Source documentation
The inner rough-product factor is split at the actual surrogate threshold. The original kernel is kept constant through the divisor expansion, so its sharp norm cutoff is unchanged.
```
theorem roughProduct_primary_stopping_split {n : Eisenstein} (hn : primary n)
    (hs : Squarefree n) {ρ X : ℝ} (hρ : 1 < ρ) (hρ₂ : ρ ≤ 2)
    (hX : 1 ≤ X) (hnX : norm n ≤ X) {R Z : ℝ} (hR : 0 < R) (hstart : R < Z)
    (ψ : ℝ → ℝ) (w : ℝ) (K : Eisenstein → ℂ) :
    (roughProduct ψ w n:ℂ)*K n =
      (∑ d ∈ metaplecticPrimaryDivisors n with R*primeSurrogate (primaryPrimeFactors d)
          (geometricPrimeBin ρ X) (geometricBinLower ρ X) < Z,
        cutoffMoebius ψ w d*K n) +
      ∑ d ∈ metaplecticPrimaryDivisors n,
        geometricStoppedElement ρ X R Z ψ w (fun _ => K n) d := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.roughProduct, OAI.CubicFirstMoment.metaplecticPrimaryDivisors, OAI.CubicFirstMoment.primeSurrogate, OAI.CubicFirstMoment.primaryPrimeFactors, OAI.CubicFirstMoment.geometricPrimeBin, OAI.CubicFirstMoment.geometricBinLower, OAI.CubicFirstMoment.cutoffMoebius, OAI.CubicFirstMoment.geometricStoppedElement

theorem OAI.CubicFirstMoment.roughProduct_finite_stopping_split line 39

Source documentation

The same exact split after summing any finite original support.

theorem roughProduct_finite_stopping_split (S : Finset Eisenstein)
    {ρ X : ℝ} (hρ : 1 < ρ) (hρ₂ : ρ ≤ 2) (hX : 1 ≤ X)
    (hS : ∀ n ∈ S, primary n ∧ Squarefree n ∧ norm n ≤ X)
    {R Z : ℝ} (hR : 0 < R) (hstart : R < Z)
    (ψ : ℝ → ℝ) (w : ℝ) (K : Eisenstein → ℂ) :
    (∑ n ∈ S, (roughProduct ψ w n:ℂ)*K n) =
      (∑ n ∈ S, ∑ d ∈ metaplecticPrimaryDivisors n with
          R*primeSurrogate (primaryPrimeFactors d)
            (geometricPrimeBin ρ X) (geometricBinLower ρ X) < Z,
        cutoffMoebius ψ w d*K n) +
      ∑ n ∈ S, ∑ d ∈ metaplecticPrimaryDivisors n,
        geometricStoppedElement ρ X R Z ψ w (fun _ => K n) d := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.roughProduct, OAI.CubicFirstMoment.metaplecticPrimaryDivisors, OAI.CubicFirstMoment.primeSurrogate, OAI.CubicFirstMoment.primaryPrimeFactors, OAI.CubicFirstMoment.geometricPrimeBin, OAI.CubicFirstMoment.geometricBinLower, OAI.CubicFirstMoment.cutoffMoebius, OAI.CubicFirstMoment.geometricStoppedElement