ae_tendsto_enorm — Mathlib

English

If for each n the a.e. limit of F n a is f a in norm, then the a.e. limit of ENNReal.ofReal ‖F n a‖ is ENNReal.ofReal ‖f a‖.

Русский

Если для каждого n почти во всех точках выполняется предел в норме, тогда для почти всех a предел ENNReal.ofReal ‖F n a‖ равен ENNReal.ofReal ‖f a‖.

LaTeX

$$$\forall n, \forall a, \text{Tendsto } (F_n a) \to f(a) \,\Rightarrow \, \forall a, \text{Tendsto } (\, \|F_n a\| \,) \to \|f(a)\|$$$

Lean4

theorem ae_tendsto_enorm (h : ∀ᵐ a ∂μ, Tendsto (fun n ↦ F' n a) atTop <| 𝓝 <| f' a) :
    ∀ᵐ a ∂μ, Tendsto (fun n ↦ ‖F' n a‖ₑ) atTop <| 𝓝 <| ‖f' a‖ₑ :=
  h.mono fun _ h ↦ Tendsto.comp (Continuous.tendsto continuous_enorm _) h

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