hasFiniteIntegral_const_iff_isFiniteMeasure

English

For a constant c with finite nonzero norm, various formulations equate HasFiniteIntegral (fun x => c) μ with IsFiniteMeasure μ.

Русский

Для константы c с конечной ненулевой нормой различные формулировки связывают HasFiniteIntegral (константа) с IsFiniteMeasure μ.

LaTeX

$$$\\|c\\| \u2260 0 \\to\\ HasFiniteIntegral (\\lambda x. c)\\mu \\leftrightarrow IsFiniteMeasure\\mu$$$

Lean4

theorem hasFiniteIntegral_const_iff_isFiniteMeasure {c : β} (hc : c ≠ 0) :
    HasFiniteIntegral (fun _ ↦ c) μ ↔ IsFiniteMeasure μ :=
  hasFiniteIntegral_const_iff_isFiniteMeasure_enorm (enorm_ne_zero.mpr hc) enorm_ne_top

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