apply setIntegral_congr_ae measurableSet_Ioi
case h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : ℂ
h : s.re > 0
⊢ 𝓜 (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) s = mellin ((Ioc 0 1).indicator fun x => 1) s
case h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : ℂ
h : s.re > 0
⊢ ∀ᵐ (x : ℝ),
    x ∈ Ioi 0 →
      (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) x * ↑x ^ (s - 1) = ↑x ^ (s - 1) • (Ioc 0 1).indicator (fun x => 1) x