eq_singularPart_measure — Mathlib

English

Given κ, η, ξ and f with κ = η.withDensity f + ξ, and a such that ξ a ⟂ η a, the value of ξ a on a set equals the singularPart of κ a with respect to η a on that set.

Русский

Пусть κ = η.withDensity f + ξ и ξ a ⟂ η a; тогда ξ a на заданном множестве равно сингулярной части κ a относительно η a на этом множестве.

LaTeX

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

Lean4

theorem eq_singularPart_measure (h : κ = η.withDensity f + ξ) (hf : Measurable (Function.uncurry f)) (a : α)
    (hξ : ξ a ⟂ₘ η a) : ξ a = (κ a).singularPart (η a) :=
  by
  have : κ a = ξ a + (η a).withDensity (f a) := by rw [h, coe_add, Pi.add_apply, η.withDensity_apply hf, add_comm]
  exact (κ a).eq_singularPart (hf.comp measurable_prodMk_left) hξ this

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