haveLebesgueDecomposition_mk — Mathlib

English

Given μ, s, t with a Lebesgue decomposition for t relative to μ, if hadd expresses s = t + μ.withDensityᵥ f with f measurable, then s has Lebesgue decomposition with respect to μ.

Русский

Пусть μ, s, t имеют разложение Лебега, и если s = t + μ.withDensityᵥ f при измеримой f, то s имеет разложение Лебега относительно μ.

LaTeX

$$$[s.HaveLebesgueDecomposition μ] \Rightarrow \text{eq}(s, t + μ.withDensityᵥ f) \Rightarrow s.HaveLebesgueDecomposition μ$$$

Lean4

theorem haveLebesgueDecomposition_mk (μ : Measure α) {f : α → ℝ} (hf : Measurable f)
    (htμ : t ⟂ᵥ μ.toENNRealVectorMeasure) (hadd : s = t + μ.withDensityᵥ f) : s.HaveLebesgueDecomposition μ :=
  by
  by_cases hfi : Integrable f μ
  · exact haveLebesgueDecomposition_mk' μ hf hfi htμ hadd
  · rw [withDensityᵥ, dif_neg hfi, add_zero] at hadd
    refine haveLebesgueDecomposition_mk' μ measurable_zero (integrable_zero _ _ μ) htμ ?_
    rwa [withDensityᵥ_zero, add_zero]

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