English
For a signed measure s and a measure μ, s has a Lebesgue decomposition with respect to μ iff either the positive part or the negative part of its Jordan decomposition fails to have such a decomposition with respect to μ.
Русский
Для знаковой меры s и меры μ равенство: s имеет разложение Лебега относительно μ тогда и только тогда, когда положительная часть или отрицательная часть её джорданового разложения не имеют такого разложения относительно μ.
LaTeX
$$$\neg s. HaveLebesgueDecomposition\,\mu \;\iff\; \neg s.toJordanDecomposition.posPart.HaveLebesgueDecomposition \mu \lor \neg s.toJordanDecomposition.negPart.HaveLebesgueDecomposition \mu$$$
Lean4
theorem not_haveLebesgueDecomposition_iff (s : SignedMeasure α) (μ : Measure α) :
¬s.HaveLebesgueDecomposition μ ↔
¬s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ ∨
¬s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ :=
⟨fun h => not_or_of_imp fun hp hn => h ⟨hp, hn⟩, fun h hl => (not_and_or.2 h) ⟨hl.1, hl.2⟩⟩
-- `inferInstance` directly does not work
-- see Note [lower instance priority]
