hasFiniteIntegral_const_iff_enorm

English

For a constant vector c with finite nonzero norm, HasFiniteIntegral (fun x => c) μ is equivalent to IsFiniteMeasure μ when the norm is not infinite.

Русский

Для константной функции c с конечной ненулевой нормой, HasFiniteIntegral (пользовательская функция, константа) эквивалентен IsFiniteMeasure μ, если ‖c‖ не бесконечно.

LaTeX

$$$\\|c\\|_\\varepsilon \\neq \\infty \\Rightarrow \\HasFiniteIntegral (\\lambda x. c)\\mu \\;\\leftrightarrow\\; \\|c\\|_\\varepsilon = 0 \\; \\lor\\; IsFiniteMeasure\\mu$$$

Lean4

theorem hasFiniteIntegral_const_iff_enorm {c : ε} (hc : ‖c‖ₑ ≠ ∞) :
    HasFiniteIntegral (fun _ : α ↦ c) μ ↔ ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ := by
  simpa [hasFiniteIntegral_iff_enorm, lt_top_iff_ne_top, ENNReal.mul_eq_top, or_iff_not_imp_left,
    isFiniteMeasure_iff] using fun h h' ↦ (hc h').elim

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