α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ¬∃ t, MeasurableSet t ∧ ↑↑μ t ≠ 0 ∧ ↑↑μ (tᶜ) ≠ 0 ∧ (⨍ (x : α) in t, f x ∂μ) ≠ ⨍ (x : α) in tᶜ, f x ∂μ
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ)
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨
    ∃ t, MeasurableSet t ∧ ↑↑μ t ≠ 0 ∧ ↑↑μ (tᶜ) ≠ 0 ∧ (⨍ (x : α) in t, f x ∂μ) ≠ ⨍ (x : α) in tᶜ, f x ∂μ
refine' or_iff_not_imp_right.mpr fun H => _
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ)
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ¬∃ t, MeasurableSet t ∧ ↑↑μ t ≠ 0 ∧ ↑↑μ (tᶜ) ≠ 0 ∧ (⨍ (x : α) in t, f x ∂μ) ≠ ⨍ (x : α) in tᶜ, f x ∂μ
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ)
push_neg at H
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t✝ : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
ht' : ↑↑μ t < ⊤
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in t, const α (⨍ (x : α), f x ∂μ) x ∂μ
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ)
refine' hfi.ae_eq_of_forall_set_integral_eq _ _ (integrable_const _) fun t ht ht' => _
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t✝ : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in t, const α (⨍ (x : α), f x ∂μ) x ∂μ
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t✝ : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
ht' : ↑↑μ t < ⊤
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in t, const α (⨍ (x : α), f x ∂μ) x ∂μ
clear ht'
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t✝ : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
⊢ (∫ (x : α) in t, f x ∂μ) = ENNReal.toReal (↑↑μ t) • ⨍ (x : α), f x ∂μ
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t✝ : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in t, const α (⨍ (x : α), f x ∂μ) x ∂μ
simp only [const_apply, set_integral_const]
case pos
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t✝ : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : ↑↑μ t = 0
⊢ (∫ (x : α) in t, f x ∂μ) = ENNReal.toReal (↑↑μ t) • ⨍ (x : α), f x ∂μ

case neg
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t✝ : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : ¬↑↑μ t = 0
⊢ (∫ (x : α) in t, f x ∂μ) = ENNReal.toReal (↑↑μ t) • ⨍ (x : α), f x ∂μ
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t✝ : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
⊢ (∫ (x : α) in t, f x ∂μ) = ENNReal.toReal (↑↑μ t) • ⨍ (x : α), f x ∂μ
by_cases h₀ : μ t = 0
case pos
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t✝ : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : ¬↑↑μ t = 0
h₀' : ↑↑μ (tᶜ) = 0
⊢ (∫ (x : α) in t, f x ∂μ) = ENNReal.toReal (↑↑μ t) • ⨍ (x : α), f x ∂μ

case neg
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t✝ : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : ¬↑↑μ t = 0
h₀' : ¬↑↑μ (tᶜ) = 0
⊢ (∫ (x : α) in t, f x ∂μ) = ENNReal.toReal (↑↑μ t) • ⨍ (x : α), f x ∂μ
case neg
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t✝ : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : ¬↑↑μ t = 0
⊢ (∫ (x : α) in t, f x ∂μ) = ENNReal.toReal (↑↑μ t) • ⨍ (x : α), f x ∂μ
by_cases h₀' : μ (tᶜ) = 0
case neg
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t✝ : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : ¬↑↑μ t = 0
h₀' : ¬↑↑μ (tᶜ) = 0
this : (⨍ (x : α), f x ∂μ) ∈ openSegment ℝ (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
⊢ (∫ (x : α) in t, f x ∂μ) = ENNReal.toReal (↑↑μ t) • ⨍ (x : α), f x ∂μ
case neg
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t✝ : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : ¬↑↑μ t = 0
h₀' : ¬↑↑μ (tᶜ) = 0
⊢ (∫ (x : α) in t, f x ∂μ) = ENNReal.toReal (↑↑μ t) • ⨍ (x : α), f x ∂μ
have := average_mem_openSegment_compl_self ht.nullMeasurableSet h₀ h₀' hfi
case neg
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t✝ : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : ¬↑↑μ t = 0
h₀' : ¬↑↑μ (tᶜ) = 0
this : (⨍ (x : α), f x ∂μ) = ⨍ (x : α) in t, f x ∂μ
⊢ (∫ (x : α) in t, f x ∂μ) = ENNReal.toReal (↑↑μ t) • ⨍ (x : α), f x ∂μ
case neg
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t✝ : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : ¬↑↑μ t = 0
h₀' : ¬↑↑μ (tᶜ) = 0
this : (⨍ (x : α), f x ∂μ) ∈ openSegment ℝ (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
⊢ (∫ (x : α) in t, f x ∂μ) = ENNReal.toReal (↑↑μ t) • ⨍ (x : α), f x ∂μ
rw [← H t ht h₀ h₀', openSegment_same, mem_singleton_iff] at this
no goals
case neg
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t✝ : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : ¬↑↑μ t = 0
h₀' : ¬↑↑μ (tᶜ) = 0
this : (⨍ (x : α), f x ∂μ) = ⨍ (x : α) in t, f x ∂μ
⊢ (∫ (x : α) in t, f x ∂μ) = ENNReal.toReal (↑↑μ t) • ⨍ (x : α), f x ∂μ
rw [this, measure_smul_set_average _ (measure_ne_top μ _)]
no goals
case pos
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t✝ : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : ↑↑μ t = 0
⊢ (∫ (x : α) in t, f x ∂μ) = ENNReal.toReal (↑↑μ t) • ⨍ (x : α), f x ∂μ
rw [restrict_eq_zero.2 h₀, integral_zero_measure, h₀, ENNReal.zero_toReal, zero_smul]
case pos
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t✝ : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : ¬↑↑μ t = 0
h₀' : t =ᶠ[ae μ] univ
⊢ (∫ (x : α) in t, f x ∂μ) = ENNReal.toReal (↑↑μ t) • ⨍ (x : α), f x ∂μ
case pos
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t✝ : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : ¬↑↑μ t = 0
h₀' : ↑↑μ (tᶜ) = 0
⊢ (∫ (x : α) in t, f x ∂μ) = ENNReal.toReal (↑↑μ t) • ⨍ (x : α), f x ∂μ
rw [← ae_eq_univ] at h₀'
no goals
case pos
α : Type u_1
E : Type u_2
F : Type ?u.1822542
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t✝ : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsFiniteMeasure μ
hfi : Integrable f
H : ∀ (t : Set α), MeasurableSet t → ↑↑μ t ≠ 0 → ↑↑μ (tᶜ) ≠ 0 → (⨍ (x : α) in t, f x ∂μ) = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : ¬↑↑μ t = 0
h₀' : t =ᶠ[ae μ] univ
⊢ (∫ (x : α) in t, f x ∂μ) = ENNReal.toReal (↑↑μ t) • ⨍ (x : α), f x ∂μ
rw [restrict_congr_set h₀', restrict_univ, measure_congr h₀', measure_smul_average]