Theorem: SmoothedChebyshevDirichlet (PrimeNumberTheoremAnd/MediumPNT.lean)

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]
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))

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]
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))

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) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) *
            ↑X ^ (2 + ↑t * I)) =
    ↑(∑' (n : ℕ), Λ n * Smooth1 ψ ε (↑n / X))
Tactic:
calc
  _ = 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)) := ?_
  _ = 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)) := ?_
  _ = ∑' 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))) := ?_
  _ = _ := ?_
State after:
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))

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))

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

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)

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))

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)))

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))

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
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)

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
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)

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)]
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)

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]
State after:
no goals

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
State after:
no goals

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
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)

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]
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)

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) * 𝓜 (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)
Tactic:
have := @MellinOfSmooth1b ψ diffΨ suppΨ 2 2 (by norm_num) ε εpos
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 < ε
this : (fun s => ‖𝓜 (fun x => ↑(Smooth1 ψ ε x)) s‖) =O[𝓟 {s | 2 ≤ s.re ∧ s.re ≤ 2}] fun s => 1 / (ε * ‖s‖ ^ 2)
⊢ ∫ (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)

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 < ε
this : (fun s => ‖𝓜 (fun x => ↑(Smooth1 ψ ε x)) s‖) =O[𝓟 {s | 2 ≤ s.re ∧ s.re ≤ 2}] fun s => 1 / (ε * ‖s‖ ^ 2)
⊢ ∫ (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)
Tactic:
simp_rw [Asymptotics.isBigO_iff] at this
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 < ε
this : ∃ c, ∀ᶠ (x : ℂ) in 𝓟 {s | 2 ≤ s.re ∧ s.re ≤ 2}, ‖‖𝓜 (fun x => ↑(Smooth1 ψ ε x)) x‖‖ ≤ c * ‖1 / (ε * ‖x‖ ^ 2)‖
⊢ ∫ (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)

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 < ε
this : ∃ c, ∀ᶠ (x : ℂ) in 𝓟 {s | 2 ≤ s.re ∧ s.re ≤ 2}, ‖‖𝓜 (fun x => ↑(Smooth1 ψ ε x)) x‖‖ ≤ c * ‖1 / (ε * ‖x‖ ^ 2)‖
⊢ ∫ (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)
Tactic:
obtain ⟨c, hc⟩ := this
State after:
case calc_2.e_a.e_a.intro
ψ : ℝ → ℝ
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 < ε
c : ℝ
hc : ∀ᶠ (x : ℂ) in 𝓟 {s | 2 ≤ s.re ∧ s.re ≤ 2}, ‖‖𝓜 (fun x => ↑(Smooth1 ψ ε x)) x‖‖ ≤ c * ‖1 / (ε * ‖x‖ ^ 2)‖
⊢ ∫ (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)

State before:
case calc_2.e_a.e_a.intro
ψ : ℝ → ℝ
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 < ε
c : ℝ
hc : ∀ᶠ (x : ℂ) in 𝓟 {s | 2 ≤ s.re ∧ s.re ≤ 2}, ‖‖𝓜 (fun x => ↑(Smooth1 ψ ε x)) x‖‖ ≤ c * ‖1 / (ε * ‖x‖ ^ 2)‖
⊢ ∫ (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)
Tactic:
simp only [Real.norm_eq_abs, Complex.abs_abs, one_div, mul_inv_rev, norm_mul,
  norm_inv, norm_pow, eventually_principal, mem_setOf_eq, and_imp] at hc
State after:
case calc_2.e_a.e_a.intro
ψ : ℝ → ℝ
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 < ε
c : ℝ
hc : ∀ (x : ℂ), 2 ≤ x.re → x.re ≤ 2 → |‖𝓜 (fun x => ↑(Smooth1 ψ ε x)) x‖| ≤ c * ((|‖x‖| ^ 2)⁻¹ * |ε|⁻¹)
⊢ ∫ (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)

State before:
case calc_2.e_a.e_a.intro
ψ : ℝ → ℝ
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 < ε
c : ℝ
hc : ∀ (x : ℂ), 2 ≤ x.re → x.re ≤ 2 → |‖𝓜 (fun x => ↑(Smooth1 ψ ε x)) x‖| ≤ c * ((|‖x‖| ^ 2)⁻¹ * |ε|⁻¹)
⊢ ∫ (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)
Tactic:
simp only [Complex.norm_eq_abs, Complex.abs_abs] at hc
State after:
case calc_2.e_a.e_a.intro
ψ : ℝ → ℝ
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 < ε
c : ℝ
hc :
  ∀ (x : ℂ), 2 ≤ x.re → x.re ≤ 2 → Complex.abs (𝓜 (fun x => ↑(Smooth1 ψ ε x)) x) ≤ c * ((Complex.abs x ^ 2)⁻¹ * |ε|⁻¹)
