intervalIntegrable_enorm_iff — Mathlib

English

Let f be AEStronglyMeasurable on μ restricted to the interval, then IntervalIntegrable(‖f‖) on μ equals IntervalIntegrable(f) on μ.

Русский

Пусть f является AEStronglyMeasurable на мере μ, ограниченной интервалом, тогда IntervalIntegrable(‖f‖) на μ равна IntervalIntegrable(f) на μ.

LaTeX

$$$\operatorname{AEStronglyMeasurable}(f,\mu|_{\mathord{I}ac}) \Rightarrow (\operatorname{IntervalIntegrable}(\|f\|)\mu a b \Leftrightarrow \operatorname{IntervalIntegrable}(f)\mu a b)$$$

Lean4

theorem intervalIntegrable_enorm_iff {μ : Measure ℝ} {a b : ℝ} (hf : AEStronglyMeasurable f (μ.restrict (Ι a b))) :
    IntervalIntegrable (fun t => ‖f t‖ₑ) μ a b ↔ IntervalIntegrable f μ a b := by
  simp_rw [intervalIntegrable_iff, IntegrableOn, integrable_enorm_iff hf]

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