hasFiniteIntegral_const_enorm — Mathlib

English

If IsFiniteMeasure μ, then HasFiniteIntegral (fun x => c) μ holds whenever ‖c‖ₑ ≠ ∞; the proof uses the constant-enorm equivalence.

Русский

При изоморфированной мере μ конечной величине (константа) при условии ‖c‖ₑ ≠ ∞ интеграл конечен.

LaTeX

$$$[IsFiniteMeasure\\mu] \\land \\|c\\|_\\varepsilon \\neq \\infty \\Rightarrow HasFiniteIntegral (\\lambda x. c)\\mu$$$

Lean4

@[fun_prop]
theorem hasFiniteIntegral_const_enorm [IsFiniteMeasure μ] {c : ε} (hc : ‖c‖ₑ ≠ ∞) :
    HasFiniteIntegral (fun _ : α ↦ c) μ :=
  (hasFiniteIntegral_const_iff_enorm hc).2 <| .inr ‹_›

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