rnDeriv_mconv' — Mathlib

English

Under Lebesgue decomposition and ν σ-finite, absolute continuity μ ≪ ν implies the RN-deriv equals 1 almost everywhere if and only if μ = ν.

Русский

При разложении Лебега и σ–конечности ν, μ ≪ ν даёт RN-деривив ν равным 1 почти наверняка тогда и только тогда, когда μ = ν.

LaTeX

$$$$ μ.rnDeriv ν =^\mathrm{ae}_{ν} 1 \iff μ = ν $$$$

Lean4

@[to_additive]
theorem rnDeriv_mconv' [SigmaFinite μ] {ν₁ ν₂ : Measure G} [SigmaFinite ν₁] [SigmaFinite ν₂] (hν₁ : ν₁ ≪ μ)
    (hν₂ : ν₂ ≪ μ) : (ν₁ ∗ₘ ν₂).rnDeriv μ =ᵐ[μ] (ν₁.rnDeriv μ) ⋆ₘₗ[μ] (ν₂.rnDeriv μ) := by
  rw [← withDensity_eq_iff_of_sigmaFinite (by fun_prop) (by fun_prop), ←
    mconv_eq_withDensity_mlconvolution_rnDeriv hν₁ hν₂, withDensity_rnDeriv_eq _ _ (mconv_absolutelyContinuous hν₂)]

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