measurableLE — Mathlib

English

measurableLE(μ, ν) is the set of all measurable functions f: α→ℝ≥0∞ such that for every measurable set A, ∫_A f dμ ≤ ν(A).

Русский

measurableLE(μ, ν) — множество измеримых функций f: α→ℝ≥0∞, удовлетворяющих для каждого измеримого множества A неравенству ∫_A f dμ ≤ ν(A).

LaTeX

$$$$ \\mathrm{measurableLE}(\\mu, \\nu) = \\{ f: \\alpha \\to \\overline{\\mathbb{R}}_{\\ge 0} \\mid \\mathrm{Measurable}(f) \\land \\forall A, \\mathrm{MeasurableSet}(A) \\to \\int\\!_A f \, d\\mu \\le \\nu(A) \\} $$$$

Lean4

/-- Given two measures `μ` and `ν`, `measurableLE μ ν` is the set of measurable
functions `f`, such that, for all measurable sets `A`, `∫⁻ x in A, f x ∂μ ≤ ν A`.

This is useful for the Lebesgue decomposition theorem. -/
def measurableLE (μ ν : Measure α) : Set (α → ℝ≥0∞) :=
  {f | Measurable f ∧ ∀ (A : Set α), MeasurableSet A → (∫⁻ x in A, f x ∂μ) ≤ ν A}

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