case inl
α : Type u_1
E : Type u_2
F : Type ?u.190069
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
f : α → E
hμ : μ = 0
⊢ (ENNReal.toReal (↑↑μ univ) • ⨍ (x : α), f x ∂μ) = ∫ (x : α), f x ∂μ

case inr
α : Type u_1
E : Type u_2
F : Type ?u.190069
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
f : α → E
hμ : μ ≠ 0
⊢ (ENNReal.toReal (↑↑μ univ) • ⨍ (x : α), f x ∂μ) = ∫ (x : α), f x ∂μ
α : Type u_1
E : Type u_2
F : Type ?u.190069
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
f : α → E
⊢ (ENNReal.toReal (↑↑μ univ) • ⨍ (x : α), f x ∂μ) = ∫ (x : α), f x ∂μ
cases' eq_or_ne μ 0 with hμ hμ
no goals
case inl
α : Type u_1
E : Type u_2
F : Type ?u.190069
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
f : α → E
hμ : μ = 0
⊢ (ENNReal.toReal (↑↑μ univ) • ⨍ (x : α), f x ∂μ) = ∫ (x : α), f x ∂μ
rw [hμ, integral_zero_measure, average_zero_measure, smul_zero]
case inr.hc
α : Type u_1
E : Type u_2
F : Type ?u.190069
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
f : α → E
hμ : μ ≠ 0
⊢ ENNReal.toReal (↑↑μ univ) ≠ 0
case inr
α : Type u_1
E : Type u_2
F : Type ?u.190069
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
f : α → E
hμ : μ ≠ 0
⊢ (ENNReal.toReal (↑↑μ univ) • ⨍ (x : α), f x ∂μ) = ∫ (x : α), f x ∂μ
rw [average_eq, smul_inv_smul₀]
case inr.hc
α : Type u_1
E : Type u_2
F : Type ?u.190069
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
f : α → E
hμ : μ ≠ 0
⊢ ↑↑μ univ ≠ 0
case inr.hc
α : Type u_1
E : Type u_2
F : Type ?u.190069
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
f : α → E
hμ : μ ≠ 0
⊢ ENNReal.toReal (↑↑μ univ) ≠ 0
refine' (ENNReal.toReal_pos _ <| measure_ne_top _ _).ne'
no goals
case inr.hc
α : Type u_1
E : Type u_2
F : Type ?u.190069
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
f : α → E
hμ : μ ≠ 0
⊢ ↑↑μ univ ≠ 0
rwa [Ne.def, measure_univ_eq_zero]