Ω : Type u_2
inst✝³ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
nonzero : μ ≠ 0
f : Ω → E
⊢ (∫ (x : Ω), f x ∂(↑↑↑μ univ)⁻¹ • ↑μ) = ∫ (ω : Ω), f ω ∂↑((mass μ)⁻¹ • μ)
Ω : Type u_2
inst✝³ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
nonzero : μ ≠ 0
f : Ω → E
⊢ average (↑μ) f = ∫ (ω : Ω), f ω ∂↑(normalize μ)
rw [μ.toMeasure_normalize_eq_of_nonzero nonzero, average]
case e_μ.e_a
Ω : Type u_2
inst✝³ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
nonzero : μ ≠ 0
f : Ω → E
⊢ (↑↑↑μ univ)⁻¹ = ↑ENNReal.ofNNRealHom (mass μ)⁻¹
Ω : Type u_2
inst✝³ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
nonzero : μ ≠ 0
f : Ω → E
⊢ (∫ (x : Ω), f x ∂(↑↑↑μ univ)⁻¹ • ↑μ) = ∫ (ω : Ω), f ω ∂↑((mass μ)⁻¹ • μ)
congr
no goals
case e_μ.e_a
Ω : Type u_2
inst✝³ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
nonzero : μ ≠ 0
f : Ω → E
⊢ (↑↑↑μ univ)⁻¹ = ↑ENNReal.ofNNRealHom (mass μ)⁻¹
simp only [RingHom.toFun_eq_coe, ENNReal.coe_ofNNRealHom,
  ENNReal.coe_inv (μ.mass_nonzero_iff.mpr nonzero), ennreal_mass]