intervalIntegrable_norm_iff — Mathlib

English

Under AEStronglyMeasurable assumption on f, IntervalIntegrable(‖f‖) and IntervalIntegrable(f) on [a,b] are equivalent.

Русский

При предположении AEStronglyMeasurable для f интервальная интегрируемость функции ‖f‖ и f на [a,b] эквивалентны.

LaTeX

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

Lean4

theorem intervalIntegrable_norm_iff {f : ℝ → E} {μ : 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_norm_iff hf]

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