English
For any a and any set s, the Dirac measure satisfies δ_a(s) = s.indicator 1 a; i.e., δ_a(s) is 1 if a ∈ s and 0 otherwise.
Русский
Для любого a и любого множества s мера Дирака удовлетворяет δ_a(s) = s.indicator 1 a; т.е. δ_a(s) = 1, если a ∈ s, и 0 в противном случае.
LaTeX
$$$ dirac a s = s.indicator 1 a $$$
Lean4
@[simp]
theorem dirac_apply [MeasurableSingletonClass α] (a : α) (s : Set α) : dirac a s = s.indicator 1 a :=
by
by_cases h : a ∈ s; · rw [dirac_apply_of_mem h, indicator_of_mem h, Pi.one_apply]
rw [indicator_of_notMem h, ← nonpos_iff_eq_zero]
calc
dirac a s ≤ dirac a { a }ᶜ := measure_mono (subset_compl_comm.1 <| singleton_subset_iff.2 h)
_ = 0 := by simp [dirac_apply' _ (measurableSet_singleton _).compl]