English
Let μ be a measure on α and l a filter. If φ is an ae-cover of μ along l, then for almost every x in α, the family of numbers (φ(i).indicator f x) converges to f x along l, for any function f into a topological β with a zero element.
Русский
Пусть μ – мера на μ(α), и \(l\) – фильтр. Если φ образует ae-покрытие μ вдоль l, тогда для почти всех \(x\) выполняется, что семейство \((\phi(i).\mathrm{indicator} f x)\) сходится к \(f(x)\) вдоль l для любой функции \(f: α \to β\) в топологическом пространстве β с нулём.
LaTeX
$$$\\forall {\\beta} [Zero\\,\\beta] [TopologicalSpace\\,\\beta] (f : \\alpha \\to \\beta) {\\phi : \\iota \\to Set\\,\\alpha}\\\\ (h\\phi : MeasureTheory.AECover μ l φ) \\\\ ∀^{\\mathrm{ae}} x \\partial μ, \\ Tendsto (\\lambda i, (φ(i)).indicator f x)\\ l\\ (\\mathcal{N} (f x))$$$
Lean4
theorem ae_tendsto_indicator {β : Type*} [Zero β] [TopologicalSpace β] (f : α → β) {φ : ι → Set α}
(hφ : AECover μ l φ) : ∀ᵐ x ∂μ, Tendsto (fun i => (φ i).indicator f x) l (𝓝 <| f x) :=
hφ.ae_eventually_mem.mono fun _x hx => tendsto_const_nhds.congr' <| hx.mono fun _n hn => (indicator_of_mem hn _).symm
