rieszMeasure — Mathlib

English

Define rieszMeasure Λ as the measure associated to the content λΛ via the Riesz representation; it satisfies ∫ f d(rieszMeasure Λ) = Λ f for suitable f.

Русский

Определим rieszMeasure Λ как меру, сопряжённую с контентом λΛ по формуле Рiesz; выполняется ∫ f d(rieszMeasure Λ) = Λ f для подходящих f.

LaTeX

$$$\\int f\\, d(\\text{rieszMeasure }Λ)= Λ f$ for appropriate f.$$

Lean4

/-- `rieszContent` gives a `Content` from `Λ : C_c(X, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0`. Here `rieszContent Λ` is
promoted to a measure. It will be later shown that
`∫ (x : X), f x ∂(rieszMeasure Λ hΛ) = Λ f` for all `f : C_c(X, ℝ≥0)`. -/
def rieszMeasure :=
  (rieszContent Λ).measure

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