α : Type u_1
β : Type ?u.1031427
γ : Type ?u.1031430
δ : Type ?u.1031433
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ
this : (fun x => g x * ENNReal.toReal (f x)) = fun x => ENNReal.toReal (f x) • g x
⊢ Integrable g ↔ Integrable fun x => g x * ENNReal.toReal (f x)
α : Type u_1
β : Type ?u.1031427
γ : Type ?u.1031430
δ : Type ?u.1031433
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ
⊢ Integrable g ↔ Integrable fun x => g x * ENNReal.toReal (f x)
have : (fun x => g x * (f x).toReal) = fun x => (f x).toReal • g x := by simp [mul_comm]
α : Type u_1
β : Type ?u.1031427
γ : Type ?u.1031430
δ : Type ?u.1031433
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ
this : (fun x => g x * ENNReal.toReal (f x)) = fun x => ENNReal.toReal (f x) • g x
⊢ Integrable g ↔ Integrable fun x => ENNReal.toReal (f x) • g x
α : Type u_1
β : Type ?u.1031427
γ : Type ?u.1031430
δ : Type ?u.1031433
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ
this : (fun x => g x * ENNReal.toReal (f x)) = fun x => ENNReal.toReal (f x) • g x
⊢ Integrable g ↔ Integrable fun x => g x * ENNReal.toReal (f x)
rw [this]
no goals
α : Type u_1
β : Type ?u.1031427
γ : Type ?u.1031430
δ : Type ?u.1031433
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ
this : (fun x => g x * ENNReal.toReal (f x)) = fun x => ENNReal.toReal (f x) • g x
⊢ Integrable g ↔ Integrable fun x => ENNReal.toReal (f x) • g x
exact integrable_withDensity_iff_integrable_smul' hf hflt
no goals
α : Type u_1
β : Type ?u.1031427
γ : Type ?u.1031430
δ : Type ?u.1031433
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ
⊢ (fun x => g x * ENNReal.toReal (f x)) = fun x => ENNReal.toReal (f x) • g x
simp [mul_comm]