α : Type u_1
β : Type ?u.1070083
γ : Type ?u.1070086
δ : Type ?u.1070089
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hfm : AEMeasurable f
hfi : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
⊢ AEStronglyMeasurable (fun x => ENNReal.toReal (f x)) μ ∧ (∫⁻ (x : α), ↑‖ENNReal.toReal (f x)‖₊ ∂μ) < ⊤
α : Type u_1
β : Type ?u.1070083
γ : Type ?u.1070086
δ : Type ?u.1070089
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hfm : AEMeasurable f
hfi : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
⊢ Memℒp (fun x => ENNReal.toReal (f x)) 1
rw [Memℒp, snorm_one_eq_lintegral_nnnorm]
no goals
α : Type u_1
β : Type ?u.1070083
γ : Type ?u.1070086
δ : Type ?u.1070089
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hfm : AEMeasurable f
hfi : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
⊢ AEStronglyMeasurable (fun x => ENNReal.toReal (f x)) μ ∧ (∫⁻ (x : α), ↑‖ENNReal.toReal (f x)‖₊ ∂μ) < ⊤
exact
  ⟨(AEMeasurable.ennreal_toReal hfm).aestronglyMeasurable,
    hasFiniteIntegral_toReal_of_lintegral_ne_top hfi⟩