internlm/Lean-Github huggingface dataset:
Theorem: Sieve.boundingSum_ge_log
Proof state before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m ≥ (√s.level).log

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≥ s.level.log / 2
Tactic:
rw [ge_iff_le]
Proof state after:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≤ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≥ s.level.log / 2
Theorem: Sieve.boundingSum_ge_log
Proof state before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≤ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≥ s.level.log / 2
Tactic:
simp_rw[one_div]
Proof state after:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≤ ∑ x ∈ Finset.Icc 1 ⌊√s.level⌋₊, (↑x)⁻¹

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≥ s.level.log / 2
Theorem: Sieve.boundingSum_ge_log
Proof state before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≤ ∑ x ∈ Finset.Icc 1 ⌊√s.level⌋₊, (↑x)⁻¹

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≥ s.level.log / 2
Tactic:
apply Aux.log_le_sum_inv (Real.sqrt s.level)
Proof state after:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ 1 ≤ √s.level

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≥ s.level.log / 2
Theorem: Sieve.boundingSum_ge_log
Proof state before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ 1 ≤ √s.level

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≥ s.level.log / 2
Tactic:
rw [Real.le_sqrt] <;> linarith[s.one_le_level]
Proof state after:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≥ s.level.log / 2
Theorem: Sieve.boundingSum_ge_log
Proof state before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≥ s.level.log / 2
Tactic:
apply ge_of_eq
Proof state after:
case h
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log = s.level.log / 2
Theorem: Sieve.boundingSum_ge_log
Proof state before:
case h
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log = s.level.log / 2
Tactic:
refine Real.log_sqrt ?h.hx
Proof state after:
case h.hx
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ 0 ≤ s.level
Theorem: Sieve.boundingSum_ge_log
Proof state before:
case h.hx
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ 0 ≤ s.level
Tactic:
linarith[s.one_le_level]
Proof state after:
no goals
Theorem: Sieve.boundingSum_ge_log
Proof state before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m
Tactic:
exact boundingSum_ge_sum s hnu hP
Proof state after:
no goals
Theorem: Sieve.rem_sum_le_of_const
Proof state before:
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ (∑ d ∈ s.prodPrimes.divisors, if ↑d ≤ s.level then 3 ^ ω d * |s.rem d| else 0) ≤ C * s.level * (1 + s.level.log) ^ 3
Tactic:
rw [←Finset.sum_filter]
Proof state after:
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ ∑ a ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω a * |s.rem a| ≤
    C * s.level * (1 + s.level.log) ^ 3
Theorem: Sieve.rem_sum_le_of_const
Proof state before:
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ ∑ a ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω a * |s.rem a| ≤
    C * s.level * (1 + s.level.log) ^ 3
Tactic:
trans (∑ d in  Finset.filter (fun d:ℕ => ↑d ≤ s.level) (s.toSieve.prodPrimes.divisors),  3 ^ ω d * C )
Proof state after:
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ ∑ a ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω a * |s.rem a| ≤
    ∑ d ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω d * C

s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ ∑ d ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω d * C ≤ C * s.level * (1 + s.level.log) ^ 3
Theorem: Sieve.rem_sum_le_of_const
Proof state before:
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ ∑ d ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω d * C ≤ C * s.level * (1 + s.level.log) ^ 3
Tactic:
rw [←Finset.sum_mul, mul_comm, mul_assoc]
Proof state after:
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ C * ∑ i ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω i ≤ C * (s.level * (1 + s.level.log) ^ 3)
Theorem: Sieve.rem_sum_le_of_const
Proof state before:
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ C * ∑ i ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω i ≤ C * (s.level * (1 + s.level.log) ^ 3)
Tactic:
gcongr
Proof state after:
case a0
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ 0 ≤ C

case h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ ∑ i ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω i ≤ s.level * (1 + s.level.log) ^ 3
Theorem: Sieve.rem_sum_le_of_const
Proof state before:
case h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ ∑ i ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω i ≤ s.level * (1 + s.level.log) ^ 3
Tactic:
rw [Finset.sum_filter]
Proof state after:
case h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ (∑ a ∈ s.prodPrimes.divisors, if ↑a ≤ s.level then 3 ^ ω a else 0) ≤ s.level * (1 + s.level.log) ^ 3
Theorem: Sieve.rem_sum_le_of_const
Proof state before:
case h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ (∑ a ∈ s.prodPrimes.divisors, if ↑a ≤ s.level then 3 ^ ω a else 0) ≤ s.level * (1 + s.level.log) ^ 3
Tactic:
apply Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow (hx := s.one_le_level)
Proof state after:
case h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ Squarefree s.prodPrimes
Theorem: Sieve.rem_sum_le_of_const
Proof state before:
case h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ Squarefree s.prodPrimes
Tactic:
apply Sieve.prodPrimes_squarefree
Proof state after:
no goals
Theorem: Sieve.rem_sum_le_of_const
Proof state before:
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ ∑ a ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω a * |s.rem a| ≤
    ∑ d ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω d * C
