norm_setIntegral_le_of_norm_le_const

English

If f is bounded by C on s, then the norm of the set integral over s is at most C times μ.real s.

Русский

Если f ограничена по значению константой C на s, то норма множества интеграла по s не превышает C μ.real s.

LaTeX

$$$$ \\left\\| \\int_{x \\in s} f(x) \\, d\\mu(x) \\right\\| \\leq C \\; \\mu_{\\mathbb{R}}(s) $$$$

Lean4

theorem norm_setIntegral_le_of_norm_le_const {C : ℝ} (hs : μ s < ∞) (hC : ∀ x ∈ s, ‖f x‖ ≤ C) :
    ‖∫ x in s, f x ∂μ‖ ≤ C * μ.real s :=
  norm_setIntegral_le_of_norm_le_const_ae' hs (Eventually.of_forall hC)

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