aefinStronglyMeasurable — Mathlib

English

If MemLp f p μ holds and p ≠ 0, p ≠ ∞, then f is AEFinStronglyMeasurable with respect to μ.

Русский

Если f удовлетворяет MemLp f p μ и p ≠ 0, p ≠ ∞, то f имеет AE-конечную сильномерируемость относительно μ.

LaTeX

$$$\text{MemLp}(f,p,\mu) \land p \neq 0 \land p \neq \infty \Longrightarrow \text{AEFinStronglyMeasurable}(f,\mu)$$$

Lean4

theorem aefinStronglyMeasurable (hf : MemLp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) :
    AEFinStronglyMeasurable f μ :=
  ⟨hf.aestronglyMeasurable.mk f,
    ((memLp_congr_ae hf.aestronglyMeasurable.ae_eq_mk).mp hf).finStronglyMeasurable_of_stronglyMeasurable
      hf.aestronglyMeasurable.stronglyMeasurable_mk hp_ne_zero hp_ne_top,
    hf.aestronglyMeasurable.ae_eq_mk⟩

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