singularPart_eq_zero_iff_absolutelyContinuous

English

Let κ and η be finite kernels. For every a, the singular part κ a with respect to η a vanishes if and only if κ a is absolutely continuous with respect to η a.

Русский

Пусть κ и η — конечные ядра. Для каждого a сингулярная часть κ a относительно η a обращается в ноль тогда, когда κ a абсолютно непрерывна относительно η a.

LaTeX

$$$singularPart\\ κ\\ η\\ a = 0 \\iff κ\\ a \\ll η\\ a$$$

Lean4

theorem singularPart_eq_zero_iff_absolutelyContinuous (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] (a : α) :
    singularPart κ η a = 0 ↔ κ a ≪ η a :=
  by
  conv_rhs => rw [← rnDeriv_add_singularPart κ η, coe_add, Pi.add_apply]
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [h, add_zero]
    exact withDensity_absolutelyContinuous _ _
  rw [Measure.AbsolutelyContinuous.add_left_iff] at h
  exact Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular h.2 (mutuallySingular_singularPart _ _ _)

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