ι : Type ?u.3012325
𝕜 : Type ?u.3012328
E : Type u_1
F : Type ?u.3012334
A : Type ?u.3012337
inst✝ : NormedAddCommGroup E
f✝ : ℝ → E
a✝ b✝ c d : ℝ
μ✝ ν : MeasureTheory.Measure ℝ
f : ℝ → E
μ : MeasureTheory.Measure ℝ
a b : ℝ
hf : AEStronglyMeasurable f (Measure.restrict μ (Ι a b))
⊢ (Integrable fun t => ‖f t‖) ↔ Integrable f
ι : Type ?u.3012325
𝕜 : Type ?u.3012328
E : Type u_1
F : Type ?u.3012334
A : Type ?u.3012337
inst✝ : NormedAddCommGroup E
f✝ : ℝ → E
a✝ b✝ c d : ℝ
μ✝ ν : MeasureTheory.Measure ℝ
f : ℝ → E
μ : MeasureTheory.Measure ℝ
a b : ℝ
hf : AEStronglyMeasurable f (Measure.restrict μ (Ι a b))
⊢ IntervalIntegrable (fun t => ‖f t‖) μ a b ↔ IntervalIntegrable f μ a b
simp_rw [intervalIntegrable_iff, IntegrableOn]
no goals
ι : Type ?u.3012325
𝕜 : Type ?u.3012328
E : Type u_1
F : Type ?u.3012334
A : Type ?u.3012337
inst✝ : NormedAddCommGroup E
f✝ : ℝ → E
a✝ b✝ c d : ℝ
μ✝ ν : MeasureTheory.Measure ℝ
f : ℝ → E
μ : MeasureTheory.Measure ℝ
a b : ℝ
hf : AEStronglyMeasurable f (Measure.restrict μ (Ι a b))
⊢ (Integrable fun t => ‖f t‖) ↔ Integrable f
exact integrable_norm_iff hf