integrable_rnDeriv — Mathlib

English

For complex measures c, s, μ with Lebesgue decompositions, the RN-derivative of s plus μ.withDensityᵥ(f) is the sum of RN-derivatives.

Русский

Для комплексной меры c и другой меры s с разложением Лебега имеем, что RN-дериватив суммы равен сумме RN-дериватов.

LaTeX

$$$ (s + t).rnDeriv μ =^{{\\mu}}_{a.e.} s.rnDeriv μ + t.rnDeriv μ $$$

Lean4

theorem integrable_rnDeriv (c : ComplexMeasure α) (μ : Measure α) : Integrable (c.rnDeriv μ) μ :=
  by
  rw [← memLp_one_iff_integrable, ← memLp_re_im_iff]
  exact
    ⟨memLp_one_iff_integrable.2 (SignedMeasure.integrable_rnDeriv _ _),
      memLp_one_iff_integrable.2 (SignedMeasure.integrable_rnDeriv _ _)⟩

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