StoppedAbsoluteMass.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The absolute, uncollected complementary factorization mass used after a free prime is cancelled. No cancellation inside beta is used.

def OAI.CubicFirstMoment.pairAbsolute line 14
lemma OAI.CubicFirstMoment.pairAbsolute_filter_nonzero line 18
lemma OAI.CubicFirstMoment.rough_pairAbsolute_bound line 37
theorem OAI.CubicFirstMoment.distinguished_pairAbsolute_bound line 57

theorem OAI.CubicFirstMoment.distinguished_pairAbsolute_mass line 84

Source documentation

Summing the absolute complementary weights costs only their linear norm range. In particular no cancellation inside the collected coefficient and no ordering of the selected bin primes is used.

theorem distinguished_pairAbsolute_mass
    (S : ι → Finset Eisenstein) (hS : ∀ i, ∀ p ∈ S i, primaryPrime p)
    (W : ι → Eisenstein → ℂ) (hW : ∀ i, ∀ p ∈ S i, ‖W i p‖ ≤ 1)
    (R D : Finset Eisenstein) (hR : ∀ r ∈ R, primary r)
    {ψ : ℝ → ℝ} (hψ : ∀ x, 0 ≤ ψ x ∧ ψ x ≤ 1)
    (hψone : ∀ x : ℝ, 0 < x → x ≤ 1 → ψ x = 1)
    (hψzero : ∀ x : ℝ, 2 ≤ x → ψ x = 0)
    {w z Y : ℝ} (hw : 1 ≤ w) (hwz : w ≤ z) (hY : 0 ≤ Y)
    {k : ℕ} (hsize : Y < w^k) :
    (∑ b ∈ (primaryElementBall Y).filter Squarefree,
      pairAbsolute R D (distinguishedTupleCoefficient S W ψ w z)
        (cutoffMoebius ψ w) b) ≤
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.pairAbsolute, OAI.CubicFirstMoment.distinguishedTupleCoefficient, OAI.CubicFirstMoment.cutoffMoebius