Theorem: MellinOfDeltaSpike (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
⊢ 𝓜 (fun x => ↑(DeltaSpike Ψ ε x)) s = 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
unfold MellinTransform DeltaSpike
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
⊢ ∫ (x : ℝ) in Ioi 0, (fun x => ↑(Ψ (x ^ (1 / ε)) / ε)) x * ↑x ^ (s - 1) =
    ∫ (x : ℝ) in Ioi 0, (fun x => ↑(Ψ x)) x * ↑x ^ (↑ε * s - 1)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
⊢ ∫ (x : ℝ) in Ioi 0, (fun x => ↑(Ψ (x ^ (1 / ε)) / ε)) x * ↑x ^ (s - 1) =
    ∫ (x : ℝ) in Ioi 0, (fun x => ↑(Ψ x)) x * ↑x ^ (↑ε * s - 1)
Tactic:
rw [← integral_comp_rpow_Ioi (fun z ↦ ((Ψ z) : ℂ) * (z : ℂ) ^ ((ε : ℂ) * s - 1))
  (one_div_ne_zero (ne_of_gt εpos))]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
⊢ ∫ (x : ℝ) in Ioi 0, (fun x => ↑(Ψ (x ^ (1 / ε)) / ε)) x * ↑x ^ (s - 1) =
    ∫ (x : ℝ) in Ioi 0, (|1 / ε| * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
⊢ ∫ (x : ℝ) in Ioi 0, (fun x => ↑(Ψ (x ^ (1 / ε)) / ε)) x * ↑x ^ (s - 1) =
    ∫ (x : ℝ) in Ioi 0, (|1 / ε| * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))
Tactic:
apply setIntegral_congr_ae measurableSet_Ioi
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
⊢ ∀ᵐ (x : ℝ),
    x ∈ Ioi 0 →
      (fun x => ↑(Ψ (x ^ (1 / ε)) / ε)) x * ↑x ^ (s - 1) =
        (|1 / ε| * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
⊢ ∀ᵐ (x : ℝ),
    x ∈ Ioi 0 →
      (fun x => ↑(Ψ (x ^ (1 / ε)) / ε)) x * ↑x ^ (s - 1) =
        (|1 / ε| * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))
Tactic:
filter_upwards with x hx
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(Ψ (x ^ (1 / ε)) / ε) * ↑x ^ (s - 1) =
    (|1 / ε| * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(Ψ (x ^ (1 / ε)) / ε) * ↑x ^ (s - 1) =
    (|1 / ε| * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))
Tactic:
have log_x_real: (Complex.log (x : ℂ)).im = 0 := by
  rw [← ofReal_log, ofReal_im]
  exact LT.lt.le hx
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε)) / ε) * ↑x ^ (s - 1) =
    (|1 / ε| * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε)) / ε) * ↑x ^ (s - 1) =
    (|1 / ε| * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))
Tactic:
rw [div_eq_mul_inv, ofReal_mul, abs_of_pos (one_div_pos.mpr εpos)]
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε))) * ↑ε⁻¹ * ↑x ^ (s - 1) =
    (1 / ε * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε))) * ↑ε⁻¹ * ↑x ^ (s - 1) =
    (1 / ε * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))
Tactic:
simp only [real_smul, ofReal_mul, ofReal_div, ofReal_one, Complex.ofReal_rpow hx]
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε))) * ↑ε⁻¹ * ↑x ^ (s - 1) =
    1 / ↑ε * ↑x ^ ↑(1 / ε - 1) * (↑(Ψ (x ^ (1 / ε))) * (↑x ^ (1 / ↑ε)) ^ (↑ε * s - 1))

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε))) * ↑ε⁻¹ * ↑x ^ (s - 1) =
    1 / ↑ε * ↑x ^ ↑(1 / ε - 1) * (↑(Ψ (x ^ (1 / ε))) * (↑x ^ (1 / ↑ε)) ^ (↑ε * s - 1))
