haveLebesgueDecomposition_spec — Mathlib

English

If HaveLebesgueDecomposition(μ, ν) holds, then μ is the sum of its singular part and ν with density μ.rnDeriv ν; moreover, μ.rnDeriv ν is measurable and μ.singularPart ν ⟂ ν.

Русский

Пусть существует разложение Лебега: μ = μ_s^ν + ν с плотностью μ.rnDeriv ν; плотность измерения измерима, а сингулярная часть взаимно одной мере ν.

LaTeX

$$$\text{Measurable}(μ.rnDeriv ν) \land μ.singularPart ν \perp_m ν \land μ = μ.singularPart ν + ν.withDensity(μ.rnDeriv ν)$$$

Lean4

theorem haveLebesgueDecomposition_spec (μ ν : Measure α) [h : HaveLebesgueDecomposition μ ν] :
    Measurable (μ.rnDeriv ν) ∧ μ.singularPart ν ⟂ₘ ν ∧ μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) :=
  by
  rw [singularPart, rnDeriv, dif_pos h, dif_pos h]
  exact Classical.choose_spec h.lebesgue_decomposition

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