α : Type u_2
β : Type ?u.20828
m : MeasurableSpace α
μ ν : Measure α
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
s : Set α
hs : MeasurableSet s
⊢ ↑{ measureOf' := fun s => if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0,
          empty' := (_ : (if MeasurableSet ∅ then ∫ (x : α) in ∅, f x ∂μ else 0) = 0),
          not_measurable' :=
            (_ : ∀ (s : Set α), ¬MeasurableSet s → (if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0) = 0),
          m_iUnion' :=
            (_ :
              ∀ (s : ℕ → Set α),
                (∀ (i : ℕ), MeasurableSet (s i)) →
                  Pairwise (Disjoint on s) →
                    HasSum (fun i => (fun s => if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0) (s i))
                      ((fun s => if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0) (⋃ (i : ℕ), s i))) }
      s =
    ∫ (x : α) in s, f x ∂μ
α : Type u_2
β : Type ?u.20828
m : MeasurableSpace α
μ ν : Measure α
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
s : Set α
hs : MeasurableSet s
⊢ ↑(withDensityᵥ μ f) s = ∫ (x : α) in s, f x ∂μ
rw [withDensityᵥ, dif_pos hf]
no goals
α : Type u_2
β : Type ?u.20828
m : MeasurableSpace α
μ ν : Measure α
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
s : Set α
hs : MeasurableSet s
⊢ ↑{ measureOf' := fun s => if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0,
          empty' := (_ : (if MeasurableSet ∅ then ∫ (x : α) in ∅, f x ∂μ else 0) = 0),
          not_measurable' :=
            (_ : ∀ (s : Set α), ¬MeasurableSet s → (if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0) = 0),
          m_iUnion' :=
            (_ :
              ∀ (s : ℕ → Set α),
                (∀ (i : ℕ), MeasurableSet (s i)) →
                  Pairwise (Disjoint on s) →
                    HasSum (fun i => (fun s => if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0) (s i))
                      ((fun s => if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0) (⋃ (i : ℕ), s i))) }
      s =
    ∫ (x : α) in s, f x ∂μ
exact dif_pos hs