setLIntegral_eq_of_support_subset

English

Two measures μ and ν are equal iff they have the same lintegral 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 setLIntegral_eq_of_support_subset {s : Set α} {f : α → ℝ≥0∞} (hsf : f.support ⊆ s) :
    ∫⁻ x in s, f x ∂μ = ∫⁻ x, f x ∂μ :=
  by
  apply le_antisymm (setLIntegral_le_lintegral s fun x ↦ f x)
  apply le_trans (le_of_eq _) (lintegral_indicator_le _ _)
  congr with x
  simp only [indicator]
  split_ifs with h
  · rfl
  · exact Function.support_subset_iff'.1 hsf x h

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