ae_tendsto_limRatio — Mathlib

English

For absolutely continuous ρ ≪ μ, the ratio ρ a / μ a converges almost everywhere to v.limRatio ρ x along the Vitali filter.

Русский

Если ρ ≪ μ, то почти всюду отношение ρ(a)/μ(a) сходится к v.limRatio ρ x вдоль фильтра Vitali.

LaTeX

$$$\forall x,\ Tendsto (a \mapsto ρ a / μ a) (v.filterAt x) (\mathcal{N}(v.limRatio ρ x)).$$$

Lean4

theorem ae_tendsto_limRatio : ∀ᵐ x ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x)) :=
  by
  filter_upwards [v.ae_tendsto_div hρ]
  intro x hx
  exact tendsto_nhds_limUnder hx

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