α : Type u_1
β : Type ?u.1258403
γ : Type ?u.1258406
δ : Type ?u.1258409
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_2
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f
hf : StronglyMeasurable f
⊢ HasFiniteIntegral f
α : Type u_1
β : Type ?u.1258403
γ : Type ?u.1258406
δ : Type ?u.1258409
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_2
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f
hf : StronglyMeasurable f
⊢ Integrable f
refine' ⟨hf.aestronglyMeasurable, _⟩
α : Type u_1
β : Type ?u.1258403
γ : Type ?u.1258406
δ : Type ?u.1258409
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_2
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f
hf : StronglyMeasurable f
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ') < ⊤

α : Type u_1
β : Type ?u.1258403
γ : Type ?u.1258406
δ : Type ?u.1258409
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_2
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f
hf : StronglyMeasurable f
⊢ Measurable fun a => ↑‖f a‖₊
α : Type u_1
β : Type ?u.1258403
γ : Type ?u.1258406
δ : Type ?u.1258409
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_2
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f
hf : StronglyMeasurable f
⊢ HasFiniteIntegral f
rw [HasFiniteIntegral, lintegral_trim hm _]
no goals
α : Type u_1
β : Type ?u.1258403
γ : Type ?u.1258406
δ : Type ?u.1258409
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_2
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f
hf : StronglyMeasurable f
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ') < ⊤
exact hf_int.2
no goals
α : Type u_1
β : Type ?u.1258403
γ : Type ?u.1258406
δ : Type ?u.1258409
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_2
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f
hf : StronglyMeasurable f
⊢ Measurable fun a => ↑‖f a‖₊
exact @StronglyMeasurable.ennnorm _ m _ _ f hf