Theorem: DeltaSpikeNonNeg_of_NonNeg (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
x ε : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ 0 ≤ DeltaSpike Ψ ε x
Tactic:
dsimp [DeltaSpike]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
x ε : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ 0 ≤ Ψ (x ^ (1 / ε)) / ε

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
x ε : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ 0 ≤ Ψ (x ^ (1 / ε)) / ε
Tactic:
have : 0 < x ^ (1 / ε) := by positivity
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
x ε : ℝ
xpos : 0 < x
εpos : 0 < ε
this : 0 < x ^ (1 / ε)
⊢ 0 ≤ Ψ (x ^ (1 / ε)) / ε

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
x ε : ℝ
xpos : 0 < x
εpos : 0 < ε
this : 0 < x ^ (1 / ε)
⊢ 0 ≤ Ψ (x ^ (1 / ε)) / ε
Tactic:
have : 0 ≤ Ψ (x ^ (1 / ε)) := Ψnonneg _ this
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
x ε : ℝ
xpos : 0 < x
εpos : 0 < ε
this✝ : 0 < x ^ (1 / ε)
this : 0 ≤ Ψ (x ^ (1 / ε))
⊢ 0 ≤ Ψ (x ^ (1 / ε)) / ε

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
x ε : ℝ
xpos : 0 < x
εpos : 0 < ε
this✝ : 0 < x ^ (1 / ε)
this : 0 ≤ Ψ (x ^ (1 / ε))
⊢ 0 ≤ Ψ (x ^ (1 / ε)) / ε
Tactic:
positivity
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
x ε : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ 0 < x ^ (1 / ε)
Tactic:
positivity
State after:
no goals