restrict_of_bounded — Mathlib

English

If a function is essentially bounded on a set of finite measure, then it has finite integral with respect to the restricted measure.

Русский

Если функция почти ограничена на множесте конечной меры, то она имеет конечную интегралу по ограниченной мере.

LaTeX

$$$ \text{HasFiniteIntegral}(f,\mu\restriction s) \quad\text{when } \mu(s)<\infty \text{ and } \|f\| \le C \text{ a.e. on } s$$$

Lean4

theorem restrict_of_bounded [NormedAddCommGroup E] {f : α → E} {s : Set α} {μ : Measure α} (C : ℝ) (hs : μ s < ∞)
    (hf : ∀ᵐ x ∂μ.restrict s, ‖f x‖ ≤ C) : HasFiniteIntegral f (μ.restrict s) :=
  haveI : IsFiniteMeasure (μ.restrict s) := ⟨by rwa [Measure.restrict_apply_univ]⟩
  .of_bounded hf

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