α : Type u_1
β : Type ?u.1692646
γ : Type ?u.1692649
δ : Type ?u.1692652
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
⊢ (∫⁻ (x : α), f x ∂if a ∈ s then dirac a else 0) = if a ∈ s then f a else 0
α : Type u_1
β : Type ?u.1692646
γ : Type ?u.1692649
δ : Type ?u.1692652
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
⊢ (∫⁻ (x : α) in s, f x ∂dirac a) = if a ∈ s then f a else 0
rw [restrict_dirac]
case inl
α : Type u_1
β : Type ?u.1692646
γ : Type ?u.1692649
δ : Type ?u.1692652
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
h✝ : a ∈ s
⊢ (∫⁻ (x : α), f x ∂dirac a) = f a

case inr
α : Type u_1
β : Type ?u.1692646
γ : Type ?u.1692649
δ : Type ?u.1692652
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
h✝ : ¬a ∈ s
⊢ (∫⁻ (x : α), f x ∂0) = 0
α : Type u_1
β : Type ?u.1692646
γ : Type ?u.1692649
δ : Type ?u.1692652
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
⊢ (∫⁻ (x : α), f x ∂if a ∈ s then dirac a else 0) = if a ∈ s then f a else 0
split_ifs
no goals
case inl
α : Type u_1
β : Type ?u.1692646
γ : Type ?u.1692649
δ : Type ?u.1692652
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
h✝ : a ∈ s
⊢ (∫⁻ (x : α), f x ∂dirac a) = f a
exact lintegral_dirac _ _
no goals
case inr
α : Type u_1
β : Type ?u.1692646
γ : Type ?u.1692649
δ : Type ?u.1692652
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
h✝ : ¬a ∈ s
⊢ (∫⁻ (x : α), f x ∂0) = 0
exact lintegral_zero_measure _