α : Type u_1
β : Type ?u.1021419
γ : Type ?u.1021422
δ : Type ?u.1021425
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → E
⊢ (Integrable fun x => ENNReal.toNNReal (f x) • g x) ↔ Integrable fun x => ENNReal.toReal (f x) • g x

case hf
α : Type u_1
β : Type ?u.1021419
γ : Type ?u.1021422
δ : Type ?u.1021425
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → E
⊢ Measurable fun x => ENNReal.toNNReal (f x)
α : Type u_1
β : Type ?u.1021419
γ : Type ?u.1021422
δ : Type ?u.1021425
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → E
⊢ Integrable g ↔ Integrable fun x => ENNReal.toReal (f x) • g x
rw [← withDensity_congr_ae (coe_toNNReal_ae_eq hflt),
  integrable_withDensity_iff_integrable_smul]
no goals
α : Type u_1
β : Type ?u.1021419
γ : Type ?u.1021422
δ : Type ?u.1021425
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → E
⊢ (Integrable fun x => ENNReal.toNNReal (f x) • g x) ↔ Integrable fun x => ENNReal.toReal (f x) • g x
rfl
no goals
case hf
α : Type u_1
β : Type ?u.1021419
γ : Type ?u.1021422
δ : Type ?u.1021425
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → E
⊢ Measurable fun x => ENNReal.toNNReal (f x)
exact hf.ennreal_toNNReal