mconv — Mathlib

English

If ν₁ and ν₂ are absolutely continuous with respect to μ, then ν₁ ∗ₘ ν₂ has a Lebesgue decomposition with respect to μ, with explicit density given by RN-derivatives.

Русский

Если ν₁ и ν₂ абсолютно непрерывны по μ, то ν₁ ∗ₘ ν₂ имеет разложение Лебега относительно μ, плотность задаётся RN-дерививами.

LaTeX

$$$$ (ν₁ ∗ₘ ν₂).HaveLebesgueDecomposition μ = ⟨0, (ν₁.rnDeriv μ) ⋆ₘₗ[μ] (ν₂.rnDeriv μ)⟩ $$$$

Lean4

@[to_additive]
theorem mconv [SFinite μ] {ν₁ ν₂ : Measure G} [ν₁.HaveLebesgueDecomposition μ] [ν₂.HaveLebesgueDecomposition μ]
    (hν₁ : ν₁ ≪ μ) (hν₂ : ν₂ ≪ μ) : (ν₁ ∗ₘ ν₂).HaveLebesgueDecomposition μ :=
  ⟨⟨0, (ν₁.rnDeriv μ) ⋆ₘₗ[μ] (ν₂.rnDeriv μ)⟩, by fun_prop, by simp, by
    simpa using mconv_eq_withDensity_mlconvolution_rnDeriv hν₁ hν₂⟩

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