LeanPool.SelbergSieve4.UpperBoundSieve

def Sieve.UpperMoebius (μ_plus : ℕ → ℝ) : Prop

A real-valued divisor weight majorizing the delta function at 1.

Equations

• Sieve.UpperMoebius μ_plus = ∀ (n : ℕ), (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, μ_plus d

structure Sieve.UpperBoundSieve : Type

Upper-bound sieve weights with their majorization property.

• μPlus : ℕ → ℝ

  Upper-bound Moebius weight.

• hμPlus : UpperMoebius self.μPlus

@[implicit_reducible]

instance Sieve.ubToμPlus : CoeFun UpperBoundSieve fun (x : UpperBoundSieve) => ℕ → ℝ

Equations

• Sieve.ubToμPlus = { coe := fun (ub : Sieve.UpperBoundSieve) => ub.μPlus }

def Sieve.LowerMoebius (μMinus : ℕ → ℝ) : Prop

A real-valued divisor weight minorizing the delta function at 1.

Equations

• Sieve.LowerMoebius μMinus = ∀ (n : ℕ), ∑ d ∈ n.divisors, μMinus d ≤ if n = 1 then 1 else 0

structure Sieve.LowerBoundSieve : Type

Lower-bound sieve weights with their minorization property.

• μMinus : ℕ → ℝ

  Lower-bound Moebius weight.

• hμMinus : LowerMoebius self.μMinus

@[implicit_reducible]

instance Sieve.lbToμMinus : CoeFun LowerBoundSieve fun (x : LowerBoundSieve) => ℕ → ℝ

Equations

• Sieve.lbToμMinus = { coe := fun (lb : Sieve.LowerBoundSieve) => lb.μMinus }