case pos
α : Type u_1
β : Type ?u.26390
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
⊢ withDensityᵥ μ (-f) = -withDensityᵥ μ f

case neg
α : Type u_1
β : Type ?u.26390
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : ¬Integrable f
⊢ withDensityᵥ μ (-f) = -withDensityᵥ μ f
α : Type u_1
β : Type ?u.26390
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
⊢ withDensityᵥ μ (-f) = -withDensityᵥ μ f
by_cases hf : Integrable f μ
case pos.h
α : Type u_1
β : Type ?u.26390
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
i : Set α
hi : MeasurableSet i
⊢ ↑(withDensityᵥ μ (-f)) i = ↑(-withDensityᵥ μ f) i
case pos
α : Type u_1
β : Type ?u.26390
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
⊢ withDensityᵥ μ (-f) = -withDensityᵥ μ f
ext1 i hi
case pos.h
α : Type u_1
β : Type ?u.26390
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
i : Set α
hi : MeasurableSet i
⊢ (∫ (x : α) in i, (-f) x ∂μ) = ∫ (a : α) in i, -f a ∂μ
case pos.h
α : Type u_1
β : Type ?u.26390
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
i : Set α
hi : MeasurableSet i
⊢ ↑(withDensityᵥ μ (-f)) i = ↑(-withDensityᵥ μ f) i
rw [VectorMeasure.neg_apply, withDensityᵥ_apply hf hi, ← integral_neg,
  withDensityᵥ_apply hf.neg hi]
no goals
case pos.h
α : Type u_1
β : Type ?u.26390
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
i : Set α
hi : MeasurableSet i
⊢ (∫ (x : α) in i, (-f) x ∂μ) = ∫ (a : α) in i, -f a ∂μ
rfl
case neg.hnc
α : Type u_1
β : Type ?u.26390
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : ¬Integrable f
⊢ ¬Integrable (-f)
case neg
α : Type u_1
β : Type ?u.26390
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : ¬Integrable f
⊢ withDensityᵥ μ (-f) = -withDensityᵥ μ f
rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg, neg_zero]
no goals
case neg.hnc
α : Type u_1
β : Type ?u.26390
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : ¬Integrable f
⊢ ¬Integrable (-f)
rwa [integrable_neg_iff]