haveLebesgueDecomposition_withDensity

English

For μ and measurable f, (μ.withDensity f).HaveLebesgueDecomposition μ.

Русский

Для меры μ и измеримой функции f меру μ с плотностью f имеет разложение по μ.

LaTeX

$$haveLebesgueDecomposition_withDensity μ (f) (hf)$$

Lean4

theorem haveLebesgueDecomposition_withDensity (μ : Measure α) {f : α → ℝ≥0∞} (hf : Measurable f) :
    (μ.withDensity f).HaveLebesgueDecomposition μ :=
  ⟨⟨⟨0, f⟩, hf, .zero_left, (zero_add _).symm⟩⟩

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