of_finite — Mathlib

English

If μ is finite and ‖c‖ ≠ ∞, HasFiniteIntegral (fun _ => c) μ holds; this is expressed via the const_iff_enorm lemma.

Русский

Если μ конечно и ‖c‖ ≠ ∞, то HasFiniteIntegral константы равенству функции по μ.

LaTeX

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

Lean4

@[simp]
theorem of_finite [Finite α] [IsFiniteMeasure μ] {f : α → β} : HasFiniteIntegral f μ :=
  let ⟨_⟩ := nonempty_fintype α
  .of_bounded <| ae_of_all μ <| norm_le_pi_norm f

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