def SelbergSieve.selbergTerms (s : BoundingSieve) : ArithmeticFunction ℝ

Equations

• SelbergSieve.selbergTerms s = BoundingSieve.nu.pmul (ArithmeticFunction.prodPrimeFactors fun (p : ℕ) => 1 / (1 - BoundingSieve.nu p))

theorem SelbergSieve.selbergTerms_apply (s : BoundingSieve) (d : ℕ) : (selbergTerms s) d = BoundingSieve.nu d * ∏ p ∈ d.primeFactors, 1 / (1 - BoundingSieve.nu p)

structure SelbergSieve.UpperBoundSieve : Type

• μPlus : ℕ → ℝ
• hμPlus : IsUpperMoebius self.μPlus

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

Equations

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

def SelbergSieve.IsLowerMoebius (μMinus : ℕ → ℝ) : Prop

Equations

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

structure SelbergSieve.LowerBoundSieve : Type

• μMinus : ℕ → ℝ
• hμMinus : IsLowerMoebius self.μMinus

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

Equations

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

theorem SelbergSieve.nu_ne_zero_of_mem_divisors_prodPrimes (s : BoundingSieve) {d : ℕ} (hd : d ∈ BoundingSieve.prodPrimes.divisors) : BoundingSieve.nu d ≠ 0

def SelbergSieve.delta (n : ℕ) : ℝ

Equations

• SelbergSieve.delta n = if n = 1 then 1 else 0

theorem SelbergSieve.siftedSum_as_delta (s : BoundingSieve) : siftedSum = ∑ d ∈ BoundingSieve.support, BoundingSieve.weights d * delta (BoundingSieve.prodPrimes.gcd d)

theorem SelbergSieve.nu_lt_self_of_dvd_prodPrimes (s : BoundingSieve) (d : ℕ) (hdP : d ∣ BoundingSieve.prodPrimes) (hd_ne_one : d ≠ 1) : BoundingSieve.nu d < 1

theorem SelbergSieve.selbergTerms_pos (s : BoundingSieve) (l : ℕ) (hl : l ∣ BoundingSieve.prodPrimes) : 0 < (selbergTerms s) l

theorem SelbergSieve.selbergTerms_mult (s : BoundingSieve) : (selbergTerms s).IsMultiplicative

theorem SelbergSieve.one_div_selbergTerms_eq_conv_moebius_nu (s : BoundingSieve) (l : ℕ) (hl : Squarefree l) (hnu_nonzero : BoundingSieve.nu l ≠ 0) : 1 / (selbergTerms s) l = ∑ d ∈ l.divisors, ↑(ArithmeticFunction.moebius (l / d)) * (BoundingSieve.nu d)⁻¹

theorem SelbergSieve.nu_eq_conv_one_div_selbergTerms (s : BoundingSieve) (d : ℕ) (hdP : d ∣ BoundingSieve.prodPrimes) : (BoundingSieve.nu d)⁻¹ = ∑ l ∈ BoundingSieve.prodPrimes.divisors, if l ∣ d then 1 / (selbergTerms s) l else 0

theorem SelbergSieve.conv_selbergTerms_eq_selbergTerms_mul_nu (s : BoundingSieve) {d : ℕ} (hd : d ∣ BoundingSieve.prodPrimes) : (∑ l ∈ BoundingSieve.prodPrimes.divisors, if l ∣ d then (selbergTerms s) l else 0) = (selbergTerms s) d * (BoundingSieve.nu d)⁻¹

theorem SelbergSieve.upper_bound_of_UpperBoundSieve (s : BoundingSieve) (μPlus : UpperBoundSieve) : siftedSum ≤ ∑ d ∈ BoundingSieve.prodPrimes.divisors, μPlus.μPlus d * multSum d

theorem SelbergSieve.siftedSum_le_mainSum_errSum_of_UpperBoundSieve (s : BoundingSieve) (μPlus : UpperBoundSieve) : siftedSum ≤ BoundingSieve.totalMass * mainSum μPlus.μPlus + errSum μPlus.μPlus

def SelbergSieve.lambdaSquared (weights : ℕ → ℝ) : ℕ → ℝ

Equations

• SelbergSieve.lambdaSquared weights d = ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0

theorem SelbergSieve.lambdaSquared_eq_zero_of_support (w : ℕ → ℝ) (y : ℝ) (hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0) (d : ℕ) (hd : ¬↑d ≤ y) : lambdaSquared w d = 0

theorem SelbergSieve.upperMoebius_of_lambda_sq (weights : ℕ → ℝ) (hw : weights 1 = 1) : IsUpperMoebius (lambdaSquared weights)

theorem SelbergSieve.lambdaSquared_mainSum_eq_quad_form (s : BoundingSieve) (w : ℕ → ℝ) : mainSum (lambdaSquared w) = ∑ d1 ∈ BoundingSieve.prodPrimes.divisors, ∑ d2 ∈ BoundingSieve.prodPrimes.divisors, BoundingSieve.nu d1 * w d1 * BoundingSieve.nu d2 * w d2 * (BoundingSieve.nu (d1.gcd d2))⁻¹

theorem SelbergSieve.lambdaSquared_mainSum_eq_diag_quad_form (s : BoundingSieve) (w : ℕ → ℝ) : mainSum (lambdaSquared w) = ∑ l ∈ BoundingSieve.prodPrimes.divisors, 1 / (selbergTerms s) l * (∑ d ∈ BoundingSieve.prodPrimes.divisors, if l ∣ d then BoundingSieve.nu d * w d else 0) ^ 2