case pos
α : Type u_1
β : Type ?u.59120
m : MeasurableSpace α
μ✝ ν : Measure α
E : Type ?u.59139
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
μ : Measure α
f : α → ℝ
hf : Integrable f
⊢ withDensityᵥ μ f ≪ᵥ toENNRealVectorMeasure μ

case neg
α : Type u_1
β : Type ?u.59120
m : MeasurableSpace α
μ✝ ν : Measure α
E : Type ?u.59139
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
μ : Measure α
f : α → ℝ
hf : ¬Integrable f
⊢ withDensityᵥ μ f ≪ᵥ toENNRealVectorMeasure μ
α : Type u_1
β : Type ?u.59120
m : MeasurableSpace α
μ✝ ν : Measure α
E : Type ?u.59139
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
μ : Measure α
f : α → ℝ
⊢ withDensityᵥ μ f ≪ᵥ toENNRealVectorMeasure μ
by_cases hf : Integrable f μ
case pos
α : Type u_1
β : Type ?u.59120
m : MeasurableSpace α
μ✝ ν : Measure α
E : Type ?u.59139
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
μ : Measure α
f : α → ℝ
hf : Integrable f
i : Set α
hi₁ : MeasurableSet i
hi₂ : ↑(toENNRealVectorMeasure μ) i = 0
⊢ ↑(withDensityᵥ μ f) i = 0
case pos
α : Type u_1
β : Type ?u.59120
m : MeasurableSpace α
μ✝ ν : Measure α
E : Type ?u.59139
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
μ : Measure α
f : α → ℝ
hf : Integrable f
⊢ withDensityᵥ μ f ≪ᵥ toENNRealVectorMeasure μ
refine' VectorMeasure.AbsolutelyContinuous.mk fun i hi₁ hi₂ => _
case pos
α : Type u_1
β : Type ?u.59120
m : MeasurableSpace α
μ✝ ν : Measure α
E : Type ?u.59139
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
μ : Measure α
f : α → ℝ
hf : Integrable f
i : Set α
hi₁ : MeasurableSet i
hi₂ : ↑↑μ i = 0
⊢ ↑(withDensityᵥ μ f) i = 0
case pos
α : Type u_1
β : Type ?u.59120
m : MeasurableSpace α
μ✝ ν : Measure α
E : Type ?u.59139
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
μ : Measure α
f : α → ℝ
hf : Integrable f
i : Set α
hi₁ : MeasurableSet i
hi₂ : ↑(toENNRealVectorMeasure μ) i = 0
⊢ ↑(withDensityᵥ μ f) i = 0
rw [toENNRealVectorMeasure_apply_measurable hi₁] at hi₂
no goals
case pos
α : Type u_1
β : Type ?u.59120
m : MeasurableSpace α
μ✝ ν : Measure α
E : Type ?u.59139
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
μ : Measure α
f : α → ℝ
hf : Integrable f
i : Set α
hi₁ : MeasurableSet i
hi₂ : ↑↑μ i = 0
⊢ ↑(withDensityᵥ μ f) i = 0
rw [withDensityᵥ_apply hf hi₁, Measure.restrict_zero_set hi₂, integral_zero_measure]
case neg
α : Type u_1
β : Type ?u.59120
m : MeasurableSpace α
μ✝ ν : Measure α
E : Type ?u.59139
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
μ : Measure α
f : α → ℝ
hf : ¬Integrable f
⊢ 0 ≪ᵥ toENNRealVectorMeasure μ
case neg
α : Type u_1
β : Type ?u.59120
m : MeasurableSpace α
μ✝ ν : Measure α
E : Type ?u.59139
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
μ : Measure α
f : α → ℝ
hf : ¬Integrable f
⊢ withDensityᵥ μ f ≪ᵥ toENNRealVectorMeasure μ
rw [withDensityᵥ, dif_neg hf]
no goals
case neg
α : Type u_1
β : Type ?u.59120
m : MeasurableSpace α
μ✝ ν : Measure α
E : Type ?u.59139
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
μ : Measure α
f : α → ℝ
hf : ¬Integrable f
⊢ 0 ≪ᵥ toENNRealVectorMeasure μ
exact VectorMeasure.AbsolutelyContinuous.zero _