integrable_indicator_iff — Mathlib

English

If e is measure-preserving, integrability of f on e(s) with respect to ν is equivalent to integrability of f ∘ e on s with respect to μ.

Русский

Если e сохраняет меру, то интегрируемость f на e(s) по ν эквивалентна интегрируемости f ∘ e на s по μ.

LaTeX

$$IntegrableOn f (e '' s) ν ↔ IntegrableOn (f ∘ e) s μ$$

Lean4

theorem integrable_indicator_iff (hs : MeasurableSet s) : Integrable (indicator s f) μ ↔ IntegrableOn f s μ := by
  simp_rw [IntegrableOn, Integrable, hasFiniteIntegral_iff_enorm, enorm_indicator_eq_indicator_enorm,
    lintegral_indicator hs, aestronglyMeasurable_indicator_iff hs]

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