integrable_of_ae_notMem_eq_zero — Mathlib

English

For f as an Lp function, mild conditions ensure integrability on sets of finite measure in the Lp sense.

Русский

Для f как Lp-функции справедливы условия интегрируемости на множествах с конечной мерой в контексте Lp.

LaTeX

$$Integrator(f, s, μ) with p≥1 and μ(s) < ∞$$

Lean4

/-- If a function is integrable on a set `s` and vanishes almost everywhere on its complement,
then it is integrable. -/
theorem integrable_of_ae_notMem_eq_zero {f : α → ε'} (hf : IntegrableOn f s μ) (h't : ∀ᵐ x ∂μ, x ∉ s → f x = 0) :
    Integrable f μ := by
  rw [← integrableOn_univ]
  apply hf.of_ae_diff_eq_zero nullMeasurableSet_univ
  filter_upwards [h't] with x hx h'x using hx h'x.2

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