have l2 : Integrable (indicator (Ioi 0) (fun x : ℝ => Ψ x)) := h1.indicator measurableSet_Ioi
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
⊢ (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y = 0
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
⊢ (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y = 0