norm_setIntegral_le_of_norm_le_const_ae

English

If f is essentially bounded by C on s with finite μ(s), then the norm of the set integral 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_ae {C : ℝ} (hs : μ s < ∞) (hC : ∀ᵐ x ∂μ.restrict s, ‖f x‖ ≤ C) :
    ‖∫ x in s, f x ∂μ‖ ≤ C * μ.real s :=
  by
  rw [← Measure.restrict_apply_univ] at *
  haveI : IsFiniteMeasure (μ.restrict s) := ⟨hs⟩
  simpa using norm_integral_le_of_norm_le_const hC

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