integrable_dirac' — Mathlib

English

In AEStronglyMeasurable setting, integrability of ‖f‖^p is equivalent to MemLp f p μ.

Русский

В условиях AEStronglyMeasurable интегрируемость ‖f‖^p эквивалентна MemLp f p μ.

LaTeX

$$AEStronglyMeasurable f μ ∧ p ≠ 0 ∧ p ≠ ∞ ⇒ (Integrable (‖f‖^p) μ ↔ MemLp f p μ)$$

Lean4

/-- Every strongly measurable function is integrable with respect to a Dirac measure.
See `integrable_dirac` for a version which requires that singletons are measurable sets but has no
hypothesis on `f`. -/
@[fun_prop]
theorem integrable_dirac' {a : α} {f : α → ε} (hf : StronglyMeasurable f) (hfa : ‖f a‖ₑ < ∞) :
    Integrable f (Measure.dirac a) :=
  ⟨hf.aestronglyMeasurable, by simpa [HasFiniteIntegral, lintegral_dirac' _ hf.enorm]⟩

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