ext n
case calc_3.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 n =>
      ∫ (t : ℝ), ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I)) =
    fun n => ↑(Λ n) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)
case calc_3.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 < ε
n : ℕ
⊢ ∫ (t : ℝ), ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) =
    ↑(Λ n) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)