measure_sub_singularPart — Mathlib

English

Lebesgue decomposition gives μ = ν.singularPart ν + ν.withDensity (μ.rnDer ν); equivalently μ - μ.singularPart ν = ν.withDensity (μ.rnDer ν).

Русский

Лебесгово разложение даёт μ = ν.singularPart ν + ν.withDensity(μ.rnDer ν); эквивалентно μ - μ.singularPart ν = ν.withDensity (μ.rnDer ν).

LaTeX

$$$ μ - μ.singularPart ν = ν.withDensity(μ.rnDer ν) $$$

Lean4

theorem measure_sub_singularPart (μ ν : Measure α) [HaveLebesgueDecomposition μ ν] [IsFiniteMeasure μ] :
    μ - μ.singularPart ν = ν.withDensity (μ.rnDeriv ν) :=
  by
  nth_rw 1 [← rnDeriv_add_singularPart μ ν]
  exact Measure.add_sub_cancel

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