α : Type u_1
β : Type ?u.164970
m✝ : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f
j : Set α
hj₁ : MeasurableSet j
hj₂ : ↑(toENNRealVectorMeasure (Measure.trim μ hm)) j = 0
⊢ ↑(VectorMeasure.trim (withDensityᵥ μ f) hm) j = 0
α : Type u_1
β : Type ?u.164970
m✝ : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f
⊢ VectorMeasure.trim (withDensityᵥ μ f) hm ≪ᵥ toENNRealVectorMeasure (Measure.trim μ hm)
refine' VectorMeasure.AbsolutelyContinuous.mk fun j hj₁ hj₂ => _
α : Type u_1
β : Type ?u.164970
m✝ : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f
j : Set α
hj₁ : MeasurableSet j
hj₂ : ↑↑μ j = 0
⊢ ↑(VectorMeasure.trim (withDensityᵥ μ f) hm) j = 0
α : Type u_1
β : Type ?u.164970
m✝ : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f
j : Set α
hj₁ : MeasurableSet j
hj₂ : ↑(toENNRealVectorMeasure (Measure.trim μ hm)) j = 0
⊢ ↑(VectorMeasure.trim (withDensityᵥ μ f) hm) j = 0
rw [Measure.toENNRealVectorMeasure_apply_measurable hj₁, trim_measurableSet_eq hm hj₁] at hj₂
α : Type u_1
β : Type ?u.164970
m✝ : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f
j : Set α
hj₁ : MeasurableSet j
hj₂ : ↑↑μ j = 0
⊢ (∫ (x : α) in j, f x ∂μ) = 0
α : Type u_1
β : Type ?u.164970
m✝ : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f
j : Set α
hj₁ : MeasurableSet j
hj₂ : ↑↑μ j = 0
⊢ ↑(VectorMeasure.trim (withDensityᵥ μ f) hm) j = 0
rw [VectorMeasure.trim_measurableSet_eq hm hj₁, withDensityᵥ_apply hfi (hm _ hj₁)]
no goals
α : Type u_1
β : Type ?u.164970
m✝ : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f
j : Set α
hj₁ : MeasurableSet j
hj₂ : ↑↑μ j = 0
⊢ (∫ (x : α) in j, f x ∂μ) = 0
simp only [Measure.restrict_eq_zero.mpr hj₂, integral_zero_measure]