dirac_apply — Mathlib

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]

Похожие утверждения