Tactic:
gcongr with d hd
Proof state after:
case h.h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
d : ℕ
hd : d ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors
⊢ |s.rem d| ≤ C
Theorem: Sieve.rem_sum_le_of_const
Proof state before:
case h.h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
d : ℕ
hd : d ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors
⊢ |s.rem d| ≤ C
Tactic:
rw [Finset.mem_filter, Nat.mem_divisors] at hd
Proof state after:
case h.h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
d : ℕ
hd : (d ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑d ≤ s.level
⊢ |s.rem d| ≤ C
Theorem: Sieve.rem_sum_le_of_const
Proof state before:
case h.h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
d : ℕ
hd : (d ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑d ≤ s.level
⊢ |s.rem d| ≤ C
Tactic:
apply hrem d
Proof state after:
case h.h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
d : ℕ
hd : (d ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑d ≤ s.level
⊢ d > 0
Theorem: Sieve.rem_sum_le_of_const
Proof state before:
case h.h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
d : ℕ
hd : (d ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑d ≤ s.level
⊢ d > 0
Tactic:
apply Nat.pos_of_ne_zero
Proof state after:
case h.h.a
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
d : ℕ
hd : (d ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑d ≤ s.level
⊢ d ≠ 0
Theorem: Sieve.rem_sum_le_of_const
Proof state before:
case h.h.a
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
d : ℕ
hd : (d ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑d ≤ s.level
⊢ d ≠ 0
Tactic:
apply ne_zero_of_dvd_ne_zero hd.1.2 hd.1.1
Proof state after:
no goals
Theorem: Sieve.rem_sum_le_of_const
Proof state before:
case a0
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ 0 ≤ C
Tactic:
linarith [abs_nonneg <| s.rem 1, hrem 1 (by norm_num)]
Proof state after:
no goals
Theorem: Sieve.rem_sum_le_of_const
Proof state before:
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ 1 > 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: LogDerivativeDirichlet
Proof state before:
s : ℂ
hs : 1 < s.re
⊢ -deriv riemannZeta s / riemannZeta s = ∑' (n : ℕ), ↑(Λ n) / ↑n ^ s
Tactic:
rw [← ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs]
Proof state after:
s : ℂ
hs : 1 < s.re
⊢ LSeries (fun n => ↑(Λ n)) s = ∑' (n : ℕ), ↑(Λ n) / ↑n ^ s
Theorem: LogDerivativeDirichlet
Proof state before:
s : ℂ
hs : 1 < s.re
⊢ LSeries (fun n => ↑(Λ n)) s = ∑' (n : ℕ), ↑(Λ n) / ↑n ^ s
Tactic:
dsimp [LSeries, LSeries.term]
Proof state after:
s : ℂ
hs : 1 < s.re
⊢ (∑' (n : ℕ), if n = 0 then 0 else ↑(Λ n) / ↑n ^ s) = ∑' (n : ℕ), ↑(Λ n) / ↑n ^ s
Theorem: LogDerivativeDirichlet
Proof state before:
s : ℂ
hs : 1 < s.re
⊢ (∑' (n : ℕ), if n = 0 then 0 else ↑(Λ n) / ↑n ^ s) = ∑' (n : ℕ), ↑(Λ n) / ↑n ^ s
Tactic:
nth_rewrite 2 [tsum_eq_add_tsum_ite (b := 0) ?_]
Proof state after:
s : ℂ
hs : 1 < s.re
⊢ (∑' (n : ℕ), if n = 0 then 0 else ↑(Λ n) / ↑n ^ s) =
    ↑(Λ 0) / ↑0 ^ s + ∑' (n : ℕ), if n = 0 then 0 else ↑(Λ n) / ↑n ^ s

s : ℂ
hs : 1 < s.re
⊢ Summable fun n => ↑(Λ n) / ↑n ^ s
Theorem: LogDerivativeDirichlet
Proof state before:
s : ℂ
hs : 1 < s.re
⊢ (∑' (n : ℕ), if n = 0 then 0 else ↑(Λ n) / ↑n ^ s) =
    ↑(Λ 0) / ↑0 ^ s + ∑' (n : ℕ), if n = 0 then 0 else ↑(Λ n) / ↑n ^ s
Tactic:
simp
Proof state after:
no goals
Theorem: LogDerivativeDirichlet
Proof state before:
s : ℂ
hs : 1 < s.re
⊢ Summable fun n => ↑(Λ n) / ↑n ^ s
Tactic:
have := ArithmeticFunction.LSeriesSummable_vonMangoldt hs
Proof state after:
s : ℂ
hs : 1 < s.re
this : LSeriesSummable (fun n => ↑(Λ n)) s
⊢ Summable fun n => ↑(Λ n) / ↑n ^ s
Theorem: LogDerivativeDirichlet
Proof state before:
s : ℂ
hs : 1 < s.re
this : LSeriesSummable (fun n => ↑(Λ n)) s
⊢ Summable fun n => ↑(Λ n) / ↑n ^ s
Tactic:
dsimp [LSeriesSummable] at this
Proof state after:
s : ℂ
hs : 1 < s.re
this : Summable (LSeries.term (fun n => ↑(Λ n)) s)
⊢ Summable fun n => ↑(Λ n) / ↑n ^ s
Theorem: LogDerivativeDirichlet
Proof state before:
s : ℂ
hs : 1 < s.re
this : Summable (LSeries.term (fun n => ↑(Λ n)) s)
⊢ Summable fun n => ↑(Λ n) / ↑n ^ s
Tactic:
convert this
Proof state after:
case h.e'_5.h
s : ℂ
hs : 1 < s.re
this : Summable (LSeries.term (fun n => ↑(Λ n)) s)
x✝ : ℕ
⊢ ↑(Λ x✝) / ↑x✝ ^ s = LSeries.term (fun n => ↑(Λ n)) s x✝
Theorem: LogDerivativeDirichlet
Proof state before:
case h.e'_5.h
s : ℂ
hs : 1 < s.re
this : Summable (LSeries.term (fun n => ↑(Λ n)) s)
x✝ : ℕ
⊢ ↑(Λ x✝) / ↑x✝ ^ s = LSeries.term (fun n => ↑(Λ n)) s x✝
Tactic:
rename ℕ => n
Proof state after:
case h.e'_5.h
s : ℂ
hs : 1 < s.re
this : Summable (LSeries.term (fun n => ↑(Λ n)) s)
n : ℕ
⊢ ↑(Λ n) / ↑n ^ s = LSeries.term (fun n => ↑(Λ n)) s n
Theorem: LogDerivativeDirichlet
Proof state before:
case h.e'_5.h
s : ℂ
hs : 1 < s.re
this : Summable (LSeries.term (fun n => ↑(Λ n)) s)
n : ℕ
⊢ ↑(Λ n) / ↑n ^ s = LSeries.term (fun n => ↑(Λ n)) s n
Tactic:
by_cases h : n = 0 <;> simp [LSeries.term, h]
Proof state after:
no goals
Theorem: integrable_x_mul_Smooth1
Proof state before:
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ MeasureTheory.IntegrableOn (fun x => x * Smooth1 ψ ε x) (Ioi 0) MeasureTheory.volume
Tactic:
sorry
Proof state after:
no goals
Theorem: vertical_integrable_Smooth1
Proof state before:
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ MeasureTheory.Integrable (fun y => ∫ (t : ℝ) in Ioi 0, ↑t ^ (1 + ↑y * I) * ↑(Smooth1 ψ ε t)) MeasureTheory.volume
Tactic:
sorry
Proof state after:
no goals
Theorem: continuousAt_Smooth1
Proof state before:
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
ε : ℝ
εpos : 0 < ε
y : ℝ
ypos : 0 < y
⊢ ContinuousAt (fun x => Smooth1 ψ ε x) y
Tactic:
apply Continuous.continuousAt
Proof state after:
case h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
ε : ℝ
εpos : 0 < ε
y : ℝ
ypos : 0 < y
⊢ Continuous fun x => Smooth1 ψ ε x
Theorem: continuousAt_Smooth1
Proof state before:
case h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
ε : ℝ
εpos : 0 < ε
y : ℝ
ypos : 0 < y
⊢ Continuous fun x => Smooth1 ψ ε x
Tactic:
unfold Smooth1 DeltaSpike MellinConvolution
Proof state after:
case h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
ε : ℝ
εpos : 0 < ε
y : ℝ
ypos : 0 < y
⊢ Continuous fun x =>
    ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * (fun x => ψ (x ^ (1 / ε)) / ε) (x / y) / ↑y
Theorem: continuousAt_Smooth1
Proof state before:
case h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
ε : ℝ
εpos : 0 < ε
y : ℝ
ypos : 0 < y
⊢ Continuous fun x =>
    ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * (fun x => ψ (x ^ (1 / ε)) / ε) (x / y) / ↑y
Tactic:
simp only [one_div, ite_mul, one_mul, zero_mul, RCLike.ofReal_real_eq_id, id_eq]
Proof state after:
case h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
ε : ℝ
εpos : 0 < ε
y : ℝ
ypos : 0 < y
⊢ Continuous fun x => ∫ (y : ℝ) in Ioi 0, (if 0 < y ∧ y ≤ 1 then ψ ((x / y) ^ ε⁻¹) / ε else 0) / y
Theorem: continuousAt_Smooth1
Proof state before:
case h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
ε : ℝ
εpos : 0 < ε
y : ℝ
ypos : 0 < y
⊢ Continuous fun x => ∫ (y : ℝ) in Ioi 0, (if 0 < y ∧ y ≤ 1 then ψ ((x / y) ^ ε⁻¹) / ε else 0) / y
Tactic:
sorry
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
Proof state before:
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
⊢ SmoothedChebyshev ψ ε X = ↑(∑' (n : ℕ), Λ n * Smooth1 ψ ε (↑n / X))
Tactic:
dsimp [SmoothedChebyshev, SmoothedChebyshevIntegrand, VerticalIntegral', VerticalIntegral]
Proof state after:
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
⊢ 1 / (2 * ↑π * I) *
      (I *
        ∫ (t : ℝ),
          -deriv riemannZeta (2 + ↑t * I) / riemannZeta (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) *
            ↑X ^ (2 + ↑t * I)) =
    ↑(∑' (n : ℕ), Λ n * Smooth1 ψ ε (↑n / X))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
⊢ 1 / (2 * ↑π * I) *
      (I *
        ∫ (t : ℝ),
          -deriv riemannZeta (2 + ↑t * I) / riemannZeta (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) *
            ↑X ^ (2 + ↑t * I)) =
    ↑(∑' (n : ℕ), Λ n * Smooth1 ψ ε (↑n / X))
Tactic:
rw [MellinTransform_eq]
Proof state after:
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
⊢ 1 / (2 * ↑π * I) *
      (I *
        ∫ (t : ℝ),
          -deriv riemannZeta (2 + ↑t * I) / riemannZeta (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) *
            ↑X ^ (2 + ↑t * I)) =
    ↑(∑' (n : ℕ), Λ n * Smooth1 ψ ε (↑n / X))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_1
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
⊢ 1 / (2 * ↑π * I) *
      (I *
        ∫ (t : ℝ),
          -deriv riemannZeta (2 + ↑t * I) / riemannZeta (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) *
            ↑X ^ (2 + ↑t * I)) =
    1 / (2 * ↑π * I) *
      (I *
        ∫ (t : ℝ),
          ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I))
Tactic:
congr
Proof state after:
case calc_1.e_a.e_a.e_f
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
⊢ (fun t =>
      -deriv riemannZeta (2 + ↑t * I) / riemannZeta (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) *
        ↑X ^ (2 + ↑t * I)) =
    fun t =>
    ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_1.e_a.e_a.e_f
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
⊢ (fun t =>
      -deriv riemannZeta (2 + ↑t * I) / riemannZeta (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) *
        ↑X ^ (2 + ↑t * I)) =
    fun t =>
    ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Tactic:
ext t
Proof state after:
case calc_1.e_a.e_a.e_f.h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
t : ℝ
⊢ -deriv riemannZeta (2 + ↑t * I) / riemannZeta (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) *
      ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_1.e_a.e_a.e_f.h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
t : ℝ
⊢ -deriv riemannZeta (2 + ↑t * I) / riemannZeta (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) *
      ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Tactic:
rw [LogDerivativeDirichlet (s := 2 + t * I) (by simp)]
Proof state after:
case calc_1.e_a.e_a.e_f.h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
t : ℝ
⊢ (∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I)) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_1.e_a.e_a.e_f.h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
t : ℝ
⊢ (∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I)) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Tactic:
rw [← tsum_mul_right, ← tsum_mul_right]
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
Proof state before:
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
t : ℝ
⊢ 1 < (2 + ↑t * I).re
Tactic:
simp
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_2
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
⊢ 1 / (2 * ↑π * I) *
      (I *
        ∫ (t : ℝ),
          ∑' (n : ℕ),
            ↑(Λ n) / ↑n ^ (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)) =
    1 / (2 * ↑π * I) *
      (I *
        ∑' (n : ℕ),
          ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I))
Tactic:
congr
Proof state after:
case calc_2.e_a.e_a
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
⊢ ∫ (t : ℝ),
      ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ),
      ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_2.e_a.e_a
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
⊢ ∫ (t : ℝ),
      ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ),
      ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Tactic:
rw [← MellinTransform_eq]
Proof state after:
case calc_2.e_a.e_a
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
⊢ ∫ (t : ℝ), ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ), ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)