⊢ ∫ (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)

State before:
case calc_2.e_a.e_a.intro
ψ : ℝ → ℝ
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 < ε
c : ℝ
hc :
  ∀ (x : ℂ), 2 ≤ x.re → x.re ≤ 2 → Complex.abs (𝓜 (fun x => ↑(Smooth1 ψ ε x)) x) ≤ c * ((Complex.abs x ^ 2)⁻¹ * |ε|⁻¹)
⊢ ∫ (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)
Tactic:
replace hc (t : ℝ) := hc (2 + t * I) (by simp) (by simp)
State after:
case calc_2.e_a.e_a.intro
ψ : ℝ → ℝ
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 < ε
c : ℝ
hc :
  ∀ (t : ℝ), Complex.abs (𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) ≤ c * ((Complex.abs (2 + ↑t * I) ^ 2)⁻¹ * |ε|⁻¹)
⊢ ∫ (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)

State before:
case calc_2.e_a.e_a.intro
ψ : ℝ → ℝ
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 < ε
c : ℝ
hc :
  ∀ (t : ℝ), Complex.abs (𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) ≤ c * ((Complex.abs (2 + ↑t * I) ^ 2)⁻¹ * |ε|⁻¹)
⊢ ∫ (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)
Tactic:
sorry
State after:
no goals

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 < ε
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

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 < ε
c : ℝ
hc :
  ∀ (x : ℂ), 2 ≤ x.re → x.re ≤ 2 → Complex.abs (𝓜 (fun x => ↑(Smooth1 ψ ε x)) x) ≤ c * ((Complex.abs x ^ 2)⁻¹ * |ε|⁻¹)
t : ℝ
⊢ 2 ≤ (2 + ↑t * I).re
Tactic:
simp
State after:
no goals

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 < ε
c : ℝ
hc :
  ∀ (x : ℂ), 2 ≤ x.re → x.re ≤ 2 → Complex.abs (𝓜 (fun x => ↑(Smooth1 ψ ε x)) x) ≤ c * ((Complex.abs x ^ 2)⁻¹ * |ε|⁻¹)
t : ℝ
⊢ (2 + ↑t * I).re ≤ 2
Tactic:
simp
State after:
no goals

State before:
case calc_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 < ε
⊢ 1 / (2 * ↑π * I) *
      (I *
        ∑' (n : ℕ),
          ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)) =
    1 / (2 * ↑π * I) *
      (I * ∑' (n : ℕ), ↑(Λ n) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))
Tactic:
field_simp
State after:
case calc_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 < ε
⊢ (I *
        ∑' (n : ℕ),
          ∫ (t : ℝ), ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I)) /
      (2 * ↑π * I) =
    (I * ∑' (n : ℕ), ↑(Λ n) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)) /
      (2 * ↑π * I)

State before:
case calc_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 < ε
⊢ (I *
        ∑' (n : ℕ),
          ∫ (t : ℝ), ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I)) /
      (2 * ↑π * I) =
    (I * ∑' (n : ℕ), ↑(Λ n) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)) /
      (2 * ↑π * I)
Tactic:
congr
State after:
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)

State before:
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)
Tactic:
ext n
State after:
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)

State before:
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)
Tactic:
rw [← MeasureTheory.integral_mul_left ]
State after:
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) =
    ∫ (a : ℝ), ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑a * I) * (↑X / ↑n) ^ (2 + ↑a * I))

State before:
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) =
    ∫ (a : ℝ), ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑a * I) * (↑X / ↑n) ^ (2 + ↑a * I))
Tactic:
congr
State after:
case calc_3.e_a.e_a.e_f.h.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 < ε
n : ℕ
⊢ (fun t => ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I)) = fun a =>
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑a * I) * (↑X / ↑n) ^ (2 + ↑a * I))

State before:
case calc_3.e_a.e_a.e_f.h.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 < ε
n : ℕ
⊢ (fun t => ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I)) = fun a =>
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑a * I) * (↑X / ↑n) ^ (2 + ↑a * I))
Tactic:
ext t
State after:
case calc_3.e_a.e_a.e_f.h.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) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))

