Two measures μ, ν are said to be mutually singular (measure_theory.measure.mutually_singular,
localized notation μ ⊥ₘ ν) if there exists a measurable set s such that μ s = 0 and
ν sᶜ = 0. The measurability of s is an unnecessary assumption (see
measure_theory.measure.mutually_singular.mk) but we keep it because this way rcases (h : μ ⊥ₘ ν)
gives us a measurable set and usually it is easy to prove measurability.
μ ⊥ₘ ν
μ s = 0
ν sᶜ = 0
rcases (h : μ ⊥ₘ ν)
In this file we define the predicate measure_theory.measure.mutually_singular and prove basic
facts about it.
measure, mutually singular
Two measures μ, ν are said to be mutually singular if there exists a measurable set s
such that μ s = 0 and ν sᶜ = 0.