hasFiniteIntegral_const_iff_isFiniteMeasure_enorm

English

If ‖c‖ ≠ 0 and ‖c‖ ≠ ∞, then HasFiniteIntegral (fun x => c) μ is equivalent to IsFiniteMeasure μ.

Русский

Если ‖c‖ ≠ 0 и ‖c‖ ≠ ∞, то HasFiniteIntegral (константа c) по μ эквивалентно IsFiniteMeasure μ.

LaTeX

$$$\\|c\\| \u2260 0 \\quad\\land\\quad \\|c\\| \u2260 \\infty \\Rightarrow \\HasFiniteIntegral (\\lambda x. c)\\mu \\iff IsFiniteMeasure\\mu$$$

Lean4

theorem hasFiniteIntegral_const_iff_isFiniteMeasure_enorm {c : ε} (hc : ‖c‖ₑ ≠ 0) (hc' : ‖c‖ₑ ≠ ∞) :
    HasFiniteIntegral (fun _ ↦ c) μ ↔ IsFiniteMeasure μ := by
  simp [hasFiniteIntegral_const_iff_enorm hc', hc, isFiniteMeasure_iff]

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