dirac

Mathlib.MeasureTheory.OuterMeasure.Operations

URI: https://scilib.ai/kg/mathlib#MeasureTheory.OuterMeasure.dirac

Lean4

/-- The dirac outer measure. -/
def dirac (a : α) : OuterMeasure α where
  measureOf s := indicator s (fun _ => 1) a
  empty := by simp
  mono {_ _} h := indicator_le_indicator_of_subset h (fun _ => zero_le _) a
  iUnion_nat s
    _ :=
    calc
      indicator (⋃ n, s n) 1 a = ⨆ n, indicator (s n) 1 a := indicator_iUnion_apply (M := ℝ≥0∞) rfl _ _ _
      _ ≤ ∑' n, indicator (s n) 1 a := iSup_le fun _ ↦ ENNReal.le_tsum _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru