dsimp [MellinConvolution]
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℝ
f_nonneg : ∀ x > 0, 0 ≤ f x
g_nonneg : ∀ x > 0, 0 ≤ g x
x : ℝ
xpos : 0 < x
⊢ 0 ≤ MellinConvolution f g x
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℝ
f_nonneg : ∀ x > 0, 0 ≤ f x
g_nonneg : ∀ x > 0, 0 ≤ g x
x : ℝ
xpos : 0 < x
⊢ 0 ≤ ∫ (y : ℝ) in Ioi 0, f y * g (x / y) / y