ae_tendsto_limRatioMeas — Mathlib

English

If ρ ≪ μ, then limRatioMeas hρ is a measurable function (AEMeasurable).

Русский

Если ρ ≪ μ, то limRatioMeas hρ измерима (AEMeasurable).

LaTeX

$$$\text{Measurable}(v.limRatioMeas hρ)$$$

Lean4

theorem ae_tendsto_limRatioMeas : ∀ᵐ x ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x)) :=
  by
  filter_upwards [v.ae_tendsto_limRatio hρ, AEMeasurable.ae_eq_mk (v.aemeasurable_limRatio hρ)]
  intro x hx h'x
  rwa [h'x] at hx

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