α : Type u_1
β : Type ?u.162140
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.162159
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ
hfi : Integrable f
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
⊢ withDensityᵥ μ f =
    toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (f x)) -
      toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (-f x))
α : Type u_1
β : Type ?u.162140
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.162159
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ
hfi : Integrable f
⊢ withDensityᵥ μ f =
    toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (f x)) -
      toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (-f x))
haveI := isFiniteMeasure_withDensity_ofReal hfi.2
α : Type u_1
β : Type ?u.162140
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.162159
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ
hfi : Integrable f
this✝ : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal ((-f) x))
⊢ withDensityᵥ μ f =
    toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (f x)) -
      toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (-f x))
α : Type u_1
β : Type ?u.162140
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.162159
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ
hfi : Integrable f
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
⊢ withDensityᵥ μ f =
    toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (f x)) -
      toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (-f x))
haveI := isFiniteMeasure_withDensity_ofReal hfi.neg.2
case h
α : Type u_1
β : Type ?u.162140
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.162159
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ
hfi : Integrable f
this✝ : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal ((-f) x))
i : Set α
⊢ MeasurableSet i →
    ↑(withDensityᵥ μ f) i =
      ↑(toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (f x)) -
            toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (-f x)))
        i
α : Type u_1
β : Type ?u.162140
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.162159
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ
hfi : Integrable f
this✝ : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal ((-f) x))
⊢ withDensityᵥ μ f =
    toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (f x)) -
      toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (-f x))
ext i
case h
α : Type u_1
β : Type ?u.162140
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.162159
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ
hfi : Integrable f
this✝ : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
⊢ ↑(withDensityᵥ μ f) i =
    ↑(toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (f x)) -
          toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (-f x)))
      i
case h
α : Type u_1
β : Type ?u.162140
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.162159
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ
hfi : Integrable f
this✝ : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal ((-f) x))
i : Set α
⊢ MeasurableSet i →
    ↑(withDensityᵥ μ f) i =
      ↑(toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (f x)) -
            toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (-f x)))
        i
intro hi
no goals
case h
α : Type u_1
β : Type ?u.162140
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.162159
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ
hfi : Integrable f
this✝ : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
⊢ ↑(withDensityᵥ μ f) i =
    ↑(toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (f x)) -
          toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (-f x)))
      i
rw [withDensityᵥ_apply hfi hi,
  integral_eq_lintegral_pos_part_sub_lintegral_neg_part hfi.integrableOn,
  VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
  toSignedMeasure_apply_measurable hi, withDensity_apply _ hi, withDensity_apply _ hi]