Tactic:
rw [← Complex.cpow_mul _ ?_ ?_, mul_sub]
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε))) * ↑ε⁻¹ * ↑x ^ (s - 1) =
    1 / ↑ε * ↑x ^ ↑(1 / ε - 1) * (↑(Ψ (x ^ (1 / ε))) * ↑x ^ (1 / ↑ε * (↑ε * s) - 1 / ↑ε * 1))

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ -π < ((↑x).log * (1 / ↑ε)).im

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ((↑x).log * (1 / ↑ε)).im ≤ π

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ (↑x).log.im = 0
Tactic:
rw [← ofReal_log, ofReal_im]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ 0 ≤ x

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ 0 ≤ x
Tactic:
exact LT.lt.le hx
State after:
no goals

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε))) * ↑ε⁻¹ * ↑x ^ (s - 1) =
    1 / ↑ε * ↑x ^ ↑(1 / ε - 1) * (↑(Ψ (x ^ (1 / ε))) * ↑x ^ (1 / ↑ε * (↑ε * s) - 1 / ↑ε * 1))
Tactic:
simp only [← mul_assoc, ofReal_sub, ofReal_div, ofReal_one, mul_one, ofReal_inv]
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε))) * (↑ε)⁻¹ * ↑x ^ (s - 1) =
    1 / ↑ε * ↑x ^ (1 / ↑ε - 1) * ↑(Ψ (x ^ (1 / ε))) * ↑x ^ (1 / ↑ε * ↑ε * s - 1 / ↑ε)

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε))) * (↑ε)⁻¹ * ↑x ^ (s - 1) =
    1 / ↑ε * ↑x ^ (1 / ↑ε - 1) * ↑(Ψ (x ^ (1 / ε))) * ↑x ^ (1 / ↑ε * ↑ε * s - 1 / ↑ε)
Tactic:
symm
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ 1 / ↑ε * ↑x ^ (1 / ↑ε - 1) * ↑(Ψ (x ^ (1 / ε))) * ↑x ^ (1 / ↑ε * ↑ε * s - 1 / ↑ε) =
    ↑(Ψ (x ^ (1 / ε))) * (↑ε)⁻¹ * ↑x ^ (s - 1)

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ 1 / ↑ε * ↑x ^ (1 / ↑ε - 1) * ↑(Ψ (x ^ (1 / ε))) * ↑x ^ (1 / ↑ε * ↑ε * s - 1 / ↑ε) =
    ↑(Ψ (x ^ (1 / ε))) * (↑ε)⁻¹ * ↑x ^ (s - 1)
Tactic:
rw [one_div_mul_cancel (by exact slitPlane_ne_zero (Or.inl εpos)), mul_comm (1 / (ε:ℂ)),
    mul_comm, ← mul_assoc, ← mul_assoc]
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑x ^ (1 * s - 1 / ↑ε) * ↑x ^ (1 / ↑ε - 1) * (1 / ↑ε) * ↑(Ψ (x ^ (1 / ε))) = ↑(Ψ (x ^ (1 / ε))) * (↑ε)⁻¹ * ↑x ^ (s - 1)

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑x ^ (1 * s - 1 / ↑ε) * ↑x ^ (1 / ↑ε - 1) * (1 / ↑ε) * ↑(Ψ (x ^ (1 / ε))) = ↑(Ψ (x ^ (1 / ε))) * (↑ε)⁻¹ * ↑x ^ (s - 1)
Tactic:
rw [← Complex.cpow_add _ _ (by exact slitPlane_ne_zero (Or.inl hx))]
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑x ^ (1 * s - 1 / ↑ε + (1 / ↑ε - 1)) * (1 / ↑ε) * ↑(Ψ (x ^ (1 / ε))) = ↑(Ψ (x ^ (1 / ε))) * (↑ε)⁻¹ * ↑x ^ (s - 1)

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑x ^ (1 * s - 1 / ↑ε + (1 / ↑ε - 1)) * (1 / ↑ε) * ↑(Ψ (x ^ (1 / ε))) = ↑(Ψ (x ^ (1 / ε))) * (↑ε)⁻¹ * ↑x ^ (s - 1)
Tactic:
ring_nf
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑ε ≠ 0
Tactic:
exact slitPlane_ne_zero (Or.inl εpos)
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑x ≠ 0
Tactic:
exact slitPlane_ne_zero (Or.inl hx)
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ -π < ((↑x).log * (1 / ↑ε)).im
Tactic:
simp [im_mul_ofReal, log_x_real, zero_mul, pi_pos]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ((↑x).log * (1 / ↑ε)).im ≤ π
Tactic:
simp [im_mul_ofReal, log_x_real, zero_mul, pi_nonneg]
State after:
no goals