absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq

English

A signed measure s is absolutely continuous with respect to μ if and only if μ.withDensityᵥ (s.rnDeriv μ) = s.

Русский

Знаковая мера s абсолютно непрерывна относительно μ тогда и только тогда, когда μ.withDensityᵥ (s.rnDeriv μ) = s.

LaTeX

$$$ s \\ll_v μ.toENNRealVectorMeasure \\iff μ.withDensityᵥ (s.rnDeriv μ) = s $$$

Lean4

/-- The Radon-Nikodym theorem for signed measures. -/
theorem absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq (s : SignedMeasure α) (μ : Measure α) [SigmaFinite μ] :
    s ≪ᵥ μ.toENNRealVectorMeasure ↔ μ.withDensityᵥ (s.rnDeriv μ) = s :=
  ⟨withDensityᵥ_rnDeriv_eq s μ, fun h => h ▸ withDensityᵥ_absolutelyContinuous _ _⟩

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