# Mutually singular measures #

Two measures `μ`

, `ν`

are said to be mutually singular (`MeasureTheory.Measure.MutuallySingular`

,
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
`MeasureTheory.Measure.MutuallySingular.mk`

) but we keep it because this way `rcases (h : μ ⟂ₘ ν)`

gives us a measurable set and usually it is easy to prove measurability.

In this file we define the predicate `MeasureTheory.Measure.MutuallySingular`

and prove basic
facts about it.

## Tags #

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`

.

## Equations

- MeasureTheory.Measure.MutuallySingular μ ν = ∃ (s : Set α), MeasurableSet s ∧ ↑↑μ s = 0 ∧ ↑↑ν sᶜ = 0

## Instances For

Two measures `μ`

, `ν`

are said to be mutually singular if there exists a measurable set `s`

such that `μ s = 0`

and `ν sᶜ = 0`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

A set such that `μ h.nullSet = 0`

and `ν h.nullSetᶜ = 0`

.