State before:
case calc_3.e_a.e_a.e_f.h.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) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))
Tactic:
by_cases n_ne_zero : n = 0
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 : ℕ
t : ℝ
n_ne_zero : n = 0
⊢ ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) =
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))

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 : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) =
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))

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

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 : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) =
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))
Tactic:
simp [n_ne_zero]
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 : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) =
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))

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 : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) =
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))
Tactic:
rw [mul_div_assoc, mul_assoc]
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 : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I))) =
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))

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 : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I))) =
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))
Tactic:
congr
State after:
case neg.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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) = (↑X / ↑n) ^ (2 + ↑t * I)

State before:
case neg.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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) = (↑X / ↑n) ^ (2 + ↑t * I)
Tactic:
rw [(div_eq_iff ?_).mpr]
State after:
case neg.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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑X ^ (2 + ↑t * I) = (↑X / ↑n) ^ (2 + ↑t * I) * ↑n ^ (2 + ↑t * I)

ψ : ℝ → ℝ
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

State before:
case neg.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 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑X ^ (2 + ↑t * I) = (↑X / ↑n) ^ (2 + ↑t * I) * ↑n ^ (2 + ↑t * I)

ψ : ℝ → ℝ
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:
have := @mul_cpow_ofReal_nonneg (a := X / (n : ℝ)) (b := (n : ℝ)) (r := 2 + t * I) ?_ ?_
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

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 ⊢
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

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₀]
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

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]
State after:
no goals

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
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

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
State after:
no goals

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
State after:
no goals

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]
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

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
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)))

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]
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)))

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]
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)))

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]}
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)))

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]
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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]}
State after:
no goals

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]
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 ≤ π

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]
State after:
no goals

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
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))

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
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))

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
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))

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
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))

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]
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))

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)
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))

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_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:
congr
State after:
case neg.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 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))

State before:
case neg.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 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))
Tactic:
rw [(by rw [div_mul]; simp : 1 / (2 * π) = 1 / (2 * π * I) * I), mul_assoc]
State after:
case neg.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 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I))) =
    ↑(Smooth1 ψ ε (↑n / X))

State before:
case neg.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 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I))) =
    ↑(Smooth1 ψ ε (↑n / X))
Tactic:
conv => lhs; rhs; rhs; rhs; intro t; rw [mul_comm]; norm_cast
State after:
case neg.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 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), ↑(↑n / X) ^ (-(2 + ↑t * I)) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))

State before:
case neg.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 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), ↑(↑n / X) ^ (-(2 + ↑t * I)) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))
Tactic:
have := MellinInversion 2 (f := fun x ↦ (Smooth1 ψ ε x : ℂ)) (x := n / X)
  (by simp [n_pos, X_pos]) ?_ ?_ ?_
State after:
case neg.e_a.refine_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 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
this : MellinInverseTransform (𝓜 fun x => ↑(Smooth1 ψ ε x)) 2 (↑n / X) = (fun x => ↑(Smooth1 ψ ε x)) (↑n / X)
⊢ 1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), ↑(↑n / X) ^ (-(2 + ↑t * I)) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))

case neg.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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MellinConvergent (fun x => ↑(Smooth1 ψ ε x)) ↑2

case neg.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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ VerticalIntegrable (mellin fun x => ↑(Smooth1 ψ ε x)) 2 MeasureTheory.volume

case neg.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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ ContinuousAt (fun x => ↑(Smooth1 ψ ε x)) (↑n / X)

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 : ℕ
n_zero : ¬n = 0
⊢ 0 < n
Tactic:
simpa only [n_zero, gt_iff_lt, false_or] using (Nat.eq_zero_or_pos n)
State after:
no goals

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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 1 / (2 * ↑π) = 1 / (2 * ↑π * I) * I
Tactic:
rw [div_mul]
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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 1 / (2 * ↑π) = 1 / (2 * ↑π * I / I)

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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 1 / (2 * ↑π) = 1 / (2 * ↑π * I / I)
Tactic:
simp
State after:
no goals

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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 0 < ↑n / X
Tactic:
simp [n_pos, X_pos]
State after:
no goals

State before:
case neg.e_a.refine_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 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
this : MellinInverseTransform (𝓜 fun x => ↑(Smooth1 ψ ε x)) 2 (↑n / X) = (fun x => ↑(Smooth1 ψ ε x)) (↑n / X)
⊢ 1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), ↑(↑n / X) ^ (-(2 + ↑t * I)) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))
Tactic:
beta_reduce at this
State after:
case neg.e_a.refine_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 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
this : MellinInverseTransform (𝓜 fun x => ↑(Smooth1 ψ ε x)) 2 (↑n / X) = ↑(Smooth1 ψ ε (↑n / X))
⊢ 1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), ↑(↑n / X) ^ (-(2 + ↑t * I)) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))

