internlm/Lean-Github huggingface dataset:
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a.e_a.refine_3
ψ : ℝ → ℝ
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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
this : (↑(X / ↑n) * ↑↑n) ^ (2 + ↑t * I) = ↑(X / ↑n) ^ (2 + ↑t * I) * ↑↑n ^ (2 + ↑t * I)
⊢ ↑X ^ (2 + ↑t * I) = (↑X / ↑n) ^ (2 + ↑t * I) * ↑n ^ (2 + ↑t * I)

case neg.e_a.e_a.refine_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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ 0 ≤ X / ↑n

case neg.e_a.e_a.refine_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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ 0 ≤ ↑n

ψ : ℝ → ℝ
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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑n ^ (2 + ↑t * I) ≠ 0
Tactic:
push_cast at this ⊢
Proof state after:
case neg.e_a.e_a.refine_3
ψ : ℝ → ℝ
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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
this : (↑X / ↑n * ↑n) ^ (2 + ↑t * I) = (↑X / ↑n) ^ (2 + ↑t * I) * ↑n ^ (2 + ↑t * I)
⊢ ↑X ^ (2 + ↑t * I) = (↑X / ↑n) ^ (2 + ↑t * I) * ↑n ^ (2 + ↑t * I)

case neg.e_a.e_a.refine_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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ 0 ≤ X / ↑n

case neg.e_a.e_a.refine_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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ 0 ≤ ↑n

ψ : ℝ → ℝ
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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑n ^ (2 + ↑t * I) ≠ 0
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a.e_a.refine_3
ψ : ℝ → ℝ
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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
this : (↑X / ↑n * ↑n) ^ (2 + ↑t * I) = (↑X / ↑n) ^ (2 + ↑t * I) * ↑n ^ (2 + ↑t * I)
⊢ ↑X ^ (2 + ↑t * I) = (↑X / ↑n) ^ (2 + ↑t * I) * ↑n ^ (2 + ↑t * I)

case neg.e_a.e_a.refine_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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ 0 ≤ X / ↑n

case neg.e_a.e_a.refine_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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ 0 ≤ ↑n

ψ : ℝ → ℝ
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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑n ^ (2 + ↑t * I) ≠ 0
Tactic:
rw [← this, div_mul_cancel₀]
Proof state after:
case neg.e_a.e_a.refine_3.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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
this : (↑X / ↑n * ↑n) ^ (2 + ↑t * I) = (↑X / ↑n) ^ (2 + ↑t * I) * ↑n ^ (2 + ↑t * I)
⊢ ↑n ≠ 0

case neg.e_a.e_a.refine_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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ 0 ≤ X / ↑n

case neg.e_a.e_a.refine_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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ 0 ≤ ↑n

ψ : ℝ → ℝ
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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑n ^ (2 + ↑t * I) ≠ 0
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a.e_a.refine_3.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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
this : (↑X / ↑n * ↑n) ^ (2 + ↑t * I) = (↑X / ↑n) ^ (2 + ↑t * I) * ↑n ^ (2 + ↑t * I)
⊢ ↑n ≠ 0
Tactic:
simp only [ne_eq, Nat.cast_eq_zero, n_ne_zero, not_false_eq_true]
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a.e_a.refine_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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ 0 ≤ X / ↑n
Tactic:
apply div_nonneg X_pos.le
Proof state after:
case neg.e_a.e_a.refine_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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ 0 ≤ ↑n
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a.e_a.refine_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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ 0 ≤ ↑n
Tactic:
simp
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a.e_a.refine_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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ 0 ≤ ↑n
Tactic:
simp
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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑n ^ (2 + ↑t * I) ≠ 0
Tactic:
simp only [ne_eq, cpow_eq_zero_iff, Nat.cast_eq_zero, not_and, not_not]
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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ n = 0 → 2 + ↑t * I = 0
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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ n = 0 → 2 + ↑t * I = 0
Tactic:
intro hn
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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
hn : n = 0
⊢ 2 + ↑t * I = 0
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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
hn : n = 0
⊢ 2 + ↑t * I = 0
Tactic:
exfalso
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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
hn : n = 0
⊢ False
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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
hn : n = 0
⊢ False
Tactic:
exact n_ne_zero hn
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_4
ψ : ℝ → ℝ
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 * ∑' (n : ℕ), ↑(Λ n) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)) =
    1 / (2 * ↑π) *
      ∑' (n : ℕ), ↑(Λ n) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)
Tactic:
conv => rw [← mul_assoc, div_mul]; lhs; lhs; rhs; simp
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_5
ψ : ℝ → ℝ
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 * ↑π) *
      ∑' (n : ℕ), ↑(Λ n) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I) =
    ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))
Tactic:
simp_rw [← tsum_mul_left, ← mul_assoc, mul_comm]
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_6
ψ : ℝ → ℝ
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 < ε
⊢ ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)) =
    ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I)))
Tactic:
have ht (t : ℝ) : -(2 + t * I) = (-1) * (2 + t * I) := by simp
Proof state after:
case calc_6
ψ : ℝ → ℝ
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 < ε
ht : ∀ (t : ℝ), -(2 + ↑t * I) = -1 * (2 + ↑t * I)
⊢ ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)) =
    ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I)))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_6
