integrable_rnDeriv — Mathlib

English

For a signed measure s and a finite measure μ, rnDeriv s μ is integrable with respect to μ, i.e., ∫ |rnDeriv s μ| dμ < ∞.

Русский

Для знаковой меры s и конечной меры μ интеграл по μ от |rnDeriv s μ| конечен: ∫ |rnDeriv s μ| dμ < ∞.

LaTeX

$$Integrable (rnDeriv s μ) μ$$

Lean4

theorem integrable_rnDeriv (s : SignedMeasure α) (μ : Measure α) : Integrable (rnDeriv s μ) μ := by
  refine Integrable.sub ?_ ?_ <;>
    · constructor
      · apply Measurable.aestronglyMeasurable
        fun_prop
      exact hasFiniteIntegral_toReal_of_lintegral_ne_top (lintegral_rnDeriv_lt_top _ μ).ne

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