State before:
case neg.e_a.refine_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 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
this : MellinInverseTransform (𝓜 fun x => ↑(Smooth1 ψ ε x)) 2 (↑n / X) = ↑(Smooth1 ψ ε (↑n / X))
⊢ 1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), ↑(↑n / X) ^ (-(2 + ↑t * I)) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))
Tactic:
dsimp [MellinInverseTransform, VerticalIntegral] at this
State after:
case neg.e_a.refine_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 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
this :
  1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), ↑(↑n / X) ^ (-(2 + ↑t * I)) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))
⊢ 1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), ↑(↑n / X) ^ (-(2 + ↑t * I)) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))

State before:
case neg.e_a.refine_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 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
this :
  1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), ↑(↑n / X) ^ (-(2 + ↑t * I)) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))
⊢ 1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), ↑(↑n / X) ^ (-(2 + ↑t * I)) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))
Tactic:
rw [← MellinTransform_eq, this]
State after:
no goals

State before:
case neg.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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MellinConvergent (fun x => ↑(Smooth1 ψ ε x)) ↑2
Tactic:
dsimp [MellinConvergent]
State after:
case neg.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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.IntegrableOn (fun t => ↑t ^ (2 - 1) * ↑(Smooth1 ψ ε t)) (Ioi 0) MeasureTheory.volume

State before:
case neg.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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.IntegrableOn (fun t => ↑t ^ (2 - 1) * ↑(Smooth1 ψ ε t)) (Ioi 0) MeasureTheory.volume
Tactic:
norm_num
State after:
case neg.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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.IntegrableOn (fun t => ↑t * ↑(Smooth1 ψ ε t)) (Ioi 0) MeasureTheory.volume

State before:
case neg.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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.IntegrableOn (fun t => ↑t * ↑(Smooth1 ψ ε t)) (Ioi 0) MeasureTheory.volume
Tactic:
norm_cast
State after:
case neg.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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.IntegrableOn (fun t => ↑(t * Smooth1 ψ ε t)) (Ioi 0) MeasureTheory.volume

State before:
case neg.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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.IntegrableOn (fun t => ↑(t * Smooth1 ψ ε t)) (Ioi 0) MeasureTheory.volume
Tactic:
exact (integrable_x_mul_Smooth1 diffΨ ψpos suppΨ mass_one ε εpos).ofReal
State after:
no goals

State before:
case neg.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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ VerticalIntegrable (mellin fun x => ↑(Smooth1 ψ ε x)) 2 MeasureTheory.volume
Tactic:
dsimp [VerticalIntegrable, mellin]
State after:
case neg.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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.Integrable (fun y => ∫ (t : ℝ) in Ioi 0, ↑t ^ (2 + ↑y * I - 1) * ↑(Smooth1 ψ ε t)) MeasureTheory.volume

State before:
case neg.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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.Integrable (fun y => ∫ (t : ℝ) in Ioi 0, ↑t ^ (2 + ↑y * I - 1) * ↑(Smooth1 ψ ε t)) MeasureTheory.volume
Tactic:
ring_nf
State after:
case neg.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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.Integrable (fun y => ∫ (t : ℝ) in Ioi 0, ↑t ^ (1 + ↑y * I) * ↑(Smooth1 ψ ε t)) MeasureTheory.volume

State before:
case neg.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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.Integrable (fun y => ∫ (t : ℝ) in Ioi 0, ↑t ^ (1 + ↑y * I) * ↑(Smooth1 ψ ε t)) MeasureTheory.volume
Tactic:
exact vertical_integrable_Smooth1 diffΨ ψpos suppΨ mass_one ε εpos
State after:
no goals

State before:
case neg.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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ ContinuousAt (fun x => ↑(Smooth1 ψ ε x)) (↑n / X)
Tactic:
refine ContinuousAt.comp (g := ofReal) RCLike.continuous_ofReal.continuousAt ?_
State after:
case neg.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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ ContinuousAt (fun x => Smooth1 ψ ε x) (↑n / X)

State before:
case neg.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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ ContinuousAt (fun x => Smooth1 ψ ε x) (↑n / X)
Tactic:
exact continuousAt_Smooth1 diffΨ ψpos suppΨ mass_one ε εpos (n / X) (by positivity)
State after:
no goals

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 : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 0 < ↑n / X
Tactic:
positivity
State after:
no goals