ext_iff_lintegral — Mathlib

English

Two measures μ and ν are equal iff their lintegrals agree for all nonnegative measurable functions.

Русский

Две меры μ и ν равны тогда и только тогда, когда их линегралы совпадают для всех неотрицательных измеримых функций.

LaTeX

$$$$ μ = ν \\;\\Leftrightarrow\\; \\forall f: α \\to \\mathbb{R}_{\\ge 0}^{\\infty},\\; f \\text{ Measurable} \\Rightarrow \\int^- a, f(a) \\ dμ = \\int^- a, f(a) \\ dν. $$$$

Lean4

theorem ext_iff_lintegral (ν : Measure α) : μ = ν ↔ ∀ f : α → ℝ≥0∞, Measurable f → ∫⁻ a, f a ∂μ = ∫⁻ a, f a ∂ν :=
  by
  refine ⟨fun h _ _ ↦ by rw [h], ?_⟩
  intro h
  ext s hs
  simp only [← lintegral_indicator_one hs]
  exact h (s.indicator 1) ((measurable_indicator_const_iff 1).mpr hs)

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