singularPart_eq_singularPart_measure

English

As κ = η.withDensity f + ξ and hξ: ξ a ⟂ η a, the singularPart κ η at a equals the measure-level singularPart of κ a relative to η a.

Русский

При κ = η.withDensity f + ξ и условии hξ: ξ a ⟂ η a, сингулярная часть κ η в точке a равна мерному уровню сингулярности κ a относительно η a.

LaTeX

$$ξ a = (κ a).singularPart(η a)$$

Lean4

theorem singularPart_eq_singularPart_measure : singularPart κ η a = (κ a).singularPart (η a) :=
  eq_singularPart_measure (rnDeriv_add_singularPart κ η).symm (measurable_rnDeriv κ η) a
    (mutuallySingular_singularPart κ η a)

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