TendstoInMeasure — Mathlib

English

If ε>0 and ε≠∞, certain measure-valued maps converge to 0 along a filter whenever the finite-measure condition holds.

Русский

Если ε>0 и ε≠∞, некоторые отображения меры сходятся к 0 по фильтру при условии конечной меры.

LaTeX

$$$\\text{TendstoInMeasure } μ f l g$ under hypotheses asserting convergence of μ{x|ε≤edist(f_i x,g x)} to 0 for ε>0, ε<∞.$$

Lean4

/-- A sequence of functions `f` is said to converge in measure to some function `g` if for all
`ε > 0`, the measure of the set `{x | ε ≤ dist (f i x) (g x)}` tends to 0 as `i` converges along
some given filter `l`. -/
def TendstoInMeasure [EDist E] {_ : MeasurableSpace α} (μ : Measure α) (f : ι → α → E) (l : Filter ι) (g : α → E) :
    Prop :=
  ∀ ε, 0 < ε → Tendsto (fun i => μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)

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