finStronglyMeasurable_of_measurable

English

If a function f: α → ℝ≥0∞ is measurable and its integral ∫ f dμ is finite (i.e., not ∞), then f is FinStronglyMeasurable with respect to μ.

Русский

Если функция f: α → ℝ≥0∞ измерима и её интеграл по μ конечен (не равен ∞), то f является FinStronglyMeasurable по μ.

LaTeX

$$$\text{Measurable}(f) \;\wedge\; \int f \, d\mu \neq \infty \quad\Rightarrow\quad \text{FinStronglyMeasurable}(f, \mu)$$$

Lean4

theorem finStronglyMeasurable_of_measurable (hf : ∫⁻ x, f x ∂μ ≠ ∞) (hf_meas : Measurable f) :
    FinStronglyMeasurable f μ :=
  ⟨SimpleFunc.eapprox f, measure_support_eapprox_lt_top hf_meas hf, SimpleFunc.tendsto_eapprox hf_meas⟩

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