by_cases h : y ≤ 1
case calc_2.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
⊢ (if y ∈ Ioc 0 1 then Ψ ((x / y) ^ (1 / ε)) / ε / y else 0) ≤ Ψ ((x / y) ^ (1 / ε)) / ε / y
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : y ≤ 1
⊢ (if y ∈ Ioc 0 1 then Ψ ((x / y) ^ (1 / ε)) / ε / y else 0) ≤ Ψ ((x / y) ^ (1 / ε)) / ε / y

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : ¬y ≤ 1
⊢ (if y ∈ Ioc 0 1 then Ψ ((x / y) ^ (1 / ε)) / ε / y else 0) ≤ Ψ ((x / y) ^ (1 / ε)) / ε / y