α : Type u_1
E : Type u_2
F : Type ?u.1491744
𝕜 : Type ?u.1491747
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1494438
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
⊢ (∫ (x : α), f x ∂if a ∈ s then Measure.dirac a else 0) = if a ∈ s then f a else 0
α : Type u_1
E : Type u_2
F : Type ?u.1491744
𝕜 : Type ?u.1491747
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1494438
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
⊢ (∫ (x : α) in s, f x ∂Measure.dirac a) = if a ∈ s then f a else 0
rw [restrict_dirac' hs]
case inl
α : Type u_1
E : Type u_2
F : Type ?u.1491744
𝕜 : Type ?u.1491747
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1494438
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
h✝ : a ∈ s
⊢ (∫ (x : α), f x ∂Measure.dirac a) = f a

case inr
α : Type u_1
E : Type u_2
F : Type ?u.1491744
𝕜 : Type ?u.1491747
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1494438
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
h✝ : ¬a ∈ s
⊢ (∫ (x : α), f x ∂0) = 0
α : Type u_1
E : Type u_2
F : Type ?u.1491744
𝕜 : Type ?u.1491747
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1494438
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
⊢ (∫ (x : α), f x ∂if a ∈ s then Measure.dirac a else 0) = if a ∈ s then f a else 0
split_ifs
no goals
case inl
α : Type u_1
E : Type u_2
F : Type ?u.1491744
𝕜 : Type ?u.1491747
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1494438
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
h✝ : a ∈ s
⊢ (∫ (x : α), f x ∂Measure.dirac a) = f a
exact integral_dirac' _ _ hf
no goals
case inr
α : Type u_1
E : Type u_2
F : Type ?u.1491744
𝕜 : Type ?u.1491747
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1494438
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
h✝ : ¬a ∈ s
⊢ (∫ (x : α), f x ∂0) = 0
exact integral_zero_measure _