Source indexedtheorem · leanprover/lean4:v4.32.0

Sieve.rem_sum_le_of_const

PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean:511 to 526

Mathematical statement

Exact Lean statement

theorem rem_sum_le_of_const (s : SelbergSieve) (C : ℝ) (hrem : ∀ d > 0, |rem (s := s.toBoundingSieve) d| ≤ C) :
    ∑ d ∈ s.prodPrimes.divisors, (if (d : ℝ) ≤ s.level then (3:ℝ) ^ ω d * |rem (s := s.toBoundingSieve) d| else 0)
      ≤ C * s.level * (1+Real.log s.level)^3

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem rem_sum_le_of_const (s : SelbergSieve) (C : ℝ) (hrem : ∀ d > 0, |rem (s := s.toBoundingSieve) d| ≤ C) :    ∑ d ∈ s.prodPrimes.divisors, (if (d : ℝ) ≤ s.level then (3:ℝ) ^ ω d * |rem (s := s.toBoundingSieve) d| else 0)      ≤ C * s.level * (1+Real.log s.level)^3 := by  rw [←Finset.sum_filter]  trans (∑ d ∈  Finset.filter (fun d:ℕ => ↑d ≤ s.level) (s.prodPrimes.divisors),  3 ^ ω d * C )  · gcongr with d hd    rw [Finset.mem_filter, Nat.mem_divisors] at hd    apply hrem d    apply Nat.pos_of_ne_zero    apply ne_zero_of_dvd_ne_zero hd.1.2 hd.1.1  rw [←Finset.sum_mul, mul_comm, mul_assoc]  gcongr  · linarith [abs_nonneg <| rem (s := s.toBoundingSieve) 1, hrem 1 (by norm_num)]  rw [Finset.sum_filter]  apply Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow (hx := s.one_le_level)  apply prodPrimes_squarefree