α : Type u_1
β : Type ?u.1023730
γ : Type ?u.1023733
δ : Type ?u.1023736
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
⊢ (fun x => ↑(f x)) =ᵐ[μ] fun x => ↑(AEMeasurable.mk f hf x)
α : Type u_1
β : Type ?u.1023730
γ : Type ?u.1023733
δ : Type ?u.1023736
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
⊢ Integrable g ↔ Integrable g
suffices (fun x => (f x : ℝ≥0∞)) =ᵐ[μ] (fun x => (hf.mk f x : ℝ≥0)) by
  rw [withDensity_congr_ae this]
case h
α : Type u_1
β : Type ?u.1023730
γ : Type ?u.1023733
δ : Type ?u.1023736
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ ↑(f x) = ↑(AEMeasurable.mk f hf x)
α : Type u_1
β : Type ?u.1023730
γ : Type ?u.1023733
δ : Type ?u.1023736
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
⊢ (fun x => ↑(f x)) =ᵐ[μ] fun x => ↑(AEMeasurable.mk f hf x)
filter_upwards [hf.ae_eq_mk] with x hx
no goals
case h
α : Type u_1
β : Type ?u.1023730
γ : Type ?u.1023733
δ : Type ?u.1023736
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ ↑(f x) = ↑(AEMeasurable.mk f hf x)
simp [hx]
no goals
α : Type u_1
β : Type ?u.1023730
γ : Type ?u.1023733
δ : Type ?u.1023736
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
this : (fun x => ↑(f x)) =ᵐ[μ] fun x => ↑(AEMeasurable.mk f hf x)
⊢ Integrable g ↔ Integrable g
rw [withDensity_congr_ae this]
case h
α : Type u_1
β : Type ?u.1023730
γ : Type ?u.1023733
δ : Type ?u.1023736
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
⊢ (fun x => ↑(AEMeasurable.mk f hf x) • g x) =ᵐ[μ] fun x => ↑(f x) • g x
α : Type u_1
β : Type ?u.1023730
γ : Type ?u.1023733
δ : Type ?u.1023736
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
⊢ (Integrable fun x => ↑(AEMeasurable.mk f hf x) • g x) ↔ Integrable fun x => ↑(f x) • g x
apply integrable_congr
case h
α : Type u_1
β : Type ?u.1023730
γ : Type ?u.1023733
δ : Type ?u.1023736
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ ↑(AEMeasurable.mk f hf x) • g x = ↑(f x) • g x
case h
α : Type u_1
β : Type ?u.1023730
γ : Type ?u.1023733
δ : Type ?u.1023736
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
⊢ (fun x => ↑(AEMeasurable.mk f hf x) • g x) =ᵐ[μ] fun x => ↑(f x) • g x
filter_upwards [hf.ae_eq_mk] with x hx
no goals
case h
α : Type u_1
β : Type ?u.1023730
γ : Type ?u.1023733
δ : Type ?u.1023736
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ ↑(AEMeasurable.mk f hf x) • g x = ↑(f x) • g x
simp [hx]