ψ : ℝ → ℝ
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 < ε
ht : ∀ (t : ℝ), -(2 + ↑t * I) = -1 * (2 + ↑t * I)
⊢ ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)) =
    ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I)))
Tactic:
have hn (n : ℂ): (n / X) ^ (-1 : ℂ) = X / n := by simp [cpow_neg_one]
Proof state after:
case calc_6
ψ : ℝ → ℝ
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 < ε
ht : ∀ (t : ℝ), -(2 + ↑t * I) = -1 * (2 + ↑t * I)
hn : ∀ (n : ℂ), (n / ↑X) ^ (-1) = ↑X / n
⊢ ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)) =
    ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I)))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_6
ψ : ℝ → ℝ
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 < ε
ht : ∀ (t : ℝ), -(2 + ↑t * I) = -1 * (2 + ↑t * I)
hn : ∀ (n : ℂ), (n / ↑X) ^ (-1) = ↑X / n
⊢ ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)) =
    ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I)))
Tactic:
have (n : ℕ): (log ((n : ℂ) / (X : ℂ)) * -1).im = 0 := by
  simp [Complex.log_im, arg_eq_zero_iff, div_nonneg (Nat.cast_nonneg _) X_pos.le]
Proof state after:
case calc_6
ψ : ℝ → ℝ
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 < ε
ht : ∀ (t : ℝ), -(2 + ↑t * I) = -1 * (2 + ↑t * I)
hn : ∀ (n : ℂ), (n / ↑X) ^ (-1) = ↑X / n
this : ∀ (n : ℕ), ((↑n / ↑X).log * -1).im = 0
⊢ ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)) =
    ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I)))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_6
ψ : ℝ → ℝ
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 < ε
ht : ∀ (t : ℝ), -(2 + ↑t * I) = -1 * (2 + ↑t * I)
hn : ∀ (n : ℂ), (n / ↑X) ^ (-1) = ↑X / n
this : ∀ (n : ℕ), ((↑n / ↑X).log * -1).im = 0
⊢ ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)) =
    ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I)))
Tactic:
have h (n : ℕ) (t : ℝ) : ((n : ℂ) / X) ^ ((-1 : ℂ) * (2 + t * I)) =
    ((n / X) ^ (-1 : ℂ)) ^ (2 + ↑t * I) := by
  rw [cpow_mul] <;> {rw [this n]; simp [Real.pi_pos, Real.pi_nonneg]}
Proof state after:
case calc_6
ψ : ℝ → ℝ
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 < ε
ht : ∀ (t : ℝ), -(2 + ↑t * I) = -1 * (2 + ↑t * I)
hn : ∀ (n : ℂ), (n / ↑X) ^ (-1) = ↑X / n
this : ∀ (n : ℕ), ((↑n / ↑X).log * -1).im = 0
h : ∀ (n : ℕ) (t : ℝ), (↑n / ↑X) ^ (-1 * (2 + ↑t * I)) = ((↑n / ↑X) ^ (-1)) ^ (2 + ↑t * I)
⊢ ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)) =
    ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I)))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_6
ψ : ℝ → ℝ
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 < ε
ht : ∀ (t : ℝ), -(2 + ↑t * I) = -1 * (2 + ↑t * I)
hn : ∀ (n : ℂ), (n / ↑X) ^ (-1) = ↑X / n
this : ∀ (n : ℕ), ((↑n / ↑X).log * -1).im = 0
h : ∀ (n : ℕ) (t : ℝ), (↑n / ↑X) ^ (-1 * (2 + ↑t * I)) = ((↑n / ↑X) ^ (-1)) ^ (2 + ↑t * I)
⊢ ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)) =
    ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I)))
