StoppingThreshold.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The exact no-stop/stopped split. The original product kernel may contain a sharp norm cutoff; no continuity is required.

def OAI.CubicFirstMoment.geometricStoppedElement line 12
lemma OAI.CubicFirstMoment.stoppingSelected_surrogate_le line 32
lemma OAI.CubicFirstMoment.geometricStoppedElement_eq_zero line 41
Source documentation
If the entire original factor set is below the threshold, every putative stopping label contributes zero individually.
```
lemma geometricStoppedElement_eq_zero {ρ X R Z : ℝ} (hρ : 1 ≤ ρ) (hR : 0 ≤ R)
    (ψ : ℝ → ℝ) (w : ℝ) (K : Eisenstein → ℂ) (n : Eisenstein)
    (hbelow : R*primeSurrogate (primaryPrimeFactors n)
      (geometricPrimeBin ρ X) (geometricBinLower ρ X) < Z) :
    geometricStoppedElement ρ X R Z ψ w K n = 0 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primeSurrogate, OAI.CubicFirstMoment.primaryPrimeFactors, OAI.CubicFirstMoment.geometricPrimeBin, OAI.CubicFirstMoment.geometricBinLower, OAI.CubicFirstMoment.geometricStoppedElement
theorem OAI.CubicFirstMoment.geometricStoppedElement_exact line 59
Source documentation
Unconditional in the end-crossing condition: the actual complete label sum is exactly the original term times its stopping indicator.
```
theorem geometricStoppedElement_exact {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)
    (ψ : ℝ → ℝ) (w : ℝ) (K : Eisenstein → ℂ) :
    geometricStoppedElement ρ X R Z ψ w K n =
      if Z ≤ R*primeSurrogate (primaryPrimeFactors n)
          (geometricPrimeBin ρ X) (geometricBinLower ρ X) then
        cutoffMoebius ψ w n*K n else 0 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.geometricStoppedElement, OAI.CubicFirstMoment.primeSurrogate, OAI.CubicFirstMoment.primaryPrimeFactors, OAI.CubicFirstMoment.geometricPrimeBin, OAI.CubicFirstMoment.geometricBinLower, OAI.CubicFirstMoment.cutoffMoebius
theorem OAI.CubicFirstMoment.stopping_threshold_split line 74

theorem OAI.CubicFirstMoment.finite_stopping_threshold_split line 90

Source documentation

The actual finite coefficient sum splits into the un-stopped part and the complete stopping-label sum, with the same kernel on both.

theorem finite_stopping_threshold_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, cutoffMoebius ψ w n*K n) =
      (∑ n ∈ S with R*primeSurrogate (primaryPrimeFactors n)
          (geometricPrimeBin ρ X) (geometricBinLower ρ X) < Z,
        cutoffMoebius ψ w n*K n) +
      ∑ n ∈ S, geometricStoppedElement ρ X R Z ψ w K n := by
…

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