Theorem: MellinConvNonNeg_of_NonNeg (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : 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
Tactic:
dsimp [MellinConvolution]
State after:
𝕂 : 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

State before:
𝕂 : 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
Tactic:
apply MeasureTheory.setIntegral_nonneg
State after:
case hs
𝕂 : 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
⊢ MeasurableSet (Ioi 0)

case hf
𝕂 : 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
⊢ ∀ x_1 ∈ Ioi 0, 0 ≤ f x_1 * g (x / x_1) / x_1

State before:
case hs
𝕂 : 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
⊢ MeasurableSet (Ioi 0)
Tactic:
exact measurableSet_Ioi
State after:
no goals

State before:
case hf
𝕂 : 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
⊢ ∀ x_1 ∈ Ioi 0, 0 ≤ f x_1 * g (x / x_1) / x_1
Tactic:
intro y ypos
State after:
case hf
𝕂 : 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
y : ℝ
ypos : y ∈ Ioi 0
⊢ 0 ≤ f y * g (x / y) / y

State before:
case hf
𝕂 : 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
y : ℝ
ypos : y ∈ Ioi 0
⊢ 0 ≤ f y * g (x / y) / y
Tactic:
simp only [mem_Ioi] at ypos
State after:
case hf
𝕂 : 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
y : ℝ
ypos : 0 < y
⊢ 0 ≤ f y * g (x / y) / y

State before:
case hf
𝕂 : 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
y : ℝ
ypos : 0 < y
⊢ 0 ≤ f y * g (x / y) / y
Tactic:
have : 0 ≤ f y := f_nonneg _ ypos
State after:
case hf
𝕂 : 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
y : ℝ
ypos : 0 < y
this : 0 ≤ f y
⊢ 0 ≤ f y * g (x / y) / y

State before:
case hf
𝕂 : 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
y : ℝ
ypos : 0 < y
this : 0 ≤ f y
⊢ 0 ≤ f y * g (x / y) / y
Tactic:
have : 0 < x / y := by positivity
State after:
case hf
𝕂 : 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
y : ℝ
ypos : 0 < y
this✝ : 0 ≤ f y
this : 0 < x / y
⊢ 0 ≤ f y * g (x / y) / y

State before:
case hf
𝕂 : 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
y : ℝ
ypos : 0 < y
this✝ : 0 ≤ f y
this : 0 < x / y
⊢ 0 ≤ f y * g (x / y) / y
Tactic:
have : 0 ≤ g (x / y) := g_nonneg _ this
State after:
case hf
𝕂 : 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
y : ℝ
ypos : 0 < y
this✝¹ : 0 ≤ f y
this✝ : 0 < x / y
this : 0 ≤ g (x / y)
⊢ 0 ≤ f y * g (x / y) / y

State before:
case hf
𝕂 : 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
y : ℝ
ypos : 0 < y
this✝¹ : 0 ≤ f y
this✝ : 0 < x / y
this : 0 ≤ g (x / y)
⊢ 0 ≤ f y * g (x / y) / y
Tactic:
positivity
State after:
no goals

State before:
𝕂 : 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
y : ℝ
ypos : 0 < y
this : 0 ≤ f y
⊢ 0 < x / y
Tactic:
positivity
State after:
no goals