Theorem: DeltaSpikeContinuous (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
diffΨ : ContDiff ℝ 1 Ψ
⊢ Continuous fun x => DeltaSpike Ψ ε x
Tactic:
apply diffΨ.continuous.comp (g := Ψ) _ |>.div_const
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
diffΨ : ContDiff ℝ 1 Ψ
⊢ Continuous fun x => x ^ (1 / ε)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
diffΨ : ContDiff ℝ 1 Ψ
⊢ Continuous fun x => x ^ (1 / ε)
Tactic:
exact continuous_id.rpow_const fun _ ↦ Or.inr <| div_nonneg (by norm_num) εpos.le
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
diffΨ : ContDiff ℝ 1 Ψ
x✝ : ℝ
⊢ 0 ≤ 1
Tactic:
norm_num
State after:
no goals