Theorem: Smooth1Nonneg (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ 0 ≤ Smooth1 Ψ ε x
Tactic:
dsimp [Smooth1]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ 0 ≤ MellinConvolution (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) (DeltaSpike Ψ ε) x

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ 0 ≤ MellinConvolution (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) (DeltaSpike Ψ ε) x
Tactic:
apply MellinConvNonNeg_of_NonNeg ?_ ?_ xpos
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ ∀ x > 0, 0 ≤ if 0 < x ∧ x ≤ 1 then 1 else 0

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ ∀ x > 0, 0 ≤ DeltaSpike Ψ ε x

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ ∀ x > 0, 0 ≤ if 0 < x ∧ x ≤ 1 then 1 else 0
Tactic:
intro y hy
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
y : ℝ
hy : y > 0
⊢ 0 ≤ if 0 < y ∧ y ≤ 1 then 1 else 0

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
y : ℝ
hy : y > 0
⊢ 0 ≤ if 0 < y ∧ y ≤ 1 then 1 else 0
Tactic:
by_cases h : y ≤ 1 <;> simp [h, hy]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ ∀ x > 0, 0 ≤ DeltaSpike Ψ ε x
Tactic:
intro y ypos
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
y : ℝ
ypos : y > 0
⊢ 0 ≤ DeltaSpike Ψ ε y

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
y : ℝ
ypos : y > 0
⊢ 0 ≤ DeltaSpike Ψ ε y
Tactic:
exact DeltaSpikeNonNeg_of_NonNeg Ψnonneg ypos εpos
State after:
no goals