Tactic:
conv => rhs; rhs; intro n; rhs; rhs; rhs; intro t; rhs; rw [ht t, h n t]; lhs; rw [hn]
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 : ℝ
⊢ -(2 + ↑t * I) = -1 * (2 + ↑t * I)
Tactic:
simp
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 < ε
ht : ∀ (t : ℝ), -(2 + ↑t * I) = -1 * (2 + ↑t * I)
n : ℂ
⊢ (n / ↑X) ^ (-1) = ↑X / n
Tactic:
simp [cpow_neg_one]
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 < ε
ht : ∀ (t : ℝ), -(2 + ↑t * I) = -1 * (2 + ↑t * I)
hn : ∀ (n : ℂ), (n / ↑X) ^ (-1) = ↑X / n
n : ℕ
⊢ ((↑n / ↑X).log * -1).im = 0
Tactic:
simp [Complex.log_im, arg_eq_zero_iff, div_nonneg (Nat.cast_nonneg _) X_pos.le]
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 < ε
ht : ∀ (t : ℝ), -(2 + ↑t * I) = -1 * (2 + ↑t * I)
hn : ∀ (n : ℂ), (n / ↑X) ^ (-1) = ↑X / n
this : ∀ (n : ℕ), ((↑n / ↑X).log * -1).im = 0
n : ℕ
t : ℝ
⊢ (↑n / ↑X) ^ (-1 * (2 + ↑t * I)) = ((↑n / ↑X) ^ (-1)) ^ (2 + ↑t * I)
Tactic:
rw [cpow_mul] <;> {rw [this n]; simp [Real.pi_pos, Real.pi_nonneg]}
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
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
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
ht : ∀ (t : ℝ), -(2 + ↑t * I) = -1 * (2 + ↑t * I)
hn : ∀ (n : ℂ), (n / ↑X) ^ (-1) = ↑X / n
this : ∀ (n : ℕ), ((↑n / ↑X).log * -1).im = 0
n : ℕ
t : ℝ
⊢ ((↑n / ↑X).log * -1).im ≤ π
Tactic:
rw [this n]
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
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
ht : ∀ (t : ℝ), -(2 + ↑t * I) = -1 * (2 + ↑t * I)
hn : ∀ (n : ℂ), (n / ↑X) ^ (-1) = ↑X / n
this : ∀ (n : ℕ), ((↑n / ↑X).log * -1).im = 0
n : ℕ
t : ℝ
⊢ 0 ≤ π
Theorem: SmoothedChebyshevDirichlet
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
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
ht : ∀ (t : ℝ), -(2 + ↑t * I) = -1 * (2 + ↑t * I)
hn : ∀ (n : ℂ), (n / ↑X) ^ (-1) = ↑X / n
this : ∀ (n : ℕ), ((↑n / ↑X).log * -1).im = 0
n : ℕ
t : ℝ
⊢ 0 ≤ π
Tactic:
simp [Real.pi_pos, Real.pi_nonneg]
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_7
ψ : ℝ → ℝ
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 < ε
⊢ ∑' (n : ℕ),
      ↑(Λ n) *
        (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I))) =
    ↑(∑' (n : ℕ), Λ n * Smooth1 ψ ε (↑n / X))
Tactic:
push_cast
Proof state after:
case calc_7
ψ : ℝ → ℝ
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 < ε
⊢ ∑' (n : ℕ),
      ↑(Λ n) *
        (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I))) =
    ∑' (a : ℕ), ↑(Λ a) * ↑(Smooth1 ψ ε (↑a / X))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_7
ψ : ℝ → ℝ
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 < ε
⊢ ∑' (n : ℕ),
      ↑(Λ n) *
        (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I))) =
    ∑' (a : ℕ), ↑(Λ a) * ↑(Smooth1 ψ ε (↑a / X))
Tactic:
congr
Proof state after:
case calc_7.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 n =>
      ↑(Λ n) *
        (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I)))) =
    fun a => ↑(Λ a) * ↑(Smooth1 ψ ε (↑a / X))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_7.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 n =>
      ↑(Λ n) *
        (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I)))) =
    fun a => ↑(Λ a) * ↑(Smooth1 ψ ε (↑a / X))
Tactic:
ext n
Proof state after:
case calc_7.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 < ε
n : ℕ
⊢ ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I))) =
    ↑(Λ n) * ↑(Smooth1 ψ ε (↑n / X))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_7.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 < ε
n : ℕ
⊢ ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I))) =
    ↑(Λ n) * ↑(Smooth1 ψ ε (↑n / X))
Tactic:
by_cases n_zero : n = 0
Proof state after:
case pos
ψ : ℝ → ℝ
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 < ε
n : ℕ
n_zero : n = 0
⊢ ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I))) =
    ↑(Λ n) * ↑(Smooth1 ψ ε (↑n / X))

case neg
ψ : ℝ → ℝ
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 < ε
n : ℕ
n_zero : ¬n = 0
⊢ ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I))) =
    ↑(Λ n) * ↑(Smooth1 ψ ε (↑n / X))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case pos
ψ : ℝ → ℝ
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 < ε
n : ℕ
n_zero : n = 0
⊢ ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I))) =
    ↑(Λ n) * ↑(Smooth1 ψ ε (↑n / X))

case neg
ψ : ℝ → ℝ
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 < ε
n : ℕ
n_zero : ¬n = 0
⊢ ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I))) =
    ↑(Λ n) * ↑(Smooth1 ψ ε (↑n / X))
Tactic:
simp [n_zero]
Proof state after:
case neg
ψ : ℝ → ℝ
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 < ε
n : ℕ
n_zero : ¬n = 0
⊢ ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I))) =
    ↑(Λ n) * ↑(Smooth1 ψ ε (↑n / X))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg
ψ : ℝ → ℝ
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 < ε
n : ℕ
n_zero : ¬n = 0
⊢ ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I))) =
    ↑(Λ n) * ↑(Smooth1 ψ ε (↑n / X))
Tactic:
have n_pos : 0 < n := by
  simpa only [n_zero, gt_iff_lt, false_or] using (Nat.eq_zero_or_pos n)
Proof state after:
case neg
ψ : ℝ → ℝ
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 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I))) =
    ↑(Λ n) * ↑(Smooth1 ψ ε (↑n / X))