English
Two vector measures v and w are mutually singular if there exists a measurable set s such that every t ⊆ s has v t = 0 and every t ⊆ s^c has w t = 0.
Русский
Две векторные меры v и w взаимоисключающие, если существует измеримое множество s такое, что для любого t ⊆ s выполняется v(t)=0, и для любого t ⊆ s^c выполняется w(t)=0.
LaTeX
$$MutuallySingular v w := ∃ s, MeasurableSet s ∧ (∀ t ⊆ s, v t = 0) ∧ (∀ t ⊆ s^c, w t = 0)$$
Lean4
/-- Two vector measures `v` and `w` are said to be mutually singular if there exists a measurable
set `s`, such that for all `t ⊆ s`, `v t = 0` and for all `t ⊆ sᶜ`, `w t = 0`.
We note that we do not require the measurability of `t` in the definition since this makes it easier
to use. This is equivalent to the definition which requires measurability. To prove
`MutuallySingular` with the measurability condition, use
`MeasureTheory.VectorMeasure.MutuallySingular.mk`. -/
def MutuallySingular (v : VectorMeasure α M) (w : VectorMeasure α N) : Prop :=
∃ s : Set α, MeasurableSet s ∧ (∀ t ⊆ s, v t = 0) ∧ ∀ t ⊆ sᶜ, w t = 0
