mconv_eq_withDensity_mlconvolution_rnDeriv

English

Under Lebesgue decomposition and finiteness hypotheses, the RN-derivative of the convolution equals the RN-derivatives convolved with μ, a.e. w.r.t μ.

Русский

При разложении Лебега и конечных предположениях, RN-деривив конволюции равен RN-дерививам, конволюированным с μ, почти везде по μ.

LaTeX

$$$$ (ν₁.mconv ν₂).rnDeriv μ =^\mathrm{ae}_{μ} (ν₁.rnDeriv μ) ⋆ₗ[μ] (ν₂.rnDeriv μ) $$$$

Lean4

@[to_additive]
theorem mconv_eq_withDensity_mlconvolution_rnDeriv [SFinite μ] {ν₁ ν₂ : Measure G} [ν₁.HaveLebesgueDecomposition μ]
    [ν₂.HaveLebesgueDecomposition μ] (hν₁ : ν₁ ≪ μ) (hν₂ : ν₂ ≪ μ) :
    ν₁ ∗ₘ ν₂ = μ.withDensity (ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ) := by
  rw [← mconv_withDensity_eq_mlconvolution (by fun_prop) (by fun_prop), withDensity_rnDeriv_eq _ _ hν₁,
    withDensity_rnDeriv_eq _ _ hν₂]

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