rnDeriv_eq_rnDeriv_measure — Mathlib

English

If κ = η.withDensity f + ξ and hf is measurability of f, then for each a, the RN-derivative measure satisfies that ᵉ there exists an almost-everywhere equality between rnDeriv κ a (η a) and the density f a with respect to η a, on the appropriate σ-algebra.

Русский

Если κ = η.withDensity f + ξ и f измеримо, то для каждого a существует почти везде равенство между rnDeriv κ a по η a и плотностью f a по отношению к η a на соответствующей мере.

LaTeX

$$f a =ᵐ[η a] ∂(κ a)/∂(η a)$$

Lean4

theorem rnDeriv_eq_rnDeriv_measure : rnDeriv κ η a =ᵐ[η a] ∂(κ a)/∂(η a) :=
  eq_rnDeriv_measure (rnDeriv_add_singularPart κ η).symm (measurable_rnDeriv κ η) a
    (mutuallySingular_singularPart κ η a)

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